PO.ID.Exact.DynamicLATE
Dynamic LATE: identification of complier effects in multi-period instrumented settings.
Setup 51 core · 29 supporting This file defines the data, regimes, counterfactual variables, history information, observable nested regressions, assumptions, and target parameters for a two-period dynamic instrumental-variables LATE design. ★ PODynLATESystem★ encouragementRegime_disjoint_treatmentRegime
Two-Period Dynamic LATE Setup
This file defines the data, regimes, counterfactual variables, history information, observable nested regressions, assumptions, and target parameters for a two-period dynamic instrumental-variables LATE design. It supplies the common interface used by the bridge and ratio-identification files.
The design has sequential binary encouragements and treatments, a baseline state, an intermediate state, and a real outcome. It supports observable nested regressions, dynamic LATE targets, when-to-treat targets, mixture targets, and the dynamic IV/LATE assumption bundle.
structure PODynLATESystem reviewed
⚑ flagged
Causalean.PO
A two-period dynamic instrumental-variable (LATE) model in the potential-outcome framework. A unit is observed over two periods: baseline covariates S₀, then in period 1 a binary encouragement / instrument Z₁ whose value space is identified with the booleans and the treatment D₁ it shifts, likewise identified with the booleans; an intermediate state S₁; then in period 2 a second encouragement Z₂ and treatment D₂, each identified with the booleans; and finally a real-valued outcome Y, identified with the real line. Sequential instrument variation identifies dynamic complier treatment effects (def:po-dynamic-late-system), and all seven nodes are required to be pairwise distinct.
def z1Var reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The first encouragement is packaged as a binary potential-outcome variable.
def z2Var reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The second encouragement is packaged as a binary potential-outcome variable.
def d1Var reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The first treatment is packaged as a binary potential-outcome variable.
def d2Var reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The second treatment is packaged as a binary potential-outcome variable.
def yVar reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The outcome is packaged as a real-valued potential-outcome variable.
Definition (Lean source)
def yVar : POVar P ℝ := ⟨S.Y, S.hYreal⟩
def factualS0 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The factual baseline state is the observed baseline covariate value.
Definition (Lean source)
noncomputable def factualS0 : P.Ω → γ₀ := S.S0.factual
def factualS1 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The factual intermediate state is the observed intermediate covariate value.
Definition (Lean source)
noncomputable def factualS1 : P.Ω → γ₁ := S.S1.factual
def factualZ1 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The factual first encouragement is the observed first-stage instrument value.
Definition (Lean source)
noncomputable def factualZ1 : P.Ω → Bool := S.z1Var.factual
def factualZ2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The factual second encouragement is the observed second-stage instrument value.
Definition (Lean source)
noncomputable def factualZ2 : P.Ω → Bool := S.z2Var.factual
def factualD1 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The factual first treatment is the observed first-stage treatment value.
Definition (Lean source)
noncomputable def factualD1 : P.Ω → Bool := S.d1Var.factual
def factualD2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The factual second treatment is the observed second-stage treatment value.
Definition (Lean source)
noncomputable def factualD2 : P.Ω → Bool := S.d2Var.factual
def factualY reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The factual outcome is the observed outcome value.
Definition (Lean source)
noncomputable def factualY : P.Ω → ℝ := S.yVar.factual
def encouragementRegime reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Regime fixing both encouragements: Z₁ ↦ z 0, Z₂ ↦ z 1.
Definition (Lean source)
noncomputable def encouragementRegime (z : Fin 2 → Bool) : Regime P.V P.X :=
Regime.ofList
[⟨S.Z1, S.hZ1bool.symm (z 0)⟩, ⟨S.Z2, S.hZ2bool.symm (z 1)⟩]
(by
simp only [map_cons, map_nil, List.nodup_cons, List.mem_singleton,
List.not_mem_nil, not_false_eq_true, List.nodup_nil, and_true]
exact S.Z1_ne_Z2)
def treatmentRegime reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Regime fixing both treatments: D₁ ↦ d 0, D₂ ↦ d 1.
Definition (Lean source)
def encZ2Regime reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Regime fixing only the stage-2 encouragement: Z₂ ↦ z₂. Used in the stage-2 ignorability condition where Z₁ remains factual.
Definition (Lean source)
noncomputable def encZ2Regime (z₂ : Bool) : Regime P.V P.X :=
Regime.single S.Z2 (S.hZ2bool.symm z₂)
lemma encouragementRegime_disjoint_treatmentRegime reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
For an encouragement vector z and a treatment path d, the encouragement regime fixing Z₁, Z₂ to z and the treatment regime fixing D₁, D₂ to d target disjoint sets of variables.
Formal statement
Proof (Lean source)
lemma encouragementRegime_disjoint_treatmentRegime (z d : Fin 2 → Bool) :
(S.encouragementRegime z).Disjoint (S.treatmentRegime d) := by
unfold encouragementRegime treatmentRegime Regime.Disjoint
rw [Regime.ofList_target, Regime.ofList_target]
rw [Finset.disjoint_left]
intro v hv hv'
simp only [map_cons, map_nil, List.toFinset_cons, List.toFinset_nil,
Finset.mem_insert] at hv hv'
rcases hv with hv | hv | hv
· subst hv
rcases hv' with hv' | hv' | hv'
· exact S.Z1_ne_D1 hv'
· exact S.Z1_ne_D2 hv'
· exact (notMem_empty _ hv').elim
· subst hv
rcases hv' with hv' | hv' | hv'
· exact S.Z2_ne_D1 hv'
· exact S.Z2_ne_D2 hv'
· exact (notMem_empty _ hv').elim
· exact (notMem_empty _ hv).elim
def encTreatRegime reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Joint encouragement-and-treatment regime r_z ⊔ r_d fixing Z₁,Z₂,D₁,D₂ simultaneously.
Definition (Lean source)
noncomputable def encTreatRegime (z d : Fin 2 → Bool) : Regime P.V P.X :=
(S.encouragementRegime z).sqcup (S.treatmentRegime d)
(S.encouragementRegime_disjoint_treatmentRegime z d)
def D1ofZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
D₁(z) := D₁ evaluated under the encouragement regime fixing both Z's. By exclusion (D₁ has no Z₂ parent in the primitive process), this equals D₁(z 0); we keep the two-coordinate form to avoid splitting cases.
def D2ofZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
D₂(z) under the encouragement regime fixing both Z's.
def DofZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Joint counterfactual treatment vector D(z) = (D₁(z), D₂(z)).
def D2ofZ2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
D₂(Z₁, z₂): stage-2 treatment when only Z₂ is fixed (and Z₁ remains factual). Used in the stage-2 ignorability bundle.
def YofD reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Y(d) under the treatment regime fixing both D's.
def YofDofZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Y(D(z)) defined directly via the encouragement regime: under the two-target encouragement intervention, D₁ and D₂ are computed from z via the structural recursion, and Y is then computed from the resulting treatment vector. This is the natural "outcome under encouragement z" map; composition consistency identifies it with the explicit composition.
def YofZ2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Y(D₁, D₂(Z₁, z₂)) realised as Y under the regime fixing only Z₂ = z₂.
def yUnderZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Y under the two-target encouragement regime, as a RegimedVar.
Definition (Lean source)
def d1UnderZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
D₁ under the two-target encouragement regime, as a RegimedVar.
Definition (Lean source)
noncomputable def d1UnderZ (z : Fin 2 → Bool) : RegimedVar P Bool :=
⟨S.d1Var, S.encouragementRegime z⟩
def d2UnderZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
D₂ under the two-target encouragement regime, as a RegimedVar.
Definition (Lean source)
noncomputable def d2UnderZ (z : Fin 2 → Bool) : RegimedVar P Bool :=
⟨S.d2Var, S.encouragementRegime z⟩
def yUnderZ2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Y under the stage-2-only encouragement regime.
Definition (Lean source)
def d2UnderZ2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
D₂ under the stage-2-only encouragement regime.
Definition (Lean source)
def historyBundle1 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Stage-1 history bundle: the singleton (S₀,). Conditioning on this σ-algebra realises · | S₀ in the outer regression.
Definition (Lean source)
noncomputable def historyBundle1 : POCFBundle P :=
POCFBundle.cons (RegimedVar.ofFactual S.S0) (POCFBundle.nil P)
def historyBundle2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Stage-2 history bundle: (S₀, S₁, Z₁, D₁). Conditioning on this σ-algebra realises · | S, D₁, Z₁ in the inner regression (the stage-2 encouragement Z₂ is not in the conditioning set; it is restricted via an indicator).
Definition (Lean source)
noncomputable def historyBundle2 : POCFBundle P :=
POCFBundle.cons (RegimedVar.ofFactual S.S0) <|
POCFBundle.cons (RegimedVar.ofFactual S.S1) <|
POCFBundle.cons (RegimedVar.ofFactual S.z1Var) <|
POCFBundle.cons (RegimedVar.ofFactual S.d1Var) <|
POCFBundle.nil P
def cfBundle1 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Stage-1 ignorability bundle (Y(D(z)), D₁(z), D₂(z)), the counterfactual target of Z₁ ⟂ · | S₀.
Definition (Lean source)
noncomputable def cfBundle1 (z : Fin 2 → Bool) : POCFBundle P :=
POCFBundle.cons (S.yUnderZ z) <|
POCFBundle.cons (S.d1UnderZ z) <|
POCFBundle.cons (S.d2UnderZ z) <|
POCFBundle.nil P
def cfBundle2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Stage-2 ignorability bundle (Y(D₁, D₂(Z₁, z₂)), D₂(Z₁, z₂)), the counterfactual target of Z₂ ⟂ · | S, D₁, Z₁.
Definition (Lean source)
noncomputable def cfBundle2 (z₂ : Bool) : POCFBundle P :=
POCFBundle.cons (S.yUnderZ2 z₂) <|
POCFBundle.cons (S.d2UnderZ2 z₂) <|
POCFBundle.nil P
def indD reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Real-valued indicator of {D = d}, i.e. 1_{D₁=d 0} · 1_{D₂=d 1}.
def indZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Real-valued indicator of {Z = z}.
def innerCondY reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Inner regression E[Y | S, D₁, Z = z] realised as the bundle ratio E[Y · 1_{Z=z} | history2] / E[1_{Z=z} | history2].
Definition (Lean source)
noncomputable def innerCondY (z : Fin 2 → Bool) : P.Ω → ℝ :=
S.historyBundle2.condExpRatio
(fun ω => S.factualY ω * S.indZ z ω) (S.indZ z) P.μ
def innerCondD reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Inner regression P(D = d | S, D₁, Z = z) realised as the bundle ratio E[1_{D=d} · 1_{Z=z} | history2] / E[1_{Z=z} | history2].
Definition (Lean source)
noncomputable def innerCondD (z d : Fin 2 → Bool) : P.Ω → ℝ :=
S.historyBundle2.condExpRatio
(fun ω => S.indD d ω * S.indZ z ω) (S.indZ z) P.μ
def cObsMean reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Outer regression of innerCondY z over (S₀, Z₁ = z₁), as a function of S₀. This is cObsMean(z; S₀).
def cObsProb reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Outer regression of innerCondD z d over (S₀, Z₁ = z₁).
def obsMean reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Unconditional version obsMean(z) := E[cObsMean(z; S₀)].
def obsProb reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Unconditional version obsProb(z, d) := E[cObsProb(z, d; S₀)].
def DofZEq reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Indicator of the dynamic complier event {ω | D(z)(ω) = d}.
def LATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Dynamic LATE θ(z, d) := E[Y(d) - Y(0) | D(z) = d], totalised as (∫_{D(z)=d} (Y(d) - Y(0)) dμ) / μ({D(z) = d}).toReal.
def cLATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Heterogeneous dynamic LATE θ(z, d, S₀): the bundle conditional version of LATE z d, realised as historyBundle1.condExpRatio of the indicator-weighted contrast.
def whenToTreatLATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
When-to-treat LATE τ_d := θ(d, d).
Definition (Lean source)
def cWhenToTreatLATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Heterogeneous when-to-treat LATE τ_d(S₀).
Definition (Lean source)
def mixtureLATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Mixture LATE β_z := E[Y(D(z)) - Y(0) | D(z) ≠ 0].
def cMixtureLATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Heterogeneous mixture LATE β_z(S₀).
Definition (Lean source)
def Preceq reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Coordinate-wise order d ≼ z: d 0 ≤ z 0 ∧ d 1 ≤ z 1.
structure Assumptions reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The dynamic instrumental-variable / LATE assumptions for the two-period system (def:po-dynamic-late-assumptions): potential-outcome consistency for the ambient system; conditional independence of the stage-1 encouragement from the counterfactual outcome and treatment path given the baseline state, and conditional independence of the stage-2 encouragement from its counterfactual outcome and treatment given the full stage-2 history; positive stage-1 and positive stage-2 propensities almost surely; a positive stage-1 and a positive stage-2 first-stage effect of encouragement on treatment, almost surely; one-sided noncompliance, whereby each stage's counterfactual treatment never exceeds its encouragement; an exclusion restriction under which the outcome depends on the encouragements only through the resulting treatments, the first-stage treatment does not depend on the second-period encouragement, and the first-period encouragement does not depend on the second-period encouragement; and integrability of the counterfactual outcome under every fixed treatment vector, under every fixed encouragement vector, and under every fixed second-period encouragement.
Definition (Lean source)
parameters
fields
consistency :
P.Consistency
ignorability1 :
ignorability2 :
∀ z₂ : Bool,
P.CondIndepCFBundle (RegimedVar.ofFactual S.z2Var) (S.cfBundle2 z₂) S.historyBundle2 P.μ
overlap1 :
∀ z₁ : Bool, ∀ᵐ ω ∂P.μ, 0 < S.historyBundle1.condExpGiven (S.z1Var.indicator z₁) P.μ ω
overlap2 :
∀ z₂ : Bool, ∀ᵐ ω ∂P.μ, 0 < S.historyBundle2.condExpGiven (S.z2Var.indicator z₂) P.μ ω
relevance1 :
relevance2 :
Exclusion: `Y` under the joint encouragement-and-treatment regime
equals `Y` under the treatment-only regime (pointwise). Captures the
primitive-process clause `Y(D, S)`.
**Primitive-process clause for `D₁`** (def:po-dynamic-late-assumptions
primitive process `D₁(Z₁, S₀)`). `D₁` does not depend on `Z₂`: the value
of `D₁` under the joint encouragement regime fixing both `Z`'s agrees
pointwise with its value under the regime fixing only `Z₁`. This is the
Lean-level encoding of the doc's "encouragements affect the terminal
outcome only through treatment and state histories" applied at `D₁`.
exclusion_D1 :
**Primitive-process clause for `Z₁`** (def:po-dynamic-late-assumptions
primitive process `Z₁(S₀)`). `Z₁` does not depend on `Z₂`: the structural
eval of `Z₁` under any regime fixing only `Z₂` agrees with its factual
eval (under the empty regime). Used by the stage-1 composition consistency
rewrite `YofDofZ_eq_YofZ2_on_z1Event` to apply `Consistency.composition`
with `r₁ := encZ2Regime z₂`, `r₂ := Regime.single Z₁ (...)` on the event
`{Z₁ = z 0}` (the `IntermediateAgrees` premise asks that `P.eval (encZ2Regime z₂) ω S.Z1`
equals the assigned value, which by this clause + factual `Z₁ = z 0` is
exactly `S.hZ1bool.symm (z 0)`).
exclusion_Z1 :
∀ (z₂ : Bool) (ω : P.Ω), P.eval (S.encZ2Regime z₂) ω S.Z1 = P.eval Regime.empty ω S.Z1
integrable_YofD :
integrable_YofDofZ :
integrable_YofZ2 :
∀ z₂ : Bool, Integrable (S.YofZ2 z₂) P.μ
29 supporting declarations (lemmas, instances)
-
measurable_D1ofZlemma — The first treatment under a two-target encouragement regime is measurable.Proof (Lean source)
-
measurable_D2ofZlemma — The second treatment under a two-target encouragement regime is measurable.Proof (Lean source)
-
measurable_DofZlemma — The joint counterfactual treatment vector under encouragement is measurable.Proof (Lean source)
lemma measurable_DofZ (z : Fin 2 → Bool) : Measurable (S.DofZ z) := by refine measurable_pi_lambda _ ?_ intro i refine i.cases ?_ ?_ · simpa [DofZ] using S.measurable_D1ofZ z · intro _; simpa [DofZ] using S.measurable_D2ofZ z -
measurable_D2ofZ2lemma — The second treatment under a stage-2-only encouragement regime is measurable.Proof (Lean source)
-
measurable_YofDlemma — The outcome under a fixed treatment vector is measurable.Proof (Lean source)
-
measurable_YofDofZlemma — The outcome under a fixed encouragement vector is measurable.Proof (Lean source)
-
measurable_YofZ2lemma — The outcome under a stage-2-only encouragement regime is measurable.Proof (Lean source)
-
measurable_factualS0lemma — The observed baseline state is measurable.conclusionMeasurable S.factualS0Proof (Lean source)
lemma measurable_factualS0 : Measurable S.factualS0 := S.S0.measurable_factual -
measurable_factualS1lemma — The observed intermediate state is measurable.conclusionMeasurable S.factualS1Proof (Lean source)
lemma measurable_factualS1 : Measurable S.factualS1 := S.S1.measurable_factual -
measurable_factualZ1lemma — The observed first encouragement is measurable.conclusionMeasurable S.factualZ1Proof (Lean source)
lemma measurable_factualZ1 : Measurable S.factualZ1 := S.z1Var.measurable_factual -
measurable_factualZ2lemma — The observed second encouragement is measurable.conclusionMeasurable S.factualZ2Proof (Lean source)
lemma measurable_factualZ2 : Measurable S.factualZ2 := S.z2Var.measurable_factual -
measurable_factualD1lemma — The observed first treatment is measurable.conclusionMeasurable S.factualD1Proof (Lean source)
lemma measurable_factualD1 : Measurable S.factualD1 := S.d1Var.measurable_factual -
measurable_factualD2lemma — The observed second treatment is measurable.conclusionMeasurable S.factualD2Proof (Lean source)
lemma measurable_factualD2 : Measurable S.factualD2 := S.d2Var.measurable_factual -
measurable_factualYlemma — The observed outcome is measurable.conclusionMeasurable S.factualYProof (Lean source)
lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
integrable_factualY_of_consistency_integrable_YofZ2lemma — Factual Y is integrable once the two stage-2 counterfactual outcomes are integrable. The proof partitions on the factual Boolean Z₂ cell and uses PO consistency to identify Y(Z₂ = z₂) with factual Y on that cell.hypothesesconclusionIntegrable S.factualY P.μProof (Lean source)
lemma integrable_factualY_of_consistency_integrable_YofZ2 [IsFiniteMeasure P.μ] (hC : P.Consistency) (hY : ∀ z₂ : Bool, Integrable (S.YofZ2 z₂) P.μ) : Integrable S.factualY P.μ := by have htrue_int : Integrable (fun ω => S.YofZ2 true ω * S.z2Var.indicator true ω) P.μ := S.z2Var.integrable_mul_indicator true (measurableSet_singleton _) (hY true) have hfalse_int : Integrable (fun ω => S.YofZ2 false ω * S.z2Var.indicator false ω) P.μ := S.z2Var.integrable_mul_indicator false (measurableSet_singleton _) (hY false) have hsum_int : Integrable ((fun ω => S.YofZ2 true ω * S.z2Var.indicator true ω) + fun ω => S.YofZ2 false ω * S.z2Var.indicator false ω) P.μ := htrue_int.add hfalse_int refine hsum_int.congr (Filter.Eventually.of_forall ?_) intro ω by_cases hω : S.factualZ2 ω = true · have hcf : S.YofZ2 true ω = S.factualY ω := POVar.cf_eq_factual_on_event hC S.yVar S.z2Var true S.Z2_ne_Y.symm hω have hind_true : S.z2Var.indicator true ω = 1 := by exact S.z2Var.indicator_apply_eq_one hω have hfalse : S.factualZ2 ω ≠ false := by rw [hω] decide have hind_false : S.z2Var.indicator false ω = 0 := by exact S.z2Var.indicator_apply_eq_zero hfalse simp [Pi.add_apply, hcf, hind_true, hind_false] · have hω_false : S.factualZ2 ω = false := by cases hz : S.factualZ2 ω <;> simp_all have hcf : S.YofZ2 false ω = S.factualY ω := POVar.cf_eq_factual_on_event hC S.yVar S.z2Var false S.Z2_ne_Y.symm hω_false have hind_true : S.z2Var.indicator true ω = 0 := by exact S.z2Var.indicator_apply_eq_zero hω have hind_false : S.z2Var.indicator false ω = 1 := by exact S.z2Var.indicator_apply_eq_one hω_false simp [Pi.add_apply, hcf, hind_true, hind_false] -
measurable_indDlemma — The joint treatment indicator is measurable.Proof (Lean source)
lemma measurable_indD (d : Fin 2 → Bool) : Measurable (S.indD d) := (S.d1Var.measurable_indicator _ (MeasurableSet.singleton _)).mul (S.d2Var.measurable_indicator _ (MeasurableSet.singleton _)) -
measurable_indZlemma — The joint encouragement indicator is measurable.Proof (Lean source)
lemma measurable_indZ (z : Fin 2 → Bool) : Measurable (S.indZ z) := (S.z1Var.measurable_indicator _ (MeasurableSet.singleton _)).mul (S.z2Var.measurable_indicator _ (MeasurableSet.singleton _)) -
measurableSet_DofZEqlemma — The dynamic complier event is measurable.Proof (Lean source)
lemma measurableSet_DofZEq (z d : Fin 2 → Bool) : MeasurableSet (S.DofZEq z d) := by have hsing : MeasurableSet ({d} : Set (Fin 2 → Bool)) := MeasurableSet.singleton _ exact S.measurable_DofZ z hsing -
integrable_factualYlemma — Compatibility projection for older call sites: factual outcome integrability is derived from consistency plus integrability of the two YofZ2 cells.Proof (Lean source)
lemma integrable_factualY [StandardBorelSpace P.Ω] (As : S.Assumptions) : Integrable S.factualY P.μ := S.integrable_factualY_of_consistency_integrable_YofZ2 As.consistency As.integrable_YofZ2
Bridges 4 core · 3 supporting This file proves the counterfactual-to-observable bridge identities for the two-period dynamic LATE setup. ★ cOutcome_bridge★ cCompliance_bridge★ outcome_bridge★ compliance_bridge
Dynamic LATE Counterfactual Bridges
This file proves the counterfactual-to-observable bridge identities for the two-period dynamic LATE setup. Conditional bridges given the baseline state are the workhorses, and the unconditional bridges follow by integration.
theorem cOutcome_bridge reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Outcome bridge (S₀-conditional). Under the dynamic LATE identifying assumptions, the baseline-conditional expectation of the counterfactual outcome Y(D(z)) for an encouragement vector z agrees almost surely with the inner-outer observable regression cObsMean z.
Formal statement
Proof (Lean source)
theorem cOutcome_bridge (As : S.Assumptions) (z d : Fin 2 → Bool)
(_hd : Preceq d z) :
S.historyBundle1.condExpGiven (S.YofDofZ z) P.μ =ᵐ[P.μ] S.cObsMean z := by
have hYofZ2_int : Integrable (S.YofZ2 (z 1)) P.μ :=
As.integrable_YofZ2 (z 1)
have hcf1_n : (S.cfBundle1 z).n = 3 := rfl
let i0 : Fin (S.cfBundle1 z).n := ⟨0, by rw [hcf1_n]; decide⟩
let ψ : (∀ i : Fin (S.cfBundle1 z).n, (S.cfBundle1 z).type i) → ℝ :=
fun f => f i0
have hψ_meas : Measurable ψ := by
change Measurable (fun f : (∀ i, (S.cfBundle1 z).type i) => f i0)
exact measurable_pi_apply i0
have hψ_eq : (fun ω => ψ ((S.cfBundle1 z).jointValue ω)) = S.YofDofZ z := by
funext ω
rfl
have hψ_int : Integrable (fun ω => ψ ((S.cfBundle1 z).jointValue ω)) P.μ := by
rw [hψ_eq]
exact As.integrable_YofDofZ z
have hF_eq :
(fun ω => S.YofDofZ z ω * S.z1Var.indicator (z 0) ω) =ᵐ[P.μ]
fun ω => ψ ((S.cfBundle1 z).jointValue ω) *
S.z1Var.indicator (z 0) ω := by
refine Filter.Eventually.of_forall (fun ω => ?_)
simp [congrFun hψ_eq ω]
have hStage1 := POCFBundle.condExpGiven_mul_of_consistency_CondIndepCFBundle
(B := S.cfBundle1 z) (C := S.historyBundle1)
(a := S.z1Var) (x := z 0)
(As.ignorability1 z) hψ_meas hψ_int (measurableSet_singleton (z 0)) hF_eq
rw [hψ_eq] at hStage1
have hσ12 : S.historyBundle1.sigma ≤ S.historyBundle2.sigma := by
have hn2 : S.historyBundle2.n = 4 := rfl
let iS0 : Fin S.historyBundle2.n := ⟨0, by rw [hn2]; decide⟩
let hb12_proj :
(∀ i, S.historyBundle2.type i) → (∀ i, S.historyBundle1.type i) :=
fun f j => Fin.cases (f iS0) (fun j0 => j0.elim0) j
have hproj_meas : Measurable hb12_proj := by
apply measurable_pi_lambda
intro j
refine Fin.cases ?_ ?_ j
· exact measurable_pi_apply iS0
· intro j0
exact j0.elim0
have hjoint : S.historyBundle1.jointValue = hb12_proj ∘ S.historyBundle2.jointValue := by
funext ω j
refine Fin.cases ?_ ?_ j
· rfl
· intro j0
exact j0.elim0
change comap S.historyBundle1.jointValue inferInstance ≤
comap S.historyBundle2.jointValue inferInstance
rw [hjoint, ← MeasurableSpace.comap_comp]
exact MeasurableSpace.comap_mono hproj_meas.comap_le
have hz1_sm2 : StronglyMeasurable[S.historyBundle2.sigma] (S.z1Var.indicator (z 0)) := by
unfold POVar.indicator
refine (stronglyMeasurable_const (b := (1 : ℝ))).indicator ?_
have hn : S.historyBundle2.n = 4 := rfl
let iZ1 : Fin S.historyBundle2.n := ⟨2, by rw [hn]; decide⟩
let A : Set (∀ i : Fin S.historyBundle2.n, S.historyBundle2.type i) :=
{f | f iZ1 = z 0}
change MeasurableSet[comap S.historyBundle2.jointValue inferInstance]
(S.z1Var.event (z 0))
refine ⟨A, ?_, ?_⟩
· dsimp [A]
have hsing : MeasurableSingletonClass (S.historyBundle2.type iZ1) :=
inferInstanceAs (MeasurableSingletonClass Bool)
exact measurable_pi_apply iZ1
(measurableSet_singleton (α := S.historyBundle2.type iZ1) (z 0))
· ext ω
rfl
have hz1_YofZ2_int : Integrable (S.z1Var.indicator (z 0) * S.YofZ2 (z 1)) P.μ := by
have h := S.z1Var.integrable_mul_indicator (z 0) (measurableSet_singleton (z 0)) hYofZ2_int
exact h.congr (Filter.Eventually.of_forall
(fun ω => by simp [mul_comm]))
have hRevPull :
(fun ω => S.z1Var.indicator (z 0) ω *
S.historyBundle2.condExpGiven (S.YofZ2 (z 1)) P.μ ω)
=ᵐ[P.μ]
S.historyBundle2.condExpGiven (S.z1Var.indicator (z 0) * S.YofZ2 (z 1)) P.μ := by
have hpull := S.historyBundle2.condExpGiven_mul_of_stronglyMeasurable_left
hz1_sm2 hz1_YofZ2_int hYofZ2_int
filter_upwards [hpull] with ω hω
simpa [Pi.mul_apply] using hω.symm
haveI : IsFiniteMeasure (P.μ.trim S.historyBundle2.sigma_le) := isFiniteMeasure_trim _
have hTower :
S.historyBundle1.condExpGiven
(S.historyBundle2.condExpGiven
(S.z1Var.indicator (z 0) * S.YofZ2 (z 1)) P.μ) P.μ
=ᵐ[P.μ]
S.historyBundle1.condExpGiven (S.z1Var.indicator (z 0) * S.YofZ2 (z 1)) P.μ := by
have h := S.historyBundle2.condExpGiven_tower_of_le
(g := S.z1Var.indicator (z 0) * S.YofZ2 (z 1)) (μ := P.μ)
(m := S.historyBundle1.sigma) hσ12
simpa [POCFBundle.condExpGiven] using h
have hCons :
(S.z1Var.indicator (z 0) * S.YofZ2 (z 1)) =ᵐ[P.μ]
(fun ω => S.YofDofZ z ω * S.z1Var.indicator (z 0) ω) := by
refine Filter.Eventually.of_forall (fun ω => ?_)
by_cases hz1 : S.factualZ1 ω = z 0
· have hi : S.z1Var.indicator (z 0) ω = 1 := S.z1Var.indicator_apply_eq_one hz1
have hc := YofDofZ_eq_YofZ2_on_z1Event (S := S) As z hz1
simp [Pi.mul_apply, hi, hc]
· have hi : S.z1Var.indicator (z 0) ω = 0 := S.z1Var.indicator_apply_eq_zero hz1
simp [Pi.mul_apply, hi]
have hOuterLhs :
S.historyBundle1.condExpGiven
(fun ω => S.innerCondY z ω * S.z1Var.indicator (z 0) ω) P.μ
=ᵐ[P.μ]
S.historyBundle1.condExpGiven
(fun ω => S.YofDofZ z ω * S.z1Var.indicator (z 0) ω) P.μ := by
refine (S.historyBundle1.condExpGiven_congr_ae
(innerCondY_mul_z1_indicator (S := S) As z)).trans ?_
refine (S.historyBundle1.condExpGiven_congr_ae hRevPull).trans ?_
refine hTower.trans ?_
exact S.historyBundle1.condExpGiven_congr_ae hCons
have hprod :
S.historyBundle1.condExpGiven
(fun ω => S.innerCondY z ω * S.z1Var.indicator (z 0) ω) P.μ
=ᵐ[P.μ]
S.historyBundle1.condExpGiven (S.z1Var.indicator (z 0)) P.μ *
S.historyBundle1.condExpGiven (S.YofDofZ z) P.μ := by
refine hOuterLhs.trans ?_
filter_upwards [hStage1] with ω hω
simpa [Pi.mul_apply, mul_comm] using hω
have hne :
∀ᵐ ω ∂P.μ, S.historyBundle1.condExpGiven (S.z1Var.indicator (z 0)) P.μ ω ≠ 0 := by
filter_upwards [As.overlap1 (z 0)] with ω hpos
linarith
have hratio := S.historyBundle1.condExpRatio_eq_of_mul hprod hne
unfold cObsMean
exact hratio.symm
theorem cCompliance_bridge reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Compliance bridge (S₀-conditional). Under the dynamic LATE identifying assumptions, for an encouragement vector z and a treatment path d with d weakly dominated coordinatewise by z, the baseline-conditional probability of the dynamic complier event D(z) = d agrees almost surely with the inner-outer observable regression cObsProb z d.
Formal statement
Proof (Lean source)
theorem cCompliance_bridge (As : S.Assumptions) (z d : Fin 2 → Bool)
(_hd : Preceq d z) :
S.historyBundle1.condExpGiven
((S.DofZEq z d).indicator (fun _ => (1 : ℝ))) P.μ
=ᵐ[P.μ] S.cObsProb z d := by
-- Same shape as `cOutcome_bridge`, using `innerCondD_mul_z1_indicator` at
-- stage 2 and stage-1 consistency to align the dynamic compliance event.
have htarget_meas : Measurable ((S.DofZEq z d).indicator (fun _ => (1 : ℝ))) :=
measurable_const.indicator (S.measurableSet_DofZEq z d)
have htarget_int : Integrable ((S.DofZEq z d).indicator (fun _ => (1 : ℝ))) P.μ :=
(integrable_const (1 : ℝ)).indicator (S.measurableSet_DofZEq z d)
have hcf1_n : (S.cfBundle1 z).n = 3 := rfl
let iD1 : Fin (S.cfBundle1 z).n := ⟨1, by rw [hcf1_n]; decide⟩
let iD2 : Fin (S.cfBundle1 z).n := ⟨2, by rw [hcf1_n]; decide⟩
let ψ : (∀ i : Fin (S.cfBundle1 z).n, (S.cfBundle1 z).type i) → ℝ :=
fun f => ({d} : Set (Fin 2 → Bool)).indicator (fun _ => (1 : ℝ))
(fun i => Fin.cases (f iD1) (fun _ => f iD2) i)
have hψ_meas : Measurable ψ := by
dsimp [ψ]
refine measurable_const.indicator ?_
exact (measurable_pi_lambda _ (fun i => by
refine Fin.cases ?_ ?_ i
· exact measurable_pi_apply iD1
· intro _
exact measurable_pi_apply iD2)) (MeasurableSet.singleton d)
have hψ_eq :
(fun ω => ψ ((S.cfBundle1 z).jointValue ω)) =
(S.DofZEq z d).indicator (fun _ => (1 : ℝ)) := by
funext ω
rfl
have hψ_int : Integrable (fun ω => ψ ((S.cfBundle1 z).jointValue ω)) P.μ := by
rw [hψ_eq]
exact htarget_int
have hF_eq :
(fun ω => (S.DofZEq z d).indicator (fun _ => (1 : ℝ)) ω *
S.z1Var.indicator (z 0) ω) =ᵐ[P.μ]
fun ω => ψ ((S.cfBundle1 z).jointValue ω) *
S.z1Var.indicator (z 0) ω := by
refine Filter.Eventually.of_forall (fun ω => ?_)
simp [congrFun hψ_eq ω]
have hStage1 := POCFBundle.condExpGiven_mul_of_consistency_CondIndepCFBundle
(B := S.cfBundle1 z) (C := S.historyBundle1)
(a := S.z1Var) (x := z 0)
(As.ignorability1 z) hψ_meas hψ_int (measurableSet_singleton (z 0)) hF_eq
rw [hψ_eq] at hStage1
have hσ12 : S.historyBundle1.sigma ≤ S.historyBundle2.sigma := by
have hn2 : S.historyBundle2.n = 4 := rfl
let iS0 : Fin S.historyBundle2.n := ⟨0, by rw [hn2]; decide⟩
let hb12_proj :
(∀ i, S.historyBundle2.type i) → (∀ i, S.historyBundle1.type i) :=
fun f j => Fin.cases (f iS0) (fun j0 => j0.elim0) j
have hproj_meas : Measurable hb12_proj := by
apply measurable_pi_lambda
intro j
refine Fin.cases ?_ ?_ j
· exact measurable_pi_apply iS0
· intro j0
exact j0.elim0
have hjoint : S.historyBundle1.jointValue = hb12_proj ∘ S.historyBundle2.jointValue := by
funext ω j
refine Fin.cases ?_ ?_ j
· rfl
· intro j0
exact j0.elim0
change comap S.historyBundle1.jointValue inferInstance ≤
comap S.historyBundle2.jointValue inferInstance
rw [hjoint, ← MeasurableSpace.comap_comp]
exact MeasurableSpace.comap_mono hproj_meas.comap_le
have hz1_sm : StronglyMeasurable[S.historyBundle2.sigma] (S.z1Var.indicator (z 0)) := by
unfold POVar.indicator
refine (stronglyMeasurable_const (b := (1 : ℝ))).indicator ?_
have hn : S.historyBundle2.n = 4 := rfl
let iZ1 : Fin S.historyBundle2.n := ⟨2, by rw [hn]; decide⟩
let A : Set (∀ i : Fin S.historyBundle2.n, S.historyBundle2.type i) :=
{f | f iZ1 = z 0}
change MeasurableSet[comap S.historyBundle2.jointValue inferInstance]
(S.z1Var.event (z 0))
refine ⟨A, ?_, ?_⟩
· dsimp [A]
have hsing : MeasurableSingletonClass (S.historyBundle2.type iZ1) :=
inferInstanceAs (MeasurableSingletonClass Bool)
exact measurable_pi_apply iZ1
(measurableSet_singleton (α := S.historyBundle2.type iZ1) (z 0))
· ext ω
rfl
have hd1_sm : StronglyMeasurable[S.historyBundle2.sigma] (S.d1Var.indicator (d 0)) := by
unfold POVar.indicator
refine (stronglyMeasurable_const (b := (1 : ℝ))).indicator ?_
have hn : S.historyBundle2.n = 4 := rfl
let iD1h : Fin S.historyBundle2.n := ⟨3, by rw [hn]; decide⟩
let A : Set (∀ i : Fin S.historyBundle2.n, S.historyBundle2.type i) :=
{f | f iD1h = d 0}
change MeasurableSet[comap S.historyBundle2.jointValue inferInstance]
(S.d1Var.event (d 0))
refine ⟨A, ?_, ?_⟩
· dsimp [A]
have hsing : MeasurableSingletonClass (S.historyBundle2.type iD1h) :=
inferInstanceAs (MeasurableSingletonClass Bool)
exact measurable_pi_apply iD1h
(measurableSet_singleton (α := S.historyBundle2.type iD1h) (d 0))
· ext ω
rfl
let q : P.Ω → ℝ := fun ω => S.z1Var.indicator (z 0) ω * S.d1Var.indicator (d 0) ω
have hq_sm : StronglyMeasurable[S.historyBundle2.sigma] q := by
dsimp [q]
exact hz1_sm.mul hd1_sm
have hd2cf_meas : Measurable (S.d2ofZ2EqIndicator (z 1) (d 1)) := by
unfold d2ofZ2EqIndicator
exact measurable_const.indicator
(S.measurable_D2ofZ2 (z 1) (MeasurableSet.singleton (d 1)))
have hd2cf_int : Integrable (S.d2ofZ2EqIndicator (z 1) (d 1)) P.μ :=
(integrable_const (1 : ℝ)).indicator
(S.measurable_D2ofZ2 (z 1) (MeasurableSet.singleton (d 1)))
have hd1_d2cf_int :
Integrable
(S.d1Var.indicator (d 0) * S.d2ofZ2EqIndicator (z 1) (d 1)) P.μ := by
have h := S.d1Var.integrable_mul_indicator (d 0) (measurableSet_singleton (d 0)) hd2cf_int
exact h.congr (Filter.Eventually.of_forall
(fun ω => by simp [mul_comm]))
have hq_d2cf_int :
Integrable (q * S.d2ofZ2EqIndicator (z 1) (d 1)) P.μ := by
have h := S.z1Var.integrable_mul_indicator (z 0) (measurableSet_singleton (z 0)) hd1_d2cf_int
exact h.congr (Filter.Eventually.of_forall
(fun ω => by dsimp [q]; ring))
have hRevPull :
(fun ω => S.z1Var.indicator (z 0) ω * S.d1Var.indicator (d 0) ω *
S.historyBundle2.condExpGiven (S.d2ofZ2EqIndicator (z 1) (d 1)) P.μ ω)
=ᵐ[P.μ]
S.historyBundle2.condExpGiven
(q * S.d2ofZ2EqIndicator (z 1) (d 1)) P.μ := by
have hpull := S.historyBundle2.condExpGiven_mul_of_stronglyMeasurable_left
hq_sm hq_d2cf_int hd2cf_int
filter_upwards [hpull] with ω hω
simpa [q, Pi.mul_apply, mul_assoc] using hω.symm
haveI : IsFiniteMeasure (P.μ.trim S.historyBundle2.sigma_le) := isFiniteMeasure_trim _
have hTower :
S.historyBundle1.condExpGiven
(S.historyBundle2.condExpGiven
(q * S.d2ofZ2EqIndicator (z 1) (d 1)) P.μ) P.μ
=ᵐ[P.μ]
S.historyBundle1.condExpGiven
(q * S.d2ofZ2EqIndicator (z 1) (d 1)) P.μ := by
have h := S.historyBundle2.condExpGiven_tower_of_le
(g := q * S.d2ofZ2EqIndicator (z 1) (d 1)) (μ := P.μ)
(m := S.historyBundle1.sigma) hσ12
simpa [POCFBundle.condExpGiven] using h
have hCons :
(q * S.d2ofZ2EqIndicator (z 1) (d 1)) =ᵐ[P.μ]
(fun ω => (S.DofZEq z d).indicator (fun _ => (1 : ℝ)) ω *
S.z1Var.indicator (z 0) ω) := by
refine Filter.Eventually.of_forall (fun ω => ?_)
by_cases hz1 : S.factualZ1 ω = z 0
· have hiZ1 : S.z1Var.indicator (z 0) ω = 1 :=
S.z1Var.indicator_apply_eq_one hz1
have hcD1 := D1ofZ_eq_factualD1_on_z1Event (S := S) As z hz1
have hcD2 := D2ofZ_eq_D2ofZ2_on_z1Event (S := S) As z hz1
by_cases hD : S.DofZ z ω = d
· have hD1 : S.D1ofZ z ω = d 0 := by
have := congrFun hD 0
simpa [DofZ] using this
have hfD1 : S.factualD1 ω = d 0 := by
simpa [hcD1] using hD1
have hD2 : S.D2ofZ z ω = d 1 := by
have := congrFun hD 1
exact this
have hcfD2 : S.D2ofZ2 (z 1) ω = d 1 := by
simpa [hcD2] using hD2
have hiD1 : S.d1Var.indicator (d 0) ω = 1 :=
S.d1Var.indicator_apply_eq_one hfD1
have hiD2 : S.d2ofZ2EqIndicator (z 1) (d 1) ω = 1 := by
unfold d2ofZ2EqIndicator
exact Set.indicator_of_mem
(show ω ∈ S.D2ofZ2 (z 1) ⁻¹' ({d 1} : Set Bool) from hcfD2) _
have hiTarget : (S.DofZEq z d).indicator (fun _ => (1 : ℝ)) ω = 1 :=
Set.indicator_of_mem (show ω ∈ S.DofZEq z d from hD) _
simp [q, hiZ1, hiD1, hiD2, hiTarget]
· have hiTarget : (S.DofZEq z d).indicator (fun _ => (1 : ℝ)) ω = 0 :=
Set.indicator_of_notMem (show ω ∉ S.DofZEq z d from hD) _
by_cases hfD1 : S.factualD1 ω = d 0
· have hiD1 : S.d1Var.indicator (d 0) ω = 1 :=
S.d1Var.indicator_apply_eq_one hfD1
have hcfD2_ne : S.D2ofZ2 (z 1) ω ≠ d 1 := by
intro hcfD2
apply hD
funext i
refine Fin.cases ?_ ?_ i
· simp [DofZ, hcD1, hfD1]
· intro j
refine Fin.cases ?_ ?_ j
· calc
S.DofZ z ω (Fin.succ 0) = S.D2ofZ z ω := by rfl
_ = S.D2ofZ2 (z 1) ω := hcD2
_ = d 1 := hcfD2
_ = d (Fin.succ 0) := by rfl
· intro j0
exact j0.elim0
have hiD2 : S.d2ofZ2EqIndicator (z 1) (d 1) ω = 0 := by
unfold d2ofZ2EqIndicator
exact Set.indicator_of_notMem
(show ω ∉ S.D2ofZ2 (z 1) ⁻¹' ({d 1} : Set Bool) from hcfD2_ne) _
simp [q, hiZ1, hiD1, hiD2, hiTarget]
· have hiD1 : S.d1Var.indicator (d 0) ω = 0 :=
S.d1Var.indicator_apply_eq_zero hfD1
simp [q, hiZ1, hiD1, hiTarget]
· have hiZ1 : S.z1Var.indicator (z 0) ω = 0 :=
S.z1Var.indicator_apply_eq_zero hz1
simp [q, hiZ1]
have hOuterLhs :
S.historyBundle1.condExpGiven
(fun ω => S.innerCondD z d ω * S.z1Var.indicator (z 0) ω) P.μ
=ᵐ[P.μ]
S.historyBundle1.condExpGiven
(fun ω => (S.DofZEq z d).indicator (fun _ => (1 : ℝ)) ω *
S.z1Var.indicator (z 0) ω) P.μ := by
refine (S.historyBundle1.condExpGiven_congr_ae
(innerCondD_mul_z1_indicator (S := S) As z d)).trans ?_
refine (S.historyBundle1.condExpGiven_congr_ae hRevPull).trans ?_
refine hTower.trans ?_
exact S.historyBundle1.condExpGiven_congr_ae hCons
have hprod :
S.historyBundle1.condExpGiven
(fun ω => S.innerCondD z d ω * S.z1Var.indicator (z 0) ω) P.μ
=ᵐ[P.μ]
S.historyBundle1.condExpGiven (S.z1Var.indicator (z 0)) P.μ *
S.historyBundle1.condExpGiven
((S.DofZEq z d).indicator (fun _ => (1 : ℝ))) P.μ := by
refine hOuterLhs.trans ?_
filter_upwards [hStage1] with ω hω
simpa [Pi.mul_apply, mul_comm] using hω
have hne :
∀ᵐ ω ∂P.μ, S.historyBundle1.condExpGiven (S.z1Var.indicator (z 0)) P.μ ω ≠ 0 := by
filter_upwards [As.overlap1 (z 0)] with ω hpos
linarith
have hratio := S.historyBundle1.condExpRatio_eq_of_mul hprod hne
unfold cObsProb
exact hratio.symm
theorem outcome_bridge reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Outcome bridge (unconditional). Under the dynamic LATE identifying assumptions, the counterfactual mean outcome E[Y(D(z))] for an encouragement vector z equals the observable nested regression obsMean z.
Formal statement
Proof (Lean source)
theorem outcome_bridge (As : S.Assumptions) (z : Fin 2 → Bool) :
∫ ω, S.YofDofZ z ω ∂P.μ = S.obsMean z := by
have hz_pre : Preceq z z := by
refine ⟨?_, ?_⟩ <;> simp
calc
∫ ω, S.YofDofZ z ω ∂P.μ
= ∫ ω, S.historyBundle1.condExpGiven (S.YofDofZ z) P.μ ω ∂P.μ := by
exact (MeasureTheory.integral_condExp S.historyBundle1.sigma_le).symm
_ = ∫ ω, S.cObsMean z ω ∂P.μ := by
exact integral_congr_ae (cOutcome_bridge (S := S) As z z hz_pre)
_ = S.obsMean z := rfl
theorem compliance_bridge reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Compliance bridge (unconditional). Given a treatment path d that is coordinatewise no greater than the instrument path z, the probability of the counterfactual dynamic complier event that the treatment path realized under instrument assignment z equals d coincides with the observable nested regression obsProb z d.
Formal statement
Proof (Lean source)
theorem compliance_bridge (As : S.Assumptions) (z d : Fin 2 → Bool)
(hd : Preceq d z) :
(P.μ (S.DofZEq z d)).toReal = S.obsProb z d := by
calc
(P.μ (S.DofZEq z d)).toReal
= ∫ ω, (S.DofZEq z d).indicator (fun _ => (1 : ℝ)) ω ∂P.μ := by
exact (MeasureTheory.integral_indicator_one (S.measurableSet_DofZEq z d)).symm
_ = ∫ ω, S.historyBundle1.condExpGiven
((S.DofZEq z d).indicator (fun _ => (1 : ℝ))) P.μ ω ∂P.μ := by
exact (MeasureTheory.integral_condExp S.historyBundle1.sigma_le).symm
_ = ∫ ω, S.cObsProb z d ω ∂P.μ := by
exact integral_congr_ae (cCompliance_bridge (S := S) As z d hd)
_ = S.obsProb z d := rfl
3 supporting declarations (lemmas, instances)
-
probDofZ_eq_zero_of_not_preceqtheorem — Under one-sided noncompliance, a treatment path not below the encouragement path has zero probability.Proof (Lean source)
theorem probDofZ_eq_zero_of_not_preceq (As : S.Assumptions) (z d : Fin 2 → Bool) (h : ¬ Preceq d z) : P.μ (S.DofZEq z d) = 0 := by refine MeasureTheory.measure_mono_null ?_ (MeasureTheory.ae_iff.mp (As.oneSidedNoncompliance z)) intro ω hω hgood apply h unfold DofZEq at hω have hD1 : S.D1ofZ z ω = d 0 := by have := congrFun hω 0 simpa [DofZ] using this have hD2 : S.D2ofZ z ω = d 1 := by have := congrFun hω 1 exact this exact ⟨by simpa [hD1] using hgood.1, by simpa [hD2] using hgood.2⟩ -
innerCondY_mul_z1_indicatortheorem — The stage-2 outcome ratio bridge identifies the inner outcome regression on a first-encouragement cell.hypothesesconclusion(fun ω => S.innerCondY z ω * S.z1Var.indicator (z 0) ω)=ᵐ[P.μ] fun ω => S.z1Var.indicator (z 0) ω * S.historyBundle2.condExpGiven (S.YofZ2 (z 1)) P.μ ωProof (Lean source)
theorem innerCondY_mul_z1_indicator (As : S.Assumptions) (z : Fin 2 → Bool) : (fun ω => S.innerCondY z ω * S.z1Var.indicator (z 0) ω) =ᵐ[P.μ] fun ω => S.z1Var.indicator (z 0) ω * S.historyBundle2.condExpGiven (S.YofZ2 (z 1)) P.μ ω := by have hcf2_n : (S.cfBundle2 (z 1)).n = 2 := rfl let i0 : Fin (S.cfBundle2 (z 1)).n := ⟨0, by rw [hcf2_n]; decide⟩ let ψ : (∀ i : Fin (S.cfBundle2 (z 1)).n, (S.cfBundle2 (z 1)).type i) → ℝ := fun f => f i0 have hψ_meas : Measurable ψ := by change Measurable (fun f : (∀ i, (S.cfBundle2 (z 1)).type i) => f i0) exact measurable_pi_apply i0 have hψ_eq : (fun ω => ψ ((S.cfBundle2 (z 1)).jointValue ω)) = S.YofZ2 (z 1) := by funext ω rfl have hψ_int : Integrable (fun ω => ψ ((S.cfBundle2 (z 1)).jointValue ω)) P.μ := by rw [hψ_eq] exact As.integrable_YofZ2 (z 1) have hF_eq : (fun ω => S.factualY ω * S.z2Var.indicator (z 1) ω) =ᵐ[P.μ] fun ω => ψ ((S.cfBundle2 (z 1)).jointValue ω) * S.z2Var.indicator (z 1) ω := by refine Filter.Eventually.of_forall (fun ω => ?_) by_cases hz2 : S.factualZ2 ω = z 1 · have hi : S.z2Var.indicator (z 1) ω = 1 := S.z2Var.indicator_apply_eq_one hz2 have hc := YofZ2_eq_factualY_on_z2Event (S := S) As (z 1) hz2 simp [hi, congrFun hψ_eq ω, hc] · have hi : S.z2Var.indicator (z 1) ω = 0 := S.z2Var.indicator_apply_eq_zero hz2 simp [hi] have hover : ∀ᵐ ω ∂P.μ, S.historyBundle2.condExpGiven (S.z2Var.indicator (z 1)) P.μ ω ≠ 0 := by filter_upwards [As.overlap2 (z 1)] with ω hpos linarith have hRatio2 : S.historyBundle2.condExpRatio (fun ω => S.factualY ω * S.z2Var.indicator (z 1) ω) (S.z2Var.indicator (z 1)) P.μ =ᵐ[P.μ] S.historyBundle2.condExpGiven (S.YofZ2 (z 1)) P.μ := by have h := POCFBundle.condExpRatio_of_consistency_CondIndepCFBundle (B := S.cfBundle2 (z 1)) (C := S.historyBundle2) (a := S.z2Var) (x := z 1) (As.ignorability2 (z 1)) hψ_meas hψ_int (measurableSet_singleton (z 1)) hF_eq hover rw [hψ_eq] at h exact h let q : P.Ω → ℝ := S.z1Var.indicator (z 0) have hq_sm : StronglyMeasurable[S.historyBundle2.sigma] q := by dsimp [q] unfold POVar.indicator refine (stronglyMeasurable_const (b := (1 : ℝ))).indicator ?_ have hn : S.historyBundle2.n = 4 := rfl let iZ1 : Fin S.historyBundle2.n := ⟨2, by rw [hn]; decide⟩ let A : Set (∀ i : Fin S.historyBundle2.n, S.historyBundle2.type i) := {f | f iZ1 = z 0} change MeasurableSet[comap S.historyBundle2.jointValue inferInstance] (S.z1Var.event (z 0)) refine ⟨A, ?_, ?_⟩ · dsimp [A] have hsing : MeasurableSingletonClass (S.historyBundle2.type iZ1) := inferInstanceAs (MeasurableSingletonClass Bool) exact measurable_pi_apply iZ1 (measurableSet_singleton (α := S.historyBundle2.type iZ1) (z 0)) · ext ω rfl have hz2_int : Integrable (S.z2Var.indicator (z 1)) P.μ := S.z2Var.integrable_indicator (z 1) (measurableSet_singleton (z 1)) have hY_z2_int : Integrable (fun ω => S.factualY ω * S.z2Var.indicator (z 1) ω) P.μ := S.z2Var.integrable_mul_indicator (z 1) (measurableSet_singleton (z 1)) As.integrable_factualY have hq_z2_int : Integrable (q * S.z2Var.indicator (z 1)) P.μ := by have h := S.z1Var.integrable_mul_indicator (z 0) (measurableSet_singleton (z 0)) hz2_int exact h.congr (Filter.Eventually.of_forall (fun ω => by dsimp [q]; ring)) have hq_Y_z2_int : Integrable (q * fun ω => S.factualY ω * S.z2Var.indicator (z 1) ω) P.μ := by have h := S.z1Var.integrable_mul_indicator (z 0) (measurableSet_singleton (z 0)) hY_z2_int exact h.congr (Filter.Eventually.of_forall (fun ω => by dsimp [q]; ring)) have hNumPull : S.historyBundle2.condExpGiven (q * fun ω => S.factualY ω * S.z2Var.indicator (z 1) ω) P.μ =ᵐ[P.μ] q * S.historyBundle2.condExpGiven (fun ω => S.factualY ω * S.z2Var.indicator (z 1) ω) P.μ := S.historyBundle2.condExpGiven_mul_of_stronglyMeasurable_left hq_sm hq_Y_z2_int hY_z2_int have hDenPull : S.historyBundle2.condExpGiven (q * S.z2Var.indicator (z 1)) P.μ =ᵐ[P.μ] q * S.historyBundle2.condExpGiven (S.z2Var.indicator (z 1)) P.μ := S.historyBundle2.condExpGiven_mul_of_stronglyMeasurable_left hq_sm hq_z2_int hz2_int filter_upwards [hRatio2, hNumPull, hDenPull] with ω hR hN hD unfold innerCondY indZ POCFBundle.condExpRatio have hargN : (fun ω => S.factualY ω * (S.z1Var.indicator (z 0) ω * S.z2Var.indicator (z 1) ω)) = q * fun ω => S.factualY ω * S.z2Var.indicator (z 1) ω := by funext ω dsimp [q] ring have hargD : (fun ω => S.z1Var.indicator (z 0) ω * S.z2Var.indicator (z 1) ω) = q * S.z2Var.indicator (z 1) := rfl rw [hargN, hargD, hN, hD] rcases S.z1Var.indicator_eq_one_or_zero (z 0) ω with hz1 | hz1 · simp [q, hz1] simpa [POCFBundle.condExpRatio] using hR · simp [q, hz1] -
innerCondD_mul_z1_indicatortheorem — Stage-2 compliance ratio bridge (multiplied by 1_{Z₁=z₁}). On the event {Z₁ = z₁},hypothesesconclusion(fun ω => S.innerCondD z d ω * S.z1Var.indicator (z 0) ω)=ᵐ[P.μ] fun ω => S.z1Var.indicator (z 0) ω * S.d1Var.indicator (d 0) ω * S.historyBundle2.condExpGiven (S.d2ofZ2EqIndicator (z 1) (d 1)) P.μ ωProof (Lean source)
theorem innerCondD_mul_z1_indicator (As : S.Assumptions) (z d : Fin 2 → Bool) : (fun ω => S.innerCondD z d ω * S.z1Var.indicator (z 0) ω) =ᵐ[P.μ] fun ω => S.z1Var.indicator (z 0) ω * S.d1Var.indicator (d 0) ω * S.historyBundle2.condExpGiven (S.d2ofZ2EqIndicator (z 1) (d 1)) P.μ ω := by have hcf2_n : (S.cfBundle2 (z 1)).n = 2 := rfl let i1 : Fin (S.cfBundle2 (z 1)).n := ⟨1, by rw [hcf2_n]; decide⟩ let ψ : (∀ i : Fin (S.cfBundle2 (z 1)).n, (S.cfBundle2 (z 1)).type i) → ℝ := fun f => ({d 1} : Set Bool).indicator (fun _ => (1 : ℝ)) (f i1) have hψ_meas : Measurable ψ := by change Measurable (fun f : (∀ i, (S.cfBundle2 (z 1)).type i) => ({d 1} : Set Bool).indicator (fun _ => (1 : ℝ)) (f i1)) exact (measurable_const.indicator (measurableSet_singleton (d 1))).comp (measurable_pi_apply i1) have hψ_eq : (fun ω => ψ ((S.cfBundle2 (z 1)).jointValue ω)) = S.d2ofZ2EqIndicator (z 1) (d 1) := by funext ω rfl have hψ_int : Integrable (fun ω => ψ ((S.cfBundle2 (z 1)).jointValue ω)) P.μ := by rw [hψ_eq] exact (integrable_const (1 : ℝ)).indicator (S.measurable_D2ofZ2 (z 1) (MeasurableSet.singleton (d 1))) have hF_eq : (fun ω => S.d2Var.indicator (d 1) ω * S.z2Var.indicator (z 1) ω) =ᵐ[P.μ] fun ω => ψ ((S.cfBundle2 (z 1)).jointValue ω) * S.z2Var.indicator (z 1) ω := by refine Filter.Eventually.of_forall (fun ω => ?_) by_cases hz2 : S.factualZ2 ω = z 1 · have hc := D2ofZ2_eq_factualD2_on_z2Event (S := S) As (z 1) hz2 by_cases hd2 : S.factualD2 ω = d 1 · have hiL : S.d2Var.indicator (d 1) ω = 1 := S.d2Var.indicator_apply_eq_one hd2 have hiR : ψ ((S.cfBundle2 (z 1)).jointValue ω) = 1 := by rw [congrFun hψ_eq ω] unfold d2ofZ2EqIndicator exact Set.indicator_of_mem (show ω ∈ S.D2ofZ2 (z 1) ⁻¹' ({d 1} : Set Bool) from by simpa [hc] using hd2) _ simp [hiL, hiR] · have hiL : S.d2Var.indicator (d 1) ω = 0 := S.d2Var.indicator_apply_eq_zero hd2 have hiR : ψ ((S.cfBundle2 (z 1)).jointValue ω) = 0 := by rw [congrFun hψ_eq ω] unfold d2ofZ2EqIndicator exact Set.indicator_of_notMem (show ω ∉ S.D2ofZ2 (z 1) ⁻¹' ({d 1} : Set Bool) from by simpa [hc] using hd2) _ simp [hiL, hiR] · have hi : S.z2Var.indicator (z 1) ω = 0 := S.z2Var.indicator_apply_eq_zero hz2 simp [hi] have hover : ∀ᵐ ω ∂P.μ, S.historyBundle2.condExpGiven (S.z2Var.indicator (z 1)) P.μ ω ≠ 0 := by filter_upwards [As.overlap2 (z 1)] with ω hpos linarith have hRatio2 : S.historyBundle2.condExpRatio (fun ω => S.d2Var.indicator (d 1) ω * S.z2Var.indicator (z 1) ω) (S.z2Var.indicator (z 1)) P.μ =ᵐ[P.μ] S.historyBundle2.condExpGiven (S.d2ofZ2EqIndicator (z 1) (d 1)) P.μ := by have h := POCFBundle.condExpRatio_of_consistency_CondIndepCFBundle (B := S.cfBundle2 (z 1)) (C := S.historyBundle2) (a := S.z2Var) (x := z 1) (As.ignorability2 (z 1)) hψ_meas hψ_int (measurableSet_singleton (z 1)) hF_eq hover rw [hψ_eq] at h exact h have hz1_sm : StronglyMeasurable[S.historyBundle2.sigma] (S.z1Var.indicator (z 0)) := by unfold POVar.indicator refine (stronglyMeasurable_const (b := (1 : ℝ))).indicator ?_ have hn : S.historyBundle2.n = 4 := rfl let iZ1 : Fin S.historyBundle2.n := ⟨2, by rw [hn]; decide⟩ let A : Set (∀ i : Fin S.historyBundle2.n, S.historyBundle2.type i) := {f | f iZ1 = z 0} change MeasurableSet[comap S.historyBundle2.jointValue inferInstance] (S.z1Var.event (z 0)) refine ⟨A, ?_, ?_⟩ · dsimp [A] have hsing : MeasurableSingletonClass (S.historyBundle2.type iZ1) := inferInstanceAs (MeasurableSingletonClass Bool) exact measurable_pi_apply iZ1 (measurableSet_singleton (α := S.historyBundle2.type iZ1) (z 0)) · ext ω rfl have hd1_sm : StronglyMeasurable[S.historyBundle2.sigma] (S.d1Var.indicator (d 0)) := by unfold POVar.indicator refine (stronglyMeasurable_const (b := (1 : ℝ))).indicator ?_ have hn : S.historyBundle2.n = 4 := rfl let iD1 : Fin S.historyBundle2.n := ⟨3, by rw [hn]; decide⟩ let A : Set (∀ i : Fin S.historyBundle2.n, S.historyBundle2.type i) := {f | f iD1 = d 0} change MeasurableSet[comap S.historyBundle2.jointValue inferInstance] (S.d1Var.event (d 0)) refine ⟨A, ?_, ?_⟩ · dsimp [A] have hsing : MeasurableSingletonClass (S.historyBundle2.type iD1) := inferInstanceAs (MeasurableSingletonClass Bool) exact measurable_pi_apply iD1 (measurableSet_singleton (α := S.historyBundle2.type iD1) (d 0)) · ext ω rfl let q : P.Ω → ℝ := fun ω => S.z1Var.indicator (z 0) ω * S.d1Var.indicator (d 0) ω have hq_sm : StronglyMeasurable[S.historyBundle2.sigma] q := by dsimp [q] exact hz1_sm.mul hd1_sm have hz2_int : Integrable (S.z2Var.indicator (z 1)) P.μ := S.z2Var.integrable_indicator (z 1) (measurableSet_singleton (z 1)) have hd2z2_int : Integrable (fun ω => S.d2Var.indicator (d 1) ω * S.z2Var.indicator (z 1) ω) P.μ := by have h := S.d2Var.integrable_mul_indicator (d 1) (measurableSet_singleton (d 1)) hz2_int exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [mul_comm])) have hd1_z2_int : Integrable (S.d1Var.indicator (d 0) * S.z2Var.indicator (z 1)) P.μ := by have h := S.d1Var.integrable_mul_indicator (d 0) (measurableSet_singleton (d 0)) hz2_int exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [mul_comm])) have hz1_z2_int : Integrable (S.z1Var.indicator (z 0) * S.z2Var.indicator (z 1)) P.μ := by have h := S.z1Var.integrable_mul_indicator (z 0) (measurableSet_singleton (z 0)) hz2_int exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [mul_comm])) have hq_z2_int : Integrable (q * S.z2Var.indicator (z 1)) P.μ := by have h := S.z1Var.integrable_mul_indicator (z 0) (measurableSet_singleton (z 0)) hd1_z2_int exact h.congr (Filter.Eventually.of_forall (fun ω => by dsimp [q]; ring)) have hd1_d2z2_int : Integrable (S.d1Var.indicator (d 0) * fun ω => S.d2Var.indicator (d 1) ω * S.z2Var.indicator (z 1) ω) P.μ := by have h := S.d1Var.integrable_mul_indicator (d 0) (measurableSet_singleton (d 0)) hd2z2_int exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [mul_comm])) have hq_d2z2_int : Integrable (q * fun ω => S.d2Var.indicator (d 1) ω * S.z2Var.indicator (z 1) ω) P.μ := by have h := S.z1Var.integrable_mul_indicator (z 0) (measurableSet_singleton (z 0)) hd1_d2z2_int exact h.congr (Filter.Eventually.of_forall (fun ω => by dsimp [q]; ring)) have hNumPull : S.historyBundle2.condExpGiven (q * fun ω => S.d2Var.indicator (d 1) ω * S.z2Var.indicator (z 1) ω) P.μ =ᵐ[P.μ] q * S.historyBundle2.condExpGiven (fun ω => S.d2Var.indicator (d 1) ω * S.z2Var.indicator (z 1) ω) P.μ := S.historyBundle2.condExpGiven_mul_of_stronglyMeasurable_left hq_sm hq_d2z2_int hd2z2_int have hDenPull : S.historyBundle2.condExpGiven (S.z1Var.indicator (z 0) * S.z2Var.indicator (z 1)) P.μ =ᵐ[P.μ] S.z1Var.indicator (z 0) * S.historyBundle2.condExpGiven (S.z2Var.indicator (z 1)) P.μ := S.historyBundle2.condExpGiven_mul_of_stronglyMeasurable_left hz1_sm hz1_z2_int hz2_int filter_upwards [hRatio2, hNumPull, hDenPull] with ω hR hN hD unfold innerCondD indD indZ POCFBundle.condExpRatio have hargN : (fun ω => (S.d1Var.indicator (d 0) ω * S.d2Var.indicator (d 1) ω) * (S.z1Var.indicator (z 0) ω * S.z2Var.indicator (z 1) ω)) = q * fun ω => S.d2Var.indicator (d 1) ω * S.z2Var.indicator (z 1) ω := by funext ω simp [q, Pi.mul_apply, mul_comm, mul_left_comm, mul_assoc] have hargD : (fun ω => S.z1Var.indicator (z 0) ω * S.z2Var.indicator (z 1) ω) = S.z1Var.indicator (z 0) * S.z2Var.indicator (z 1) := rfl rw [hargN, hargD, hN, hD] rcases S.z1Var.indicator_eq_one_or_zero (z 0) ω with hz1 | hz1 · rcases S.d1Var.indicator_eq_one_or_zero (d 0) ω with hd1 | hd1 · simp [q, hz1, hd1] simpa [POCFBundle.condExpRatio] using hR · simp [q, hz1, hd1] · simp [q, hz1]
Consistency 1 core · 4 supporting This file proves pointwise consistency rewrites for the two-period dynamic LATE system. ★ D2ofZ_eq_D2ofZ2_on_z1Event
Two-Period Dynamic LATE Consistency
This file proves pointwise consistency rewrites for the two-period dynamic LATE system. The lemmas identify counterfactual outcomes and treatments with factual or smaller-regime variables on the corresponding observed encouragement events.
theorem D2ofZ_eq_D2ofZ2_on_z1Event reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Second-stage treatment does not depend on first-stage regime detail once the actual first-period instrument matches the counterfactual one. At any outcome at which the factual first-period instrument equals the first coordinate of the instrument path z, the potential second-period treatment under the encouragement regime z coincides pointwise with the potential second-period treatment under the regime that fixes only the second-period instrument to z 1.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
YofZ2_eq_factualY_on_z2Eventtheorem — On {Z₂ = z₂}, Y(D₁, D₂(Z₁, z₂)) = factualY pointwise.hypothesesconclusionS.YofZ2 z₂ ω = S.factualY ωProof (Lean source)
theorem YofZ2_eq_factualY_on_z2Event (As : S.Assumptions) (z₂ : Bool) {ω : P.Ω} (hω : S.factualZ2 ω = z₂) : S.YofZ2 z₂ ω = S.factualY ω := by -- Direct application of `POVar.cf_eq_factual_on_event` with `a := S.yVar`, -- `w := S.z2Var`, `y := z₂`. Distinctness `S.Y ≠ S.Z2` from `S.Z2_ne_Y`. exact POVar.cf_eq_factual_on_event As.consistency S.yVar S.z2Var z₂ S.Z2_ne_Y.symm hω -
D2ofZ2_eq_factualD2_on_z2Eventtheorem — On {Z₂ = z₂}, D₂(Z₁, z₂) = factualD2 pointwise.hypothesesconclusionS.D2ofZ2 z₂ ω = S.factualD2 ωProof (Lean source)
theorem D2ofZ2_eq_factualD2_on_z2Event (As : S.Assumptions) (z₂ : Bool) {ω : P.Ω} (hω : S.factualZ2 ω = z₂) : S.D2ofZ2 z₂ ω = S.factualD2 ω := by -- Same pattern as above with `a := S.d2Var`, distinctness `S.D2 ≠ S.Z2`. exact POVar.cf_eq_factual_on_event As.consistency S.d2Var S.z2Var z₂ S.Z2_ne_D2.symm hω -
YofDofZ_eq_YofZ2_on_z1Eventtheorem — On {Z₁ = z 0}, Y under encouragementRegime z agrees with Y under encZ2Regime (z 1).hypothesesconclusionS.YofDofZ z ω = S.YofZ2 (z 1) ωProof (Lean source)
theorem YofDofZ_eq_YofZ2_on_z1Event (As : S.Assumptions) (z : Fin 2 → Bool) {ω : P.Ω} (hω : S.factualZ1 ω = z 0) : S.YofDofZ z ω = S.YofZ2 (z 1) ω := by unfold YofDofZ YofZ2 POVar.cf yVar exact congrArg _ (eval_encouragement_eq_eval_encZ2_on_z1Event As z hω S.Y S.Z1_ne_Y.symm S.Z2_ne_Y.symm) -
D1ofZ_eq_factualD1_on_z1Eventtheorem — On {Z₁ = z 0}, D₁ under encouragementRegime z agrees with the factual D₁.hypothesesconclusionS.D1ofZ z ω = S.factualD1 ωProof (Lean source)
theorem D1ofZ_eq_factualD1_on_z1Event (As : S.Assumptions) (z : Fin 2 → Bool) {ω : P.Ω} (hω : S.factualZ1 ω = z 0) : S.D1ofZ z ω = S.factualD1 ω := by -- Step 1: `S.d1Var.cf (encouragementRegime z) ω = S.d1Var.cf (Regime.single Z₁ ..) ω` -- via `As.exclusion_D1`. -- Step 2: `S.d1Var.cf (Regime.single Z₁ ..) ω = S.factualD1 ω` via -- `POVar.cf_eq_factual_on_event` with `a := S.d1Var`, `w := S.z1Var`, -- `y := z 0`, distinctness `S.D1 ≠ S.Z1` (from `S.Z1_ne_D1.symm`), -- and the event hypothesis `hω`. -- Note: `S.D1ofZ z ω = S.d1Var.cf (encouragementRegime z) ω` by definition, -- and `S.d1Var.cfUnder S.z1Var (z 0) = S.d1Var.cf (Regime.single Z₁ ..)` -- by `POVar.cfUnder` def. calc S.D1ofZ z ω = S.d1Var.cf (Regime.single S.Z1 (S.hZ1bool.symm (z 0))) ω := by simpa [D1ofZ] using As.exclusion_D1 z ω _ = S.factualD1 ω := by exact POVar.cf_eq_factual_on_event As.consistency S.d1Var S.z1Var (z 0) S.Z1_ne_D1.symm hω
WhenToTreat 4 core · 6 supporting This file proves the Wald-style ratio identifications for the dynamic when-to-treat and mixture LATE parameters. ★ whenToTreat_wald★ mixtureLATE_wald★ cWhenToTreat_wald★ cMixtureLATE_wald
Two-period dynamic LATE when-to-treat ratios
This file proves the Wald-style ratio identifications for the dynamic when-to-treat and mixture LATE parameters. The arguments combine bridge identities for two-period encouragement regimes with one-sided noncompliance and composition-consistency rewrites on the observed encouragement event.
theorem whenToTreat_wald reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
When-to-treat dynamic LATE Wald identity (unconditional). For a treatment path d equal to (1,0) or (0,1) — treatment started in period 1 and stopped, or delayed to period 2, the when-to-treat local average treatment effect τ_d equals the Wald ratio of the observable mean contrast obsMean(d) − obsMean(0,0) to the observable compliance probability obsProb(d,d).
Formal statement
Proof (Lean source)
theorem whenToTreat_wald (As : S.Assumptions) (d : Fin 2 → Bool)
(hd : d = ![true, false] ∨ d = ![false, true]) :
S.whenToTreatLATE d
= (S.obsMean d - S.obsMean ![false, false]) / S.obsProb d d := by
-- Numerator: combine the outcome bridge (twice) with the
-- one-sided-noncompliance decomposition.
have hNum : (∫ ω in S.DofZEq d d,
(S.YofD d ω - S.YofD ![false, false] ω) ∂P.μ)
= S.obsMean d - S.obsMean ![false, false] := by
have hbr_d : ∫ ω, S.YofDofZ d ω ∂P.μ = S.obsMean d := by
exact outcome_bridge As d
have hbr_0 : ∫ ω, S.YofDofZ ![false, false] ω ∂P.μ
= S.obsMean ![false, false] := by
exact outcome_bridge As ![false, false]
have hdiff := int_outcome_difference_identity As d hd
-- ∫ Y(D(d)) - ∫ Y(D(0)) = ∫_{D(d)=d} (Y(d)-Y(0)) dμ
-- and the LHS rewrites to obsMean(d) - obsMean(0) via the bridges.
rw [hbr_d, hbr_0] at hdiff
linarith [hdiff]
-- Denominator: compliance bridge.
have hDen : (P.μ (S.DofZEq d d)).toReal = S.obsProb d d := by
have hd_pre : Preceq d d := by
rcases hd with h | h <;>
(subst h; refine ⟨?_, ?_⟩ <;> simp)
exact compliance_bridge As d d hd_pre
-- Combine.
unfold whenToTreatLATE LATE
rw [hNum, hDen]
theorem mixtureLATE_wald reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Mixture dynamic LATE Wald identity (unconditional). Under the dynamic LATE identifying assumptions, for an encouragement vector z, the mixture dynamic local average treatment effect mixtureLATE z equals the Wald ratio of the observable mean contrast obsMean z − obsMean(0,0) to the observable noncompliance probability 1 − obsProb(z, 0,0).
Formal statement
Proof (Lean source)
theorem mixtureLATE_wald (As : S.Assumptions) (z : Fin 2 → Bool) :
S.mixtureLATE z
= (S.obsMean z - S.obsMean ![false, false]) / (1 - S.obsProb z ![false, false]) := by
let z0 : Fin 2 → Bool := ![false, false]
have hset : {ω | S.DofZ z ω ≠ z0} = (S.DofZEq z z0)ᶜ := by
ext ω
rfl
have hpre_z0 : Preceq z0 z := by
refine ⟨?_, ?_⟩ <;> simp [z0]
have hpre_00 : Preceq z0 z0 := by
refine ⟨?_, ?_⟩ <;> simp [z0]
have hbr_z : ∫ ω, S.YofDofZ z ω ∂P.μ = S.obsMean z := by
exact outcome_bridge As z
have hbr_0 : ∫ ω, S.YofDofZ z0 ω ∂P.μ = S.obsMean z0 := by
exact outcome_bridge As z0
have hY0_int :
∫ ω, S.YofD z0 ω ∂P.μ = ∫ ω, S.YofDofZ z0 ω ∂P.μ := by
exact (MeasureTheory.integral_congr_ae (YofDofZ_zero_ae_eq_YofD_zero As).symm)
have hzero_set :
∫ ω in S.DofZEq z z0, (S.YofDofZ z ω - S.YofD z0 ω) ∂P.μ = 0 := by
have hpoint : ∀ᵐ ω ∂P.μ,
ω ∈ S.DofZEq z z0 → S.YofDofZ z ω - S.YofD z0 ω = 0 := by
filter_upwards [YofDofZ_eq_YofD_on_DofZEq As z z0] with ω hω hmem
rw [hω hmem]
ring
rw [MeasureTheory.setIntegral_congr_ae (S.measurableSet_DofZEq z z0) hpoint]
simp
have hNum :
(∫ ω in {ω | S.DofZ z ω ≠ z0}, (S.YofDofZ z ω - S.YofD z0 ω) ∂P.μ)
= S.obsMean z - S.obsMean z0 := by
have hint : Integrable (fun ω => S.YofDofZ z ω - S.YofD z0 ω) P.μ :=
(As.integrable_YofDofZ z).sub (As.integrable_YofD z0)
calc
(∫ ω in {ω | S.DofZ z ω ≠ z0}, (S.YofDofZ z ω - S.YofD z0 ω) ∂P.μ)
= ∫ ω in (S.DofZEq z z0)ᶜ, (S.YofDofZ z ω - S.YofD z0 ω) ∂P.μ := by
rw [hset]
_ = ∫ ω, (S.YofDofZ z ω - S.YofD z0 ω) ∂P.μ
- ∫ ω in S.DofZEq z z0, (S.YofDofZ z ω - S.YofD z0 ω) ∂P.μ := by
exact MeasureTheory.setIntegral_compl (S.measurableSet_DofZEq z z0) hint
_ = ∫ ω, (S.YofDofZ z ω - S.YofD z0 ω) ∂P.μ := by
rw [hzero_set, sub_zero]
_ = (∫ ω, S.YofDofZ z ω ∂P.μ) - (∫ ω, S.YofD z0 ω ∂P.μ) := by
rw [MeasureTheory.integral_sub (As.integrable_YofDofZ z) (As.integrable_YofD z0)]
_ = S.obsMean z - S.obsMean z0 := by
rw [hbr_z, hY0_int, hbr_0]
have hDen :
(P.μ {ω | S.DofZ z ω ≠ z0}).toReal = 1 - S.obsProb z z0 := by
calc
(P.μ {ω | S.DofZ z ω ≠ z0}).toReal
= (P.μ (S.DofZEq z z0)ᶜ).toReal := by
rw [hset]
_ = 1 - (P.μ (S.DofZEq z z0)).toReal := by
simpa [MeasureTheory.measureReal_def] using
(MeasureTheory.probReal_compl_eq_one_sub
(μ := P.μ) (s := S.DofZEq z z0) (S.measurableSet_DofZEq z z0))
_ = 1 - S.obsProb z z0 := by
rw [compliance_bridge As z z0 hpre_z0]
unfold mixtureLATE
rw [hNum, hDen]
theorem cWhenToTreat_wald reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
When-to-treat dynamic LATE Wald identity (heterogeneous in S₀). For a treatment path d equal to (1,0) or (0,1), the baseline-covariate-conditional when-to-treat effect τ_d(S₀) agrees almost surely with the ratio of the conditional observable-mean contrast cObsMean(d;S₀) − cObsMean(0;S₀) to the conditional observable compliance probability cObsProb(d,d;S₀).
Formal statement
Proof (Lean source)
theorem cWhenToTreat_wald (As : S.Assumptions) (d : Fin 2 → Bool)
(hd : d = ![true, false] ∨ d = ![false, true]) :
S.cWhenToTreatLATE d =ᵐ[P.μ]
fun ω => (S.cObsMean d ω - S.cObsMean ![false, false] ω) / S.cObsProb d d ω := by
let z0 : Fin 2 → Bool := ![false, false]
have hd_pre : Preceq d d := by
rcases hd with h | h <;>
(subst h; refine ⟨?_, ?_⟩ <;> simp)
have hpre_00 : Preceq z0 z0 := by
refine ⟨?_, ?_⟩ <;> simp [z0]
have hpoint :
(fun ω => S.YofDofZ d ω - S.YofDofZ z0 ω) =ᵐ[P.μ]
fun ω => (S.YofD d ω - S.YofD z0 ω) *
(S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω := by
filter_upwards [YofDofZ_decomposition As d hd,
YofDofZ_zero_ae_eq_YofD_zero As,
DofZ_in_two_values As d hd] with ω hdecomp hzero hcase
rw [hdecomp, hzero]
rcases hcase with h | h
· have h1 : (S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω = 1 := by
exact Set.indicator_of_mem (s := S.DofZEq d d) (f := fun _ => (1 : ℝ)) h
have h2 : (S.DofZEq d z0).indicator (fun _ => (1 : ℝ)) ω = 0 := by
apply Set.indicator_of_notMem
intro h0
have hd_ne_zero : d ≠ z0 := by
rcases hd with hdz | hdz <;> subst hdz <;> simp [z0]
exact hd_ne_zero (h.symm.trans h0)
rw [h1, h2]
ring_nf
simp [z0]
· have h1 : (S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω = 0 := by
apply Set.indicator_of_notMem
intro hd'
have hd_ne_zero : d ≠ z0 := by
rcases hd with hdz | hdz <;> subst hdz <;> simp [z0]
exact hd_ne_zero (hd'.symm.trans h)
have h2 : (S.DofZEq d z0).indicator (fun _ => (1 : ℝ)) ω = 1 := by
exact Set.indicator_of_mem (s := S.DofZEq d z0)
(f := fun _ => (1 : ℝ)) h
rw [h1, h2]
ring_nf
have hce_congr :
S.historyBundle1.condExpGiven
(fun ω => S.YofDofZ d ω - S.YofDofZ z0 ω) P.μ
=ᵐ[P.μ]
S.historyBundle1.condExpGiven
(fun ω => (S.YofD d ω - S.YofD z0 ω) *
(S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω) P.μ := by
exact S.historyBundle1.condExpGiven_congr_ae hpoint
have hsub :
S.historyBundle1.condExpGiven
(fun ω => S.YofDofZ d ω - S.YofDofZ z0 ω) P.μ
=ᵐ[P.μ]
fun ω => S.historyBundle1.condExpGiven (S.YofDofZ d) P.μ ω -
S.historyBundle1.condExpGiven (S.YofDofZ z0) P.μ ω := by
unfold POCFBundle.condExpGiven
exact
(MeasureTheory.condExp_sub (μ := P.μ)
(f := S.YofDofZ d) (g := S.YofDofZ z0)
(As.integrable_YofDofZ d) (As.integrable_YofDofZ z0)
S.historyBundle1.sigma)
have hbr_d := cOutcome_bridge As d d hd_pre
have hbr_0 := cOutcome_bridge As z0 z0 hpre_00
have hNum :
S.historyBundle1.condExpGiven
(fun ω => (S.YofD d ω - S.YofD z0 ω) *
(S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω) P.μ
=ᵐ[P.μ]
fun ω => S.cObsMean d ω - S.cObsMean z0 ω := by
filter_upwards [hce_congr, hsub, hbr_d, hbr_0] with ω hcg hs hbd hb0
rw [← hcg, hs, hbd, hb0]
have hDen := cCompliance_bridge As d d hd_pre
unfold cWhenToTreatLATE cLATE POCFBundle.condExpRatio
filter_upwards [hNum, hDen] with ω hN hD
rw [hN, hD]
theorem cMixtureLATE_wald reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Mixture dynamic LATE Wald identity (heterogeneous in S₀). Under the dynamic LATE identifying assumptions, for an encouragement vector z, the baseline-conditional mixture dynamic LATE cMixtureLATE z agrees almost surely with the ratio of the baseline-conditional mean contrast cObsMean z − cObsMean(0,0) to the baseline-conditional noncompliance probability 1 − cObsProb(z, 0,0).
Formal statement
Proof (Lean source)
theorem cMixtureLATE_wald (As : S.Assumptions) (z : Fin 2 → Bool) :
(S.cMixtureLATE z =ᵐ[P.μ]
fun ω => (S.cObsMean z ω - S.cObsMean ![false, false] ω) /
(1 - S.cObsProb z ![false, false] ω)) := by
let z0 : Fin 2 → Bool := ![false, false]
have hpre_z0 : Preceq z0 z := by
refine ⟨?_, ?_⟩ <;> simp [z0]
have hpre_00 : Preceq z0 z0 := by
refine ⟨?_, ?_⟩ <;> simp [z0]
have hpoint :
(fun ω => S.YofDofZ z ω - S.YofDofZ z0 ω) =ᵐ[P.μ]
fun ω => (S.YofDofZ z ω - S.YofD z0 ω) *
({ω | S.DofZ z ω ≠ z0}).indicator (fun _ => (1 : ℝ)) ω := by
filter_upwards [YofDofZ_zero_ae_eq_YofD_zero As,
YofDofZ_eq_YofD_on_DofZEq As z z0] with ω hzero hzero_event
by_cases h : S.DofZ z ω = z0
· have hind :
({ω | S.DofZ z ω ≠ z0}).indicator (fun _ => (1 : ℝ)) ω = 0 := by
apply Set.indicator_of_notMem
simpa using h
rw [hzero, hzero_event h, hind]
ring
· have hind :
({ω | S.DofZ z ω ≠ z0}).indicator (fun _ => (1 : ℝ)) ω = 1 := by
exact Set.indicator_of_mem (s := {ω | S.DofZ z ω ≠ z0})
(f := fun _ => (1 : ℝ)) h
rw [hzero, hind]
ring
have hce_congr :
S.historyBundle1.condExpGiven
(fun ω => S.YofDofZ z ω - S.YofDofZ z0 ω) P.μ
=ᵐ[P.μ]
S.historyBundle1.condExpGiven
(fun ω => (S.YofDofZ z ω - S.YofD z0 ω) *
({ω | S.DofZ z ω ≠ z0}).indicator (fun _ => (1 : ℝ)) ω) P.μ := by
exact S.historyBundle1.condExpGiven_congr_ae hpoint
have hsub :
S.historyBundle1.condExpGiven
(fun ω => S.YofDofZ z ω - S.YofDofZ z0 ω) P.μ
=ᵐ[P.μ]
fun ω => S.historyBundle1.condExpGiven (S.YofDofZ z) P.μ ω -
S.historyBundle1.condExpGiven (S.YofDofZ z0) P.μ ω := by
unfold POCFBundle.condExpGiven
exact
(MeasureTheory.condExp_sub (μ := P.μ)
(f := S.YofDofZ z) (g := S.YofDofZ z0)
(As.integrable_YofDofZ z) (As.integrable_YofDofZ z0)
S.historyBundle1.sigma)
have hbr_z := cOutcome_bridge As z z0 hpre_z0
have hbr_0 := cOutcome_bridge As z0 z0 hpre_00
have hNum :
S.historyBundle1.condExpGiven
(fun ω => (S.YofDofZ z ω - S.YofD z0 ω) *
({ω | S.DofZ z ω ≠ z0}).indicator (fun _ => (1 : ℝ)) ω) P.μ
=ᵐ[P.μ]
fun ω => S.cObsMean z ω - S.cObsMean z0 ω := by
filter_upwards [hce_congr, hsub, hbr_z, hbr_0] with ω hcg hs hbz hb0
rw [← hcg, hs, hbz, hb0]
have hInd :
(({ω | S.DofZ z ω ≠ z0}).indicator (fun _ => (1 : ℝ)) : P.Ω → ℝ)
= fun ω => (1 : ℝ) - (S.DofZEq z z0).indicator (fun _ => (1 : ℝ)) ω := by
funext ω
by_cases h : S.DofZ z ω = z0
· have hne : ω ∉ {ω | S.DofZ z ω ≠ z0} := by
simpa using h
rw [Set.indicator_of_notMem hne,
Set.indicator_of_mem (s := S.DofZEq z z0) (f := fun _ => (1 : ℝ)) h]
ring
· have hzero : ω ∉ S.DofZEq z z0 := by
simpa [DofZEq] using h
rw [Set.indicator_of_mem (s := {ω | S.DofZ z ω ≠ z0})
(f := fun _ => (1 : ℝ)) h,
Set.indicator_of_notMem hzero]
ring
have hconst :
S.historyBundle1.condExpGiven (fun _ : P.Ω => (1 : ℝ)) P.μ
= fun _ : P.Ω => (1 : ℝ) := by
unfold POCFBundle.condExpGiven
exact MeasureTheory.condExp_const S.historyBundle1.sigma_le (1 : ℝ)
have hind_int :
Integrable ((S.DofZEq z z0).indicator (fun _ => (1 : ℝ)) : P.Ω → ℝ) P.μ := by
exact (integrable_const (1 : ℝ)).indicator (S.measurableSet_DofZEq z z0)
have hden_sub :
S.historyBundle1.condExpGiven
(fun ω => (1 : ℝ) - (S.DofZEq z z0).indicator (fun _ => (1 : ℝ)) ω) P.μ
=ᵐ[P.μ]
fun ω => (1 : ℝ) -
S.historyBundle1.condExpGiven
((S.DofZEq z z0).indicator (fun _ => (1 : ℝ))) P.μ ω := by
have hsub' :
S.historyBundle1.condExpGiven
(fun ω => (fun _ : P.Ω => (1 : ℝ)) ω -
(S.DofZEq z z0).indicator (fun _ => (1 : ℝ)) ω) P.μ
=ᵐ[P.μ]
fun ω => S.historyBundle1.condExpGiven (fun _ : P.Ω => (1 : ℝ)) P.μ ω -
S.historyBundle1.condExpGiven
((S.DofZEq z z0).indicator (fun _ => (1 : ℝ))) P.μ ω := by
unfold POCFBundle.condExpGiven
exact
(MeasureTheory.condExp_sub (μ := P.μ)
(f := fun _ : P.Ω => (1 : ℝ))
(g := (S.DofZEq z z0).indicator (fun _ => (1 : ℝ)))
(integrable_const (1 : ℝ)) hind_int S.historyBundle1.sigma)
filter_upwards [hsub'] with ω hω
rw [hω, hconst]
have hDen_bridge := cCompliance_bridge As z z0 hpre_z0
have hDen :
S.historyBundle1.condExpGiven
(({ω | S.DofZ z ω ≠ z0}).indicator (fun _ => (1 : ℝ))) P.μ
=ᵐ[P.μ]
fun ω => 1 - S.cObsProb z z0 ω := by
have hcompl := S.historyBundle1.condExpGiven_congr_ae
(μ := P.μ) (Filter.Eventually.of_forall (congrFun hInd))
filter_upwards [hcompl, hden_sub, hDen_bridge] with ω hc hs hb
rw [hc, hs, hb]
unfold cMixtureLATE POCFBundle.condExpRatio
filter_upwards [hNum, hDen] with ω hN hD
rw [hN, hD]
6 supporting declarations (lemmas, instances)
-
YofDofZ_eq_YofD_on_DofZEqtheorem — On the event {D(z) = d}, the encouragement-regime outcome Y(D(z)) agrees pointwise with the treatment-regime outcome Y(d).hypothesesconclusion∀ᵐ ω ∂P.μifS.DofZ z ω = dthenS.YofDofZ z ω = S.YofD d ωProof (Lean source)
theorem YofDofZ_eq_YofD_on_DofZEq (As : S.Assumptions) (z d : Fin 2 → Bool) : ∀ᵐ ω ∂P.μ, S.DofZ z ω = d → S.YofDofZ z ω = S.YofD d ω := by refine Filter.Eventually.of_forall ?_ intro ω hd -- Step 0: extract coordinate-wise treatment values from `S.DofZ z ω = d`. have hd1 : S.D1ofZ z ω = d 0 := by have := congrFun hd 0 simpa [DofZ] using this have hd2 : S.D2ofZ z ω = d 1 := by have := congrFun hd 1 exact this -- Y disjoint from regime targets (uses distinctness Z_i ≠ Y, D_i ≠ Y). have hYdisj : _root_.Disjoint ({S.Y} : Finset P.V) ((S.encouragementRegime z).target ∪ (S.treatmentRegime d).target) := by unfold encouragementRegime treatmentRegime rw [Regime.ofList_target, Regime.ofList_target] simp only [map_cons, map_nil, List.toFinset_cons, List.toFinset_nil, Finset.disjoint_singleton_left, mem_union, Finset.mem_insert, not_or] refine ⟨⟨S.Z1_ne_Y.symm, S.Z2_ne_Y.symm, fun h => (notMem_empty _ h).elim⟩, ⟨S.D1_ne_Y.symm, S.D2_ne_Y.symm, fun h => (notMem_empty _ h).elim⟩⟩ -- Construct IntermediateAgrees from D1ofZ z ω = d 0 and D2ofZ z ω = d 1. have hIA : P.IntermediateAgrees (S.encouragementRegime z) (S.treatmentRegime d) ω := by intro v hv -- treatmentRegime's target is {D₁, D₂}. Case-split. have hv' : v = S.D1 ∨ v = S.D2 := by unfold treatmentRegime at hv rw [Regime.ofList_target] at hv simp only [map_cons, map_nil, List.toFinset_cons, List.toFinset_nil, Finset.mem_insert] at hv rcases hv with hv | hv | hv · exact inl hv · exact inr hv · exact (notMem_empty _ hv).elim rcases hv' with rfl | rfl · -- v = S.D1 rw [treatmentRegime_assign_D1] have : S.hD1bool (P.eval (S.encouragementRegime z) ω S.D1) = d 0 := hd1 have := congrArg S.hD1bool.symm this simpa using this · -- v = S.D2 rw [treatmentRegime_assign_D2] have : S.hD2bool (P.eval (S.encouragementRegime z) ω S.D2) = d 1 := hd2 have := congrArg S.hD2bool.symm this simpa using this -- Apply composition consistency: poVariable (r_z ⊔ r_d) {Y} = poVariable r_z {Y}. have hComp := As.consistency.composition (S.encouragementRegime z) (S.treatmentRegime d) (S.encouragementRegime_disjoint_treatmentRegime z d) {S.Y} hYdisj ω hIA -- Extract pointwise eval at S.Y. have hEvalEq : P.eval (S.encTreatRegime z d) ω S.Y = P.eval (S.encouragementRegime z) ω S.Y := by have := congrFun hComp ⟨S.Y, mem_singleton_self _⟩ exact this -- Use exclusion: yVar.cf (encTreatRegime z d) ω = YofD d ω. have hExcl := As.exclusion z d ω -- Combine. have hYofDofZ : S.YofDofZ z ω = S.yVar.cf (S.encTreatRegime z d) ω := by change S.yVar.cf (S.encouragementRegime z) ω = S.yVar.cf (S.encTreatRegime z d) ω unfold POVar.cf congr 1 exact hEvalEq.symm rw [hYofDofZ, hExcl] -
DofZ_zero_eq_zerotheorem — Under one-sided noncompliance, the zero-encouragement counterfactual treatment is identically zero a.s.: D(0) = 0 a.s.Proof (Lean source)
theorem DofZ_zero_eq_zero (As : S.Assumptions) : ∀ᵐ ω ∂P.μ, S.DofZ ![false, false] ω = ![false, false] := by filter_upwards [As.oneSidedNoncompliance ![false, false]] with ω hω obtain ⟨h1, h2⟩ := hω have hz0 : (![false, false] : Fin 2 → Bool) 0 = false := rfl have hz1 : (![false, false] : Fin 2 → Bool) 1 = false := rfl rw [hz0] at h1 rw [hz1] at h2 have hD1 : S.D1ofZ ![false, false] ω = false := by cases h : S.D1ofZ ![false, false] ω <;> [rfl; (rw [h] at h1; exact absurd h1 (by decide))] have hD2 : S.D2ofZ ![false, false] ω = false := by cases h : S.D2ofZ ![false, false] ω <;> [rfl; (rw [h] at h2; exact absurd h2 (by decide))] funext i refine i.cases ?_ ?_ · simp [DofZ, hD1] · intro _; simp [DofZ, hD2] -
YofDofZ_zero_ae_eq_YofD_zerotheorem — A.s. Y(D(0)) = Y(0), the zero-encouragement composition collapse.Proof (Lean source)
theorem YofDofZ_zero_ae_eq_YofD_zero (As : S.Assumptions) : S.YofDofZ ![false, false] =ᵐ[P.μ] S.YofD ![false, false] := by have hcomp := YofDofZ_eq_YofD_on_DofZEq As ![false, false] ![false, false] filter_upwards [hcomp, DofZ_zero_eq_zero As] with ω hcomp hzero exact hcomp hzero -
DofZ_in_two_valuestheorem — For d ≼ z and one-sided noncompliance, D(z) ∈ {d, 0} a.s. when d is one of the two single-period treatment vectors (1,0) or (0,1), because the only d' ≼ z with d' ≠ d and d' ≠ 0 would have to flip a coordinate that one-sided rules out. Used to decompose Y(D(z)) on the encouragement event into the two-piece sum Y(d)·1_{D(z)=d} + Y(0)·1_{D(z)=0}.hypothesesProof (Lean source)
theorem DofZ_in_two_values (As : S.Assumptions) (d : Fin 2 → Bool) (hd : d = ![true, false] ∨ d = ![false, true]) : ∀ᵐ ω ∂P.μ, S.DofZ d ω = d ∨ S.DofZ d ω = ![false, false] := by filter_upwards [As.oneSidedNoncompliance d] with ω hω obtain ⟨h1, h2⟩ := hω rcases hd with hd | hd · subst d have hz0 : (![true, false] : Fin 2 → Bool) 0 = true := rfl have hz1 : (![true, false] : Fin 2 → Bool) 1 = false := rfl rw [hz0] at h1 rw [hz1] at h2 have hD2 : S.D2ofZ ![true, false] ω = false := by cases h : S.D2ofZ ![true, false] ω <;> [rfl; (rw [h] at h2; exact absurd h2 (by decide))] cases hD1 : S.D1ofZ ![true, false] ω · right funext i refine i.cases ?_ ?_ · simp [DofZ, hD1] · intro _; simp [DofZ, hD2] · left funext i refine i.cases ?_ ?_ · simp [DofZ, hD1] · intro _; simp [DofZ, hD2] · subst d have hz0 : (![false, true] : Fin 2 → Bool) 0 = false := rfl have hz1 : (![false, true] : Fin 2 → Bool) 1 = true := rfl rw [hz0] at h1 rw [hz1] at h2 have hD1 : S.D1ofZ ![false, true] ω = false := by cases h : S.D1ofZ ![false, true] ω <;> [rfl; (rw [h] at h1; exact absurd h1 (by decide))] cases hD2 : S.D2ofZ ![false, true] ω · right funext i refine i.cases ?_ ?_ · simp [DofZ, hD1] · intro _; simp [DofZ, hD2] · left funext i refine i.cases ?_ ?_ · simp [DofZ, hD1] · intro _; simp [DofZ, hD2] -
YofDofZ_decompositiontheorem — Under one-sided noncompliance, the encouragement-regime outcome under encouragement d ∈ {(1,0), (0,1)} decomposes pointwise as Y(d)·1_{D(d)=d} + Y(0)·1_{D(d)=0} a.s.hypothesesProof (Lean source)
theorem YofDofZ_decomposition (As : S.Assumptions) (d : Fin 2 → Bool) (hd : d = ![true, false] ∨ d = ![false, true]) : S.YofDofZ d =ᵐ[P.μ] fun ω => S.YofD d ω * (S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω + S.YofD ![false, false] ω * (S.DofZEq d ![false, false]).indicator (fun _ => (1 : ℝ)) ω := by filter_upwards [DofZ_in_two_values As d hd, YofDofZ_eq_YofD_on_DofZEq As d d, YofDofZ_eq_YofD_on_DofZEq As d ![false, false]] with ω hcase hdd hd0 rcases hcase with h | h · have h1 : (S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω = 1 := by exact Set.indicator_of_mem (s := S.DofZEq d d) (f := fun _ => (1 : ℝ)) h have h2 : (S.DofZEq d ![false, false]).indicator (fun _ => (1 : ℝ)) ω = 0 := by apply Set.indicator_of_notMem intro h0 have hd_ne_zero : d ≠ ![false, false] := by rcases hd with rfl | rfl <;> decide exact hd_ne_zero (h.symm.trans h0) rw [h1, h2] ring_nf exact hdd h · have h1 : (S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω = 0 := by apply Set.indicator_of_notMem intro hd' have hd_ne_zero : d ≠ ![false, false] := by rcases hd with rfl | rfl <;> decide exact hd_ne_zero (hd'.symm.trans h) have h2 : (S.DofZEq d ![false, false]).indicator (fun _ => (1 : ℝ)) ω = 1 := by exact Set.indicator_of_mem (s := S.DofZEq d ![false, false]) (f := fun _ => (1 : ℝ)) h rw [h1, h2] ring_nf exact hd0 h -
int_outcome_difference_identitytheorem — The numerator identity: the difference of the encouragement-regime outcome integrals collapses to the conditional contrast on {D(d) = d}.hypothesesProof (Lean source)
theorem int_outcome_difference_identity (As : S.Assumptions) (d : Fin 2 → Bool) (hd : d = ![true, false] ∨ d = ![false, true]) : (∫ ω, S.YofDofZ d ω ∂P.μ) - (∫ ω, S.YofDofZ ![false, false] ω ∂P.μ) = ∫ ω in S.DofZEq d d, (S.YofD d ω - S.YofD ![false, false] ω) ∂P.μ := by have hpoint : (fun ω => S.YofDofZ d ω - S.YofDofZ ![false, false] ω) =ᵐ[P.μ] fun ω => (S.YofD d ω - S.YofD ![false, false] ω) * (S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω := by filter_upwards [YofDofZ_decomposition As d hd, YofDofZ_zero_ae_eq_YofD_zero As, DofZ_in_two_values As d hd] with ω hdecomp hzero hcase rw [hdecomp, hzero] rcases hcase with h | h · have h1 : (S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω = 1 := by exact Set.indicator_of_mem (s := S.DofZEq d d) (f := fun _ => (1 : ℝ)) h have h2 : (S.DofZEq d ![false, false]).indicator (fun _ => (1 : ℝ)) ω = 0 := by apply Set.indicator_of_notMem intro h0 have hd_ne_zero : d ≠ ![false, false] := by rcases hd with rfl | rfl <;> decide exact hd_ne_zero (h.symm.trans h0) rw [h1, h2] ring_nf · have h1 : (S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω = 0 := by apply Set.indicator_of_notMem intro hd' have hd_ne_zero : d ≠ ![false, false] := by rcases hd with rfl | rfl <;> decide exact hd_ne_zero (hd'.symm.trans h) have h2 : (S.DofZEq d ![false, false]).indicator (fun _ => (1 : ℝ)) ω = 1 := by exact Set.indicator_of_mem (s := S.DofZEq d ![false, false]) (f := fun _ => (1 : ℝ)) h rw [h1, h2] ring_nf rw [← MeasureTheory.integral_sub (As.integrable_YofDofZ d) (As.integrable_YofDofZ ![false, false])] rw [MeasureTheory.integral_congr_ae hpoint] have h_rw : (fun ω => (S.YofD d ω - S.YofD ![false, false] ω) * (S.DofZEq d d).indicator (fun _ => (1 : ℝ)) ω) = (S.DofZEq d d).indicator (fun ω => S.YofD d ω - S.YofD ![false, false] ω) := by funext ω by_cases hω : ω ∈ S.DofZEq d d · simp [Set.indicator_of_mem hω] · simp [Set.indicator_of_notMem hω] rw [h_rw, MeasureTheory.integral_indicator (S.measurableSet_DofZEq d d)]