PO.ID.Exact.DynamicLATE
Dynamic LATE: identification of complier effects in multi-period instrumented settings.
Setup 51 core · 30 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 model in a potential-outcome system contains baseline covariates, an intermediate state, two encouragement nodes, two treatment nodes, and a real-valued outcome node, together with binary encouragement identifications, binary treatment identifications, a real-valued outcome identification, and pairwise distinctness of all seven nodes. These variables support dynamic complier treatment effects; identification requires separate assumptions and Wald identities.
def z1Var reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The first-period encouragement variable exposes the initial binary instrument in a two-period dynamic LATE system.
Definition (Lean source)
parameters
given by
⟨S.Z1, S.hZ1bool⟩
def z2Var reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The second-period encouragement variable exposes the later binary instrument in a two-period dynamic LATE system.
Definition (Lean source)
parameters
given by
⟨S.Z2, S.hZ2bool⟩
def d1Var reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The first-period treatment variable exposes initial binary uptake in a two-period dynamic LATE system.
Definition (Lean source)
parameters
given by
⟨S.D1, S.hD1bool⟩
def d2Var reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The second-period treatment variable exposes later binary uptake in a two-period dynamic LATE system.
Definition (Lean source)
parameters
given by
⟨S.D2, S.hD2bool⟩
def yVar reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The real-valued outcome variable exposes the terminal response in a two-period dynamic LATE system.
Definition (Lean source)
parameters
def
given by
⟨S.Y, S.hYreal⟩
def factualS0 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observed baseline state records pre-encouragement covariates for each unit in a two-period dynamic LATE system.
Definition (Lean source)
parameters
def
factualS0 S :
P.Ω → γ₀
given by
S.S0.factual
def factualS1 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observed intermediate state records the covariates available between periods in a two-period dynamic LATE system.
Definition (Lean source)
parameters
def
factualS1 S :
P.Ω → γ₁
given by
S.S1.factual
def factualZ1 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observed first-period encouragement records each unit's initial instrument value in a two-period dynamic LATE system.
Definition (Lean source)
parameters
def
given by
S.z1Var.factual
def factualZ2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observed second-period encouragement records each unit's later instrument value in a two-period dynamic LATE system.
Definition (Lean source)
parameters
def
given by
S.z2Var.factual
def factualD1 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observed first-period treatment records initial uptake for each unit in a two-period dynamic LATE system.
Definition (Lean source)
parameters
def
given by
S.d1Var.factual
def factualD2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observed second-period treatment records later uptake for each unit in a two-period dynamic LATE system.
Definition (Lean source)
parameters
def
given by
S.d2Var.factual
def factualY reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observed terminal outcome records each unit's realized response in a two-period dynamic LATE system.
Definition (Lean source)
parameters
def
factualY S :
P.Ω → ℝ
given by
S.yVar.factual
def encouragementRegime reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The joint encouragement regime fixes both period-specific instruments in a two-period dynamic LATE system to a chosen binary path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
given by
Regime.ofList [⟨S.Z1, S.hZ1bool.symm (z 0)⟩, ⟨S.Z2, S.hZ2bool.symm (z 1)⟩] (by simp only [List.map_cons, List.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
The joint treatment regime fixes both period-specific treatments in a two-period dynamic LATE system to a chosen binary path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
given by
Regime.ofList [⟨S.D1, S.hD1bool.symm (d 0)⟩, ⟨S.D2, S.hD2bool.symm (d 1)⟩] (by simp only [List.map_cons, List.map_nil, List.nodup_cons, List.mem_singleton, List.not_mem_nil, not_false_eq_true, List.nodup_nil, and_true] exact S.D1_ne_D2)
def encZ2Regime reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The second-stage-only encouragement regime intervenes on the later instrument in a two-period dynamic LATE system at a chosen binary value, leaving period one natural.
Definition (Lean source)
parameters
def
given by
Regime.single S.Z2 (S.hZ2bool.symm z₂)
lemma encouragementRegime_disjoint_treatmentRegime reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Joint encouragement and treatment interventions target disjoint node sets for any chosen encouragement and treatment paths, so the two regimes can be combined without a conflicting assignment.
Formal statement
hypotheses
γ₀ :
Type
γ₁ :
Type
conclusion
(S.encouragementRegime z).Disjoint (S.treatmentRegime d)
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 [List.map_cons, List.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
The combined encouragement-and-treatment regime fixes all four period-specific variables in a two-period dynamic LATE system to the selected encouragement and treatment paths.
Definition (Lean source)
def D1ofZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
First-period treatment under encouragement records initial uptake in a two-period dynamic LATE system when both instruments follow the selected path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
given by
S.d1Var.cf (S.encouragementRegime z)
def D2ofZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Second-period treatment under encouragement records later uptake in a two-period dynamic LATE system when both instruments follow the selected path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
given by
S.d2Var.cf (S.encouragementRegime z)
def DofZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The treatment path induced by encouragement joins both potential treatment decisions in a two-period dynamic LATE system under the selected instrument path.
def D2ofZ2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Second-period treatment under a late encouragement intervention records later uptake in a two-period dynamic LATE system when only the second instrument is fixed.
Definition (Lean source)
parameters
def
given by
S.d2Var.cf (S.encZ2Regime z₂)
def YofD reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Outcome under a treatment path records the terminal response in a two-period dynamic LATE system when both treatments follow the selected path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
YofD S d :
P.Ω → ℝ
given by
S.yVar.cf (S.treatmentRegime d)
def YofDofZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Outcome under an encouragement path records the terminal response in a two-period dynamic LATE system when both instruments follow the selected path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
YofDofZ S z :
P.Ω → ℝ
given by
S.yVar.cf (S.encouragementRegime z)
def YofZ2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Outcome under a late encouragement intervention records the terminal response in a two-period dynamic LATE system when only the second instrument is fixed.
Definition (Lean source)
parameters
def
YofZ2 S z₂ :
P.Ω → ℝ
given by
S.yVar.cf (S.encZ2Regime z₂)
def yUnderZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The regimed outcome under encouragement couples the terminal response in a two-period dynamic LATE system with the joint instrument path that generates it.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
given by
⟨S.yVar, S.encouragementRegime z⟩
def d1UnderZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The regimed first-period treatment couples initial uptake in a two-period dynamic LATE system with the joint instrument path that generates it.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
given by
⟨S.d1Var, S.encouragementRegime z⟩
def d2UnderZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The regimed second-period treatment couples later uptake in a two-period dynamic LATE system with the joint instrument path that generates it.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
given by
⟨S.d2Var, S.encouragementRegime z⟩
def yUnderZ2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The regimed outcome under a late intervention couples the terminal response in a two-period dynamic LATE system with the second-period encouragement that is fixed.
Definition (Lean source)
parameters
def
given by
⟨S.yVar, S.encZ2Regime z₂⟩
def d2UnderZ2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The regimed second-period treatment under a late intervention couples later uptake in a two-period dynamic LATE system with the second-period encouragement that is fixed.
Definition (Lean source)
parameters
def
given by
⟨S.d2Var, S.encZ2Regime z₂⟩
def historyBundle1 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The first-stage observed history in a two-period dynamic LATE system contains exactly the baseline state available before the initial encouragement.
Definition (Lean source)
parameters
def
given by
POCFBundle.cons (RegimedVar.ofFactual S.S0) (POCFBundle.nil P)
def historyBundle2 reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The second-stage observed history in a two-period dynamic LATE system contains baseline and intermediate states together with the first encouragement and treatment.
Definition (Lean source)
parameters
def
given by
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
The first-stage counterfactual bundle collects the outcome and both treatment responses in a two-period dynamic LATE system under the selected encouragement path, the joint object required for initial sequential ignorability.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
given by
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
The second-stage counterfactual bundle collects the outcome and later treatment response in a two-period dynamic LATE system under the selected late encouragement, the object required for second-stage ignorability.
Definition (Lean source)
parameters
def
given by
POCFBundle.cons (S.yUnderZ2 z₂) <| POCFBundle.cons (S.d2UnderZ2 z₂) <| POCFBundle.nil P
def indD reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observed treatment-path indicator selects units in a two-period dynamic LATE system whose two realized treatments match the chosen path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
indD S d :
P.Ω → ℝ
given by
fun ω => S.d1Var.indicator (d 0) ω * S.d2Var.indicator (d 1) ω
def indZ reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observed encouragement-path indicator selects units in a two-period dynamic LATE system whose two realized instruments match the chosen path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
indZ S z :
P.Ω → ℝ
given by
fun ω => S.z1Var.indicator (z 0) ω * S.z2Var.indicator (z 1) ω
def innerCondY reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The inner observable outcome regression conditions the terminal outcome in a two-period dynamic LATE system on the full second-stage history and the selected encouragement path, forming the first layer of the g-formula bridge.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
innerCondY S z :
P.Ω → ℝ
given by
S.historyBundle2.condExpRatio (fun ω => S.factualY ω * S.indZ z ω) (S.indZ z) P.μ
def innerCondD reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The inner observable treatment-path regression gives the conditional probability of a selected treatment path in a two-period dynamic LATE system, given the full second-stage history and encouragement path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
innerCondD S z d :
P.Ω → ℝ
given by
S.historyBundle2.condExpRatio (fun ω => S.indD d ω * S.indZ z ω) (S.indZ z) P.μ
def cObsMean reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The baseline-conditional observable outcome mean averages the inner outcome regression in a two-period dynamic LATE system over post-baseline history for the selected encouragement path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
cObsMean S z :
P.Ω → ℝ
given by
S.historyBundle1.condExpRatio (fun ω => S.innerCondY z ω * S.z1Var.indicator (z 0) ω) (S.z1Var.indicator (z 0)) P.μ
def cObsProb reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The baseline-conditional observable treatment-path probability averages the inner probability for a treatment path in a two-period dynamic LATE system over post-baseline history under the selected encouragement path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
cObsProb S z d :
P.Ω → ℝ
given by
S.historyBundle1.condExpRatio (fun ω => S.innerCondD z d ω * S.z1Var.indicator (z 0) ω) (S.z1Var.indicator (z 0)) P.μ
def obsMean reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observable g-formula mean averages the baseline-conditional nested regression in a two-period dynamic LATE system for the selected encouragement path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
obsMean S z :
ℝ
given by
∫ ω, S.cObsMean z ω ∂P.μ
def obsProb reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The observable g-formula treatment-path probability averages the nested regression for a selected treatment path in a two-period dynamic LATE system under the selected encouragement path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
obsProb S z d :
ℝ
given by
∫ ω, S.cObsProb z d ω ∂P.μ
def DofZEq reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The dynamic-complier event selects units in a two-period dynamic LATE system whose treatment response to an encouragement path equals the target treatment path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
given by
{ ω | S.DofZ z ω = d }
def LATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The dynamic local average treatment effect in a two-period dynamic LATE system averages the outcome contrast between a target treatment path and no treatment among units induced to that path by the selected encouragement, using zero when the subgroup is empty.
def cLATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The baseline-conditional dynamic LATE in a two-period dynamic LATE system localizes the effect of a target treatment path versus no treatment among units induced by the selected encouragement path to each baseline state.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
cLATE S z d :
P.Ω → ℝ
def whenToTreatLATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The when-to-treat LATE in a two-period dynamic LATE system evaluates a single path both as the encouragement schedule and as the treatment timing it induces.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
whenToTreatLATE S d :
ℝ
given by
S.LATE d d
def cWhenToTreatLATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The baseline-conditional when-to-treat LATE in a two-period dynamic LATE system evaluates a single path as both encouragement and induced treatment timing within each baseline stratum.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
cWhenToTreatLATE S d :
P.Ω → ℝ
given by
S.cLATE d d
def mixtureLATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The mixture LATE in a two-period dynamic LATE system averages the outcome gain induced by an encouragement path among all units moved to any nonzero treatment path.
Definition (Lean source)
def cMixtureLATE reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The baseline-conditional mixture LATE in a two-period dynamic LATE system localizes the outcome gain induced by an encouragement path among units moved to any nonzero treatment path.
Definition (Lean source)
parameters
γ₀ :
Type
γ₁ :
Type
def
cMixtureLATE S z :
P.Ω → ℝ
def Preceq reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Coordinatewise path order records that one binary path never exceeds a second path, the comparison used to express one-sided noncompliance period by period.
structure Assumptions reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The dynamic instrumental-variable / LATE assumptions for the two-period system (def:po-dynamic-late-assumptions): factual potential-outcome consistency for the ambient system; composition consistency for its sequential encouragement and treatment regimes; 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
assumes
consistency :
P.Consistency
compositionConsistency :
P.CompositionConsistency
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 :
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).
exclusion_D1 :
S.d1Var.cf (S.encouragementRegime z) ω
= S.d1Var.cf (Regime.single S.Z1 (S.hZ1bool.symm (z 0))) ω
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_Z1 :
∀ (z₂ : Bool) (ω : P.Ω), P.eval (S.encZ2Regime z₂) ω S.Z1 = P.eval Regime.empty ω S.Z1
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 CompositionConsistency.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)).
integrable_YofD :
integrable_YofDofZ :
integrable_YofZ2 :
∀ z₂ : Bool, Integrable (S.YofZ2 z₂) P.μ
30 supporting declarations (lemmas, instances)
-
Z1_ne_Z2lemma — The two encouragements occupy distinct nodes in the dynamic LATE system, so their joint intervention cannot assign one variable twice.hypothesesconclusionS.Z1 ≠ S.Z2Proof (Lean source)
lemma Z1_ne_Z2 : S.Z1 ≠ S.Z2 := by have := S.vars_inj.ne (show (2 : Fin 7) ≠ 4 by decide) simpa [varVec_apply_two, varVec_apply_four] using this -
D1_ne_D2lemma — The two treatments occupy distinct nodes in the dynamic LATE system, so a treatment-path intervention is well defined.hypothesesconclusionS.D1 ≠ S.D2Proof (Lean source)
lemma D1_ne_D2 : S.D1 ≠ S.D2 := by have := S.vars_inj.ne (show (3 : Fin 7) ≠ 5 by decide) simpa [varVec_apply_three, varVec_apply_five] using this -
D1_ne_Ylemma — First-period treatment and the terminal outcome occupy distinct nodes in the dynamic LATE system, separating intervention from response.hypothesesconclusionS.D1 ≠ S.YProof (Lean source)
lemma D1_ne_Y : S.D1 ≠ S.Y := by have := S.vars_inj.ne (show (3 : Fin 7) ≠ 6 by decide) simpa [varVec_apply_three, varVec_apply_six] using this -
D2_ne_Ylemma — Second-period treatment and the terminal outcome occupy distinct nodes in the dynamic LATE system, separating intervention from response.hypothesesconclusionS.D2 ≠ S.YProof (Lean source)
lemma D2_ne_Y : S.D2 ≠ S.Y := by have := S.vars_inj.ne (show (5 : Fin 7) ≠ 6 by decide) simpa [varVec_apply_five, varVec_apply_six] using this -
Z1_ne_Ylemma — First-period encouragement and the terminal outcome occupy distinct nodes in the dynamic LATE system, separating assignment from response.hypothesesconclusionS.Z1 ≠ S.YProof (Lean source)
lemma Z1_ne_Y : S.Z1 ≠ S.Y := by have := S.vars_inj.ne (show (2 : Fin 7) ≠ 6 by decide) simpa [varVec_apply_two, varVec_apply_six] using this -
Z2_ne_Ylemma — Second-period encouragement and the terminal outcome occupy distinct nodes in the dynamic LATE system, separating assignment from response.hypothesesconclusionS.Z2 ≠ S.YProof (Lean source)
lemma Z2_ne_Y : S.Z2 ≠ S.Y := by have := S.vars_inj.ne (show (4 : Fin 7) ≠ 6 by decide) simpa [varVec_apply_four, varVec_apply_six] using this -
Z1_ne_D1lemma — First-period encouragement and treatment occupy distinct nodes in the dynamic LATE system, allowing the instrument to shift rather than equal uptake.hypothesesconclusionS.Z1 ≠ S.D1Proof (Lean source)
lemma Z1_ne_D1 : S.Z1 ≠ S.D1 := by have := S.vars_inj.ne (show (2 : Fin 7) ≠ 3 by decide) simpa [varVec_apply_two, varVec_apply_three] using this -
Z1_ne_D2lemma — First-period encouragement and second-period treatment occupy distinct nodes in the dynamic LATE system, keeping the sequential intervention targets separate.hypothesesconclusionS.Z1 ≠ S.D2Proof (Lean source)
lemma Z1_ne_D2 : S.Z1 ≠ S.D2 := by have := S.vars_inj.ne (show (2 : Fin 7) ≠ 5 by decide) simpa [varVec_apply_two, varVec_apply_five] using this -
Z2_ne_D1lemma — Second-period encouragement and first-period treatment occupy distinct nodes in the dynamic LATE system, keeping the sequential intervention targets separate.hypothesesconclusionS.Z2 ≠ S.D1Proof (Lean source)
lemma Z2_ne_D1 : S.Z2 ≠ S.D1 := by have := S.vars_inj.ne (show (4 : Fin 7) ≠ 3 by decide) simpa [varVec_apply_four, varVec_apply_three] using this -
Z2_ne_D2lemma — Second-period encouragement and treatment occupy distinct nodes in the dynamic LATE system, allowing the later instrument to shift rather than equal uptake.hypothesesconclusionS.Z2 ≠ S.D2Proof (Lean source)
lemma Z2_ne_D2 : S.Z2 ≠ S.D2 := by have := S.vars_inj.ne (show (4 : Fin 7) ≠ 5 by decide) simpa [varVec_apply_four, varVec_apply_five] using this -
YofDofZ_eqlemma — Outcome under a joint encouragement path is exactly the counterfactual outcome evaluated in that intervention regime for the dynamic LATE system and chosen instrument path, connecting the economic notation to the regime semantics.hypothesesγ₀ :sharedTypeγ₁ :sharedTypeconclusionS.YofDofZ z = S.yVar.cf (S.encouragementRegime z)Proof (Lean source)
@[causal_defs_simps] lemma YofDofZ_eq (z : Fin 2 → Bool) : S.YofDofZ z = S.yVar.cf (S.encouragementRegime z) := rfl -
measurable_D1ofZlemma — First-period treatment under an encouragement path is measurable, so a dynamic LATE system can form events and moments for that path.Proof (Lean source)
@[fun_prop] lemma measurable_D1ofZ (z : Fin 2 → Bool) : Measurable (S.D1ofZ z) := S.d1Var.measurable_cf _ -
measurable_D2ofZlemma — Second-period treatment under an encouragement path is measurable, so a dynamic LATE system can form events and moments for that path.Proof (Lean source)
@[fun_prop] lemma measurable_D2ofZ (z : Fin 2 → Bool) : Measurable (S.D2ofZ z) := S.d2Var.measurable_cf _ -
measurable_DofZlemma — The induced treatment path is measurable, so the dynamic LATE system has measurable dynamic-complier events for each encouragement path.Proof (Lean source)
@[fun_prop] 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 — Later treatment under a second-stage-only intervention is measurable, so the system supports conditional treatment probabilities for that late encouragement.hypothesesconclusionMeasurable (S.D2ofZ2 z₂)Proof (Lean source)
@[fun_prop] lemma measurable_D2ofZ2 (z₂ : Bool) : Measurable (S.D2ofZ2 z₂) := S.d2Var.measurable_cf _ -
measurable_YofDlemma — Outcome under a fixed treatment path is measurable, permitting causal outcome averages in the system for that path.Proof (Lean source)
@[fun_prop] lemma measurable_YofD (d : Fin 2 → Bool) : Measurable (S.YofD d) := S.yVar.measurable_cf _ -
measurable_YofDofZlemma — Outcome under a fixed encouragement path is measurable, permitting g-formula moments in the system for that path.Proof (Lean source)
@[fun_prop] lemma measurable_YofDofZ (z : Fin 2 → Bool) : Measurable (S.YofDofZ z) := S.yVar.measurable_cf _ -
measurable_YofZ2lemma — Outcome under a second-stage-only intervention is measurable, permitting sequential regression in the system for that late encouragement.hypothesesconclusionMeasurable (S.YofZ2 z₂)Proof (Lean source)
-
measurable_factualS0lemma — The observed baseline state is measurable, so the system can condition its first-stage regression on pre-encouragement information.hypothesesconclusionMeasurable S.factualS0Proof (Lean source)
@[fun_prop] lemma measurable_factualS0 : Measurable S.factualS0 := S.S0.measurable_factual -
measurable_factualS1lemma — The observed intermediate state is measurable, so the system can include it in the second-stage history.hypothesesconclusionMeasurable S.factualS1Proof (Lean source)
@[fun_prop] lemma measurable_factualS1 : Measurable S.factualS1 := S.S1.measurable_factual -
measurable_factualZ1lemma — The observed first encouragement is measurable, making initial assignment cells available in the system.hypothesesconclusionMeasurable S.factualZ1Proof (Lean source)
@[fun_prop] lemma measurable_factualZ1 : Measurable S.factualZ1 := S.z1Var.measurable_factual -
measurable_factualZ2lemma — The observed second encouragement is measurable, making later assignment cells available in the system.hypothesesconclusionMeasurable S.factualZ2Proof (Lean source)
@[fun_prop] lemma measurable_factualZ2 : Measurable S.factualZ2 := S.z2Var.measurable_factual -
measurable_factualD1lemma — The observed first treatment is measurable, so initial uptake can enter the later history in the system.hypothesesconclusionMeasurable S.factualD1Proof (Lean source)
@[fun_prop] lemma measurable_factualD1 : Measurable S.factualD1 := S.d1Var.measurable_factual -
measurable_factualD2lemma — The observed second treatment is measurable, making realized treatment paths events in the system.hypothesesconclusionMeasurable S.factualD2Proof (Lean source)
@[fun_prop] lemma measurable_factualD2 : Measurable S.factualD2 := S.d2Var.measurable_factual -
measurable_factualYlemma — The observed terminal outcome is measurable, so its nested conditional means are defined in the system.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
integrable_factualY_of_consistency_integrable_YofZ2lemma — The observed outcome is integrable whenever consistency links it to the integrable potential outcomes under both second-period encouragement values in the dynamic LATE system. This licenses the observable outcome regressions.hypothesesγ₀ :sharedTypeγ₁ :sharedTypeIsFiniteMeasure P.μhC :P.ConsistencyhY :∀ z₂ : Bool, Integrable (S.YofZ2 z₂) P.μconclusionIntegrable 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 treatment-path indicator is measurable, so the dynamic LATE system can condition on matching a chosen treatment path.Proof (Lean source)
@[fun_prop] 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 encouragement-path indicator is measurable, so the dynamic LATE system can condition on matching a chosen instrument path.Proof (Lean source)
@[fun_prop] 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 — Each dynamic-complier subgroup is measurable, so the dynamic LATE system can average outcomes among units induced by an encouragement path to a treatment path.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.hypothesesγ₀ :sharedTypeγ₁ :sharedTypeAs :S.AssumptionsconclusionIntegrable S.factualY P.μProof (Lean source)
@[fun_prop] 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 · 4 supporting This file proves the counterfactual-to-observable bridge identities for the two-period dynamic LATE setup. ★ cOutcome_bridge★ cCompliance_bridge★ outcome_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.
def d2ofZ2EqIndicator reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
The late-treatment response-cell indicator marks units in a dynamic LATE system whose second-period treatment under a fixed late encouragement equals the selected treatment value.
Definition (Lean source)
parameters
def
d2ofZ2EqIndicator S z₂ b :
P.Ω → ℝ
given by
(S.D2ofZ2 z₂ ⁻¹' {b}).indicator (fun _ => (1 : ℝ))
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
hypotheses
γ₀ :
Type
As :
S.Assumptions
conclusion
S.historyBundle1.condExpGiven (S.YofDofZ z) P.μ =ᵐ[P.μ] S.cObsMean z
Proof (Lean source)
theorem cOutcome_bridge (As : S.Assumptions) (z : Fin 2 → Bool) :
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_indicator_ae_eq_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 (baseline-conditional). Under the dynamic LATE identifying assumptions, for a selected encouragement path and target treatment path, the baseline-conditional probability that the induced treatment path matches the target agrees almost surely with its observable two-stage nested regression.
Formal statement
hypotheses
γ₀ :
Type
As :
S.Assumptions
conclusion
S.historyBundle1.condExpGiven ((S.DofZEq z d).indicator (fun _ => (1 : ℝ))) P.μ
=ᵐ[P.μ] S.cObsProb z d
Proof (Lean source)
theorem cCompliance_bridge (As : S.Assumptions) (z d : Fin 2 → Bool) :
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_indicator_ae_eq_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 ω (succ 0) = S.D2ofZ z ω := by rfl
_ = S.D2ofZ2 (z 1) ω := hcD2
_ = d 1 := hcfD2
_ = d (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
hypotheses
γ₀ :
Type
As :
S.Assumptions
conclusion
∫ ω, S.YofDofZ z ω ∂P.μ = S.obsMean z
Proof (Lean source)
theorem outcome_bridge (As : S.Assumptions) (z : Fin 2 → Bool) :
∫ ω, S.YofDofZ z ω ∂P.μ = S.obsMean z := by
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)
_ = S.obsMean z := rfl
4 supporting declarations (lemmas, instances)
-
probDofZ_eq_zero_of_not_preceqtheorem — A treatment path that exceeds its encouragement path has zero probability under the dynamic LATE assumptions, for the encouragement and treatment paths whenever coordinatewise dominance fails.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 inner observed outcome regression, restricted to the first-encouragement cell, equals the history-conditional potential outcome under the second encouragement under the dynamic LATE assumptions for the selected encouragement path. This is the inner layer of the sequential g-formula bridge.hypothesesγ₀ :sharedTypeAs :S.Assumptionsconclusion(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_indicator_ae_eq_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 — The inner observed treatment-path regression, restricted to the first-encouragement cell, equals the first-treatment indicator times the history-conditional late-treatment response probability under the dynamic LATE assumptions, for the selected encouragement and treatment paths. This identifies the inner compliance regression.hypothesesγ₀ :sharedTypeAs :S.Assumptionsconclusion(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_indicator_ae_eq_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] -
compliance_bridgetheorem — Compliance bridge (unconditional). Under the dynamic LATE identifying assumptions, for a selected encouragement path and target treatment path, the population share whose induced treatment path matches the target equals the observable g-formula path probability.hypothesesγ₀ :sharedTypeAs :S.Assumptionsconclusion(P.μ (S.DofZEq z d)).toReal = S.obsProb z dProof (Lean source)
theorem compliance_bridge (As : S.Assumptions) (z d : Fin 2 → Bool) : (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) _ = S.obsProb z d := rfl
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
Potential second-period treatment under a full encouragement path equals treatment from fixing only the later encouragement under the dynamic LATE assumptions, for an encouragement path and a unit whose observed initial encouragement matches it. The matching condition makes first-stage regime detail irrelevant.
Formal statement
hypotheses
γ₀ :
Type
As :
S.Assumptions
ω :
P.Ω
hω :
S.factualZ1 ω = z 0
conclusion
S.D2ofZ z ω = S.D2ofZ2 (z 1) ω
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
YofZ2_eq_factualY_on_z2Eventtheorem — Consistency identifies the potential outcome under a fixed late encouragement with the observed outcome under the dynamic LATE assumptions, for a second-period encouragement and a unit observed in that encouragement cell.hypothesesγ₀ :sharedTypeAs :S.Assumptionsz₂ :ω :P.Ωhω :S.factualZ2 ω = z₂conclusionS.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 — Consistency identifies potential second-period treatment under a fixed late encouragement with observed second-period treatment under the dynamic LATE assumptions, for a late encouragement and a unit observed in that cell.hypothesesγ₀ :sharedTypeAs :S.Assumptionsz₂ :ω :P.Ωhω :S.factualZ2 ω = z₂conclusionS.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 — A full encouragement-path outcome agrees with the outcome from fixing only the later encouragement under the dynamic LATE assumptions, for an encouragement path and a unit whose observed initial encouragement matches that path. This removes irrelevant first-stage regime detail.hypothesesγ₀ :sharedTypeAs :S.Assumptionsω :P.Ωhω :S.factualZ1 ω = z 0conclusionS.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 — Potential first-period treatment under an encouragement path equals observed first-period treatment under the dynamic LATE assumptions, for an encouragement path and a unit whose observed initial encouragement matches it. This is the stage-one consistency bridge.hypothesesγ₀ :sharedTypeAs :S.Assumptionsω :P.Ωhω :S.factualZ1 ω = z 0conclusionS.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 3 core · 7 supporting This file proves the Wald-style ratio identifications for the dynamic when-to-treat and mixture LATE parameters. ★ 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 mixtureLATE_wald reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Mixture dynamic LATE Wald identity (unconditional). Under the dynamic LATE assumptions, for an encouragement path, the mixture LATE equals the observable Wald ratio.
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 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]
unfold mixtureLATE
rw [hNum, hDen]
theorem cWhenToTreat_wald reviewed
⚑ flagged
Causalean.PO.PODynLATESystem
Baseline-conditional when-to-treat Wald identity. Under the dynamic LATE identifying assumptions, for a path that treats in period one only or period two only, the timing-specific conditional effect equals almost surely the conditional observable-mean contrast against zero encouragement divided by the conditional compliance probability.
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 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
condexp_linearity [As.integrable_YofDofZ d, As.integrable_YofDofZ z0]
have hbr_d := cOutcome_bridge As d
have hbr_0 := cOutcome_bridge As z0
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
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 assumptions, for an encouragement path, the conditional mixture LATE equals its observable Wald ratio almost surely.
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 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
condexp_linearity [As.integrable_YofDofZ z, As.integrable_YofDofZ z0]
have hbr_z := cOutcome_bridge As z
have hbr_0 := cOutcome_bridge As z0
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
condexp_linearity
filter_upwards [hsub'] with ω hω
rw [hω, hconst]
have hDen_bridge := cCompliance_bridge As z 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]
7 supporting declarations (lemmas, instances)
-
YofDofZ_eq_YofD_on_DofZEqtheorem — Outcome under encouragement equals outcome under the treatment path it induces under the dynamic LATE assumptions, for an encouragement path and realized treatment path. This composition bridge turns encouragement effects into treatment effects.hypothesesγ₀ :sharedTypeAs :S.Assumptionsconclusion∀ᵐ ω ∂P.μ, S.DofZ z ω = d → S.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 [List.map_cons, List.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 [List.map_cons, List.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.compositionConsistency.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 — Zero encouragement induces the all-zero treatment path almost surely under the dynamic LATE assumptions. One-sided noncompliance rules out treatment without encouragement.hypothesesProof (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 — Outcome under zero encouragement equals outcome under no treatment almost surely under the dynamic LATE assumptions, providing the baseline term for Wald contrasts.hypothesesProof (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 — A one-period treatment-timing encouragement induces either its matching treatment path or no treatment, almost surely under the dynamic LATE assumptions, when the selected path starts treatment in exactly one of the two periods. One-sided noncompliance eliminates every other response path.hypothesesγ₀ :sharedTypeAs :S.AssumptionsProof (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 — Outcome under a one-period treatment-timing encouragement decomposes into the target-path outcome on compliers and the no-treatment outcome otherwise, almost surely under the dynamic LATE assumptions, for the selected path when it treats in exactly one period.hypothesesγ₀ :sharedTypeAs :S.AssumptionsProof (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 mean outcome contrast between a one-period timing encouragement and zero encouragement equals the treatment-effect contrast restricted to units induced into that timing under the dynamic LATE assumptions, for the selected timing path when it treats in exactly one period. This supplies the Wald numerator.hypothesesγ₀ :sharedTypeAs :S.AssumptionsProof (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)] -
whenToTreat_waldtheorem — When-to-treat dynamic LATE Wald identity (unconditional). Under the dynamic LATE identifying assumptions, for a path that treats in period one only or period two only, the timing-specific local average treatment effect equals the observable mean contrast against zero encouragement divided by the observable compliance probability.hypothesesγ₀ :sharedTypeAs :S.AssumptionsProof (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 exact compliance_bridge As d d -- Combine. unfold whenToTreatLATE LATE rw [hNum, hDen]