PO.ID.Exact.VariableIntensityIV.VariableIntensity
For a treatment with ordered levels 0, …, J and two instrument values z₀ and z₁, the Wald ratio (E[Y | Z = z₁] − E[Y | Z = z₀]) / (E[D | Z = z₁] − E[D | Z = z₀]) equals the Angrist–Imbens average causal response: a weigh
Basic 32 core · 15 supporting This part defines the ordered-treatment IV system, its factual and counterfactual variables, margin-crossing quantities, population contrasts, and validity assumptions. ★ VariableIntensityIVSystem★ YofDofZ_def
Variable-intensity IV definitions and counterfactual bundles
This part defines the ordered-treatment IV system, its factual and counterfactual variables, margin-crossing quantities, population contrasts, and validity assumptions.
structure VariableIntensityIVSystem reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV
A variable-intensity IV system on an ambient potential-outcome model, finite instrument support, and ordered dose scale records an instrument, an ordered treatment intensity, and a real outcome, with at least one treatment margin, the stated value-space identifications, and distinct instrument, treatment, and outcome nodes.
Definition (Lean source)
parameters
fields
The ordered treatment has at least one margin.
hJ_pos :
0 < J
Instrument system variable.
Z :
P.V
Treatment-intensity system variable.
D :
P.V
Outcome system variable.
Y :
P.V
The instrument value space is identified with the finite set `𝒵`.
hZ𝒵 :
P.X Z ≃ᵐ 𝒵
The treatment value space is identified with the ordered levels `Fin (J+1)`.
hDintensity :
P.X D ≃ᵐ Fin (J + 1)
The outcome value space is identified with `ℝ`.
hYreal :
P.X Y ≃ᵐ ℝ
Instrument and treatment are distinct variables.
hZD :
Z ≠ D
Treatment and outcome are distinct variables.
hDY :
D ≠ Y
Instrument and outcome are distinct variables.
hZY :
Z ≠ Y
def zVar reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The finite-valued instrument variable exposes the assignment node of a variable-intensity IV system on its observed support.
Definition (Lean source)
parameters
def
given by
⟨S.Z, S.hZ𝒵⟩
def dVar reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The ordered treatment-intensity variable exposes uptake in a variable-intensity IV system on levels from zero through the maximum dose.
Definition (Lean source)
parameters
given by
⟨S.D, S.hDintensity⟩
def yVar reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The real-valued outcome variable exposes the response node of a variable-intensity IV system on the scale used for causal contrasts.
Definition (Lean source)
parameters
def
given by
⟨S.Y, S.hYreal⟩
def DofZ reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
Potential treatment intensity records the dose each unit in a variable-intensity IV system would take under a fixed instrument value, determining which dose margins the instrument moves that unit across.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z :
𝒵
def
given by
S.dVar.cfUnder S.zVar z
def YofD reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
Treatment-indexed potential outcome records the response each unit in a variable-intensity IV system would have under an intervention fixing the dose.
Definition (Lean source)
parameters
def
YofD S d :
P.Ω → ℝ
given by
S.yVar.cfUnder S.dVar d
def factualZ reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The observed instrument records each unit's realized assignment in a variable-intensity IV system.
Definition (Lean source)
parameters
def
factualZ S :
P.Ω → 𝒵
given by
S.zVar.factual
def factualD reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The observed treatment intensity records each unit's realized dose in a variable-intensity IV system.
Definition (Lean source)
parameters
def
given by
S.dVar.factual
def factualY reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The observed outcome records each unit's realized response in a variable-intensity IV system.
Definition (Lean source)
parameters
def
factualY S :
P.Ω → ℝ
given by
S.yVar.factual
def zEvent reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
An observed instrument cell selects units in a variable-intensity IV system whose realized assignment equals the chosen support value.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z :
𝒵
def
given by
S.zVar.event z
def dUnderZ reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The regimed treatment response couples potential dose in a variable-intensity IV system with the fixed instrument value that generates it, enabling exogeneity statements.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z :
𝒵
def
given by
⟨S.dVar, Regime.single S.Z (S.hZ𝒵.symm z)⟩
def yUnderD reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The regimed outcome response couples potential outcome in a variable-intensity IV system with the fixed treatment level that generates it.
Definition (Lean source)
parameters
def
given by
⟨S.yVar, Regime.single S.D (S.hDintensity.symm d)⟩
def outcomeBundle reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The dose-response counterfactual bundle collects potential outcomes at every ordered treatment level in a variable-intensity IV system, allowing joint instrument independence to cover the whole response schedule.
Definition (Lean source)
parameters
def
given by
clause 1
n := J + 1
clause 2
type := fun _ => ℝ
clause 3
inst := fun _ => inferInstance
clause 4
vars := fun d => S.yUnderD d
def cfContrastBundle reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The directed-contrast counterfactual bundle joins both potential treatments and the full dose-response schedule in a variable-intensity IV system for the two instrument values being compared.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
def
given by
POCFBundle.cons (S.dUnderZ z0) (POCFBundle.cons (S.dUnderZ z1) S.outcomeBundle)
def marginResponse reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The unit-level causal response on a treatment margin is the potential-outcome change across that adjacent dose increment in a variable-intensity IV system.
Definition (Lean source)
parameters
def
marginResponse S j :
P.Ω → ℝ
given by
fun ω
=> S.YofD (OrderedTreatment.upperLevel j) ω - S.YofD (OrderedTreatment.lowerLevel j) ω
def crossingEvent reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
A margin-crossing subgroup contains units in a variable-intensity IV system whose potential dose crosses the selected treatment margin when the instrument moves between the two selected values.
Definition (Lean source)
parameters
def
given by
{ω | OrderedTreatment.Crossing (S.DofZ z0 ω) (S.DofZ z1 ω) j}
def crossingProb reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The margin-crossing probability is the population share in a variable-intensity IV system moved across the selected treatment margin by the directed instrument contrast.
def totalCrossingProb reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
Total crossing probability is the sum of the shares moved across each treatment margin in a variable-intensity IV system by the directed instrument contrast; under monotonicity it is the first-stage denominator.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
def
totalCrossingProb S z0 z1 :
ℝ
given by
∑ j : Fin J, S.crossingProb z0 z1 j
def crossingWeight reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
A normalized margin-crossing weight is the share of the total first stage contributed by one treatment margin in a variable-intensity IV system for the directed instrument contrast.
Definition (Lean source)
parameters
def
crossingWeight S z0 z1 j :
ℝ
given by
OrderedTreatment.normalizedWeight (S.crossingProb z0 z1) j
def indicatorWeightedEffect reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The indicator-weighted margin effect is the population contribution from one causal dose margin among units in a variable-intensity IV system moved across it by the directed instrument contrast.
Definition (Lean source)
parameters
def
indicatorWeightedEffect S z0 z1 j :
ℝ
given by
∫ ω in S.crossingEvent z0 z1 j, S.marginResponse j ω ∂P.μ
def unnormalizedACRContrast reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The unnormalized average-causal-response contrast sums causal responses over every margin crossed in a variable-intensity IV system by the directed instrument contrast.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
def
unnormalizedACRContrast S z0 z1 :
ℝ
given by
∑ j : Fin J, S.indicatorWeightedEffect z0 z1 j
def indicatorWeightedACR reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The indicator-weighted average causal response divides the aggregate crossed-margin effect in a variable-intensity IV system by the total crossing probability for the directed instrument contrast.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
def
indicatorWeightedACR S z0 z1 :
ℝ
given by
S.unnormalizedACRContrast z0 z1 / S.totalCrossingProb z0 z1
def conditionalMarginResponse reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The conditional margin response averages the unit causal response on one treatment margin among units in a variable-intensity IV system whose dose crosses it under the directed instrument contrast.
Definition (Lean source)
parameters
def
conditionalMarginResponse S z0 z1 j :
ℝ
given by
normalizedRestrictedIntegral P.μ (S.crossingEvent z0 z1 j) (S.marginResponse j)
def averageCausalResponse reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The Angrist--Imbens average causal response averages margin-specific causal responses in a variable-intensity IV system with weights equal to their shares of the directed instrument contrast's first stage.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
def
averageCausalResponse S z0 z1 :
ℝ
given by
∑ j : Fin J, S.crossingWeight z0 z1 j * S.conditionalMarginResponse z0 z1 j
def YofDofZ reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The composed dose-response schedule evaluates each unit's treatment-indexed response in a variable-intensity IV system at the potential dose selected by the chosen instrument value.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z :
𝒵
def
YofDofZ S z :
P.Ω → ℝ
given by
fun ω => S.YofD (S.DofZ z ω) ω
lemma YofDofZ_def reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The composed dose-response schedule equals the treatment-indexed response evaluated at the selected potential dose for the potential-outcome system, finite instrument support, and ordered dose scale, the variable-intensity IV system, and the chosen instrument value.
Formal statement
hypotheses
𝒵 :
Type u_1
J :
ℕ
z :
𝒵
conclusion
S.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
def firstStageContrast reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The potential first-stage contrast is the mean dose change induced in a variable-intensity IV system by moving between two instrument values.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
def
firstStageContrast S z0 z1 :
ℝ
given by
∫ ω, (OrderedTreatment.intensityValue (S.DofZ z1 ω) - OrderedTreatment.intensityValue (S.DofZ z0 ω)) ∂P.μ
def reducedFormContrast reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The composed-response contrast is the mean difference between the treatment-indexed response schedules selected in a variable-intensity IV system by two instrument values.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
def
reducedFormContrast S z0 z1 :
ℝ
given by
∫ ω, (S.YofDofZ z1 ω - S.YofDofZ z0 ω) ∂P.μ
def condExpDZ reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The observed first-stage cell mean averages realized treatment intensity in a variable-intensity IV system among units receiving the selected instrument value.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z :
𝒵
def
condExpDZ S z :
ℝ
given by
normalizedRestrictedIntegral P.μ (S.zEvent z) (fun ω => OrderedTreatment.intensityValue (S.factualD ω))
def condExpYZ reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The observed reduced-form cell mean averages realized outcomes in a variable-intensity IV system among units receiving the selected instrument value.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z :
𝒵
def
condExpYZ S z :
ℝ
given by
normalizedRestrictedIntegral P.μ (S.zEvent z) S.factualY
def wald reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
The directed Wald estimand divides the observed outcome-cell contrast in a variable-intensity IV system by the corresponding treatment-intensity contrast between two instrument values.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
def
wald S z0 z1 :
ℝ
given by
(S.condExpYZ z1 - S.condExpYZ z0) / (S.condExpDZ z1 - S.condExpDZ z0)
structure ValidContrastAssumptions reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
IV validity for a directed instrument contrast in a variable-intensity system combines consistency of observed and potential treatment and outcome, joint instrument independence from the relevant treatment and outcome responses, monotone dose movement, a positive first stage, and integrable potential outcomes at every dose.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
assumes
consistency :
P.Consistency
Consistency (SUTVA): observed D/Y equal the realized potential
intensity/outcome, D = D(Z), Y = Y(D).
hIndependence :
P.IndepCF (RegimedVar.ofFactual S.zVar) (S.cfContrastBundle z0 z1) P.μ
The instrument is independent of the contrast-relevant treatment and outcome schedules.
hMonotone :
∀ᵐ ω ∂P.μ, S.DofZ z0 ω ≤ S.DofZ z1 ω
Potential treatment weakly increases along the directed instrument contrast almost surely.
hRelevance :
0 < S.firstStageContrast z0 z1
The directed potential first-stage contrast is strictly positive.
hIntegrableY :
∀ d, Integrable (S.YofD d) P.μ
The potential outcome at every treatment level is integrable.
15 supporting declarations (lemmas, instances)
-
measurable_DofZlemma — Potential treatment at a fixed instrument value is measurable, so the IV system can form treatment-response probabilities for that assignment.Proof (Lean source)
@[fun_prop] lemma measurable_DofZ (z : 𝒵) : Measurable (S.DofZ z) := S.dVar.measurable_cfUnder S.zVar z -
measurable_YofDlemma — Potential outcome at a fixed dose is measurable, permitting causal response averages in the IV system at that treatment level.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 observed instrument is measurable, making assignment cells observable in the IV system.hypothesesconclusionMeasurable S.factualZProof (Lean source)
@[fun_prop] lemma measurable_factualZ : Measurable S.factualZ := S.zVar.measurable_factual -
measurable_factualDlemma — The observed treatment intensity is measurable, so realized dose events are defined in the IV system.hypothesesconclusionMeasurable S.factualDProof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The observed outcome is measurable, so its population moments are defined in the IV system.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurableSet_zEventlemma — Each observed instrument cell is measurable, allowing the IV system to condition observed moments on the selected assignment.Proof (Lean source)
lemma measurableSet_zEvent (z : 𝒵) : MeasurableSet (S.zEvent z) := S.zVar.measurableSet_event z (MeasurableSet.singleton z) -
measurable_intensityValuelemma — The numeric encoding of ordered treatment levels is measurable for the finite dose scale, allowing treatment intensity to enter population moments.hypothesesJ :sharedℕconclusionMeasurable (fun d : Fin (J + 1) => OrderedTreatment.intensityValue d) -
measurable_intensityValue_DofZlemma — Potential treatment intensity at a fixed instrument value is measurable, so the IV system can use it in first-stage moments for that assignment.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 — Potential treatment intensity at a fixed instrument value is integrable in the IV system for that assignment, because the finite ordered dose scale is bounded.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 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) -
measurableSet_crossingEventlemma — Each treatment-margin crossing subgroup is measurable for the potential-outcome system, instrument support, ordered dose scale, IV system, directed instrument contrast, and margin, so its population share is well defined.hypothesesconclusionMeasurableSet (S.crossingEvent z0 z1 j)Proof (Lean source)
lemma measurableSet_crossingEvent (z0 z1 : 𝒵) (j : Fin J) : MeasurableSet (S.crossingEvent z0 z1 j) := by unfold crossingEvent OrderedTreatment.Crossing have hA : MeasurableSet {d : Fin (J + 1) | OrderedTreatment.upperLevel j ≤ d} := Set.Finite.measurableSet (Set.toFinite _) have hB : MeasurableSet {d : Fin (J + 1) | d < OrderedTreatment.upperLevel j} := Set.Finite.measurableSet (Set.toFinite _) exact (hA.preimage (S.measurable_DofZ z1)).inter (hB.preimage (S.measurable_DofZ z0)) -
crossingIndicator_fun_eq_indicatorlemma — The algebraic margin-crossing indicator equals the indicator of the corresponding crossing subgroup for the potential-outcome system, instrument support, ordered dose scale, IV system, directed contrast, and margin, linking telescoping algebra to event probabilities.hypothesesconclusion(fun ω => OrderedTreatment.crossingIndicator (S.DofZ z0 ω) (S.DofZ z1 ω) j)= (S.crossingEvent z0 z1 j).indicator (fun _ => (1 : ℝ))Proof (Lean source)
lemma crossingIndicator_fun_eq_indicator (z0 z1 : 𝒵) (j : Fin J) : (fun ω => OrderedTreatment.crossingIndicator (S.DofZ z0 ω) (S.DofZ z1 ω) j) = (S.crossingEvent z0 z1 j).indicator (fun _ => (1 : ℝ)) := by funext ω by_cases hC : OrderedTreatment.Crossing (S.DofZ z0 ω) (S.DofZ z1 ω) j · have hω : ω ∈ S.crossingEvent z0 z1 j := hC simp [OrderedTreatment.crossingIndicator, hC, Set.indicator_of_mem hω] · have hω : ω ∉ S.crossingEvent z0 z1 j := by simpa [crossingEvent] using hC simp [OrderedTreatment.crossingIndicator, hC, Set.indicator_of_notMem hω] -
marginResponse_mul_crossingIndicator_eq_indicatorlemma — Weighting a margin response by the crossing indicator is exactly restriction to the margin-crossing subgroup for the potential-outcome system, instrument support, ordered dose scale, IV system, directed contrast, and margin. This turns telescoped outcome changes into subgroup integrals.hypothesesconclusion(fun ω => S.marginResponse j ω * OrderedTreatment.crossingIndicator (S.DofZ z0 ω) (S.DofZ z1 ω) j)= (S.crossingEvent z0 z1 j).indicator (S.marginResponse j)Proof (Lean source)
lemma marginResponse_mul_crossingIndicator_eq_indicator (z0 z1 : 𝒵) (j : Fin J) : (fun ω => S.marginResponse j ω * OrderedTreatment.crossingIndicator (S.DofZ z0 ω) (S.DofZ z1 ω) j) = (S.crossingEvent z0 z1 j).indicator (S.marginResponse j) := by funext ω by_cases hC : OrderedTreatment.Crossing (S.DofZ z0 ω) (S.DofZ z1 ω) j · have hω : ω ∈ S.crossingEvent z0 z1 j := hC simp [OrderedTreatment.crossingIndicator, hC, Set.indicator_of_mem hω] · have hω : ω ∉ S.crossingEvent z0 z1 j := by simpa [crossingEvent] using hC simp [OrderedTreatment.crossingIndicator, hC, Set.indicator_of_notMem hω] -
measurable_YofDofZlemma — The composed dose-response schedule is measurable, so the variable-intensity IV system admits moments of that schedule for the chosen instrument value.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 Finset.measurable_sum _ ?_ intro d _ exact (S.measurable_YofD d).indicator ((MeasurableSet.singleton d).preimage (S.measurable_DofZ z)) -
integrable_marginResponselemma — Each unit-level margin response is integrable in the variable-intensity IV system under the contrast's outcome-integrability assumption, for the selected treatment margin. This licenses margin-specific causal averages.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)) -
integrable_YofDofZlemma — The composed dose-response schedule is integrable for the potential-outcome system, finite instrument support, ordered dose scale, IV system, and contrast endpoints whenever the contrast assumptions hold, at any instrument value. This licenses the composed-response contrast.hypotheses𝒵 :sharedType u_1J :sharedℕz0 z1 :𝒵hValid :S.ValidContrastAssumptions z0 z1z :𝒵conclusionIntegrable (S.YofDofZ z) P.μProof (Lean source)
lemma integrable_YofDofZ {z0 z1 : 𝒵} (hValid : S.ValidContrastAssumptions z0 z1) (z : 𝒵) : Integrable (S.YofDofZ z) P.μ := by have hbound : ∀ᵐ ω ∂P.μ, ‖S.YofDofZ z ω‖ ≤ (fun ω => ∑ d : Fin (J + 1), ‖S.YofD d ω‖) ω := Filter.Eventually.of_forall fun ω => by unfold YofDofZ exact Finset.single_le_sum (fun d _ => norm_nonneg (S.YofD d ω)) (Finset.mem_univ _) have hsum_int : Integrable (fun ω => ∑ d : Fin (J + 1), ‖S.YofD d ω‖) P.μ := by classical induction (Finset.univ : Finset (Fin (J + 1))) using Finset.induction_on with | empty => simp | insert a s has ih => simp only [Finset.sum_insert has] exact (hValid.hIntegrableY a).norm.add ih exact hsum_int.mono' (S.measurable_YofDofZ z).aestronglyMeasurable hbound
Identification 3 core · 9 supporting This part develops the consistency bridges and proves the first-stage, reduced-form, and average-causal-response identification results for one directed instrument contrast. ★ reducedForm_eq_sum_crossingEffects★ indicatorWeightedACR_eq_averageCausalResponse★ directedPairWald_eq_averageCausalResponse
Directed-pair variable-intensity IV identification
This part develops the consistency bridges and proves the first-stage, reduced-form, and average-causal-response identification results for one directed instrument contrast. It is a pairwise Wald specialization, not a population 2SLS characterization for multivalued instruments.
theorem reducedForm_eq_sum_crossingEffects reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
Reduced-form decomposition across crossed margins. For a directed instrument contrast, 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 equals the sum of margin-specific causal responses among units whose dose crosses each margin when assignment moves from the baseline to the comparison value.
Formal statement
hypotheses
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
hValid :
S.ValidContrastAssumptions z0 z1
conclusion
S.reducedFormContrast z0 z1 = ∑ j : Fin J, S.indicatorWeightedEffect z0 z1 j
Proof (Lean source)
theorem reducedForm_eq_sum_crossingEffects {z0 z1 : 𝒵}
(hValid : S.ValidContrastAssumptions z0 z1) :
S.reducedFormContrast z0 z1 =
∑ j : Fin J, S.indicatorWeightedEffect z0 z1 j := by
unfold reducedFormContrast YofDofZ indicatorWeightedEffect
have hpoint :
(fun ω => S.YofD (S.DofZ z1 ω) ω - S.YofD (S.DofZ z0 ω) ω)
=ᵐ[P.μ]
fun ω => ∑ j : Fin J, S.marginResponse j ω *
OrderedTreatment.crossingIndicator (S.DofZ z0 ω) (S.DofZ z1 ω) j :=
hValid.hMonotone.mono fun ω hmono => by
simpa [OrderedTreatment.marginIncrement, marginResponse] using
OrderedTreatment.ordered_telescope_indicator
(J := J) (fun d : Fin (J + 1) => S.YofD d ω) hmono
calc
∫ ω, (S.YofD (S.DofZ z1 ω) ω - S.YofD (S.DofZ z0 ω) ω) ∂P.μ
= ∫ ω, ∑ j : Fin J, S.marginResponse j ω *
OrderedTreatment.crossingIndicator (S.DofZ z0 ω) (S.DofZ z1 ω) j ∂P.μ := by
exact MeasureTheory.integral_congr_ae hpoint
_ = ∑ j : Fin J, ∫ ω, S.marginResponse j ω *
OrderedTreatment.crossingIndicator (S.DofZ z0 ω) (S.DofZ z1 ω) j ∂P.μ := by
rw [MeasureTheory.integral_finset_sum]
intro i _hi
rw [S.marginResponse_mul_crossingIndicator_eq_indicator z0 z1 i]
exact (S.integrable_marginResponse hValid i).indicator
(S.measurableSet_crossingEvent z0 z1 i)
_ = ∑ j : Fin J, ∫ ω in S.crossingEvent z0 z1 j, S.marginResponse j ω ∂P.μ := by
refine Finset.sum_congr rfl ?_
intro j _hj
rw [S.marginResponse_mul_crossingIndicator_eq_indicator z0 z1 j]
rw [MeasureTheory.integral_indicator (S.measurableSet_crossingEvent z0 z1 j)]
theorem indicatorWeightedACR_eq_averageCausalResponse reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
Indicator-weighted and conditional-mean ACR forms agree. In a variable-intensity IV system, for any pair of instrument values, the ratio of total causal-response contributions on crossed margins to total crossing probability equals the crossing-probability-weighted average of margin-specific conditional causal responses.
Formal statement
hypotheses
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
conclusion
S.indicatorWeightedACR z0 z1 = S.averageCausalResponse z0 z1
Proof (Lean source)
theorem indicatorWeightedACR_eq_averageCausalResponse {z0 z1 : 𝒵} :
S.indicatorWeightedACR z0 z1 = S.averageCausalResponse z0 z1 := by
simp only [indicatorWeightedACR, averageCausalResponse, crossingWeight,
OrderedTreatment.normalizedWeight,
normalizedWeight, totalCrossingProb,
conditionalMarginResponse, unnormalizedACRContrast, indicatorWeightedEffect, crossingProb]
rw [Finset.sum_div]
apply Finset.sum_congr rfl
intro j _hj
rw [← eventCondExp_mul_measure_toReal P.μ (S.crossingEvent z0 z1 j)
(measure_ne_top _ _) (S.marginResponse j)]
ring_nf
theorem directedPairWald_eq_averageCausalResponse reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
Directed-pair Wald average-causal-response specialization. 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 directed-pair average causal response: the crossing-probability-weighted average, over treatment-intensity margins, of the conditional mean causal response among units whose dose crosses that margin under the directed instrument contrast.
Formal statement
Proof (Lean source)
theorem directedPairWald_eq_averageCausalResponse {z0 z1 : 𝒵}
(hValid : S.ValidContrastAssumptions z0 z1)
(hCell0 : 0 < (P.μ (S.zEvent z0)).toReal)
(hCell1 : 0 < (P.μ (S.zEvent z1)).toReal) :
S.wald z0 z1 = S.averageCausalResponse z0 z1 := by
have hDZ0 := S.condExpDZ_left_eq_integral hValid hCell0
have hDZ1 := S.condExpDZ_right_eq_integral hValid hCell1
have hYZ0 := S.condExpYZ_left_eq_integral hValid hCell0
have hYZ1 := S.condExpYZ_right_eq_integral hValid hCell1
have hDint0 := S.integrable_intensityValue_DofZ z0
have hDint1 := S.integrable_intensityValue_DofZ z1
have hYint0 := S.integrable_YofDofZ hValid z0
have hYint1 := S.integrable_YofDofZ hValid z1
unfold wald
rw [hYZ1, hYZ0, hDZ1, hDZ0]
rw [← MeasureTheory.integral_sub hYint1 hYint0,
← MeasureTheory.integral_sub hDint1 hDint0]
change S.reducedFormContrast z0 z1 / S.firstStageContrast z0 z1 =
S.averageCausalResponse z0 z1
rw [← S.indicatorWeightedACR_eq_averageCausalResponse]
simp [indicatorWeightedACR, unnormalizedACRContrast, totalCrossingProb,
S.reducedForm_eq_sum_crossingEffects hValid, S.firstStage_eq_sum_crossingProb hValid]
9 supporting declarations (lemmas, instances)
-
DofZ_eq_factualD_on_zEventlemma — Consistency identifies potential treatment at an instrument value with observed treatment inside that instrument cell under the consistency condition, for the instrument value and a unit in its observed cell.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 — Consistency identifies observed outcome with potential outcome at realized treatment under the consistency condition, for the unit being evaluated.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 — The observed treatment mean in the first instrument cell equals mean potential treatment under that instrument value under the directed-contrast IV assumptions when the first cell has positive probability. This is the left first-stage bridge.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 = normalizedRestrictedIntegral P.μ (S.zVar.event z0) (fun ω => OrderedTreatment.intensityValue (S.factualD ω)) := rfl rw [hbridge, POSystem.eventCondExp_of_ae_eq_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 — The observed treatment mean in the second instrument cell equals mean potential treatment under that instrument value under the directed-contrast IV assumptions when the second cell has positive probability. This is the right first-stage bridge.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 = normalizedRestrictedIntegral P.μ (S.zVar.event z1) (fun ω => OrderedTreatment.intensityValue (S.factualD ω)) := rfl rw [hbridge, POSystem.eventCondExp_of_ae_eq_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 — The observed outcome mean in the first instrument cell equals mean outcome under the treatment induced by that instrument value under the directed-contrast IV assumptions when the first cell has positive probability.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 := succ (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 Finset.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 False.elim (hi hEq.symm) · exact if_neg hEq · intro h simp at h have hbridge : S.condExpYZ z0 = normalizedRestrictedIntegral P.μ (S.zVar.event z0) S.factualY := rfl rw [hbridge, POSystem.eventCondExp_of_ae_eq_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 False.elim (hi hEq.symm) · exact if_neg hEq · intro h simp at h -
condExpYZ_right_eq_integrallemma — The observed outcome mean in the second instrument cell equals mean outcome under the treatment induced by that instrument value under the directed-contrast IV assumptions when the second cell has positive probability.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 := succ (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 Finset.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 False.elim (hi hEq.symm) · exact if_neg hEq · intro h simp at h have hbridge : S.condExpYZ z1 = normalizedRestrictedIntegral P.μ (S.zVar.event z1) S.factualY := rfl rw [hbridge, POSystem.eventCondExp_of_ae_eq_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 False.elim (hi hEq.symm) · exact if_neg hEq · intro h simp at h -
firstStage_eq_sum_crossingProbtheorem — The potential first-stage contrast equals the sum of treatment-margin crossing probabilities under the directed-contrast IV assumptions. Monotonicity makes each unit's dose change count exactly the margins it crosses.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 — Every margin-crossing weight is nonnegative under the directed-contrast IV assumptions, for the selected treatment margin, because monotonicity and a positive first stage turn crossing shares into convex weights.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 — The margin-crossing weights sum to one under the directed-contrast IV assumptions, so the average causal response is a genuine weighted average.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
SpecialCases 7 core · 2 supporting This part gives binary-treatment and constant-response specializations and defines interfaces for a linear-score moment ratio and a supplied signed-contrast decomposition. ★ wald_eq_late_of_binaryIntensity★ wald_eq_marginResponseAverage
Variable-intensity IV special cases and linear-score interfaces
This part gives binary-treatment and constant-response specializations and defines interfaces for a linear-score moment ratio and a supplied signed-contrast decomposition.
def binaryMargin reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem.SpecialCases
The unique binary-treatment margin is the sole adjacent dose increment when the ordered treatment scale has exactly one margin.
theorem wald_eq_late_of_binaryIntensity reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem.SpecialCases
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
hypotheses
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
hValid :
S.ValidContrastAssumptions z0 z1
hCell0 :
0 < (P.μ (S.zEvent z0)).toReal
hCell1 :
0 < (P.μ (S.zEvent z1)).toReal
hBinaryIntensity :
J = 1
conclusion
S.wald z0 z1
= normalizedRestrictedIntegral P.μ (S.crossingEvent z0 z1 (binaryMargin hBinaryIntensity)) (S.marginResponse (binaryMargin hBinaryIntensity))
Proof (Lean source)
theorem wald_eq_late_of_binaryIntensity {z0 z1 : 𝒵}
(hValid : S.ValidContrastAssumptions z0 z1)
(hCell0 : 0 < (P.μ (S.zEvent z0)).toReal)
(hCell1 : 0 < (P.μ (S.zEvent z1)).toReal)
(hBinaryIntensity : J = 1) :
S.wald z0 z1 =
normalizedRestrictedIntegral P.μ
(S.crossingEvent z0 z1 (binaryMargin hBinaryIntensity))
(S.marginResponse (binaryMargin hBinaryIntensity)) := by
subst hBinaryIntensity
rw [S.directedPairWald_eq_averageCausalResponse hValid hCell0 hCell1]
have hweight : S.crossingWeight z0 z1 0 = 1 := by
simpa using S.sum_crossingWeight_eq_one hValid
simp [averageCausalResponse, binaryMargin, conditionalMarginResponse, hweight]
theorem wald_eq_marginResponseAverage reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem.SpecialCases
Margin-specific response average specialization. For a candidate margin-response schedule, 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
hypotheses
𝒵 :
Type u_1
J :
ℕ
z0 z1 :
𝒵
m :
Fin J → ℝ
hValid :
S.ValidContrastAssumptions z0 z1
hCell0 :
0 < (P.μ (S.zEvent z0)).toReal
hCell1 :
0 < (P.μ (S.zEvent z1)).toReal
hMarginResponse :
∀ j : Fin J, m j = S.conditionalMarginResponse z0 z1 j
conclusion
S.wald z0 z1 = ∑ j : Fin J, S.crossingWeight z0 z1 j * m j
Proof (Lean source)
theorem wald_eq_marginResponseAverage {z0 z1 : 𝒵} (m : Fin J → ℝ)
(hValid : S.ValidContrastAssumptions z0 z1)
(hCell0 : 0 < (P.μ (S.zEvent z0)).toReal)
(hCell1 : 0 < (P.μ (S.zEvent z1)).toReal)
(hMarginResponse : ∀ j : Fin J, m j = S.conditionalMarginResponse z0 z1 j) :
S.wald z0 z1 = ∑ j : Fin J, S.crossingWeight z0 z1 j * m j := by
rw [S.directedPairWald_eq_averageCausalResponse hValid hCell0 hCell1]
simp [averageCausalResponse, hMarginResponse]
structure LinearScoreMomentSpec reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
A linear-score IV moment-ratio specification for a variable-intensity IV system and score dimension supplies instrument-score coordinates, a coefficient vector, centered score coordinates, and a nonzero score-treatment moment.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
k :
ℕ
fields
Instrument-score coordinate schedule.
score :
𝒵 → Fin k → ℝ
User-supplied coefficient vector for the linear instrument score.
gammaD :
Fin k → ℝ
Every score coordinate has population mean zero.
centered :
∀ r : Fin k, ∫ ω, score (S.factualZ ω) r ∂P.μ = 0
The linear-score--treatment moment is nonzero.
denom_nonzero :
∫ ω, (∑ r : Fin k, gammaD r * score (S.factualZ ω) r) * OrderedTreatment.intensityValue (S.factualD ω) ∂P.μ
≠ 0
def linearCombination reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem.LinearScoreMomentSpec
The linear instrument-score combination weights the centered score coordinates in the supplied score specification by its user-provided coefficient vector.
Definition (Lean source)
parameters
k :
ℕ
𝒵 :
Type u_1
T :
S.LinearScoreMomentSpec k
def
linearCombination T :
P.Ω → ℝ
given by
fun ω => ∑ r : Fin k, T.gammaD r * T.score (S.factualZ ω) r
def momentRatio reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem.LinearScoreMomentSpec
The linear-score IV moment ratio divides the score-outcome moment by the score-treatment moment for the supplied score and coefficient vector. The stored nonzero condition makes this ratio well defined.
Definition (Lean source)
parameters
k :
ℕ
𝒵 :
Type u_1
T :
S.LinearScoreMomentSpec k
def
momentRatio T :
ℝ
given by
(∫ ω, T.linearCombination ω * S.factualY ω ∂P.μ) / (∫ ω, T.linearCombination ω * OrderedTreatment.intensityValue (S.factualD ω) ∂P.μ)
structure LinearScoreContrastDecomposition reviewed
⚑ flagged
Causalean.PO.ID.Exact.VariableIntensityIV.VariableIntensityIVSystem
A supplied signed-pair decomposition for a linear-score moment-ratio specification records weights on ordered instrument-cell pairs, denominator contributions, numerator contributions, and stored numerator and denominator expansions.
Definition (Lean source)
parameters
𝒵 :
Type u_1
J :
ℕ
k :
ℕ
T :
S.LinearScoreMomentSpec k
fields
Signed weight on an ordered instrument-cell contrast.
contrastWeight :
𝒵 × 𝒵 → ℝ
Supplied denominator contribution attached to each ordered pair.
pairFirstStage :
𝒵 × 𝒵 → ℝ
Supplied numerator contribution attached to each ordered pair.
pairReducedForm :
𝒵 × 𝒵 → ℝ
The score-outcome numerator moment equals the supplied finite signed sum.
reducedForm_decomp :
∫ ω, T.linearCombination ω * S.factualY ω ∂P.μ
= ∑ p : 𝒵 × 𝒵, contrastWeight p * pairReducedForm p
The score-treatment denominator moment equals the supplied finite signed sum.
firstStage_decomp :
∫ ω, T.linearCombination ω * OrderedTreatment.intensityValue (S.factualD ω) ∂P.μ
= ∑ p : 𝒵 × 𝒵, contrastWeight p * pairFirstStage p
2 supporting declarations (lemmas, instances)
-
crossingEvent_eq_complianceEventlemma — With a single treatment margin, the crossing subgroup is exactly the classical complier population that moves from zero to the maximum treatment level in the variable-intensity IV system, for the two instrument values under the binary-scale condition.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 : (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 — The directed Wald estimand equals a common causal response shared by every treatment margin under the variable-intensity IV assumptions, positive first instrument-cell mass, positive second instrument-cell mass, and the constant-response condition. The margin weights disappear because they sum to one.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.directedPairWald_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]