Estimation.MinimaxATE.Causal
Causal grounding for the MinimaxATE lower bounds: a finite backdoor SCM and potential-outcome system, the causalATE target, and bridges that recenter the lower bound from the observed-data contrast to the causal ATE.
Construction 23 core · 8 supporting This file builds, from a finite data-generating process (m, g) on a finite covariate space C, a concrete generalized SCM realizing the textbook backdoor triangle and lifts it through Causalean.PO.Bridge.FromSCM.POSystem. ★ wTopo_lt★ wParent_mem
Causal Grounding of the Minimax ATE Model
This file builds, from a finite data-generating process (m, g) on a finite
covariate space C, a concrete generalized SCM realizing the textbook backdoor
triangle and lifts it through Causalean.PO.Bridge.FromSCM.POSystem.ofSCM to a
POBackdoorSystem. Its potential-outcome ATE S.ATE = E[Y(1) − Y(0)] is what
the minimax lower bound is really about; the bridge MinimaxATE/Causal/Bridge.lean
identifies S.ATE with the observed-data contrast ate g used by the proof
machinery.
The DAG is the backdoor triangle on the OBSERVED covariate Xc:
Un → Xc → A → Y with Xc → Y, plus independent latent noise roots
Ea → A, Ey → Y:
* Un ~ Uniform(C), the latent covariate draw; the observed covariate node
Xc := Un copies it (Causalean SCM observed nodes must be endogenous);
* treatment A := 1{Ea ≤ m Xc}, so A | X=x ~ Bernoulli(m x) (Ea ~ U[0,1]);
* outcome Y(a) := 1{Ey ≤ g a Xc} and Y := A·Y(1) + (1−A)·Y(0)
(Ey ~ U[0,1]), the consistency assignment; Ea ⟂ Ey | X so unconfoundedness
A ⟂ (Y(1), Y(0)) | X holds.
The construction is stated directly for a finite covariate C and the
propensity/outcome pair (m, g). The main
public objects are the witness graph data WNode, wDAG, and wSWIGGraph; the
structural functions treatFun and outFun; the laws unifLaw and covLaw;
the concrete SCM dgpSCM; and the induced potential-outcome/backdoor systems
dgpPO and dgpBackdoor.
inductive WNode reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
The finite backdoor witness-node type consists of the observed covariate node, the treatment node, the outcome node, the latent covariate-draw node, the treatment-noise node, and the outcome-noise node.
Definition (Lean source)
inductive
WNode :
Type
constructors
Xc :
| A | Y | Un | Ea | Ey
deriving DecidableEq
def wEdge reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
The edge relation of the finite backdoor witness graph contains the arrow from the latent covariate draw to the observed covariate, the arrow from the observed covariate to treatment, the arrow from the observed covariate to outcome, the arrow from treatment to outcome, the arrow from treatment noise to treatment, and the arrow from outcome noise to outcome; every other ordered pair has no arrow.
def wTopo reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
The topological ordering of a witness-graph node assigns rank zero to the latent covariate draw, rank one to treatment noise, rank two to outcome noise, rank three to the observed covariate, rank four to treatment, and rank five to the outcome.
Definition (Lean source)
def
given by
clause 1
| Un => 0
clause 2
| Ea => 1
clause 3
| Ey => 2
clause 4
| Xc => 3
clause 5
| A => 4
clause 6
| Y => 5
theorem wTopo_lt reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
Every edge of the finite backdoor witness graph points strictly forward in the chosen topological order on its nodes.
Formal statement
def wDAG reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
The directed acyclic graph for the finite backdoor witness is the graph whose nodes are the witness nodes and whose arrows are the specified witness-graph edge relation.
def wSWIGGraph reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
The single-world intervention graph for the finite backdoor witness has the witness directed acyclic graph, no fixed nodes, observed nodes for the covariate, treatment, and outcome, and unobserved nodes for the three latent noise variables.
Definition (Lean source)
given by
clause 1
clause 2
fixed := ∅
clause 3
observed := {SWIGNode.random Xc, SWIGNode.random A, SWIGNode.random Y}
clause 4
unobserved := {SWIGNode.random Un, SWIGNode.random Ea, SWIGNode.random Ey}
clause 5
fixed_is_fixed := by intro s hs; simp at hs
clause 6
clause 7
clause 8
obs_unobs_disjoint := by decide
clause 9
dag_edges_classified := by decide
clause 10
fixed_image_in_observed := by intro s hs; simp at hs
clause 11
fixed_are_roots := by intro s hs; simp at hs
clause 12
unobs_are_roots := by intro u hu; simp at hu rcases hu with rfl | rfl | rfl <;> simpa [initialSWIG] using (swig_random_root_of_root wDAG ∅ _ (by decide))
clause 13
fixed_outside_fixed_isolated := by intro n _ cases n <;> exact ⟨by decide, by decide⟩
clause 14
all_children_in_observed := by decide
def WΩ reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a covariate space, the value space assigned to each witness-graph node is the covariate space for the observed covariate, the binary space for treatment, the real line for the outcome, the covariate space for the latent covariate draw, the real line for treatment noise, and the real line for outcome noise.
def treatFun reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
Given a real-valued propensity score and a real-valued treatment-noise draw, the binary treatment assignment is true exactly when the noise draw is no greater than the propensity score.
Definition (Lean source)
def outFun reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
Given a covariate space, an outcome-regression function indexed by binary treatment and covariate value, a binary treatment value, a covariate value, and a real-valued outcome-noise draw, the real-valued outcome is one exactly when the noise draw is no greater than the corresponding outcome-regression value, and is zero otherwise.
theorem wParent_mem reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For any edge from node p to node c in the finite backdoor witness graph, the SWIG node for p is a parent of the SWIG node for c in the initial SWIG built from that graph.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem wParent_mem {p c : WNode} (h : wEdge p c) :
(SWIGNode.random p) ∈ (initialSWIG wDAG).parents (SWIGNode.random c) := by
rw [DAG.mem_parents, initialSWIG_random_edge]; exact h
def parentVal reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
Given a covariate space, a child witness node, the supplied values of all parents of that child, a parent witness node, and an arrow from that parent to the child, the extracted parent value is that parent’s supplied value.
Definition (Lean source)
parameters
def
given by
vals ⟨SWIGNode.random p, wParent_mem h⟩
def unifLaw reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
The latent-noise probability law is the uniform probability distribution on the closed unit interval of the real line.
def covLaw reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure, the covariate probability law assigns equal probability to every covariate value.
Definition (Lean source)
def dgpSCM reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function for the two treatment arms, the structural causal model has a uniformly distributed latent covariate, independent unit-interval treatment and outcome noises, treatment generated by thresholding its noise at the propensity, and outcome generated by thresholding its noise at the arm-specific outcome regression.
Definition (Lean source)
parameters
given by
clause 1
toSWIGGraph := wSWIGGraph
clause 2
edgeTypes := EdgeTypeAssignment.allNonparametric (initialSWIG wDAG)
clause 3
iota_valueSpace := by intro s exact (notMem_empty s.val s.property).elim
clause 4
structFun := fun v vals
=> match v with | ⟨SWIGNode.random Xc, _⟩ => (parentVal (C := C) vals (show wEdge Un Xc from trivial) : C) | ⟨SWIGNode.random A, _⟩ => treatFun (m (parentVal (C := C) vals (show wEdge Xc A from trivial))) (parentVal (C := C) vals (show wEdge Ea A from trivial)) | ⟨SWIGNode.random Y, _⟩ => outFun (C := C) g (parentVal (C := C) vals (show wEdge A Y from trivial)) (parentVal (C := C) vals (show wEdge Xc Y from trivial)) (parentVal (C := C) vals (show wEdge Ey Y from trivial)) | ⟨SWIGNode.random Un, h⟩ => absurd h (by decide) | ⟨SWIGNode.random Ea, h⟩ => absurd h (by decide) | ⟨SWIGNode.random Ey, h⟩ => absurd h (by decide) | ⟨SWIGNode.fixed n, h⟩ => (by simp only [wSWIGGraph, Finset.mem_insert, Finset.mem_singleton] at h rcases h with h | h | h <;> exact absurd h (by simp) : False).elim
clause 5
structFun_measurable := by intro v rcases v with ⟨n, hn⟩ cases n with | random a
=> cases a <;> simp [parentVal, treatFun, outFun] · exact measurable_pi_apply _ · let iEa : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random A)} := ⟨SWIGNode.random Ea, wParent_mem (show wEdge Ea A from trivial)⟩ let iX : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random A)} := ⟨SWIGNode.random Xc, wParent_mem (show wEdge Xc A from trivial)⟩ have hEa : Measurable (fun vals : (∀ w : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random A)}, swigΩ (WΩ C) w.val) => (show ℝ from vals iEa)) := by exact measurable_pi_apply iEa have hX : Measurable (fun vals : (∀ w : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random A)}, swigΩ (WΩ C) w.val) => (show C from vals iX)) := by exact measurable_pi_apply iX show Measurable (fun vals : (∀ w : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random A)}, swigΩ (WΩ C) w.val) => if (show ℝ from vals iEa) ≤ m (show C from vals iX) then true else false) refine Measurable.ite ?_ measurable_const measurable_const exact measurableSet_le hEa ((measurable_of_finite m).comp hX) · let iEy : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random Y)} := ⟨SWIGNode.random Ey, wParent_mem (show wEdge Ey Y from trivial)⟩ let iA : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random Y)} := ⟨SWIGNode.random A, wParent_mem (show wEdge A Y from trivial)⟩ let iX : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random Y)} := ⟨SWIGNode.random Xc, wParent_mem (show wEdge Xc Y from trivial)⟩ have hEy : Measurable (fun vals : (∀ w : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random Y)}, swigΩ (WΩ C) w.val) => (show ℝ from vals iEy)) := by exact measurable_pi_apply iEy have hA : Measurable (fun vals : (∀ w : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random Y)}, swigΩ (WΩ C) w.val) => (show Bool from vals iA)) := by exact measurable_pi_apply iA have hX : Measurable (fun vals : (∀ w : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random Y)}, swigΩ (WΩ C) w.val) => (show C from vals iX)) := by exact measurable_pi_apply iX have hg : Measurable (fun vals : (∀ w : {w // w ∈ (initialSWIG wDAG).parents (SWIGNode.random Y)}, swigΩ (WΩ C) w.val) => g (show Bool from vals iA) (show C from vals iX)) := (measurable_of_finite (fun p : Bool × C => g p.1 p.2)).comp (hA.prodMk hX) refine Measurable.ite ?_ measurable_const measurable_const exact measurableSet_le hEy hg | fixed a => simp [wSWIGGraph] at hn
clause 6
clause 7
isProbability_latent := by intro u rcases u with ⟨n, hn⟩ cases n with | random n
=> cases n <;> simp [wSWIGGraph] at hn ⊢ · exact instIsProbabilityMeasureCovLaw C · exact instIsProbabilityMeasureUnifLaw · exact instIsProbabilityMeasureUnifLaw | fixed n => simp [wSWIGGraph] at hn
def dgpFixed reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function, the background assignment for the witness causal model assigns no fixed values.
Definition (Lean source)
def dgpPO reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function, the induced potential-outcome system is the one generated by the witness structural causal model with its empty background assignment.
def AIdx reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function, the treatment index is the observed treatment node of the induced potential-outcome system.
def YIdx reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function, the outcome index is the observed outcome node of the induced potential-outcome system.
def XIdx reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function, the covariate index is the observed covariate node of the induced potential-outcome system.
def AEquiv reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function, the measurable identification of the treatment node’s value space with the binary treatment space is the identity map.
def YEquiv reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function, the measurable identification of the outcome node’s value space with the real line is the identity map.
def XEquiv reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function, the measurable identification of the covariate node’s value space with the covariate space is the identity map.
def dgpBackdoor reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function, the backdoor potential-outcome system uses the constructed treatment, outcome, and covariate nodes as its treatment, outcome, and adjustment variables.
8 supporting declarations (lemmas, instances)
-
instDecidableEqWNodeinstancederiving DecidableEq -
instFintypeinstance — The finite enumeration of backdoor witness nodes consists of the six witness nodes, with every witness node included and a proof that this enumeration is exhaustive. -
instDecidableRelWNodeWEdgeinstance — The procedure deciding whether an ordered pair of witness nodes is an edge examines the finite witness-graph edge relation.instancegiven byby intro a b; cases a <;> cases b <;> simp [wEdge] <;> infer_instance -
WΩ_measinstance — For a covariate space equipped with a measurable structure and each witness node, the measurable-space structure for that witness-node value space is the given covariate measurable structure for the observed covariate, the binary measurable structure for treatment, the real-line measurable structure for outcome, the given covariate measurable structure for the latent covariate draw, the real-line measurable structure for treatment noise, and the real-line measurable structure for outcome noise.parametersC :sharedTypen :instancegiven byclause 1| Xc => inferInstanceAs (MeasurableSpace C)clause 2| A => inferInstanceAs (MeasurableSpace Bool)clause 3| Y => inferInstanceAs (MeasurableSpace ℝ)clause 4| Un => inferInstanceAs (MeasurableSpace C)clause 5| Ea => inferInstanceAs (MeasurableSpace ℝ)clause 6| Ey => inferInstanceAs (MeasurableSpace ℝ) -
WΩ_borelinstance — For a covariate space with measurable and standard-Borel structures and each witness node, the standard-Borel structure for that witness-node value space is the given structure for the observed covariate, the binary structure for treatment, the real-line structure for outcome, the given structure for the latent covariate draw, the real-line structure for treatment noise, and the real-line structure for outcome noise.parametersC :sharedTypen :instancegiven byclause 1| Xc => inferInstanceAs (StandardBorelSpace C)clause 2| A => inferInstanceAs (StandardBorelSpace Bool)clause 3| Y => inferInstanceAs (StandardBorelSpace ℝ)clause 4| Un => inferInstanceAs (StandardBorelSpace C)clause 5| Ea => inferInstanceAs (StandardBorelSpace ℝ)clause 6| Ey => inferInstanceAs (StandardBorelSpace ℝ) -
WΩ_nonemptyinstance — For a nonempty covariate space and each witness node, the nonemptiness certificate for that witness-node value space is the given certificate for the observed covariate, a binary value for treatment, a real value for outcome, the given certificate for the latent covariate draw, a real value for treatment noise, and a real value for outcome noise.parametersC :sharedTypen :instancegiven byclause 1| Xc => inferInstanceAs (Nonempty C)clause 2| A => inferInstanceAs (Nonempty Bool)clause 3| Y => inferInstanceAs (Nonempty ℝ)clause 4| Un => inferInstanceAs (Nonempty C)clause 5| Ea => inferInstanceAs (Nonempty ℝ)clause 6| Ey => inferInstanceAs (Nonempty ℝ) -
instIsProbabilityMeasureUnifLawinstance — The uniform law on the closed unit interval is a probability measure.instancegiven byby unfold unifLaw constructor simp [Real.volume_Icc] -
instIsProbabilityMeasureCovLawinstance — For a finite, nonempty covariate space with a measurable structure, the uniform covariate law is a probability measure.
Bridge_Part1 6 core · 11 supporting This first part defines the causal ATE of the constructed backdoor system and proves consistency, coordinate formulas for its factual and potential-outcome variables, and elementary integral and conditional-expectation f ★ dgp_condExp_ea_threshold_const
Causal Grounding of the Minimax ATE Model: Foundations
This first part defines the causal ATE of the constructed backdoor system and proves consistency,
coordinate formulas for its factual and potential-outcome variables, and elementary integral and
conditional-expectation facts used by the later bridge parts. The final identification theorem is
proved in Bridge_Part3.lean.
def causalATE reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function, the causal average treatment effect is the average treatment effect of the constructed finite backdoor potential-outcome system.
Definition (Lean source)
abbrev iUn reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a propensity function and an outcome-regression function, the covariate-noise index identifies the latent disturbance that generates covariates in the constructed potential-outcome system. It is used to read the factual covariate from a latent realization.
Definition (Lean source)
abbrev iEa reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a propensity function and an outcome-regression function, the treatment-assignment-noise index identifies the latent disturbance that determines treatment in the constructed potential-outcome system. It is used to express the factual treatment rule.
Definition (Lean source)
abbrev iEy reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a propensity function and an outcome-regression function, the outcome-noise index identifies the latent disturbance that generates outcomes in the constructed potential-outcome system. It is used to express factual and counterfactual outcome rules.
Definition (Lean source)
def dgpXSingletonEquiv reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
The covariate singleton equivalence identifies a covariate value with the configuration containing that value at the covariate node alone. It lets the constructed system compare ordinary covariate values with graph-indexed configurations.
Definition (Lean source)
parameters
C :
Type
def
given by
clause 1
clause 2
clause 3
left_inv := fun x
clause 4
right_inv := fun x
clause 5
clause 6
lemma dgp_condExp_ea_threshold_const reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite standard-Borel covariate population, propensity function, and two outcome regressions, a fixed covariate value, and the requirement that its propensity lies between zero and one, the conditional mean of the latent treatment threshold indicator given the covariate equals that propensity almost surely.
Formal statement
hypotheses
Proof (Lean source)
lemma dgp_condExp_ea_threshold_const (x : C) (ht : m x ∈ Icc (0 : ℝ) 1) :
(dgpPO m g).μ[fun ℓ : SCM.LatentValues (dgpSCM m g) =>
if (show ℝ from ℓ (iEa (C := C) m g)) ≤ m x then (1 : ℝ) else 0 |
MeasurableSpace.comap
(fun ℓ : SCM.LatentValues (dgpSCM m g) => ℓ (iUn (C := C) m g)) inferInstance]
=ᵐ[(dgpPO m g).μ] fun _ => m x := by
let eFun : SCM.LatentValues (dgpSCM m g) → ℝ := fun ℓ => ℓ (iEa (C := C) m g)
let uFun : SCM.LatentValues (dgpSCM m g) → C := fun ℓ => ℓ (iUn (C := C) m g)
let eInd : SCM.LatentValues (dgpSCM m g) → ℝ :=
fun ℓ => if eFun ℓ ≤ m x then (1 : ℝ) else 0
have he_sm : StronglyMeasurable[MeasurableSpace.comap eFun inferInstance] eInd := by
letI : MeasurableSpace (SCM.LatentValues (dgpSCM m g)) :=
MeasurableSpace.comap eFun inferInstance
have he_meas : Measurable eFun := comap_measurable eFun
have hset : MeasurableSet {ℓ : SCM.LatentValues (dgpSCM m g) | eFun ℓ ≤ m x} :=
measurableSet_le he_meas measurable_const
exact (Measurable.ite hset measurable_const measurable_const).stronglyMeasurable
have hle_e : MeasurableSpace.comap eFun inferInstance ≤
(inferInstance : MeasurableSpace (SCM.LatentValues (dgpSCM m g))) := by
dsimp [eFun]
exact (measurable_pi_apply (iEa (C := C) m g)).comap_le
have hle_u : MeasurableSpace.comap uFun inferInstance ≤
(inferInstance : MeasurableSpace (SCM.LatentValues (dgpSCM m g))) := by
dsimp [uFun]
exact (measurable_pi_apply (iUn (C := C) m g)).comap_le
haveI : IsProbabilityMeasure (dgpPO m g).μ := dgpPO_isProb
haveI : IsFiniteMeasure (dgpPO m g).μ := inferInstance
haveI : IsFiniteMeasure ((dgpPO m g).μ.trim hle_u) :=
isFiniteMeasure_trim (μ := (dgpPO m g).μ) hle_u
have hsig : SigmaFinite ((dgpPO m g).μ.trim hle_u) :=
MeasureTheory.IsFiniteMeasure.toSigmaFinite ((dgpPO m g).μ.trim hle_u)
have hmain := by
exact @MeasureTheory.condExp_indep_eq
(SCM.LatentValues (dgpSCM m g)) ℝ _ _ _
(MeasurableSpace.comap eFun inferInstance)
(MeasurableSpace.comap uFun inferInstance)
(inferInstance : MeasurableSpace (SCM.LatentValues (dgpSCM m g)))
((dgpPO m g).μ) eInd hle_e hle_u hsig he_sm dgp_indep_ea_un
have hmain' :
(dgpPO m g).μ[fun ℓ : SCM.LatentValues (dgpSCM m g) =>
if (show ℝ from ℓ (iEa (C := C) m g)) ≤ m x then (1 : ℝ) else 0 |
MeasurableSpace.comap
(fun ℓ : SCM.LatentValues (dgpSCM m g) => ℓ (iUn (C := C) m g)) inferInstance]
=ᵐ[(dgpPO m g).μ]
fun _ => ∫ ℓ : SCM.LatentValues (dgpSCM m g),
(if (show ℝ from ℓ (iEa (C := C) m g)) ≤ m x then (1 : ℝ) else 0) ∂(dgpPO m g).μ := by
exact hmain
refine hmain'.trans ?_
exact Filter.Eventually.of_forall fun ℓ => by
dsimp [eInd, eFun, uFun]
change (∫ ℓ : SCM.LatentValues (dgpSCM m g),
(if (show ℝ from ℓ (iEa (C := C) m g)) ≤ m x then (1 : ℝ) else 0) ∂(dgpPO m g).μ) =
m x
exact dgp_integral_ea_threshold (m := m) (g := g) x ht
11 supporting declarations (lemmas, instances)
-
dgpPO_isProbinstance — For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable, a propensity function, and an outcome-regression function for both treatment arms, the population law of the constructed potential-outcome system is a probability measure.parametersinstancegiven byby change IsProbabilityMeasure (SCM.latentProduct (dgpSCM m g)) infer_instance -
dgpPO_boreltheorem — The constructed potential-outcome system has a standard Borel sample space.Proof (Lean source)
theorem dgpPO_borel : StandardBorelSpace (dgpPO m g).Ω := by change StandardBorelSpace (SCM.LatentValues (dgpSCM m g)) haveI : ∀ n : SWIGNode WNode, StandardBorelSpace (swigΩ (WΩ C) n) := by intro n; cases n <;> infer_instance exact pi_countable -
dgpPO_standardBorelinstance — For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable and a standard-Borel structure, a propensity function, and an outcome-regression function for both treatment arms, the sample space of the constructed potential-outcome system has a standard-Borel structure.parametersinstancegiven by -
dgp_factualX_eq_latentUnlemma — For a finite covariate space, propensity function, and outcome regression, the constructed backdoor data-generating process's factual covariate equals its latent covariate coordinate.Proof (Lean source)
lemma dgp_factualX_eq_latentUn : (dgpBackdoor m g).factualX = (fun ℓ : SCM.LatentValues (dgpSCM m g) => ℓ (iUn (C := C) m g)) := by funext ℓ simp only [POBackdoorSystem.factualX, POVar.factual, POVar.cf] change (dgpBackdoor m g).xVar.equiv (inducedEval (dgpSCM m g) (dgpFixed m g) Regime.empty ℓ (XIdx m g)) = ℓ (iUn (C := C) m g) rw [inducedEval_empty_eq_evalMap (dgpSCM m g) (dgpFixed m g) ℓ (XIdx m g)] change (XEquiv m g) ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) = ℓ (iUn (C := C) m g) rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [dgpSCM, wSWIGGraph]⟩] unfold XEquiv dgpSCM parentVal iUn rfl -
dgp_factualD_eq_treatFunlemma — For a finite covariate space, propensity function, and outcome regression, the constructed backdoor process's factual treatment is the threshold treatment function of its latent covariate and treatment-noise coordinates.Proof (Lean source)
lemma dgp_factualD_eq_treatFun : (dgpBackdoor m g).factualD = (fun ℓ : SCM.LatentValues (dgpSCM m g) => treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) := by funext ℓ simp only [POBackdoorSystem.factualD, POVar.factual, POVar.cf] change (dgpBackdoor m g).dVar.equiv (inducedEval (dgpSCM m g) (dgpFixed m g) Regime.empty ℓ (AIdx m g)) = treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)) rw [inducedEval_empty_eq_evalMap (dgpSCM m g) (dgpFixed m g) ℓ (AIdx m g)] change (AEquiv m g) ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.A, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) = treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)) rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.A, by simp [dgpSCM, wSWIGGraph]⟩] change treatFun (m ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩)) (ℓ (iEa (C := C) m g)) = treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)) rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [dgpSCM, wSWIGGraph]⟩] unfold dgpSCM parentVal iUn rfl -
dgp_factualY_eq_outFunlemma — For a finite covariate space, propensity function, and outcome regression, the constructed backdoor process's factual outcome is its outcome function evaluated at the threshold treatment, latent covariate, and outcome-noise coordinates.hypothesesProof (Lean source)
lemma dgp_factualY_eq_outFun : (dgpBackdoor m g).factualY = (fun ℓ : SCM.LatentValues (dgpSCM m g) => outFun (C := C) g (treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g))) := by funext ℓ simp only [POBackdoorSystem.factualY, POVar.factual, POVar.cf] change (dgpBackdoor m g).yVar.equiv (inducedEval (dgpSCM m g) (dgpFixed m g) Regime.empty ℓ (YIdx m g)) = outFun (C := C) g (treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g)) rw [inducedEval_empty_eq_evalMap (dgpSCM m g) (dgpFixed m g) ℓ (YIdx m g)] change (YEquiv m g) ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Y, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) = outFun (C := C) g (treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g)) rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Y, by simp [dgpSCM, wSWIGGraph]⟩] change outFun (C := C) g ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.A, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) (ℓ (iEy (C := C) m g)) = outFun (C := C) g (treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g)) have hAeval : (dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.A, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩ = treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)) := by rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.A, by simp [dgpSCM, wSWIGGraph]⟩] change treatFun (m ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩)) (ℓ (iEa (C := C) m g)) = treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)) rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [dgpSCM, wSWIGGraph]⟩] unfold dgpSCM parentVal iUn rfl have hXeval : (dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩ = ℓ (iUn (C := C) m g) := by rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [dgpSCM, wSWIGGraph]⟩] unfold dgpSCM parentVal iUn rfl rw [hAeval, hXeval] -
dgp_YofD_eq_outFunlemma — For a finite covariate space, propensity function, outcome regression, and treatment value, the constructed backdoor process's potential outcome at that treatment equals its outcome function of the latent covariate and outcome-noise coordinates.hypothesesconclusion(dgpBackdoor m g).YofD dProof (Lean source)
lemma dgp_YofD_eq_outFun (d : Bool) : (dgpBackdoor m g).YofD d = (fun ℓ : SCM.LatentValues (dgpSCM m g) => outFun (C := C) g d (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g))) := by funext ℓ let r : Regime (ObsIdx (dgpSCM m g)) (obsValue (dgpSCM m g)) := Regime.single (AIdx m g) d let M' := (dgpSCM m g).fixSet (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) unfold POBackdoorSystem.YofD POVar.cfUnder POVar.cf change (YEquiv m g) (M'.evalMap (combinedFixed (dgpSCM m g) (dgpFixed m g) r) ℓ ⟨SWIGNode.random WNode.Y, by simp [M', SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) = outFun (C := C) g d (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g)) let ξ : ∀ w : {w // w ∈ M'.dag.parents (SWIGNode.random WNode.Y)}, swigΩ (WΩ C) w.val := fun w => if huo : w.val ∈ M'.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M'.fixed then combinedFixed (dgpSCM m g) (dgpFixed m g) r ⟨w.val, hfix⟩ else have hedge : M'.dag.edge w.val (SWIGNode.random WNode.Y) := M'.dag.mem_parents.mp w.property have hobs : w.val ∈ M'.observed := by rcases Finset.mem_union.mp (M'.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo M'.evalMap (combinedFixed (dgpSCM m g) (dgpFixed m g) r) ℓ ⟨w.val, mem_union_left _ hobs⟩ rw [SCM.evalMap_fixSet_observed_apply (dgpSCM m g) (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (combinedFixed (dgpSCM m g) (dgpFixed m g) r) ℓ ⟨SWIGNode.random WNode.Y, by simp [dgpSCM, wSWIGGraph]⟩] change (YEquiv m g) ((dgpSCM m g).structFun ⟨SWIGNode.random WNode.Y, by simp [dgpSCM, wSWIGGraph]⟩ (SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ)) = outFun (C := C) g d (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g)) simp only [YEquiv, dgpSCM] change outFun (C := C) g (parentVal (C := C) (SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ) (show wEdge WNode.A WNode.Y from trivial)) (parentVal (C := C) (SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ) (show wEdge WNode.Xc WNode.Y from trivial)) (parentVal (C := C) (SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ) (show wEdge WNode.Ey WNode.Y from trivial)) = outFun (C := C) g d (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g)) have hTargetA : regimeTargetN (dgpSCM m g) r = {WNode.A} := by dsimp [r] exact dgp_regimeTargetN_single_A (m := m) (g := g) d have hDmem : WNode.A ∈ regimeTargetN (dgpSCM m g) r := by simpa [hTargetA] have hAtgt : (AIdx m g) ∈ r.target := by change (AIdx m g) ∈ ({AIdx m g} : Finset (ObsIdx (dgpSCM m g))) exact mem_singleton_self (AIdx m g) have hAval : (AIdx m g).val = SWIGNode.random WNode.A := by rfl have hA : parentVal (C := C) (SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ) (show wEdge WNode.A WNode.Y from trivial) = d := by change SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ ⟨SWIGNode.random WNode.A, wParent_mem (show wEdge WNode.A WNode.Y from trivial)⟩ = d refine (SCM.fixMonoParentMap_apply_random (Ω := WΩ C) (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) WNode.A hDmem ξ _).trans ?_ dsimp [ξ] have hAf_unobs : SWIGNode.fixed WNode.A ∉ M'.unobserved := by show SWIGNode.fixed WNode.A ∉ (dgpSCM m g).unobserved simp [dgpSCM, wSWIGGraph] have hAf_fixed : SWIGNode.fixed WNode.A ∈ M'.fixed := mem_union_right _ (Finset.mem_image.mpr ⟨WNode.A, hDmem, rfl⟩) rw [dif_neg hAf_unobs, dif_pos hAf_fixed] change (combinedFixed (dgpSCM m g) (dgpFixed m g) r ⟨SWIGNode.fixed WNode.A, hAf_fixed⟩ : Bool) = d rw [combinedFixed_new (dgpSCM m g) (dgpFixed m g) r (AIdx m g) hAtgt WNode.A hDmem hAval] rfl rw [hA] have hXeval : M'.evalMap (combinedFixed (dgpSCM m g) (dgpFixed m g) r) ℓ ⟨SWIGNode.random WNode.Xc, mem_union_left _ (by simp [M', dgpSCM, wSWIGGraph])⟩ = ℓ (iUn (C := C) m g) := by rw [SCM.evalMap_fixSet_observed_apply (dgpSCM m g) (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (combinedFixed (dgpSCM m g) (dgpFixed m g) r) ℓ ⟨SWIGNode.random WNode.Xc, by simp [dgpSCM, wSWIGGraph]⟩] simp only [dgpSCM] change SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Xc) _ ⟨SWIGNode.random WNode.Un, wParent_mem (show wEdge WNode.Un WNode.Xc from trivial)⟩ = ℓ (iUn (C := C) m g) refine (SCM.fixMonoParentMap_apply_random_notMem (Ω := WΩ C) (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Xc) _ WNode.Un (by simpa [hTargetA]) _).trans ?_ exact dif_pos (iUn (C := C) m g).property have hXnot : WNode.Xc ∉ regimeTargetN (dgpSCM m g) r := by simpa [hTargetA] have hX : parentVal (C := C) (SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ) (show wEdge WNode.Xc WNode.Y from trivial) = ℓ (iUn (C := C) m g) := by change SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ ⟨SWIGNode.random WNode.Xc, wParent_mem (show wEdge WNode.Xc WNode.Y from trivial)⟩ = ℓ (iUn (C := C) m g) refine (SCM.fixMonoParentMap_apply_random_notMem (Ω := WΩ C) (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ WNode.Xc hXnot _).trans ?_ dsimp [ξ] have hXc_unobs : SWIGNode.random WNode.Xc ∉ M'.unobserved := by show SWIGNode.random WNode.Xc ∉ (dgpSCM m g).unobserved simp [dgpSCM, wSWIGGraph] have hXc_fixed : SWIGNode.random WNode.Xc ∉ M'.fixed := by show SWIGNode.random WNode.Xc ∉ (dgpSCM m g).fixed ∪ (regimeTargetN (dgpSCM m g) r).image SWIGNode.fixed intro hmem rcases Finset.mem_union.mp hmem with h | h · exact absurd h (by show SWIGNode.random WNode.Xc ∉ (∅ : Finset (SWIGNode WNode)) simp) · obtain ⟨D, -, hD⟩ := Finset.mem_image.mp h simp at hD rw [dif_neg hXc_unobs, dif_neg hXc_fixed] exact hXeval rw [hX] have hEynot : WNode.Ey ∉ regimeTargetN (dgpSCM m g) r := by simpa [hTargetA] have hEy : parentVal (C := C) (SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ) (show wEdge WNode.Ey WNode.Y from trivial) = ℓ (iEy (C := C) m g) := by change SCM.fixMonoParentMap (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ ⟨SWIGNode.random WNode.Ey, wParent_mem (show wEdge WNode.Ey WNode.Y from trivial)⟩ = ℓ (iEy (C := C) m g) refine (SCM.fixMonoParentMap_apply_random_notMem (Ω := WΩ C) (dgpSCM m g).toSWIGGraph (regimeTargetN (dgpSCM m g) r) (regimeTargetN_obs (dgpSCM m g) r) (regimeTargetN_notFixed (dgpSCM m g) r) (SWIGNode.random WNode.Y) ξ WNode.Ey hEynot _).trans ?_ dsimp [ξ] exact dif_pos (iEy (C := C) m g).property rw [hEy] -
dgp_dIndicator_true_eq_thresholdlemma — For a finite covariate space, propensity function, and outcome regression, the indicator of factual treatment being true in the constructed process equals the indicator that treatment noise does not exceed the propensity at the latent covariate.Proof (Lean source)
lemma dgp_dIndicator_true_eq_threshold : (dgpBackdoor m g).dVar.indicator true = (fun ℓ : SCM.LatentValues (dgpSCM m g) => if (show ℝ from ℓ (iEa (C := C) m g)) ≤ m (show C from ℓ (iUn (C := C) m g)) then (1 : ℝ) else 0) := by funext ℓ unfold POVar.indicator POVar.event change (((dgpBackdoor m g).factualD ⁻¹' {true}).indicator (fun _ => (1 : ℝ))) ℓ = (if (show ℝ from ℓ (iEa (C := C) m g)) ≤ m (show C from ℓ (iUn (C := C) m g)) then (1 : ℝ) else 0) have hval : (dgpBackdoor m g).factualD ℓ = treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)) := by rw [dgp_factualD_eq_treatFun (m := m) (g := g)] by_cases h : (show ℝ from ℓ (iEa (C := C) m g)) ≤ m (show C from ℓ (iUn (C := C) m g)) · have hb : (dgpBackdoor m g).factualD ℓ = true := by rw [hval] unfold treatFun simp only [decide_eq_true_eq] exact h rw [Set.indicator_of_mem (show ℓ ∈ (dgpBackdoor m g).factualD ⁻¹' ({true} : Set Bool) from hb), if_pos h] · have hb : (dgpBackdoor m g).factualD ℓ = false := by rw [hval] unfold treatFun simp only [decide_eq_false_iff_not] exact h have hnot : ℓ ∉ (dgpBackdoor m g).factualD ⁻¹' ({true} : Set Bool) := by intro hmem have hmem' : (dgpBackdoor m g).factualD ℓ = true := hmem rw [hb] at hmem' exact Bool.noConfusion hmem' rw [Set.indicator_of_notMem hnot, if_neg h] -
unifLaw_integral_Iic_indicatorlemma — For a threshold between zero and one, the uniform-law integral of the indicator that a draw does not exceed the threshold equals the threshold.Proof (Lean source)
lemma unifLaw_integral_Iic_indicator (t : ℝ) (ht : t ∈ Icc (0 : ℝ) 1) : ∫ e, (if e ≤ t then (1 : ℝ) else 0) ∂unifLaw = t := by have hs : MeasurableSet (Set.Iic t : Set ℝ) := measurableSet_Iic have hfun : (fun e : ℝ => if e ≤ t then (1 : ℝ) else 0) = (Set.Iic t).indicator (fun _ => (1 : ℝ)) := by funext e by_cases h : e ≤ t · simp [Set.indicator_of_mem, h] · simp [Set.indicator_of_notMem, h] rw [hfun] have hint : ∫ e, (Set.Iic t).indicator (fun _ : ℝ => (1 : ℝ)) e ∂unifLaw = unifLaw.real (Set.Iic t) := by exact MeasureTheory.integral_indicator_one (μ := unifLaw) hs rw [hint] rw [MeasureTheory.measureReal_def] unfold unifLaw rw [Measure.restrict_apply hs] have hset : Set.Iic t ∩ Icc (0 : ℝ) 1 = Icc (0 : ℝ) t := by ext e constructor · intro h exact ⟨h.2.1, h.1⟩ · intro h exact ⟨h.2, ⟨h.1, le_trans h.2 ht.2⟩⟩ rw [hset, Real.volume_Icc] rw [ENNReal.toReal_ofReal] · simp · simpa using ht.1 -
integrable_of_measurable_zero_onelemma — On a finite measure space, for a real-valued function, if the function is measurable and takes only the values zero and one, then it is integrable.Proof (Lean source)
lemma integrable_of_measurable_zero_one {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {f : Ω → ℝ} (hf : Measurable f) (h01 : ∀ ω, f ω = 0 ∨ f ω = 1) : Integrable f μ := by refine Integrable.of_bound hf.aestronglyMeasurable 1 (Filter.Eventually.of_forall ?_) intro ω rcases h01 ω with h | h <;> simp [h]
Bridge_Part2 1 core · 1 supporting This second part proves the variable-threshold conditional-expectation identities for the treatment and outcome noises in the constructed backdoor system. ★ dgp_condExp_outcome_threshold_var
Causal Grounding of the Minimax ATE Model: Conditional Expectations
This second part proves the variable-threshold conditional-expectation identities for the
treatment and outcome noises in the constructed backdoor system. The causal assumptions,
backdoor-estimation-system assembly, and final ATE identification are proved in
Bridge_Part3.lean.
lemma dgp_condExp_outcome_threshold_var reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite standard-Borel covariate population, propensity function, and two outcome regressions, if these functions define a valid data-generating process, then the conditional mean of the generated outcome given treatment and covariates equals the corresponding outcome regression almost surely.
Formal statement
hypotheses
conclusion
(dgpPO m g).μ[fun ℓ : SCM.LatentValues (dgpSCM m g) => outFun (C := C) g (treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g)) | comap (fun ℓ : SCM.LatentValues (dgpSCM m g) => (treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)), ℓ (iUn (C := C) m g))) inferInstance]
Proof (Lean source)
lemma dgp_condExp_outcome_threshold_var (hv : ValidDGP m g) :
(dgpPO m g).μ[fun ℓ : SCM.LatentValues (dgpSCM m g) =>
outFun (C := C) g
(treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)))
(ℓ (iUn (C := C) m g))
(ℓ (iEy (C := C) m g)) |
comap
(fun ℓ : SCM.LatentValues (dgpSCM m g) =>
(treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)),
ℓ (iUn (C := C) m g))) inferInstance]
=ᵐ[(dgpPO m g).μ]
fun ℓ => g
(treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)))
(ℓ (iUn (C := C) m g)) := by
classical
let dxFun : SCM.LatentValues (dgpSCM m g) → Bool × C :=
fun ℓ => (treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)),
ℓ (iUn (C := C) m g))
let eFun : SCM.LatentValues (dgpSCM m g) → ℝ := fun ℓ => ℓ (iEy (C := C) m g)
let cell : Bool × C → SCM.LatentValues (dgpSCM m g) → ℝ :=
fun p ℓ => if dxFun ℓ = p then (1 : ℝ) else 0
let eth : Bool × C → SCM.LatentValues (dgpSCM m g) → ℝ :=
fun p ℓ => if eFun ℓ ≤ g p.1 p.2 then (1 : ℝ) else 0
let piece : Bool × C → SCM.LatentValues (dgpSCM m g) → ℝ :=
fun p ℓ => cell p ℓ * eth p ℓ
have hdx_meas : Measurable dxFun := by
dsimp [dxFun]
have hUn : Measurable (fun ℓ : SCM.LatentValues (dgpSCM m g) =>
(show C from ℓ (iUn (C := C) m g))) :=
measurable_pi_apply (iUn (C := C) m g)
have hEa : Measurable (fun ℓ : SCM.LatentValues (dgpSCM m g) =>
(show ℝ from ℓ (iEa (C := C) m g))) :=
measurable_pi_apply (iEa (C := C) m g)
have htreat : Measurable
(fun ℓ : SCM.LatentValues (dgpSCM m g) =>
treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) := by
show Measurable
(fun ℓ : SCM.LatentValues (dgpSCM m g) =>
if (show ℝ from ℓ (iEa (C := C) m g)) ≤
m (show C from ℓ (iUn (C := C) m g)) then true else false)
refine Measurable.ite ?_ measurable_const measurable_const
exact measurableSet_le hEa ((measurable_of_finite m).comp hUn)
exact htreat.prodMk hUn
have hle_σDX :
comap dxFun inferInstance ≤
(inferInstance : MeasurableSpace (SCM.LatentValues (dgpSCM m g))) :=
hdx_meas.comap_le
have hcell_sm : ∀ p, StronglyMeasurable[comap dxFun inferInstance] (cell p) := by
intro p
have hdx_meas' :
@Measurable (SCM.LatentValues (dgpSCM m g)) (Bool × C)
(comap dxFun inferInstance) inferInstance dxFun :=
comap_measurable dxFun
have hs :
@MeasurableSet (SCM.LatentValues (dgpSCM m g))
(comap dxFun inferInstance)
{ℓ : SCM.LatentValues (dgpSCM m g) | dxFun ℓ = p} :=
(MeasurableSet.singleton p).preimage hdx_meas'
letI : MeasurableSpace (SCM.LatentValues (dgpSCM m g)) :=
comap dxFun inferInstance
exact (Measurable.ite hs measurable_const measurable_const).stronglyMeasurable
have heth_meas : ∀ p, Measurable (eth p) := by
intro p
change @Measurable (SCM.LatentValues (dgpSCM m g)) ℝ
(inferInstance : MeasurableSpace (SCM.LatentValues (dgpSCM m g))) inferInstance
(eth p)
dsimp [eth, eFun]
exact Measurable.ite
(measurableSet_le
(show Measurable (fun ℓ : SCM.LatentValues (dgpSCM m g) =>
(show ℝ from ℓ (iEy (C := C) m g))) from
measurable_pi_apply (iEy (C := C) m g))
measurable_const)
measurable_const measurable_const
have heth_int : ∀ p, Integrable (eth p) (dgpPO m g).μ := by
intro p
exact integrable_of_measurable_zero_one (μ := (dgpPO m g).μ) (heth_meas p) fun ℓ => by
dsimp [eth]
split_ifs <;> simp
have hpiece_int : ∀ p, Integrable (piece p) (dgpPO m g).μ := by
intro p
refine integrable_of_measurable_zero_one (μ := (dgpPO m g).μ) ?_ ?_
· change Measurable (piece p)
exact ((hcell_sm p).mono hle_σDX).measurable.mul (heth_meas p)
· intro ℓ
dsimp [piece, cell, eth]
split_ifs <;> simp
have hpiece_pull : ∀ p,
(dgpPO m g).μ[piece p | comap dxFun inferInstance]
=ᵐ[(dgpPO m g).μ] cell p * (fun _ => g p.1 p.2) := by
intro p
have hpull :
(dgpPO m g).μ[piece p | comap dxFun inferInstance]
=ᵐ[(dgpPO m g).μ]
cell p * (dgpPO m g).μ[eth p | comap dxFun inferInstance] := by
have hmul : piece p = cell p * eth p := rfl
rw [hmul]
exact MeasureTheory.condExp_mul_of_stronglyMeasurable_left
(μ := (dgpPO m g).μ) (m := comap dxFun inferInstance)
(hcell_sm p) (hpiece_int p) (heth_int p)
refine hpull.trans ?_
have hconst :
(dgpPO m g).μ[eth p | comap dxFun inferInstance]
=ᵐ[(dgpPO m g).μ] fun _ => g p.1 p.2 := by
exact dgp_condExp_ey_threshold_const (m := m) (g := g) p.1 p.2 (hv.g_mem p.1 p.2)
filter_upwards [hconst] with ℓ hℓ
change cell p ℓ *
(dgpPO m g).μ[eth p | comap dxFun inferInstance] ℓ =
cell p ℓ * g p.1 p.2
exact congrArg (fun y => cell p ℓ * y) hℓ
have hsource :
(fun ℓ : SCM.LatentValues (dgpSCM m g) =>
outFun (C := C) g (dxFun ℓ).1 (dxFun ℓ).2 (eFun ℓ))
=
(∑ p : Bool × C, piece p) := by
funext ℓ
simp only [Finset.sum_apply]
rw [Finset.sum_eq_single (dxFun ℓ)]
· dsimp [piece, cell, eth, outFun]
simp
· intro p _ hp
have hp' : dxFun ℓ ≠ p := fun h => hp h.symm
dsimp [piece, cell]
simp [hp']
· intro hnot
exact (hnot (Finset.mem_univ (dxFun ℓ))).elim
have htarget :
(fun ℓ : SCM.LatentValues (dgpSCM m g) => g (dxFun ℓ).1 (dxFun ℓ).2) =
(∑ p : Bool × C, cell p * fun _ : SCM.LatentValues (dgpSCM m g) => g p.1 p.2) := by
funext ℓ
simp only [Finset.sum_apply, Pi.mul_apply]
rw [Finset.sum_eq_single (dxFun ℓ)]
· dsimp [cell]
simp
· intro p _ hp
have hp' : dxFun ℓ ≠ p := fun h => hp h.symm
dsimp [cell]
simp [hp']
· intro hnot
exact (hnot (Finset.mem_univ (dxFun ℓ))).elim
have hsum :
(dgpPO m g).μ[(∑ p : Bool × C, piece p) | comap dxFun inferInstance]
=ᵐ[(dgpPO m g).μ]
(∑ p : Bool × C, (dgpPO m g).μ[piece p | comap dxFun inferInstance]) := by
simpa using
(MeasureTheory.condExp_finset_sum
(μ := (dgpPO m g).μ) (s := (Finset.univ : Finset (Bool × C)))
(f := piece) (by intro p _; exact hpiece_int p)
(comap dxFun inferInstance))
refine (MeasureTheory.condExp_congr_ae (μ := (dgpPO m g).μ)
(m := comap dxFun inferInstance)
(Filter.EventuallyEq.of_eq hsource)).trans ?_
refine hsum.trans ?_
refine (eventuallyEq_sum fun p _ => hpiece_pull p).trans ?_
exact Filter.EventuallyEq.of_eq htarget.symm
1 supporting declaration (lemmas, instances)
-
dgp_condExp_ea_threshold_varlemma — For a finite covariate space, propensity function, and outcome regression, if they define a valid data-generating process, then the conditional expectation of the treatment-noise threshold indicator given the latent covariate equals the propensity evaluated at that covariate.hypothesesProof (Lean source)
lemma dgp_condExp_ea_threshold_var (hv : ValidDGP m g) : (dgpPO m g).μ[fun ℓ : SCM.LatentValues (dgpSCM m g) => if (show ℝ from ℓ (iEa (C := C) m g)) ≤ m (show C from ℓ (iUn (C := C) m g)) then (1 : ℝ) else 0 | comap (fun ℓ : SCM.LatentValues (dgpSCM m g) => ℓ (iUn (C := C) m g)) inferInstance] =ᵐ[(dgpPO m g).μ] fun ℓ => m (show C from ℓ (iUn (C := C) m g)) := by classical let uFun : SCM.LatentValues (dgpSCM m g) → C := fun ℓ => ℓ (iUn (C := C) m g) let eFun : SCM.LatentValues (dgpSCM m g) → ℝ := fun ℓ => ℓ (iEa (C := C) m g) let cell : C → SCM.LatentValues (dgpSCM m g) → ℝ := fun x ℓ => if uFun ℓ = x then (1 : ℝ) else 0 let eth : C → SCM.LatentValues (dgpSCM m g) → ℝ := fun x ℓ => if eFun ℓ ≤ m x then (1 : ℝ) else 0 let piece : C → SCM.LatentValues (dgpSCM m g) → ℝ := fun x ℓ => cell x ℓ * eth x ℓ have hle_σUn : comap uFun inferInstance ≤ (inferInstance : MeasurableSpace (SCM.LatentValues (dgpSCM m g))) := by dsimp [uFun] exact (measurable_pi_apply (iUn (C := C) m g)).comap_le have hcell_sm : ∀ x, StronglyMeasurable[comap uFun inferInstance] (cell x) := by intro x have hu_meas : @Measurable (SCM.LatentValues (dgpSCM m g)) C (comap uFun inferInstance) inferInstance uFun := comap_measurable uFun have hs : @MeasurableSet (SCM.LatentValues (dgpSCM m g)) (comap uFun inferInstance) {ℓ : SCM.LatentValues (dgpSCM m g) | uFun ℓ = x} := (MeasurableSet.singleton x).preimage hu_meas letI : MeasurableSpace (SCM.LatentValues (dgpSCM m g)) := comap uFun inferInstance exact (Measurable.ite hs measurable_const measurable_const).stronglyMeasurable have heth_meas : ∀ x, Measurable (eth x) := by intro x change @Measurable (SCM.LatentValues (dgpSCM m g)) ℝ (inferInstance : MeasurableSpace (SCM.LatentValues (dgpSCM m g))) inferInstance (eth x) dsimp [eth, eFun] exact Measurable.ite (measurableSet_le (show Measurable (fun ℓ : SCM.LatentValues (dgpSCM m g) => (show ℝ from ℓ (iEa (C := C) m g))) from measurable_pi_apply (iEa (C := C) m g)) measurable_const) measurable_const measurable_const have heth_int : ∀ x, Integrable (eth x) (dgpPO m g).μ := by intro x exact integrable_of_measurable_zero_one (μ := (dgpPO m g).μ) (heth_meas x) fun ℓ => by dsimp [eth] split_ifs <;> simp have hpiece_int : ∀ x, Integrable (piece x) (dgpPO m g).μ := by intro x refine integrable_of_measurable_zero_one (μ := (dgpPO m g).μ) ?_ ?_ · change Measurable (piece x) exact ((hcell_sm x).mono hle_σUn).measurable.mul (heth_meas x) · intro ℓ dsimp [piece, cell, eth] split_ifs <;> simp have hpiece_pull : ∀ x, (dgpPO m g).μ[piece x | comap uFun inferInstance] =ᵐ[(dgpPO m g).μ] cell x * (fun _ => m x) := by intro x have hpull : (dgpPO m g).μ[piece x | comap uFun inferInstance] =ᵐ[(dgpPO m g).μ] cell x * (dgpPO m g).μ[eth x | comap uFun inferInstance] := by have hmul : piece x = cell x * eth x := rfl rw [hmul] exact MeasureTheory.condExp_mul_of_stronglyMeasurable_left (μ := (dgpPO m g).μ) (m := comap uFun inferInstance) (hcell_sm x) (hpiece_int x) (heth_int x) refine hpull.trans ?_ have hconst : (dgpPO m g).μ[eth x | comap uFun inferInstance] =ᵐ[(dgpPO m g).μ] fun _ => m x := by exact dgp_condExp_ea_threshold_const (m := m) (g := g) x (hv.m_mem x) filter_upwards [hconst] with ℓ hℓ change cell x ℓ * (dgpPO m g).μ[eth x | comap uFun inferInstance] ℓ = cell x ℓ * m x exact congrArg (fun y => cell x ℓ * y) hℓ have hsource : (fun ℓ : SCM.LatentValues (dgpSCM m g) => if eFun ℓ ≤ m (uFun ℓ) then (1 : ℝ) else 0) = (∑ x : C, piece x) := by funext ℓ simp only [Finset.sum_apply] rw [Finset.sum_eq_single (uFun ℓ)] · dsimp [piece, cell, eth] simp · intro x _ hx have hx' : uFun ℓ ≠ x := fun h => hx h.symm dsimp [piece, cell] simp [hx'] · intro hnot exact (hnot (Finset.mem_univ (uFun ℓ))).elim have htarget : (fun ℓ : SCM.LatentValues (dgpSCM m g) => m (uFun ℓ)) = (∑ x : C, cell x * fun _ : SCM.LatentValues (dgpSCM m g) => m x) := by funext ℓ simp only [Finset.sum_apply, Pi.mul_apply] rw [Finset.sum_eq_single (uFun ℓ)] · dsimp [cell] simp · intro x _ hx have hx' : uFun ℓ ≠ x := fun h => hx h.symm dsimp [cell] simp [hx'] · intro hnot exact (hnot (Finset.mem_univ (uFun ℓ))).elim have hsum : (dgpPO m g).μ[(∑ x : C, piece x) | comap uFun inferInstance] =ᵐ[(dgpPO m g).μ] (∑ x : C, (dgpPO m g).μ[piece x | comap uFun inferInstance]) := by simpa using (MeasureTheory.condExp_finset_sum (μ := (dgpPO m g).μ) (s := (Finset.univ : Finset C)) (f := piece) (by intro x _; exact hpiece_int x) (comap uFun inferInstance)) refine (MeasureTheory.condExp_congr_ae (μ := (dgpPO m g).μ) (m := comap uFun inferInstance) (Filter.EventuallyEq.of_eq hsource)).trans ?_ refine hsum.trans ?_ refine (eventuallyEq_sum fun x _ => hpiece_pull x).trans ?_ exact Filter.EventuallyEq.of_eq htarget.symm
Bridge_Part3 2 core · 8 supporting This third part completes the interface between the causal layer (the POBackdoorSystem built in Construction.lean) and the observed-data contrast ate g on which the minimax proof machinery computes. ★ causalATE_eq_ate
Causal Grounding of the Minimax ATE Model: Identification
This third part completes the interface between the causal layer (the
POBackdoorSystem built in Construction.lean) and the observed-data contrast ate g on which
the minimax proof machinery computes.
The headline theorem is causalATE_eq_ate:
causalATE m g = ate g (under strict overlap 0 < m x < 1)
where causalATE m g := (dgpBackdoor m g).ATE = ∫ (Y(1) − Y(0)) dμ is the
potential-outcome ATE of the constructed backdoor system. With this in hand the
causal-centered lower bounds in Causal/Minimax.lean are bounds on the causal
estimand, identified by backdoor adjustment, not merely on a regression contrast.
The final proof routes through the reusable BackdoorEstimationSystem.θ₀_eq_ATE
(Estimation/ATE/Setup.lean): instantiate the estimation system with value-space
regression μ_val := g and propensity e_val := m, so that
θ₀ = ∫ (g 1 − g 0) dP_X and θ₀ = S.ATE; then P_X = Uniform(C) collapses
θ₀ to the average (1/card C) Σ_x (g 1 x − g 0 x) = ate g.
This part proves dgp_unconfoundedness and dgp_adjustedCE_eq_g, the genuine
causal-layer obligations: the d-separation lift and the outcome-regression
conditional-mean computation of the constructed SCM law. It also proves
dgp_propScore_eq_m, dgp_overlap, dgp_assumptions, and dgp_P_X_eq_covLaw, then uses
dgpBES to assemble the backdoor-estimation-system interface needed for the final bridge theorem.
def dgpBES reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
For a finite, nonempty covariate space equipped with a measurable structure whose singletons are measurable and with a standard Borel structure, a propensity function, an outcome-regression function, evidence that they form a valid data-generating process, and strict overlap of the propensity at every covariate value, the backdoor estimation system is the constructed potential-outcome system equipped with those supplied propensity and outcome-regression functions.
Definition (Lean source)
parameters
def
given by
clause 1
toPOBackdoorSystem := dgpBackdoor m g
clause 2
μ_val := g
clause 3
μ_meas := fun _ => measurable_of_finite _
clause 4
e_val := m
clause 5
e_meas := measurable_of_finite _
clause 6
e_pos := fun x => (hso x).1
clause 7
e_lt_one := fun x => (hso x).2
clause 8
μ_reg_compat := fun d => (dgp_adjustedCE_eq_g hv hso d).symm
clause 9
e_compat := dgp_propScore_eq_m hv
theorem causalATE_eq_ate reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
Causal identification bridge. Suppose the data-generating process (m, g) is valid and satisfies strict overlap: the propensity m lies strictly between 0 and 1 at every covariate value. Then the causal average treatment effect E[Y(1) − Y(0)] of the backdoor potential-outcome system built from (m, g) equals the finite observed-data contrast ate g = (1/|C|)·Σₓ(g(1,x) − g(0,x)).
Formal statement
Proof (Lean source)
theorem causalATE_eq_ate (hv : ValidDGP m g) (hso : ∀ x, m x ∈ Ioo (0 : ℝ) 1) :
causalATE m g = ate g := by
have hθ : (dgpBES (m := m) (g := g) hv hso).θ₀ =
(dgpBES (m := m) (g := g) hv hso).toPOBackdoorSystem.ATE :=
(dgpBES (m := m) (g := g) hv hso).θ₀_eq_ATE
(dgp_assumptions (m := m) (g := g) hv hso)
-- `causalATE = S.ATE = θ₀ = ∫ (g 1 − g 0) dP_X`, and `P_X = Uniform(C)` turns
-- the integral into the average `(1/card C) Σ_x (g 1 x − g 0 x) = ate g`.
rw [causalATE]
change (dgpBES (m := m) (g := g) hv hso).toPOBackdoorSystem.ATE = ate g
rw [← hθ]
unfold BackdoorEstimationSystem.θ₀ BackdoorEstimationSystem.P_X dgpBES
rw [dgp_P_X_eq_covLaw (m := m) (g := g)]
unfold covLaw ate
rw [PMF.integral_eq_sum]
simp [PMF.uniformOfFintype_apply]
calc
∑ x, (Fintype.card C : ℝ)⁻¹ * (g true x - g false x)
= ∑ x, ((Fintype.card C : ℝ)⁻¹ * g true x -
(Fintype.card C : ℝ)⁻¹ * g false x) := by
apply Finset.sum_congr rfl
intro x _
ring
_ = ∑ x, (Fintype.card C : ℝ)⁻¹ * g true x -
∑ x, (Fintype.card C : ℝ)⁻¹ * g false x := by
rw [Finset.sum_sub_distrib]
_ = (Fintype.card C : ℝ)⁻¹ * ∑ x, g true x -
(Fintype.card C : ℝ)⁻¹ * ∑ x, g false x := by
rw [← Finset.mul_sum, ← Finset.mul_sum]
_ = (Fintype.card C : ℝ)⁻¹ * (∑ x, g true x - ∑ x, g false x) := by
ring
8 supporting declarations (lemmas, instances)
-
dgp_unconfoundednesstheorem — Unconfoundedness A ⟂ (Y(1), Y(0)) | X. The treatment noise Ea and outcome noise Ey are independent latent roots given the covariate, so the realized treatment is conditionally independent of the potential-outcome bundle given X. Discharged via POSystem.ofSCM_condIndepCF_of_dSep (d-separation in the split graph + value correspondences).hypothesesconclusion(dgpPO m g).CondIndepCF (RegimedVar.ofFactual (dgpBackdoor m g).dVar) (dgpBackdoor m g).cfBundle (RegimedVar.ofFactual (dgpBackdoor m g).xVar) (dgpPO m g).μProof (Lean source)
theorem dgp_unconfoundedness : (dgpPO m g).CondIndepCF (RegimedVar.ofFactual (dgpBackdoor m g).dVar) (dgpBackdoor m g).cfBundle (RegimedVar.ofFactual (dgpBackdoor m g).xVar) (dgpPO m g).μ := by classical let X : Finset (SWIGNode WNode) := {SWIGNode.random WNode.A} let Y : Finset (SWIGNode WNode) := {SWIGNode.random WNode.Ey, SWIGNode.random WNode.Un} let Z : Finset (SWIGNode WNode) := {SWIGNode.random WNode.Xc} let cVar : POVar (dgpPO m g) (ValuesOn Z (swigΩ (WΩ C))) := ⟨XIdx m g, by exact dgpXSingletonEquiv (C := C)⟩ let c : RegimedVar (dgpPO m g) (ValuesOn Z (swigΩ (WΩ C))) := RegimedVar.ofFactual cVar let aMap : ValuesOn X (swigΩ (WΩ C)) → Bool := fun vals => vals ⟨SWIGNode.random WNode.A, by simp [X]⟩ let BMap : ValuesOn Y (swigΩ (WΩ C)) → (∀ i : Fin (dgpBackdoor m g).cfBundle.n, (dgpBackdoor m g).cfBundle.type i) := fun vals i => by dsimp [POBackdoorSystem.cfBundle, POCFBundle.cons, POCFBundle.nil] at i ⊢ exact Fin.cases (outFun (C := C) g true (vals ⟨SWIGNode.random WNode.Un, by simp [Y]⟩) (vals ⟨SWIGNode.random WNode.Ey, by simp [Y]⟩)) (fun j => Fin.cases (outFun (C := C) g false (vals ⟨SWIGNode.random WNode.Un, by simp [Y]⟩) (vals ⟨SWIGNode.random WNode.Ey, by simp [Y]⟩)) (fun k => k.elim0) j) i haveI : StandardBorelSpace (POSystem.ofSCM (dgpSCM m g) (dgpFixed m g)).Ω := by change StandardBorelSpace (dgpPO m g).Ω exact dgpPO_borel haveI : StandardBorelSpace (∀ i : Fin (dgpBackdoor m g).cfBundle.n, (dgpBackdoor m g).cfBundle.type i) := by haveI : ∀ i : Fin (dgpBackdoor m g).cfBundle.n, StandardBorelSpace ((dgpBackdoor m g).cfBundle.type i) := by intro i dsimp [POBackdoorSystem.cfBundle, POCFBundle.cons, POCFBundle.nil] at i ⊢ exact Fin.cases (inferInstance : StandardBorelSpace ℝ) (fun j => Fin.cases (inferInstance : StandardBorelSpace ℝ) (fun k => k.elim0) j) i exact StandardBorelSpace.pi_countable haveI : Nonempty (∀ i : Fin (dgpBackdoor m g).cfBundle.n, (dgpBackdoor m g).cfBundle.type i) := by haveI : ∀ i : Fin (dgpBackdoor m g).cfBundle.n, Nonempty ((dgpBackdoor m g).cfBundle.type i) := by intro i dsimp [POBackdoorSystem.cfBundle, POCFBundle.cons, POCFBundle.nil] at i ⊢ exact Fin.cases (inferInstance : Nonempty ℝ) (fun j => Fin.cases (inferInstance : Nonempty ℝ) (fun k => k.elim0) j) i infer_instance have hci : (dgpPO m g).CondIndepCF (RegimedVar.ofFactual (dgpBackdoor m g).dVar) (dgpBackdoor m g).cfBundle c (dgpPO m g).μ := by refine POSystem.ofSCM_condIndepCF_of_dSep (M := dgpSCM m g) (s := dgpFixed m g) (X := X) (Y := Y) (Z := Z) ?hX ?hY ?hZ ?hdSep (RegimedVar.ofFactual (dgpBackdoor m g).dVar) (dgpBackdoor m g).cfBundle c aMap BMap ?haMap ?hBMap ?ha_value ?hB_value ?hc_value · intro v hv simp [X] at hv subst v simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph] · intro v hv simp [Y] at hv rcases hv with rfl | rfl <;> simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph] · intro v hv simp [Z] at hv subst v simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph] · change (initialSWIG wDAG).dSep ({SWIGNode.random WNode.A} : Finset (SWIGNode WNode)) ({SWIGNode.random WNode.Ey, SWIGNode.random WNode.Un} : Finset (SWIGNode WNode)) ({SWIGNode.random WNode.Xc} : Finset (SWIGNode WNode)) decide · dsimp [aMap] exact measurable_pi_apply (⟨SWIGNode.random WNode.A, by simp [X]⟩ : {w // w ∈ X}) · refine measurable_pi_lambda _ ?_ intro i fin_cases i · dsimp [BMap] unfold outFun exact Measurable.ite (measurableSet_le (measurable_pi_apply (⟨SWIGNode.random WNode.Ey, by simp [Y]⟩ : {w // w ∈ Y})) ((measurable_of_finite (g true)).comp (measurable_pi_apply (⟨SWIGNode.random WNode.Un, by simp [Y]⟩ : {w // w ∈ Y})))) measurable_const measurable_const · dsimp [BMap] unfold outFun exact Measurable.ite (measurableSet_le (measurable_pi_apply (⟨SWIGNode.random WNode.Ey, by simp [Y]⟩ : {w // w ∈ Y})) ((measurable_of_finite (g false)).comp (measurable_pi_apply (⟨SWIGNode.random WNode.Un, by simp [Y]⟩ : {w // w ∈ Y})))) measurable_const measurable_const · funext ℓ change (dgpBackdoor m g).factualD ℓ = (dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.A, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩ rw [dgp_factualD_eq_treatFun (m := m) (g := g)] symm rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.A, by simp [dgpSCM, wSWIGGraph]⟩] change treatFun (m ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩)) (ℓ (iEa (C := C) m g)) = treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g)) rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [dgpSCM, wSWIGGraph]⟩] unfold dgpSCM parentVal iUn rfl · funext ℓ i dsimp [POCFBundle.jointValue, POBackdoorSystem.cfBundle, POCFBundle.cons, POCFBundle.nil, BMap] fin_cases i · change (dgpBackdoor m g).YofD true ℓ = outFun (C := C) g true ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Un, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Ey, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) rw [dgp_YofD_eq_outFun (m := m) (g := g) true] rfl · change (dgpBackdoor m g).YofD false ℓ = outFun (C := C) g false ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Un, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Ey, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) rw [dgp_YofD_eq_outFun (m := m) (g := g) false] rfl · funext ℓ z rcases z with ⟨v, hv⟩ simp [Z] at hv subst v change (dgpBackdoor m g).factualX ℓ = (dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩ rw [dgp_factualX_eq_latentUn (m := m) (g := g)] change ℓ (iUn (C := C) m g) = (dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩ rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [dgpSCM, wSWIGGraph]⟩] unfold dgpSCM parentVal iUn rfl have hc_eq : c.value = singletonValues (α := swigΩ (WΩ C)) (v := SWIGNode.random WNode.Xc) ∘ (RegimedVar.ofFactual (dgpBackdoor m g).xVar).value := by funext ℓ z rcases z with ⟨v, hv⟩ simp [Z] at hv subst v rfl refine POSystem.condIndepCF_congr_cond ?_ hci rw [hc_eq] apply le_antisymm · have hx_meas : @Measurable (dgpPO m g).Ω C (comap (RegimedVar.ofFactual (dgpBackdoor m g).xVar).value inferInstance) inferInstance (RegimedVar.ofFactual (dgpBackdoor m g).xVar).value := comap_measurable _ exact ((measurable_singletonValues (α := swigΩ (WΩ C)) (v := SWIGNode.random WNode.Xc)).comp hx_meas).comap_le · have hsingleton_meas : @Measurable (dgpPO m g).Ω (ValuesOn ({SWIGNode.random WNode.Xc} : Finset (SWIGNode WNode)) (swigΩ (WΩ C))) (comap (singletonValues (α := swigΩ (WΩ C)) (v := SWIGNode.random WNode.Xc) ∘ (RegimedVar.ofFactual (dgpBackdoor m g).xVar).value) inferInstance) inferInstance (singletonValues (α := swigΩ (WΩ C)) (v := SWIGNode.random WNode.Xc) ∘ (RegimedVar.ofFactual (dgpBackdoor m g).xVar).value) := comap_measurable _ have hx_meas : @Measurable (dgpPO m g).Ω C (comap (singletonValues (α := swigΩ (WΩ C)) (v := SWIGNode.random WNode.Xc) ∘ (RegimedVar.ofFactual (dgpBackdoor m g).xVar).value) inferInstance) inferInstance (RegimedVar.ofFactual (dgpBackdoor m g).xVar).value := by exact (measurable_singletonValue (α := swigΩ (WΩ C)) (v := SWIGNode.random WNode.Xc)).comp hsingleton_meas exact hx_meas.comap_le -
dgp_propScore_eq_mtheorem — The constructed treatment propensity equals the supplied propensity function given the covariate.hypothesesconclusion=ᵐ[(dgpPO m g).μ] (fun ω => m ((dgpBackdoor m g).factualX ω))Proof (Lean source)
theorem dgp_propScore_eq_m (hv : ValidDGP m g) : (dgpBackdoor m g).propScore true =ᵐ[(dgpPO m g).μ] (fun ω => m ((dgpBackdoor m g).factualX ω)) := by unfold POBackdoorSystem.propScore rw [POBackdoorSystem.sigmaX, dgp_factualX_eq_latentUn (m := m) (g := g), dgp_dIndicator_true_eq_threshold (m := m) (g := g)] exact dgp_condExp_ea_threshold_var (m := m) (g := g) hv -
dgp_adjustedCE_eq_gtheorem — The constructed adjusted conditional mean equals the supplied outcome regression in each treatment arm.hypothesesconclusion(dgpBackdoor m g).adjustedCE d=ᵐ[(dgpPO m g).μ] (fun ω => g d ((dgpBackdoor m g).factualX ω))Proof (Lean source)
theorem dgp_adjustedCE_eq_g (hv : ValidDGP m g) (hso : ∀ x, m x ∈ Ioo (0 : ℝ) 1) (d : Bool) : (dgpBackdoor m g).adjustedCE d =ᵐ[(dgpPO m g).μ] (fun ω => g d ((dgpBackdoor m g).factualX ω)) := by let S : POBackdoorSystem (dgpPO m g) C := dgpBackdoor m g have hY : Integrable S.factualY (dgpPO m g).μ := by refine MeasureTheory.Integrable.of_bound S.measurable_factualY.aestronglyMeasurable 1 (Filter.Eventually.of_forall ?_) intro ℓ rw [show S.factualY = (fun ℓ : SCM.LatentValues (dgpSCM m g) => outFun (C := C) g (treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g))) from dgp_factualY_eq_outFun (m := m) (g := g)] by_cases h : (show ℝ from ℓ (iEy (C := C) m g)) ≤ g (treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) (ℓ (iUn (C := C) m g)) · simp [outFun, h] · simp [outFun, h] have hov : ∀ᵐ ω ∂(dgpPO m g).μ, 0 < S.propScore true ω ∧ S.propScore true ω < 1 := by filter_upwards [dgp_propScore_eq_m (m := m) (g := g) hv] with ω hω rw [hω] exact ⟨(hso _).1, (hso _).2⟩ have h_ne : ∀ᵐ ω ∂(dgpPO m g).μ, S.propScore d ω ≠ 0 := S.propScore_ne_of_overlap hov d have houtcome : S.outcomeReg =ᵐ[(dgpPO m g).μ] fun ω => g (S.factualD ω) (S.factualX ω) := by unfold POBackdoorSystem.outcomeReg POBackdoorSystem.sigmaDX POBackdoorSystem.factualDX rw [show S.factualY = (fun ℓ : SCM.LatentValues (dgpSCM m g) => outFun (C := C) g (treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) (ℓ (iUn (C := C) m g)) (ℓ (iEy (C := C) m g))) from dgp_factualY_eq_outFun (m := m) (g := g)] rw [show S.factualD = (fun ℓ : SCM.LatentValues (dgpSCM m g) => treatFun (m (ℓ (iUn (C := C) m g))) (ℓ (iEa (C := C) m g))) from dgp_factualD_eq_treatFun (m := m) (g := g)] rw [show S.factualX = (fun ℓ : SCM.LatentValues (dgpSCM m g) => ℓ (iUn (C := C) m g)) from dgp_factualX_eq_latentUn (m := m) (g := g)] exact dgp_condExp_outcome_threshold_var (m := m) (g := g) hv have hratio_def : S.adjustedCE d = S.xVar.condExpRatio (fun ω => S.factualY ω * S.dVar.indicator d ω) (S.dVar.indicator d) (dgpPO m g).μ := by funext ω unfold POBackdoorSystem.adjustedCE POBackdoorSystem.propScore POBackdoorSystem.sigmaX POBackdoorSystem.factualX POVar.condExpRatio POVar.condExpGiven rfl rw [hratio_def] refine S.xVar.condExpRatio_eq_of_mul (g := fun ω => S.factualY ω * S.dVar.indicator d ω) (h := S.dVar.indicator d) (target := fun ω => g d (S.factualX ω)) ?_ ?_ · let s : Set (dgpPO m g).Ω := S.dVar.event d let target : (dgpPO m g).Ω → ℝ := fun ω => g d (S.factualX ω) have hsDX : MeasurableSet[S.sigmaDX] s := by change MeasurableSet[comap S.factualDX inferInstance] (S.factualD ⁻¹' {d}) exact ⟨Prod.fst ⁻¹' {d}, measurableSet_singleton d |>.preimage measurable_fst, rfl⟩ have hs : MeasurableSet s := S.dVar.measurableSet_event d (measurableSet_singleton d) have hmul_indicator : (fun ω => S.factualY ω * S.dVar.indicator d ω) = s.indicator S.factualY := by funext ω by_cases hω : ω ∈ s · have hind : S.dVar.indicator d ω = 1 := S.dVar.indicator_apply_eq_one hω rw [hind, mul_one, Set.indicator_of_mem hω] · have hD : S.factualD ω ≠ d := hω have hind : S.dVar.indicator d ω = 0 := S.dVar.indicator_apply_eq_zero hD rw [hind, mul_zero, Set.indicator_of_notMem hω] have htarget_meas : Measurable[S.sigmaX] target := by have hg_d : Measurable (fun x : C => g d x) := measurable_of_finite _ change Measurable[comap S.factualX inferInstance] ((fun x : C => g d x) ∘ S.factualX) exact hg_d.comp (comap_measurable S.factualX) have htarget_sm : StronglyMeasurable[S.sigmaX] target := htarget_meas.stronglyMeasurable have houtcome_target : s.indicator S.outcomeReg =ᵐ[(dgpPO m g).μ] s.indicator target := by filter_upwards [houtcome] with ω hω by_cases hmem : ω ∈ s · have hD : S.factualD ω = d := hmem rw [Set.indicator_of_mem hmem, Set.indicator_of_mem hmem, hω, hD] · rw [Set.indicator_of_notMem hmem, Set.indicator_of_notMem hmem] have htower : (dgpPO m g).μ[s.indicator S.factualY | S.sigmaX] =ᵐ[(dgpPO m g).μ] (dgpPO m g).μ[s.indicator S.outcomeReg | S.sigmaX] := by simpa [s, POBackdoorSystem.outcomeReg] using condExp_setIndicator_condExp_of_le (μ := (dgpPO m g).μ) (m := S.sigmaX) (m' := S.sigmaDX) S.sigmaX_le_sigmaDX S.sigmaDX_le hsDX hY have hleft : (dgpPO m g).μ[fun ω => S.factualY ω * S.dVar.indicator d ω | S.sigmaX] =ᵐ[(dgpPO m g).μ] (dgpPO m g).μ[s.indicator target | S.sigmaX] := (MeasureTheory.condExp_congr_ae (m := S.sigmaX) (μ := (dgpPO m g).μ) (Filter.EventuallyEq.of_eq hmul_indicator)).trans (htower.trans (MeasureTheory.condExp_congr_ae (m := S.sigmaX) (μ := (dgpPO m g).μ) houtcome_target)) have hind_int : Integrable (S.dVar.indicator d) (dgpPO m g).μ := S.dVar.integrable_indicator d (measurableSet_singleton d) have htarget_mul_indicator : target * S.dVar.indicator d = s.indicator target := by funext ω by_cases hω : ω ∈ s · have hind : S.dVar.indicator d ω = 1 := S.dVar.indicator_apply_eq_one hω rw [Pi.mul_apply, hind, mul_one, Set.indicator_of_mem hω] · have hD : S.factualD ω ≠ d := hω have hind : S.dVar.indicator d ω = 0 := S.dVar.indicator_apply_eq_zero hD rw [Pi.mul_apply, hind, mul_zero, Set.indicator_of_notMem hω] have htarget_mul_int : Integrable (target * S.dVar.indicator d) (dgpPO m g).μ := by rw [htarget_mul_indicator] exact (MeasureTheory.Integrable.indicator (MeasureTheory.integrable_condExp (μ := (dgpPO m g).μ) (m := S.sigmaDX) (f := S.factualY)) hs) |>.congr houtcome_target have hpull : (dgpPO m g).μ[target * S.dVar.indicator d | S.sigmaX] =ᵐ[(dgpPO m g).μ] target * (dgpPO m g).μ[S.dVar.indicator d | S.sigmaX] := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (m := S.sigmaX) (μ := (dgpPO m g).μ) htarget_sm htarget_mul_int hind_int change (dgpPO m g).μ[fun ω => S.factualY ω * S.dVar.indicator d ω | S.sigmaX] =ᵐ[(dgpPO m g).μ] (dgpPO m g).μ[S.dVar.indicator d | S.sigmaX] * target refine hleft.trans ?_ refine (MeasureTheory.condExp_congr_ae (m := S.sigmaX) (μ := (dgpPO m g).μ) (Filter.EventuallyEq.of_eq htarget_mul_indicator.symm)).trans ?_ exact hpull.trans (Filter.EventuallyEq.of_eq (by funext ω exact mul_comm _ _)) · have hEq : S.xVar.condExpGiven (S.dVar.indicator d) (dgpPO m g).μ = S.propScore d := by unfold POVar.condExpGiven POBackdoorSystem.propScore POBackdoorSystem.sigmaX POBackdoorSystem.factualX rfl rw [hEq] exact h_ne -
dgp_overlaptheorem — The constructed propensity satisfies overlap whenever the supplied propensity is strictly between zero and one.hypothesesconclusion∀ᵐ ω ∂(dgpPO m g).μ, 0 < (dgpBackdoor m g).propScore true ω ∧ (dgpBackdoor m g).propScore true ω < 1Proof (Lean source)
theorem dgp_overlap (hv : ValidDGP m g) (hso : ∀ x, m x ∈ Ioo (0 : ℝ) 1) : ∀ᵐ ω ∂(dgpPO m g).μ, 0 < (dgpBackdoor m g).propScore true ω ∧ (dgpBackdoor m g).propScore true ω < 1 := by filter_upwards [dgp_propScore_eq_m (m := m) (g := g) hv] with ω hω rw [hω]; exact ⟨(hso _).1, (hso _).2⟩ -
dgp_integrable_Y1theorem — The treated potential outcome is integrable because it is bounded Bernoulli-valued.hypothesesconclusionProof (Lean source)
@[fun_prop] theorem dgp_integrable_Y1 : Integrable ((dgpBackdoor m g).YofD true) (dgpPO m g).μ := by exact dgp_integrable_YofD (m := m) (g := g) true -
dgp_integrable_Y0theorem — The control potential outcome is integrable because it is bounded Bernoulli-valued.hypothesesconclusionProof (Lean source)
@[fun_prop] theorem dgp_integrable_Y0 : Integrable ((dgpBackdoor m g).YofD false) (dgpPO m g).μ := by exact dgp_integrable_YofD (m := m) (g := g) false -
dgp_assumptionstheorem — The constructed finite backdoor system satisfies the standard backdoor assumptions.hypothesesconclusion(dgpBackdoor m g).Assumptions where consistencyProof (Lean source)
theorem dgp_assumptions (hv : ValidDGP m g) (hso : ∀ x, m x ∈ Ioo (0 : ℝ) 1) : (dgpBackdoor m g).Assumptions where consistency := dgp_consistency unconfoundedness := dgp_unconfoundedness overlap := dgp_overlap hv hso integrable_Y1 := dgp_integrable_Y1 integrable_Y0 := dgp_integrable_Y0 -
dgp_P_X_eq_covLawtheorem — The factual covariate marginal of the constructed system is uniform on the finite covariate space.hypothesesconclusionProof (Lean source)
theorem dgp_P_X_eq_covLaw : (dgpPO m g).μ.map (dgpBackdoor m g).factualX = covLaw C := by let iUn : {u // u ∈ (dgpSCM m g).unobserved} := ⟨SWIGNode.random WNode.Un, by simp [dgpSCM, wSWIGGraph]⟩ have hx : (dgpBackdoor m g).factualX = (fun ℓ : SCM.LatentValues (dgpSCM m g) => ℓ iUn) := by funext ℓ simp only [POBackdoorSystem.factualX, POVar.factual, POVar.cf] change (dgpBackdoor m g).xVar.equiv (inducedEval (dgpSCM m g) (dgpFixed m g) Regime.empty ℓ (XIdx m g)) = ℓ iUn rw [inducedEval_empty_eq_evalMap (dgpSCM m g) (dgpFixed m g) ℓ (XIdx m g)] change (XEquiv m g) ((dgpSCM m g).evalMap (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [SCM.randomVars, SWIGGraph.randomVars, dgpSCM, wSWIGGraph]⟩) = ℓ iUn rw [SCM.evalMap_observed_unfold (dgpSCM m g) (dgpFixed m g) ℓ ⟨SWIGNode.random WNode.Xc, by simp [dgpSCM, wSWIGGraph]⟩] unfold XEquiv dgpSCM parentVal rfl rw [hx] change Measure.map (Function.eval iUn) (SCM.latentProduct (dgpSCM m g)) = covLaw C letI : ∀ u : {u // u ∈ (dgpSCM m g).unobserved}, IsProbabilityMeasure ((dgpSCM m g).latentDist u) := (dgpSCM m g).isProbability_latent haveI : ∀ u : {u // u ∈ (dgpSCM m g).unobserved}, SigmaFinite ((dgpSCM m g).latentDist u) := fun _ => inferInstance rw [SCM.latentProduct, MeasureTheory.Measure.pi_map_eval] simp only [measure_univ, Finset.prod_const_one, one_smul] change covLaw C = covLaw C rfl
Minimax 3 core · 11 supporting This file re-centers the VaryingCenterCase1 and VaryingCenterCase2 minimax lower bounds onto the genuine causal estimand causalATE = E[Y(1) - Y(0)] of the concrete backdoor potential outcome system. ★ minimax_lower_bound_var_causal
Causal re-centering of the cell-varying minimax converses
This file re-centers the VaryingCenterCase1 and VaryingCenterCase2 minimax lower
bounds onto the genuine causal estimand causalATE = E[Y(1) - Y(0)] of the
concrete backdoor potential outcome system. The observed-data contrast ate g
remains the internal computational handle: the minimax model and Le Cam machinery
live below the causal layer, so nMiss/minimaxMiss themselves cannot be
re-centered without a circular import. The bridge causalATE_eq_ate identifies
the two targets under validity and strict overlap.
The file defines the causal-centered risk functional minimaxMissCausal, a
causal two-point witness wrapper TwoPointWitnessCausal, and the reusable Le Cam
lemmas twoPointWitnessCausal_lower_bound and twoPointWitnessCausal_quarter.
It then proves the causal-centered cell-varying lower bounds
minimax_lower_bound_var_causal for Case 1 and
minimax_lower_bound_var2_causal for Case 2, adding the strict-overlap
side conditions needed to invoke causalATE_eq_ate on the null and perturbed
witnesses.
def minimaxMissCausal reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE
For a finite nonempty covariate space with measurable singletons, centered propensity and outcome-regression functions, two real radii with no sign restrictions, a sample size, an estimator based on that many observed records, and a real error threshold, the causal-centered minimax miss probability is the supremum over the nuisance class of the probability that the estimator's absolute error from the average potential-outcome treatment effect reaches the threshold.
Definition (Lean source)
structure TwoPointWitnessCausal reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE
Two-point Le Cam witness whose realizability target is minimaxMissCausal.
Definition (Lean source)
parameters
fields
s :
ℝ
c :
ℝ
prob :
∀ j, IsProbabilityMeasure (Q j)
θ :
Bool → ℝ
dominated :
(Q j).real {x | s ≤ |est x - θ j|} ≤ minimaxMissCausal mhat ghat εg εm n est s
theorem minimax_lower_bound_var_causal reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.VarConstr
Causal-centered structure-agnostic minimax lower bound (Case-1-shaped family). For a first cell-varying construction P with K paired cells, a sample size n, and nuisance-error budgets εg and εm, suppose the squared propensity perturbation stays within the budget εm, the squared outcome-regression perturbation stays within the budget εg, the perturbed propensity remains strictly below 1 in every cell, and both budgets are nonnegative. If in addition the aggregate separation budget across cells is at most 1 and the sample size satisfies the stated regularity regime relative to that budget, then for every measurable estimator, the causal-centered miss probability — of missing the true backdoor-identified ATE E[Y(1) − Y(0)] by at least half the displayed separation gap — is at least 1/4 for some data-generating process in the class; the strict perturbed-overlap hypothesis is exactly what lets the observed-data first-family bound be re-centered onto the genuine causal estimand.
Formal statement
hypotheses
K :
ℕ
P :
n :
ℕ
NeZero K
εg εm :
ℝ
hm :
∀ j, (P.m₀ j * (P.β / P.g₁ j)) ^ 2 ≤ εm
hg :
∀ j, P.g₁ j ^ 2 * (P.α + P.β) ^ 2 / (P.g₁ j - P.β) ^ 2 ≤ εg
hmU_strict :
∀ j, P.m₀ j * (1 + P.β / P.g₁ j) < 1
hεg :
0 ≤ εg
hεm :
0 ≤ εm
hΓsum :
∑ j, P.ΓV j / (K : ℝ) ≤ 1
hreg :
(n : ℝ) ^ 2 / 2 * ∑ j, (P.ΓV j / (K : ℝ)) ^ 2 ≤ log 2
hest :
Measurable est
conclusion
1 / 4
≤ minimaxMissCausal P.mhatV P.ghatV εg εm n est ((card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β * (P.α + P.β)) * (∑ j : Fin K, P.g₁ j / (P.g₁ j ^ 2 - P.β ^ 2)) / 2)
Proof (Lean source)
theorem minimax_lower_bound_var_causal (P : VarConstr K) {n : ℕ} [NeZero K]
{εg εm : ℝ}
(hm : ∀ j, (P.m₀ j * (P.β / P.g₁ j)) ^ 2 ≤ εm)
(hg : ∀ j, P.g₁ j ^ 2 * (P.α + P.β) ^ 2 / (P.g₁ j - P.β) ^ 2 ≤ εg)
(hmU_strict : ∀ j, P.m₀ j * (1 + P.β / P.g₁ j) < 1)
(hεg : 0 ≤ εg) (hεm : 0 ≤ εm)
(hΓsum : ∑ j, P.ΓV j / (K : ℝ) ≤ 1)
(hreg : (n : ℝ) ^ 2 / 2 * ∑ j, (P.ΓV j / (K : ℝ)) ^ 2 ≤ log 2)
{est : (Fin n → Obs (Fin K × Bool)) → ℝ} (hest : Measurable est) :
1 / 4 ≤ minimaxMissCausal P.mhatV P.ghatV εg εm n est
((card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β * (P.α + P.β))
* (∑ j : Fin K, P.g₁ j / (P.g₁ j ^ 2 - P.β ^ 2)) / 2) := by
set gap := (card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β * (P.α + P.β))
* ∑ j : Fin K, P.g₁ j / (P.g₁ j ^ 2 - P.β ^ 2) with hgap
have hgap0 : 0 ≤ gap := by
have h := P.ate_gap_nonneg (fun _ => true)
rwa [P.ate_gapV (fun _ => true)] at h
set s := gap / 2 with hs
set θ0 := ate (P.ghatV (K := K)) with hθ0
let W : TwoPointWitnessCausal (Fin K × Bool) n P.mhatV P.ghatV εg εm :=
{ s := s
c := 1 / 2
Q := fun j => cond j (QtrueV P n) (QfalseV P n)
prob := by
intro j
cases j
· exact QfalseV_isProb P n
· exact QtrueV_isProb P n
θ := fun j => cond j (θ0 + gap) θ0
sep := by
change 2 * s ≤ |(θ0 + gap) - θ0|
rw [add_sub_cancel_left, abs_of_nonneg hgap0, hs]
linarith
tvBound := by simpa using P.tvDist_QfalseV_QtrueV_le_half (n := n) hΓsum hreg
dominated := by
intro est' j
cases j
· change (QfalseV P n).real {x | s ≤ |est' x - θ0|}
≤ minimaxMissCausal P.mhatV P.ghatV εg εm n est' s
have hb := P.realV_le_minimaxMissCausal (n := n)
(inClass_nullV P hεg hεm) est' s
have hbridge :
causalATE (P.mhatV (K := K)) P.ghatV = ate P.ghatV :=
causalATE_eq_ate (P.validDGP_hatV (K := K)) (P.mhatV_strictOverlap (K := K))
rw [hbridge, ← hθ0] at hb
exact hb
· change (QtrueV P n).real {x | s ≤ |est' x - (θ0 + gap)|}
≤ minimaxMissCausal P.mhatV P.ghatV εg εm n est' s
haveI : ∀ lam : Fin K → Bool, IsProbabilityMeasure (QpertV P n lam) :=
fun lam => QpertV_isProb P n lam
unfold QtrueV
refine mixtureReal_le (signWeight K) (signWeight_sum K)
(fun lam => QpertV P n lam) _ _ ?_
intro lam
have hb := P.realV_le_minimaxMissCausal (n := n) (P.inClassV hm hg hεg lam) est' s
have hkey : ate (P.gPertV lam) = θ0 + gap := by
have := P.ate_gapV lam
rw [hθ0, hgap]
linarith [this]
have hbridge :
causalATE (P.mPertV lam) (P.gPertV lam) = ate (P.gPertV lam) :=
causalATE_eq_ate (P.validDGP_pertV lam)
(P.mPertV_strictOverlap hmU_strict lam)
rw [hbridge, hkey] at hb
exact hb }
exact twoPointWitnessCausal_quarter W (le_refl _) hest
11 supporting declarations (lemmas, instances)
-
bddAbove_nMissCausal_rangetheorem — Each in-class causal-centered miss probability is bounded above by 1.hypothesesconclusionBddAbove (Set.range fun p : InClassDGP mhat ghat εg εm => (productLaw p.2.valid n).real {x | s ≤ |est x - causalATE (C := C) p.1.1 p.1.2|})Proof (Lean source)
theorem bddAbove_nMissCausal_range (mhat : C → ℝ) (ghat : Bool → C → ℝ) (εg εm : ℝ) (n : ℕ) (est : (Fin n → Obs C) → ℝ) (s : ℝ) : BddAbove (Set.range fun p : InClassDGP mhat ghat εg εm => (productLaw p.2.valid n).real {x | s ≤ |est x - causalATE (C := C) p.1.1 p.1.2|}) := by refine ⟨1, ?_⟩ rintro y ⟨p, rfl⟩ calc (productLaw p.2.valid n).real {x | s ≤ |est x - causalATE (C := C) p.1.1 p.1.2|} ≤ (productLaw p.2.valid n).real univ := measureReal_mono (Set.subset_univ _) (measure_ne_top _ _) _ = 1 := by rw [probReal_univ] -
nMissCausal_le_minimaxMissCausaltheorem — A specific in-class DGP's causal-centered miss probability is dominated by the causal-centered minimax miss.hypothesesεg εm :ℝs :ℝp :conclusionProof (Lean source)
theorem nMissCausal_le_minimaxMissCausal {mhat : C → ℝ} {ghat : Bool → C → ℝ} {εg εm : ℝ} {n : ℕ} {est : (Fin n → Obs C) → ℝ} {s : ℝ} (p : InClassDGP mhat ghat εg εm) : (productLaw p.2.valid n).real {x | s ≤ |est x - causalATE (C := C) p.1.1 p.1.2|} ≤ minimaxMissCausal mhat ghat εg εm n est s := le_ciSup (bddAbove_nMissCausal_range mhat ghat εg εm n est s) p -
twoPointWitnessCausal_lower_boundtheorem — Le Cam lower bound for a causal-centered two-point witness.hypothesesC :sharedTypen :sharedℕmhat :sharedC → ℝεg :sharedℝεm :sharedℝW :TwoPointWitnessCausal C n mhat ghat εg εmhest :Measurable estconclusion(1 - W.c) / 2 ≤ minimaxMissCausal mhat ghat εg εm n est W.sProof (Lean source)
theorem twoPointWitnessCausal_lower_bound (W : TwoPointWitnessCausal C n mhat ghat εg εm) {est : (Fin n → Obs C) → ℝ} (hest : Measurable est) : (1 - W.c) / 2 ≤ minimaxMissCausal mhat ghat εg εm n est W.s := by haveI := W.prob false haveI := W.prob true have hsep : 2 * W.s ≤ |W.θ false - W.θ true| := by rw [abs_sub_comm] exact W.sep have h := two_point_lower_bound_of_tvDist_le (P₀ := W.Q false) (P₁ := W.Q true) hest hsep W.tvBound refine h.trans ?_ rw [max_le_iff] exact ⟨W.dominated est false, W.dominated est true⟩ -
twoPointWitnessCausal_quartertheorem — A causal-centered witness with c ≤ 1/2 yields a 1/4 minimax miss lower bound.hypothesesC :sharedTypen :sharedℕmhat :sharedC → ℝεg :sharedℝεm :sharedℝW :TwoPointWitnessCausal C n mhat ghat εg εmhc :W.c ≤ 1 / 2hest :Measurable estconclusion1 / 4 ≤ minimaxMissCausal mhat ghat εg εm n est W.sProof (Lean source)
theorem twoPointWitnessCausal_quarter (W : TwoPointWitnessCausal C n mhat ghat εg εm) (hc : W.c ≤ 1 / 2) {est : (Fin n → Obs C) → ℝ} (hest : Measurable est) : 1 / 4 ≤ minimaxMissCausal mhat ghat εg εm n est W.s := by refine le_trans ?_ (twoPointWitnessCausal_lower_bound W hest) linarith -
mhatV_strictOverlaptheorem — The null VaryingCenterCase1 witness has strict propensity overlap.hypothesesconclusionP.mhatV x ∈ Ioo (0 : ℝ) 1 -
mPertV_strictOverlaptheorem — The perturbed VaryingCenterCase1 witness has strict propensity overlap.hypothesesconclusionP.mPertV lam x ∈ Ioo (0 : ℝ) 1Proof (Lean source)
theorem mPertV_strictOverlap (P : VarConstr K) [NeZero K] (hmU_strict : ∀ j, P.m₀ j * (1 + P.β / P.g₁ j) < 1) (lam : Fin K → Bool) : ∀ x : Fin K × Bool, P.mPertV lam x ∈ Ioo (0 : ℝ) 1 := by intro x constructor · simp only [mPertV] exact mul_pos (P.hm₀0 x.1) (P.denomV_pos lam x) · simp only [mPertV] have hr := P.ratio_nonneg x.1 have hr1 := P.ratio_lt_one x.1 have hm0 := P.hm₀0 x.1 have hm1 := P.hm₀1 x.1 have hstrict := hmU_strict x.1 rcases Δ_mem lam x with h | h · rw [h] nlinarith · rw [h] nlinarith -
realV_le_minimaxMissCausaltheorem — An in-class DGP's causal-centered miss probability is dominated by minimaxMissCausal.hypothesesconclusion≤ minimaxMissCausal P.mhatV P.ghatV εg εm n est sProof (Lean source)
theorem realV_le_minimaxMissCausal (P : VarConstr K) {n : ℕ} [NeZero K] {εg εm : ℝ} {m : Fin K × Bool → ℝ} {g : Bool → Fin K × Bool → ℝ} (hin : InClass (P.mhatV (K := K)) P.ghatV εg εm m g) (est : (Fin n → Obs (Fin K × Bool)) → ℝ) (s : ℝ) : (productLaw hin.valid n).real {x | s ≤ |est x - causalATE (C := Fin K × Bool) m g|} ≤ minimaxMissCausal P.mhatV P.ghatV εg εm n est s := by simpa using nMissCausal_le_minimaxMissCausal (⟨(m, g), hin⟩ : InClassDGP (P.mhatV (K := K)) P.ghatV εg εm) (est := est) (s := s) -
mhat2_strictOverlaptheorem — The null VaryingCenterCase2 witness has strict propensity overlap.hypothesesconclusionP.mhat2 x ∈ Ioo (0 : ℝ) 1Proof (Lean source)
theorem mhat2_strictOverlap (P : VarConstr2 K) [NeZero K] : ∀ x : Fin K × Bool, P.mhat2 x ∈ Ioo (0 : ℝ) 1 := by intro x exact ⟨P.hm₀0 x.1, P.hm₀1 x.1⟩ -
mPert2_strictOverlaptheorem — The perturbed VaryingCenterCase2 witness has strict propensity overlap.hypothesesconclusionP.mPert2 lam x ∈ Ioo (0 : ℝ) 1Proof (Lean source)
theorem mPert2_strictOverlap (P : VarConstr2 K) [NeZero K] (hκ_strict : ∀ j, P.κ j < 1) (hmU_strict : ∀ j, P.m₀ j * (1 + P.κ j) < 1) (lam : Fin K → Bool) : ∀ x : Fin K × Bool, P.mPert2 lam x ∈ Ioo (0 : ℝ) 1 := by intro x constructor · rw [P.mPert2_eq lam x] have hm0 := P.hm₀0 x.1 have hκ0 := P.κ_nonneg x.1 have hκ1 := hκ_strict x.1 rcases Δ_mem lam x with h | h · rw [h]; nlinarith · rw [h]; nlinarith · rw [P.mPert2_eq lam x] have hm1 := P.hm₀1 x.1 have hκ0 := P.κ_nonneg x.1 have hκ1 := hκ_strict x.1 have hstrict := hmU_strict x.1 rcases Δ_mem lam x with h | h · rw [h]; simpa using hstrict · rw [h]; nlinarith -
real2_le_minimaxMissCausaltheorem — An in-class Case-2 DGP's causal-centered miss probability is dominated by minimaxMissCausal.hypothesesconclusion≤ minimaxMissCausal P.mhat2 P.ghat2 εg εm n est sProof (Lean source)
theorem real2_le_minimaxMissCausal (P : VarConstr2 K) {n : ℕ} [NeZero K] {εg εm : ℝ} {m : Fin K × Bool → ℝ} {g : Bool → Fin K × Bool → ℝ} (hin : InClass (P.mhat2 (K := K)) P.ghat2 εg εm m g) (est : (Fin n → Obs (Fin K × Bool)) → ℝ) (s : ℝ) : (productLaw hin.valid n).real {x | s ≤ |est x - causalATE (C := Fin K × Bool) m g|} ≤ minimaxMissCausal P.mhat2 P.ghat2 εg εm n est s := by simpa using nMissCausal_le_minimaxMissCausal (⟨(m, g), hin⟩ : InClassDGP (P.mhat2 (K := K)) P.ghat2 εg εm) (est := est) (s := s) -
minimax_lower_bound_var2_causaltheorem — Causal-centered structure-agnostic minimax lower bound (Case-2-shaped family). For a second cell-varying construction P with K paired cells, a sample size n, and nuisance-error budgets εg and εm, suppose the treated-arm bump is strictly positive, the propensity perturbation stays within εm, the outcome perturbation stays within εg, the propensity coefficient is strictly below one, the perturbed propensity remains strictly below one, both budgets are nonnegative, the aggregate overlap coefficient is at most one, and the sample size satisfies the stated regularity condition. Then for every measurable estimator, the causal-centered miss probability at half the displayed strictly positive ATE separation is at least 1/4 for some data-generating process in the class.hypothesesK :sharedℕP :n :ℕNeZero Kεg εm :ℝhβpos :0 < P.βhm :∀ j, (P.m₀ j * P.κ j) ^ 2 ≤ εmhg :∀ j, P.β ^ 2 * (P.α * P.g₁ j + 1) ^ 2 / (1 - P.β / P.g₁ j - P.α * P.β) ^ 2 ≤ εghκ_strict :∀ j, P.κ j < 1hmU_strict :∀ j, P.m₀ j * (1 + P.κ j) < 1hεg :0 ≤ εghεm :0 ≤ εmhΓsum :∑ j, P.ΓV2 j / (K : ℝ) ≤ 1hreg :(n : ℝ) ^ 2 / 2 * ∑ j, (P.ΓV2 j / (K : ℝ)) ^ 2 ≤ log 2hest :Measurable estconclusion1 / 4≤ minimaxMissCausal P.mhat2 P.ghat2 εg εm n est ((card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β) * (∑ j : Fin K, P.g₁ j * (P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) + P.β) / (P.g₁ j ^ 2 * (1 - P.α * P.β) ^ 2 - P.β ^ 2)) / 2)Proof (Lean source)
theorem minimax_lower_bound_var2_causal (P : VarConstr2 K) {n : ℕ} [NeZero K] {εg εm : ℝ} (hβpos : 0 < P.β) (hm : ∀ j, (P.m₀ j * P.κ j) ^ 2 ≤ εm) (hg : ∀ j, P.β ^ 2 * (P.α * P.g₁ j + 1) ^ 2 / (1 - P.β / P.g₁ j - P.α * P.β) ^ 2 ≤ εg) (hκ_strict : ∀ j, P.κ j < 1) (hmU_strict : ∀ j, P.m₀ j * (1 + P.κ j) < 1) (hεg : 0 ≤ εg) (hεm : 0 ≤ εm) (hΓsum : ∑ j, P.ΓV2 j / (K : ℝ) ≤ 1) (hreg : (n : ℝ) ^ 2 / 2 * ∑ j, (P.ΓV2 j / (K : ℝ)) ^ 2 ≤ log 2) {est : (Fin n → Obs (Fin K × Bool)) → ℝ} (hest : Measurable est) : 1 / 4 ≤ minimaxMissCausal P.mhat2 P.ghat2 εg εm n est ((card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β) * (∑ j : Fin K, P.g₁ j * (P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) + P.β) / (P.g₁ j ^ 2 * (1 - P.α * P.β) ^ 2 - P.β ^ 2)) / 2) := by set gap := (card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β) * ∑ j : Fin K, P.g₁ j * (P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) + P.β) / (P.g₁ j ^ 2 * (1 - P.α * P.β) ^ 2 - P.β ^ 2) with hgap have hgap_pos : 0 < gap := by have hcard : 0 < (card (Fin K × Bool) : ℝ)⁻¹ := by have hcard_nat : 0 < card (Fin K × Bool) := Fintype.card_pos exact inv_pos.mpr (by exact_mod_cast hcard_nat) have h2β : 0 < 2 * P.β := by positivity have hsum_pos : 0 < ∑ j : Fin K, P.g₁ j * (P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) + P.β) / (P.g₁ j ^ 2 * (1 - P.α * P.β) ^ 2 - P.β ^ 2) := by apply Finset.sum_pos · intro j _ have hg1 := P.hg₁0 j have hE := P.denomE_pos j have hab := P.alphabeta_le_one j have hinner : 0 < P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) + P.β := by have hnonneg : 0 ≤ P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) := by apply mul_nonneg (mul_nonneg P.hα (sq_nonneg _)) linarith linarith exact div_pos (mul_pos hg1 hinner) hE · exact univ_nonempty rw [hgap] exact mul_pos (mul_pos hcard h2β) hsum_pos set s := gap / 2 with hs set θ0 := ate (P.ghat2 (K := K)) with hθ0 let W : TwoPointWitnessCausal (Fin K × Bool) n P.mhat2 P.ghat2 εg εm := { s := s c := 1 / 2 Q := fun j => cond j (Qtrue2 P n) (Qfalse2 P n) prob := by intro j cases j · exact Qfalse2_isProb P n · exact Qtrue2_isProb P n θ := fun j => cond j (θ0 + gap) θ0 sep := by change 2 * s ≤ |(θ0 + gap) - θ0| rw [add_sub_cancel_left, abs_of_pos hgap_pos, hs] linarith tvBound := by simpa using P.tvDist_Qfalse2_Qtrue2_le_half (n := n) hΓsum hreg dominated := by intro est' j cases j · change (Qfalse2 P n).real {x | s ≤ |est' x - θ0|} ≤ minimaxMissCausal P.mhat2 P.ghat2 εg εm n est' s have hb := P.real2_le_minimaxMissCausal (n := n) (inClass_null2 P hεg hεm) est' s have hbridge : causalATE (P.mhat2 (K := K)) P.ghat2 = ate P.ghat2 := causalATE_eq_ate (P.validDGP_hat2 (K := K)) (P.mhat2_strictOverlap (K := K)) rw [hbridge, ← hθ0] at hb exact hb · change (Qtrue2 P n).real {x | s ≤ |est' x - (θ0 + gap)|} ≤ minimaxMissCausal P.mhat2 P.ghat2 εg εm n est' s haveI : ∀ lam : Fin K → Bool, IsProbabilityMeasure (Qpert2 P n lam) := fun lam => Qpert2_isProb P n lam unfold Qtrue2 refine mixtureReal_le (signWeight K) (signWeight_sum K) (fun lam => Qpert2 P n lam) _ _ ?_ intro lam have hb := P.real2_le_minimaxMissCausal (n := n) (P.inClass2 hm hg hεg lam) est' s have hkey : ate (P.gPert2 lam) = θ0 + gap := by have := P.ate_gap2 lam rw [hθ0, hgap] linarith [this] have hbridge : causalATE (P.mPert2 lam) (P.gPert2 lam) = ate (P.gPert2 lam) := causalATE_eq_ate (P.validDGP_pert2 lam) (P.mPert2_strictOverlap hκ_strict hmU_strict lam) rw [hbridge, hkey] at hb exact hb } exact twoPointWitnessCausal_quarter W (le_refl _) hest