PO.ID.Exact.VariableIntensityIV
Variable-intensity instrumental variables: Angrist-Imbens average causal response over ordered treatment margins.
OrderedTreatment 8 core · 3 supporting This file provides algebra for finite ordered treatment or intensity levels: it defines adjacent margins, crossing indicators, and telescoping identities that express a change across ordered levels as the sum of crossed ★ ordered_telescope_identity
Variable-Intensity IV Ordered Treatment
This file provides algebra for finite ordered treatment or intensity levels: it defines adjacent margins, crossing indicators, and telescoping identities that express a change across ordered levels as the sum of crossed marginal increments, and re-exports the generic normalized finite weights. These are used in variable-intensity instrumental-variable characterizations.
For a sequence of adjacent margins and a margin, the lower treatment level is the lower endpoint of that margin in the ordered list of levels.
For a sequence of adjacent margins and a margin, the upper treatment level is the upper endpoint of that margin in the ordered list of levels.
For a sequence of adjacent margins and an ordered treatment level, the numeric intensity value is that level's position in the ordered list, expressed as a real number.
Definition (Lean source)
For a sequence of adjacent margins, a real-valued function on the ordered treatment levels, and a margin, the margin increment is the function value at that margin's upper endpoint minus its value at the lower endpoint.
Definition (Lean source)
For a sequence of adjacent margins, an initial treatment level, a final treatment level, and a margin, the crossing condition holds exactly when the movement starts below that margin's upper endpoint and ends at or above it.
Definition (Lean source)
For a sequence of adjacent margins, an initial treatment level, a final treatment level, and a margin, the crossing indicator equals one when the movement crosses that margin and zero otherwise.
Ordered telescoping for the identity intensity map. For an ordered treatment level a no larger than b among J + 1 ordered intensity levels, the numeric gap b − a equals the number of unit margins j → j+1 that the movement from a to b crosses.
Formal statement
Proof (Lean source)
Given a finite collection of indices, a real weight assigned to each index, and one index, the normalized finite weight is that index's weight divided by the sum of all weights.
Definition (Lean source)
3 supporting declarations (lemmas, instances)
-
ordered_telescope_indicatorlemma — Ordered telescoping across crossed margins for an arbitrary real-valued function on finite ordered levels.hypothesesconclusionProof (Lean source)
lemma ordered_telescope_indicator {J : ℕ} (f : Fin (J + 1) → ℝ) {a b : Fin (J + 1)} (hab : a ≤ b) : f b - f a = ∑ j : Fin J, marginIncrement f j * crossingIndicator a b j := by classical let F : ℕ → ℝ := fun n => if h : n < J + 1 then f ⟨n, h⟩ else 0 have hNat : a.val ≤ b.val := (Fin.val_fin_le).2 hab calc f b - f a = F b.val - F a.val := by have haJ : a.val ≤ J := Nat.le_of_lt_succ a.isLt have hbJ : b.val ≤ J := Nat.le_of_lt_succ b.isLt simp [F, haJ, hbJ] _ = ∑ i ∈ Ico a.val b.val, (F (i + 1) - F i) := by rw [Finset.sum_Ico_sub F hNat] _ = ∑ j : Fin J, marginIncrement f j * crossingIndicator a b j := by have hIco : Ico a.val b.val = (range J).filter (fun x => a.val ≤ x ∧ x < b.val) := by ext x simp [Finset.mem_Ico] omega rw [hIco, Finset.sum_filter, Finset.sum_fin_eq_sum_range] apply Finset.sum_congr rfl intro x hx have hxJ : x < J := by simpa using hx have hxleJ : x ≤ J := by omega simp [F, marginIncrement, lowerLevel, upperLevel, crossingIndicator_eq_ite_val, hxJ, hxleJ] -
normalizedWeight_nonneglemma — Nonnegativity of normalized weights from nonnegative raw weights and a positive normalizing sum.hypothesesconclusion0 ≤ normalizedWeight a iProof (Lean source)
lemma normalizedWeight_nonneg {ι : Type*} [Fintype ι] (a : ι → ℝ) (ha : ∀ i, 0 ≤ a i) (hsum : 0 < ∑ i, a i) (i : ι) : 0 ≤ normalizedWeight a i := by exact normalizedWeight_nonneg a ha hsum i -
sum_normalizedWeight_eq_onelemma — Normalized finite weights sum to one when the normalizing sum is positive.hypothesesconclusion∑ i, normalizedWeight a i = 1Proof (Lean source)
lemma sum_normalizedWeight_eq_one {ι : Type*} [Fintype ι] (a : ι → ℝ) (hsum : 0 < ∑ i, a i) : ∑ i, normalizedWeight a i = 1 := by exact sum_normalizedWeight_eq_one a hsum.ne'
VariableIntensity 41 core · 23 supporting This file formalizes a finite ordered-treatment instrumental-variable system for an Angrist-Imbens style directed instrument contrast, inside the potential-outcome framework (POSystem). ★ VariableIntensityIVSystem★ reducedForm_eq_sum_crossingEffects★ indicatorWeightedACR_eq_averageCausalResponse★ wald_eq_averageCausalResponse★ wald_eq_late_of_binaryIntensity★ wald_eq_marginResponseAverage
Variable-Intensity Instrumental Variables
This file formalizes a finite ordered-treatment instrumental-variable system for
an Angrist-Imbens style directed instrument contrast, inside the
potential-outcome framework (POSystem). The instrument, treatment intensity,
and outcome are system variables; potential intensities D(z) and
treatment-indexed potential outcomes Y(d) are genuine counterfactuals
(POVar.cfUnder), and consistency / instrument-independence are the project's
canonical PO assumptions (POSystem.Consistency, POSystem.IndepCF) rather than
ad-hoc structure fields.
It defines margin-specific causal responses, crossing events, and the population objects needed to express average causal responses over crossed treatment margins; the directed Wald estimand; the headline average-causal-response characterization; binary-treatment and constant-response specializations; and an interface-only population 2SLS score/decomposition layer.
A variable-intensity IV system records an instrument, an ordered treatment intensity, and an outcome inside a potential-outcome system, with the treatment taking at least one margin.
Definition (Lean source)
Given a variable-intensity IV system, the instrument potential-outcome variable is that system's instrument, represented with its finite instrument-value space.
Definition (Lean source)
Given a variable-intensity IV system, the treatment-intensity potential-outcome variable is its ordered treatment, whose admissible levels run from zero through .
Definition (Lean source)
Given a variable-intensity IV system, the outcome potential-outcome variable is its real-valued outcome.
Definition (Lean source)
Given a variable-intensity IV system and an instrument value, the potential treatment intensity assigns every unit the ordered treatment level that would be observed if the instrument were fixed to that value.
Definition (Lean source)
Given a variable-intensity IV system and a treatment level, the treatment-indexed potential outcome assigns every unit the outcome that would be observed if treatment intensity were fixed to that level.
Definition (Lean source)
Given a variable-intensity IV system, the factual instrument assigns each unit its observed instrument value.
Definition (Lean source)
Given a variable-intensity IV system, the factual treatment intensity assigns each unit its observed ordered treatment level.
Definition (Lean source)
Given a variable-intensity IV system, the factual outcome assigns each unit its observed real-valued outcome.
Definition (Lean source)
Given a variable-intensity IV system and an instrument value, the instrument cell is the set of units whose factual instrument equals that value.
Definition (Lean source)
Given a variable-intensity IV system and an instrument value, the regimed treatment variable is the treatment variable under the regime that fixes the instrument to that value.
Definition (Lean source)
Given a variable-intensity IV system and a treatment level, the regimed outcome variable is the outcome variable under the regime that fixes treatment to that level.
Definition (Lean source)
Given a variable-intensity IV system, the outcome counterfactual bundle contains the potential outcomes at every one of the ordered treatment levels.
Definition (Lean source)
Given a variable-intensity IV system and two instrument values, the contrast counterfactual bundle contains the potential treatments under those values and all treatment-indexed potential outcomes.
Definition (Lean source)
Given a variable-intensity IV system and a treatment margin, the unit-level margin response assigns each unit the difference between its potential outcomes at the upper and lower levels of that margin.
Definition (Lean source)
Given a variable-intensity IV system, two instrument values, and a treatment margin, the crossing event is the set of units whose potential treatment moves across that margin when the instrument changes from the first value to the second.
Definition (Lean source)
Given a variable-intensity IV system, two instrument values, and a treatment margin, the crossing probability is the probability of the corresponding crossing event.
Given a variable-intensity IV system and two instrument values, the total crossing probability is the sum of the crossing probabilities over all treatment margins.
Definition (Lean source)
Given a variable-intensity IV system, two instrument values, and a treatment margin, the normalized margin-crossing weight is that margin's crossing probability divided by total crossing probability.
Definition (Lean source)
Given a variable-intensity IV system, two instrument values, and a treatment margin, the indicator-weighted margin effect is the population mean of the unit-level margin response restricted to the corresponding crossing event.
Definition (Lean source)
Given a variable-intensity IV system and two instrument values, the unnormalized average-causal-response contrast is the sum of indicator-weighted margin effects over all treatment margins.
Definition (Lean source)
Given a variable-intensity IV system and two instrument values, the indicator-weighted average causal response is the unnormalized contrast divided by total crossing probability.
Definition (Lean source)
Given a variable-intensity IV system, two instrument values, and a treatment margin, the conditional margin response is the average unit-level causal response among units whose potential treatment crosses that margin when the instrument changes from the first value to the second.
Definition (Lean source)
Given a variable-intensity IV system and two instrument values, the Angrist--Imbens average causal response is the crossing-probability-weighted sum of conditional margin responses.
Definition (Lean source)
Given a variable-intensity IV system and an instrument value, the instrument-induced potential outcome assigns each unit the potential outcome at the treatment level induced by that instrument value.
Definition (Lean source)
Given a variable-intensity IV system and two instrument values, the potential first-stage contrast is the population mean of the difference between the real-valued potential treatment intensities under the second and first values.
Definition (Lean source)
Given a variable-intensity IV system and two instrument values, the potential reduced-form contrast is the population mean of the difference between instrument-induced potential outcomes under the second and first values.
Definition (Lean source)
Given a variable-intensity IV system and an instrument value, the observed first-stage conditional mean is the conditional mean of factual treatment intensity in the instrument cell at that value.
Definition (Lean source)
Given a variable-intensity IV system and an instrument value, the observed reduced-form conditional mean is the conditional mean of the factual outcome in the instrument cell at that value.
Definition (Lean source)
Given a variable-intensity IV system and two instrument values, the directed Wald estimand is the difference in observed conditional outcome means divided by the corresponding difference in observed conditional treatment-intensity means.
Definition (Lean source)
IV-validity assumptions for a fixed directed contrast (z0,z1).
Definition (Lean source)
Consistency (SUTVA): observed D/Y equal the realized potential
intensity/outcome, D = D(Z), Y = Y(D).
H1: instrument independence from the contrast-relevant counterfactuals,
Z ⟂ (D(z0), D(z1), Y(0),…,Y(J)).
H5: directed monotonicity, D(z1) ≥ D(z0), a.s.
H6: positive first stage.
H7: treatment-indexed potential outcomes are integrable.
Reduced-form decomposition across crossed margins. Fix a directed instrument contrast (z0, z1). Under the variable-intensity IV validity assumptions — SUTVA consistency of treatment and outcome, instrument independence from the potential treatments and treatment-indexed potential outcomes, almost-sure directed monotonicity of the potential treatment intensity in the instrument, a positive first stage, and integrability of every treatment-indexed potential outcome, the potential reduced-form contrast E[Y(D(z1)) − Y(D(z0))] equals the sum, over treatment-intensity margins, of the expected unit causal response on each margin restricted to the event that the instrument move from z0 to z1 crosses that margin.
Formal statement
Proof (Lean source)
Indicator-weighted and conditional-mean ACR forms agree. For any pair of instrument values z0 and z1, the indicator-weighted average causal response — the ratio of the summed crossing-indicator-weighted outcome contrasts to the summed crossing probabilities — equals the crossing-probability- weighted average of the conditional-mean margin responses.
Formal statement
Proof (Lean source)
Angrist-Imbens average-causal-response characterization. Under the variable-intensity IV validity assumptions, with the instrument cell Z = z0 having positive probability and the instrument cell Z = z1 having positive probability, the directed Wald estimand — the ratio of the reduced-form to first-stage conditional-mean contrasts across the two instrument cells — equals the Angrist-Imbens average causal response: the crossing-probability-weighted average, over treatment-intensity margins, of the conditional mean causal response given that the instrument move from z0 to z1 crosses that margin.
Formal statement
Proof (Lean source)
Given the condition that there is exactly one treatment margin, the unique binary-treatment margin is the sole margin of the ordered treatment scale.
Binary-intensity specialization: Wald recovers LATE. Under the variable-intensity IV validity assumptions, with positive probability of the instrument cell Z = z0, positive probability of the instrument cell Z = z1, and a single treatment margin, J = 1, the directed Wald estimand equals the conditional mean unit causal response given the unique crossing event — the classical binary-treatment local average treatment effect.
Formal statement
Proof (Lean source)
Margin-specific response average specialization. Under the variable-intensity IV validity assumptions, with positive probability of the instrument cell Z = z0, positive probability of the instrument cell Z = z1, and a candidate margin-response function m that agrees, on each treatment-intensity margin, with the conditional mean causal response given that margin's crossing event, the directed Wald estimand equals the crossing-probability-weighted average of m across margins.
Formal statement
Proof (Lean source)
Centered finite instrument score used to define an interface-only population 2SLS estimand for multivalued instruments.
Definition (Lean source)
Given a population 2SLS score, the first-stage fitted treatment assigns each unit the linear projection of its factual treatment intensity onto that score.
Definition (Lean source)
Given a population 2SLS score, the population 2SLS estimand is the ratio of the population mean fitted-treatment--outcome product to the population mean fitted-treatment--treatment product.
Definition (Lean source)
Deferred interface for expanding a multivalued-instrument 2SLS estimand into finite directed contrasts. A later theorem can add sign-alignment assumptions to turn this signed decomposition into a convex ACR average.
Definition (Lean source)
23 supporting declarations (lemmas, instances)
-
measurable_DofZlemma — The potential treatment under a fixed instrument value is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_DofZ (z : 𝒵) : Measurable (S.DofZ z) := S.dVar.measurable_cfUnder S.zVar z -
measurable_YofDlemma — The potential outcome under a fixed treatment value is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_YofD (d : Fin (J + 1)) : Measurable (S.YofD d) := S.yVar.measurable_cfUnder S.dVar d -
measurable_factualZlemma — The factual instrument is measurable.hypothesesconclusionMeasurable S.factualZProof (Lean source)
@[fun_prop] lemma measurable_factualZ : Measurable S.factualZ := S.zVar.measurable_factual -
measurable_factualDlemma — The factual treatment is measurable.hypothesesconclusionMeasurable S.factualDProof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The factual outcome is measurable.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurableSet_zEventlemma — The factual instrument cell is measurable.Proof (Lean source)
lemma measurableSet_zEvent (z : 𝒵) : MeasurableSet (S.zEvent z) := S.zVar.measurableSet_event z (MeasurableSet.singleton z) -
measurable_intensityValuelemma — Reading an ordered treatment level as a real intensity is a measurable map on the finite level set.hypothesesJ :sharedℕconclusionMeasurable (fun d : Fin (J + 1) => OrderedTreatment.intensityValue d) -
measurable_intensityValue_DofZlemma — The real intensity of the potential treatment at a fixed instrument value is a measurable function of the unit.hypotheses𝒵 :sharedType u_1J :sharedℕz :𝒵conclusionMeasurable (fun ω => OrderedTreatment.intensityValue (S.DofZ z ω))Proof (Lean source)
@[fun_prop] lemma measurable_intensityValue_DofZ (z : 𝒵) : Measurable (fun ω => OrderedTreatment.intensityValue (S.DofZ z ω)) := (measurable_intensityValue (J := J)).comp (S.measurable_DofZ z) -
integrable_intensityValue_DofZlemma — The real intensity of the potential treatment at a fixed instrument value is integrable, being a bounded measurable function under a finite measure.hypotheses𝒵 :sharedType u_1J :sharedℕz :𝒵conclusionIntegrable (fun ω => OrderedTreatment.intensityValue (S.DofZ z ω)) P.μProof (Lean source)
@[fun_prop] lemma integrable_intensityValue_DofZ (z : 𝒵) : Integrable (fun ω => OrderedTreatment.intensityValue (S.DofZ z ω)) P.μ := by have hbdd : ∀ ω, ‖OrderedTreatment.intensityValue (S.DofZ z ω)‖ ≤ (J : ℝ) := by intro ω change |((S.DofZ z ω).val : ℝ)| ≤ (J : ℝ) rw [abs_of_nonneg (by exact_mod_cast zero_le (S.DofZ z ω).val)] exact_mod_cast Nat.le_of_lt_succ (S.DofZ z ω).isLt exact (MeasureTheory.integrable_const (J : ℝ)).mono' (S.measurable_intensityValue_DofZ z).aestronglyMeasurable (Filter.Eventually.of_forall hbdd) -
YofDofZ_deflemma — The potential outcome under the treatment intensity that an instrument value induces sends a unit to that unit's potential outcome at the induced intensity.hypotheses𝒵 :sharedType u_1J :sharedℕz :𝒵conclusionS.YofDofZ z = fun ω => S.YofD (S.DofZ z ω) ωProof (Lean source)
@[causal_defs_simps] lemma YofDofZ_def (z : 𝒵) : S.YofDofZ z = fun ω => S.YofD (S.DofZ z ω) ω := rfl -
measurable_YofDofZlemma — The potential outcome under the instrument-induced treatment level is a measurable function of the unit.Proof (Lean source)
@[fun_prop] lemma measurable_YofDofZ (z : 𝒵) : Measurable (S.YofDofZ z) := by classical unfold YofDofZ have hsum : (fun ω => S.YofD (S.DofZ z ω) ω) = fun ω => ∑ d : Fin (J + 1), ({d} : Set (Fin (J + 1))).indicator (fun _ => S.YofD d ω) (S.DofZ z ω) := by funext ω rw [Finset.sum_eq_single (S.DofZ z ω)] · simp · intro d _ hd simp [hd] · intro h simp at h rw [hsum] refine measurable_sum _ ?_ intro d _ exact (S.measurable_YofD d).indicator ((MeasurableSet.singleton d).preimage (S.measurable_DofZ z)) -
integrable_marginResponselemma — Integrability of a margin response, derived from H7.hypothesesconclusionIntegrable (S.marginResponse j) P.μProof (Lean source)
lemma integrable_marginResponse {z0 z1 : 𝒵} (hValid : S.ValidContrastAssumptions z0 z1) (j : Fin J) : Integrable (S.marginResponse j) P.μ := by exact (hValid.hIntegrableY (OrderedTreatment.upperLevel j)).sub (hValid.hIntegrableY (OrderedTreatment.lowerLevel j)) -
DofZ_eq_factualD_on_zEventlemma — On zEvent z, the counterfactual intensity D(z) equals the factual D.hypotheses𝒵 :sharedType u_1J :sharedℕhC :P.Consistencyz :𝒵ω :P.Ωhω :ω ∈ S.zEvent zconclusionS.DofZ z ω = S.factualD ωProof (Lean source)
lemma DofZ_eq_factualD_on_zEvent (hC : P.Consistency) (z : 𝒵) {ω : P.Ω} (hω : ω ∈ S.zEvent z) : S.DofZ z ω = S.factualD ω := POVar.cf_eq_factual_on_event hC S.dVar S.zVar z S.hZD.symm hω -
factualY_eq_YofD_factualDlemma — Factual Y equals the counterfactual Y(factualD ω).hypotheses𝒵 :sharedType u_1J :sharedℕhC :P.Consistencyω :P.ΩconclusionS.factualY ω = S.YofD (S.factualD ω) ωProof (Lean source)
lemma factualY_eq_YofD_factualD (hC : P.Consistency) (ω : P.Ω) : S.factualY ω = S.YofD (S.factualD ω) ω := POVar.factual_eq_cfUnder_self_selected hC S.yVar S.dVar S.hDY.symm ω -
condExpDZ_left_eq_integrallemma — First-stage bridge (left cell z0): the observed first-stage conditional mean equals the unconditional expectation of the potential intensity D(z0).hypotheses𝒵 :sharedType u_1J :sharedℕz0 z1 :𝒵hValid :S.ValidContrastAssumptions z0 z1hCell0 :0 < (P.μ (S.zEvent z0)).toRealconclusionS.condExpDZ z0 = ∫ ω, OrderedTreatment.intensityValue (S.DofZ z0 ω) ∂P.μProof (Lean source)
lemma condExpDZ_left_eq_integral {z0 z1 : 𝒵} (hValid : S.ValidContrastAssumptions z0 z1) (hCell0 : 0 < (P.μ (S.zEvent z0)).toReal) : S.condExpDZ z0 = ∫ ω, OrderedTreatment.intensityValue (S.DofZ z0 ω) ∂P.μ := by have hμne_zero : P.μ (S.zVar.event z0) ≠ 0 := fun h => absurd hCell0 (by simp [show S.zEvent z0 = S.zVar.event z0 from rfl, h]) have hμne_top : P.μ (S.zVar.event z0) ≠ ⊤ := measure_ne_top _ _ let idx0 : Fin (S.cfContrastBundle z0 z1).n := ⟨0, by simp [cfContrastBundle, outcomeBundle, POCFBundle.cons]⟩ let hproj : (∀ i : Fin (S.cfContrastBundle z0 z1).n, (S.cfContrastBundle z0 z1).type i) → ℝ := fun f => OrderedTreatment.intensityValue (f idx0) have hh_meas : Measurable hproj := by change Measurable fun f : (∀ i : Fin (S.cfContrastBundle z0 z1).n, (S.cfContrastBundle z0 z1).type i) => OrderedTreatment.intensityValue (f idx0) exact (measurable_intensityValue (J := J)).comp (measurable_pi_apply idx0) have h_cons : ∀ ω ∈ S.zVar.event z0, OrderedTreatment.intensityValue (S.factualD ω) = hproj ((S.cfContrastBundle z0 z1).jointValue ω) := by intro ω hω rw [← S.DofZ_eq_factualD_on_zEvent hValid.consistency z0 hω] change OrderedTreatment.intensityValue (S.DofZ z0 ω) = OrderedTreatment.intensityValue ((S.cfContrastBundle z0 z1).jointValue ω idx0) rfl have hbridge : S.condExpDZ z0 = eventCondExp P.μ (S.zVar.event z0) (fun ω => OrderedTreatment.intensityValue (S.factualD ω)) := rfl rw [hbridge, POSystem.eventCondExp_of_consistency_IndepCF hValid.hIndependence (a := S.zVar) hh_meas (MeasurableSet.singleton z0) (ae_restrict_of_forall_mem (S.measurableSet_zEvent z0) h_cons) hμne_zero hμne_top] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω change OrderedTreatment.intensityValue ((S.cfContrastBundle z0 z1).jointValue ω idx0) = OrderedTreatment.intensityValue (S.DofZ z0 ω) rfl -
condExpDZ_right_eq_integrallemma — First-stage bridge (right cell z1).hypotheses𝒵 :sharedType u_1J :sharedℕz0 z1 :𝒵hValid :S.ValidContrastAssumptions z0 z1hCell1 :0 < (P.μ (S.zEvent z1)).toRealconclusionS.condExpDZ z1 = ∫ ω, OrderedTreatment.intensityValue (S.DofZ z1 ω) ∂P.μProof (Lean source)
lemma condExpDZ_right_eq_integral {z0 z1 : 𝒵} (hValid : S.ValidContrastAssumptions z0 z1) (hCell1 : 0 < (P.μ (S.zEvent z1)).toReal) : S.condExpDZ z1 = ∫ ω, OrderedTreatment.intensityValue (S.DofZ z1 ω) ∂P.μ := by have hμne_zero : P.μ (S.zVar.event z1) ≠ 0 := fun h => absurd hCell1 (by simp [show S.zEvent z1 = S.zVar.event z1 from rfl, h]) have hμne_top : P.μ (S.zVar.event z1) ≠ ⊤ := measure_ne_top _ _ let idx1 : Fin (S.cfContrastBundle z0 z1).n := ⟨1, by simp [cfContrastBundle, outcomeBundle, POCFBundle.cons]⟩ let hproj : (∀ i : Fin (S.cfContrastBundle z0 z1).n, (S.cfContrastBundle z0 z1).type i) → ℝ := fun f => OrderedTreatment.intensityValue (f idx1) have hh_meas : Measurable hproj := by change Measurable fun f : (∀ i : Fin (S.cfContrastBundle z0 z1).n, (S.cfContrastBundle z0 z1).type i) => OrderedTreatment.intensityValue (f idx1) exact (measurable_intensityValue (J := J)).comp (measurable_pi_apply idx1) have h_cons : ∀ ω ∈ S.zVar.event z1, OrderedTreatment.intensityValue (S.factualD ω) = hproj ((S.cfContrastBundle z0 z1).jointValue ω) := by intro ω hω rw [← S.DofZ_eq_factualD_on_zEvent hValid.consistency z1 hω] change OrderedTreatment.intensityValue (S.DofZ z1 ω) = OrderedTreatment.intensityValue ((S.cfContrastBundle z0 z1).jointValue ω idx1) rfl have hbridge : S.condExpDZ z1 = eventCondExp P.μ (S.zVar.event z1) (fun ω => OrderedTreatment.intensityValue (S.factualD ω)) := rfl rw [hbridge, POSystem.eventCondExp_of_consistency_IndepCF hValid.hIndependence (a := S.zVar) hh_meas (MeasurableSet.singleton z1) (ae_restrict_of_forall_mem (S.measurableSet_zEvent z1) h_cons) hμne_zero hμne_top] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω change OrderedTreatment.intensityValue ((S.cfContrastBundle z0 z1).jointValue ω idx1) = OrderedTreatment.intensityValue (S.DofZ z1 ω) rfl -
condExpYZ_left_eq_integrallemma — Reduced-form bridge (left cell z0): the observed reduced-form conditional mean equals the unconditional expectation of Y(D(z0)).hypotheses𝒵 :sharedType u_1J :sharedℕz0 z1 :𝒵hValid :S.ValidContrastAssumptions z0 z1hCell0 :0 < (P.μ (S.zEvent z0)).toRealconclusionS.condExpYZ z0 = ∫ ω, S.YofDofZ z0 ω ∂P.μProof (Lean source)
lemma condExpYZ_left_eq_integral {z0 z1 : 𝒵} (hValid : S.ValidContrastAssumptions z0 z1) (hCell0 : 0 < (P.μ (S.zEvent z0)).toReal) : S.condExpYZ z0 = ∫ ω, S.YofDofZ z0 ω ∂P.μ := by classical have hμne_zero : P.μ (S.zVar.event z0) ≠ 0 := fun h => absurd hCell0 (by simp [show S.zEvent z0 = S.zVar.event z0 from rfl, h]) have hμne_top : P.μ (S.zVar.event z0) ≠ ⊤ := measure_ne_top _ _ let idx0 : Fin (S.cfContrastBundle z0 z1).n := ⟨0, by simp [cfContrastBundle, outcomeBundle, POCFBundle.cons]⟩ let idxY (i : Fin (J + 1)) : Fin (S.cfContrastBundle z0 z1).n := Fin.succ (Fin.succ i) let hproj : (∀ i : Fin (S.cfContrastBundle z0 z1).n, (S.cfContrastBundle z0 z1).type i) → ℝ := fun f => ∑ i : Fin (J + 1), if f idx0 = i then f (idxY i) else 0 have hh_meas : Measurable hproj := by change Measurable fun f : (∀ i : Fin (S.cfContrastBundle z0 z1).n, (S.cfContrastBundle z0 z1).type i) => ∑ i : Fin (J + 1), if f idx0 = i then f (idxY i) else 0 refine measurable_sum _ ?_ intro i _hi refine Measurable.ite ?_ (measurable_pi_apply (idxY i)) measurable_const exact (MeasurableSet.singleton i).preimage (measurable_pi_apply idx0) have h_cons : ∀ ω ∈ S.zVar.event z0, S.factualY ω = hproj ((S.cfContrastBundle z0 z1).jointValue ω) := by intro ω hω rw [S.factualY_eq_YofD_factualD hValid.consistency ω, ← S.DofZ_eq_factualD_on_zEvent hValid.consistency z0 hω] have hJV0 : (S.cfContrastBundle z0 z1).jointValue ω idx0 = S.DofZ z0 ω := rfl have hJVY : ∀ i : Fin (J + 1), (S.cfContrastBundle z0 z1).jointValue ω (idxY i) = S.YofD i ω := by intro i rfl change S.YofD (S.DofZ z0 ω) ω = ∑ i : Fin (J + 1), if (S.cfContrastBundle z0 z1).jointValue ω idx0 = i then (S.cfContrastBundle z0 z1).jointValue ω (idxY i) else 0 rw [hJV0] rw [Finset.sum_eq_single (S.DofZ z0 ω)] · exact (hJVY _).symm.trans (if_pos rfl).symm · intro i _hi hi by_cases hEq : S.DofZ z0 ω = i · exact elim (hi hEq.symm) · exact if_neg hEq · intro h simp at h have hbridge : S.condExpYZ z0 = eventCondExp P.μ (S.zVar.event z0) S.factualY := rfl rw [hbridge, POSystem.eventCondExp_of_consistency_IndepCF hValid.hIndependence (a := S.zVar) hh_meas (MeasurableSet.singleton z0) (ae_restrict_of_forall_mem (S.measurableSet_zEvent z0) h_cons) hμne_zero hμne_top] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω have hJV0 : (S.cfContrastBundle z0 z1).jointValue ω idx0 = S.DofZ z0 ω := rfl have hJVY : ∀ i : Fin (J + 1), (S.cfContrastBundle z0 z1).jointValue ω (idxY i) = S.YofD i ω := by intro i rfl change (∑ i : Fin (J + 1), if (S.cfContrastBundle z0 z1).jointValue ω idx0 = i then (S.cfContrastBundle z0 z1).jointValue ω (idxY i) else 0) = S.YofDofZ z0 ω unfold YofDofZ rw [hJV0] rw [Finset.sum_eq_single (S.DofZ z0 ω)] · exact (if_pos rfl).trans (hJVY _) · intro i _hi hi by_cases hEq : S.DofZ z0 ω = i · exact elim (hi hEq.symm) · exact if_neg hEq · intro h simp at h -
condExpYZ_right_eq_integrallemma — Reduced-form bridge (right cell z1).hypotheses𝒵 :sharedType u_1J :sharedℕz0 z1 :𝒵hValid :S.ValidContrastAssumptions z0 z1hCell1 :0 < (P.μ (S.zEvent z1)).toRealconclusionS.condExpYZ z1 = ∫ ω, S.YofDofZ z1 ω ∂P.μProof (Lean source)
lemma condExpYZ_right_eq_integral {z0 z1 : 𝒵} (hValid : S.ValidContrastAssumptions z0 z1) (hCell1 : 0 < (P.μ (S.zEvent z1)).toReal) : S.condExpYZ z1 = ∫ ω, S.YofDofZ z1 ω ∂P.μ := by classical have hμne_zero : P.μ (S.zVar.event z1) ≠ 0 := fun h => absurd hCell1 (by simp [show S.zEvent z1 = S.zVar.event z1 from rfl, h]) have hμne_top : P.μ (S.zVar.event z1) ≠ ⊤ := measure_ne_top _ _ let idx1 : Fin (S.cfContrastBundle z0 z1).n := ⟨1, by simp [cfContrastBundle, outcomeBundle, POCFBundle.cons]⟩ let idxY (i : Fin (J + 1)) : Fin (S.cfContrastBundle z0 z1).n := Fin.succ (Fin.succ i) let hproj : (∀ i : Fin (S.cfContrastBundle z0 z1).n, (S.cfContrastBundle z0 z1).type i) → ℝ := fun f => ∑ i : Fin (J + 1), if f idx1 = i then f (idxY i) else 0 have hh_meas : Measurable hproj := by change Measurable fun f : (∀ i : Fin (S.cfContrastBundle z0 z1).n, (S.cfContrastBundle z0 z1).type i) => ∑ i : Fin (J + 1), if f idx1 = i then f (idxY i) else 0 refine measurable_sum _ ?_ intro i _hi refine Measurable.ite ?_ (measurable_pi_apply (idxY i)) measurable_const exact (MeasurableSet.singleton i).preimage (measurable_pi_apply idx1) have h_cons : ∀ ω ∈ S.zVar.event z1, S.factualY ω = hproj ((S.cfContrastBundle z0 z1).jointValue ω) := by intro ω hω rw [S.factualY_eq_YofD_factualD hValid.consistency ω, ← S.DofZ_eq_factualD_on_zEvent hValid.consistency z1 hω] have hJV1 : (S.cfContrastBundle z0 z1).jointValue ω idx1 = S.DofZ z1 ω := rfl have hJVY : ∀ i : Fin (J + 1), (S.cfContrastBundle z0 z1).jointValue ω (idxY i) = S.YofD i ω := by intro i rfl change S.YofD (S.DofZ z1 ω) ω = ∑ i : Fin (J + 1), if (S.cfContrastBundle z0 z1).jointValue ω idx1 = i then (S.cfContrastBundle z0 z1).jointValue ω (idxY i) else 0 rw [hJV1] rw [Finset.sum_eq_single (S.DofZ z1 ω)] · exact (hJVY _).symm.trans (if_pos rfl).symm · intro i _hi hi by_cases hEq : S.DofZ z1 ω = i · exact elim (hi hEq.symm) · exact if_neg hEq · intro h simp at h have hbridge : S.condExpYZ z1 = eventCondExp P.μ (S.zVar.event z1) S.factualY := rfl rw [hbridge, POSystem.eventCondExp_of_consistency_IndepCF hValid.hIndependence (a := S.zVar) hh_meas (MeasurableSet.singleton z1) (ae_restrict_of_forall_mem (S.measurableSet_zEvent z1) h_cons) hμne_zero hμne_top] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω have hJV1 : (S.cfContrastBundle z0 z1).jointValue ω idx1 = S.DofZ z1 ω := rfl have hJVY : ∀ i : Fin (J + 1), (S.cfContrastBundle z0 z1).jointValue ω (idxY i) = S.YofD i ω := by intro i rfl change (∑ i : Fin (J + 1), if (S.cfContrastBundle z0 z1).jointValue ω idx1 = i then (S.cfContrastBundle z0 z1).jointValue ω (idxY i) else 0) = S.YofDofZ z1 ω unfold YofDofZ rw [hJV1] rw [Finset.sum_eq_single (S.DofZ z1 ω)] · exact (if_pos rfl).trans (hJVY _) · intro i _hi hi by_cases hEq : S.DofZ z1 ω = i · exact elim (hi hEq.symm) · exact if_neg hEq · intro h simp at h -
firstStage_eq_sum_crossingProbtheorem — First-stage denominator equals the sum of crossing probabilities.hypotheses𝒵 :sharedType u_1J :sharedℕz0 z1 :𝒵hValid :S.ValidContrastAssumptions z0 z1conclusionS.firstStageContrast z0 z1 = ∑ j : Fin J, S.crossingProb z0 z1 jProof (Lean source)
theorem firstStage_eq_sum_crossingProb {z0 z1 : 𝒵} (hValid : S.ValidContrastAssumptions z0 z1) : S.firstStageContrast z0 z1 = ∑ j : Fin J, S.crossingProb z0 z1 j := by unfold firstStageContrast crossingProb have hpoint : (fun ω => OrderedTreatment.intensityValue (S.DofZ z1 ω) - OrderedTreatment.intensityValue (S.DofZ z0 ω)) =ᵐ[P.μ] fun ω => ∑ j : Fin J, OrderedTreatment.crossingIndicator (S.DofZ z0 ω) (S.DofZ z1 ω) j := hValid.hMonotone.mono fun _ hmono => OrderedTreatment.ordered_telescope_identity hmono calc ∫ ω, (OrderedTreatment.intensityValue (S.DofZ z1 ω) - OrderedTreatment.intensityValue (S.DofZ z0 ω)) ∂P.μ = ∫ ω, ∑ j : Fin J, OrderedTreatment.crossingIndicator (S.DofZ z0 ω) (S.DofZ z1 ω) j ∂P.μ := by exact MeasureTheory.integral_congr_ae hpoint _ = ∑ j : Fin J, ∫ ω, OrderedTreatment.crossingIndicator (S.DofZ z0 ω) (S.DofZ z1 ω) j ∂P.μ := by rw [MeasureTheory.integral_finset_sum] intro i _hi rw [S.crossingIndicator_fun_eq_indicator z0 z1 i] exact (MeasureTheory.integrable_const (μ := P.μ) (1 : ℝ)).indicator (S.measurableSet_crossingEvent z0 z1 i) _ = ∑ j : Fin J, (P.μ (S.crossingEvent z0 z1 j)).toReal := by refine Finset.sum_congr rfl ?_ intro j _hj rw [S.crossingIndicator_fun_eq_indicator z0 z1 j] exact MeasureTheory.integral_indicator_one (S.measurableSet_crossingEvent z0 z1 j) -
crossingWeight_nonneglemma — Crossing weights are nonnegative for a valid directed contrast.hypothesesconclusion0 ≤ S.crossingWeight z0 z1 jProof (Lean source)
lemma crossingWeight_nonneg {z0 z1 : 𝒵} (hValid : S.ValidContrastAssumptions z0 z1) (j : Fin J) : 0 ≤ S.crossingWeight z0 z1 j := by have hProb : ∀ i : Fin J, 0 ≤ S.crossingProb z0 z1 i := by intro i exact ENNReal.toReal_nonneg have hSum : 0 < ∑ i : Fin J, S.crossingProb z0 z1 i := by rw [← S.firstStage_eq_sum_crossingProb hValid] exact hValid.hRelevance exact OrderedTreatment.normalizedWeight_nonneg (S.crossingProb z0 z1) hProb hSum j -
sum_crossingWeight_eq_onelemma — Crossing weights sum to one for a valid directed contrast.hypotheses𝒵 :sharedType u_1J :sharedℕz0 z1 :𝒵hValid :S.ValidContrastAssumptions z0 z1conclusion∑ j : Fin J, S.crossingWeight z0 z1 j = 1Proof (Lean source)
lemma sum_crossingWeight_eq_one {z0 z1 : 𝒵} (hValid : S.ValidContrastAssumptions z0 z1) : ∑ j : Fin J, S.crossingWeight z0 z1 j = 1 := by have hSum : 0 < ∑ i : Fin J, S.crossingProb z0 z1 i := by rw [← S.firstStage_eq_sum_crossingProb hValid] exact hValid.hRelevance exact OrderedTreatment.sum_normalizedWeight_eq_one (S.crossingProb z0 z1) hSum -
crossingEvent_eq_complianceEventlemma — Under J = 1, the unique crossing event coincides with the complier event {D(z1) = Fin.last J ∧ D(z0) = 0}, i.e. the unit jump from level 0 to the maximum level. When J = 1, Fin.last 1 = 1 : Fin 2, so this recovers exactly the binary-treatment LATE complier event {D(z1) = 1 ∧ D(z0) = 0} of Imbens-Angrist (1994): β_Wald(z0,z1) = E[Y(1) − Y(0) | D(z1) = Fin.last J ∧ D(z0) = 0].hypotheses𝒵 :sharedType u_1J :sharedℕz0 z1 :𝒵hJ :J = 1conclusionS.crossingEvent z0 z1 (binaryMargin hJ)Proof (Lean source)
lemma crossingEvent_eq_complianceEvent (z0 z1 : 𝒵) (hJ : J = 1) : S.crossingEvent z0 z1 (binaryMargin hJ) = {ω | S.DofZ z1 ω = last J ∧ S.DofZ z0 ω = (0 : Fin (J + 1))} := by subst hJ ext ω simp only [binaryMargin, crossingEvent, OrderedTreatment.Crossing, OrderedTreatment.upperLevel, Set.mem_setOf_eq, last] have hone : (Fin.succ (0 : Fin 1)) = (⟨1, by omega⟩ : Fin 2) := by decide rw [hone] have hone_val : (⟨1, by omega⟩ : Fin 2).val = 1 := rfl constructor · rintro ⟨h1, h2⟩ refine ⟨le_antisymm (Fin.le_last _) h1, Fin.ext ?_⟩ have hv2 : (S.DofZ z0 ω).val < (⟨1, by omega⟩ : Fin 2).val := Fin.val_fin_lt.mpr h2 rw [hone_val] at hv2 have hge : 0 ≤ (S.DofZ z0 ω).val := zero_le _ simp only [Fin.val_zero] omega · rintro ⟨h1, h2⟩ refine ⟨h1 ▸ le_refl _, Fin.val_fin_lt.mp ?_⟩ rw [hone_val] have hv2 : (S.DofZ z0 ω).val = (0 : Fin 2).val := congr_arg val h2 simp only [Fin.val_zero] at hv2 omega -
wald_eq_constantResponsetheorem — Constant marginal response specialization.hypotheses𝒵 :sharedType u_1J :sharedℕz0 z1 :𝒵τ :ℝhValid :S.ValidContrastAssumptions z0 z1hCell0 :0 < (P.μ (S.zEvent z0)).toRealhCell1 :0 < (P.μ (S.zEvent z1)).toRealhConstantResponse :∀ j : Fin J, S.marginResponse j =ᵐ[P.μ] fun _ => τconclusionS.wald z0 z1 = τProof (Lean source)
theorem wald_eq_constantResponse {z0 z1 : 𝒵} {τ : ℝ} (hValid : S.ValidContrastAssumptions z0 z1) (hCell0 : 0 < (P.μ (S.zEvent z0)).toReal) (hCell1 : 0 < (P.μ (S.zEvent z1)).toReal) (hConstantResponse : ∀ j : Fin J, S.marginResponse j =ᵐ[P.μ] fun _ => τ) : S.wald z0 z1 = τ := by rw [S.wald_eq_averageCausalResponse hValid hCell0 hCell1] rw [← S.indicatorWeightedACR_eq_averageCausalResponse] unfold indicatorWeightedACR unnormalizedACRContrast totalCrossingProb indicatorWeightedEffect crossingProb have hterm : ∀ j : Fin J, (∫ ω in S.crossingEvent z0 z1 j, S.marginResponse j ω ∂P.μ) = τ * (P.μ (S.crossingEvent z0 z1 j)).toReal := by intro j rw [MeasureTheory.setIntegral_congr_ae (S.measurableSet_crossingEvent z0 z1 j) ((hConstantResponse j).mono fun _ hx _ => hx)] rw [MeasureTheory.setIntegral_const, MeasureTheory.Measure.real_def] exact smul_eq_mul _ _ |>.trans (mul_comm _ _) rw [Finset.sum_congr rfl (fun j _ => hterm j), ← Finset.mul_sum] have hpos : 0 < ∑ j : Fin J, (P.μ (S.crossingEvent z0 z1 j)).toReal := by simpa [crossingProb] using (by rw [← S.firstStage_eq_sum_crossingProb hValid] exact hValid.hRelevance : 0 < ∑ j : Fin J, S.crossingProb z0 z1 j) field_simp [ne_of_gt hpos]