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 24 core · 9 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.
Mirrors the proven-shape witness construction in
CausalSmith/.../STAT_AteOverlapDecay_Clean/Witness/Construction.lean (Causalean
cannot import CausalSmith, so the construction is reproduced here, specialized to
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
These are the nodes of the finite backdoor witness graph.
Definition (Lean source)
inductive WNode
| Xc | A | Y | Un | Ea | Ey
deriving DecidableEq
def repr reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal.WNode
This gives a printable representation for the witness graph nodes.
def wEdge reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the edge relation for the finite backdoor witness graph.
def wTopo reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This topological order places latent roots before the observed covariate, treatment, and outcome.
Definition (Lean source)
def wTopo : WNode → ℕ
| Un => 0
| Ea => 1
| Ey => 2
| Xc => 3
| A => 4
| 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.
def wDAG reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the directed acyclic graph for the finite backdoor witness.
def wSWIGGraph reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the SWIG graph with observed covariate, treatment, and outcome nodes and latent noise roots.
Definition (Lean source)
def wSWIGGraph : SWIGGraph WNode where
dag := initialSWIG wDAG
fixed := ∅
observed := {SWIGNode.random Xc, SWIGNode.random A, SWIGNode.random Y}
unobserved := {SWIGNode.random Un, SWIGNode.random Ea, SWIGNode.random Ey}
fixed_is_fixed := by intro s hs; simp at hs
observed_is_random := by
intro v hv; simp at hv
rcases hv with rfl | rfl | rfl <;> exact ⟨_, rfl⟩
unobserved_is_random := by
intro u hu; simp at hu
rcases hu with rfl | rfl | rfl <;> exact ⟨_, rfl⟩
obs_unobs_disjoint := by native_decide
dag_edges_classified := by native_decide
fixed_image_in_observed := by intro s hs; simp at hs
fixed_are_roots := by intro s hs; simp at hs
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 native_decide))
fixed_outside_fixed_isolated := by
intro n _
cases n <;> exact ⟨by native_decide, by native_decide⟩
all_children_in_observed := by native_decide
def WΩ reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This assigns value spaces to the witness graph nodes.
def treatFun reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This structural function turns a uniform treatment noise draw into a Boolean treatment.
def outFun reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This structural function turns treatment, covariate, and outcome noise into a Bernoulli outcome.
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
This extracts a parent node's value from the tuple of parent values supplied to a structural function.
def unifLaw reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the uniform law on the unit interval used for the latent noise roots.
def covLaw reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the uniform law on the finite covariate space.
Definition (Lean source)
def dgpSCM reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the concrete stochastic structural causal model for a finite propensity and outcome regression.
Definition (Lean source)
noncomputable def dgpSCM (m : C → ℝ) (g : Bool → C → ℝ) :
SCM WNode (WΩ C) where
toSWIGGraph := wSWIGGraph
edgeTypes := EdgeTypeAssignment.allNonparametric (initialSWIG wDAG)
iota_valueSpace := by
intro s
exact (notMem_empty s.val s.property).elim
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, mem_singleton] at h
rcases h with h | h | h <;> exact absurd h (by simp) : False).elim
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
-- `decide P` and `if P then true else false` are definitionally equal,
-- so we may take the `ite` route and avoid any rewrite inside the goal.
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
latentDist := fun u => by
rcases u with ⟨n, hn⟩
exact
match n, hn with
| SWIGNode.random Un, _ => covLaw C
| SWIGNode.random Ea, _ => unifLaw
| SWIGNode.random Ey, _ => unifLaw
| _, _ => (0 : Measure _)
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
This is the empty background assignment for the witness SCM.
Definition (Lean source)
noncomputable def dgpFixed (m : C → ℝ) (g : Bool → C → ℝ) :
SCM.FixedValues (dgpSCM m g) :=
fun s => (notMem_empty s.val s.property).elim
def dgpPO reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the potential-outcome system induced by the witness structural causal model.
def AIdx reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the observed-node index of the treatment in the induced potential-outcome system.
def YIdx reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the observed-node index of the outcome in the induced potential-outcome system.
def XIdx reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the observed-node index of the covariate in the induced potential-outcome system.
def AEquiv reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This identifies the treatment node's value space with Booleans.
def YEquiv reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This identifies the outcome node's value space with real numbers.
def XEquiv reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This identifies the covariate node's value space with the finite covariate type.
def dgpBackdoor reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the backdoor potential-outcome system extracted from the finite witness construction.
Definition (Lean source)
noncomputable def dgpBackdoor (m : C → ℝ) (g : Bool → C → ℝ) :
POBackdoorSystem (dgpPO m g) C where
D := AIdx m g
Y := YIdx m g
Xvar := ⟨XIdx m g, XEquiv m g⟩
hDbool := AEquiv m g
hYreal := YEquiv m g
hDY := by
intro h; have := congrArg val h
simp only [AIdx, YIdx] at this; exact absurd this (by decide)
hDX := by
intro h; have := congrArg val h
simp only [AIdx, XIdx] at this; exact absurd this (by decide)
hYX := by
intro h; have := congrArg val h
simp only [YIdx, XIdx] at this; exact absurd this (by decide)
9 supporting declarations (lemmas, instances)
-
instDecidableEqWNodeinstancederiving DecidableEq -
instDecidableRelWNodeWEdgeinstance — The witness graph edge relation is decidable.instance : DecidableRel wEdge := by intro a b; cases a <;> cases b <;> simp [wEdge] <;> infer_instance -
WΩ_measinstance — Each witness node value space has its measurable-space structure.noncomputable instance WΩ_meas : ∀ n, MeasurableSpace (WΩ C n) | Xc => inferInstanceAs (MeasurableSpace C) | A => inferInstanceAs (MeasurableSpace Bool) | Y => inferInstanceAs (MeasurableSpace ℝ) | Un => inferInstanceAs (MeasurableSpace C) | Ea => inferInstanceAs (MeasurableSpace ℝ) | Ey => inferInstanceAs (MeasurableSpace ℝ) -
WΩ_borelinstance — Each witness node value space is standard Borel.noncomputable instance WΩ_borel : ∀ n, StandardBorelSpace (WΩ C n) | Xc => inferInstanceAs (StandardBorelSpace C) | A => inferInstanceAs (StandardBorelSpace Bool) | Y => inferInstanceAs (StandardBorelSpace ℝ) | Un => inferInstanceAs (StandardBorelSpace C) | Ea => inferInstanceAs (StandardBorelSpace ℝ) | Ey => inferInstanceAs (StandardBorelSpace ℝ) -
WΩ_nonemptyinstance — Each witness node value space is nonempty. -
instIsProbabilityMeasureUnifLawinstance — The unit-interval uniform law is a probability measure.instance instIsProbabilityMeasureUnifLaw : IsProbabilityMeasure unifLaw := by unfold unifLaw constructor simp [Real.volume_Icc] -
instIsProbabilityMeasureCovLawinstance — The finite covariate uniform law is a probability measure.instance instIsProbabilityMeasureCovLaw : IsProbabilityMeasure (covLaw C) := by unfold covLaw; infer_instance
Bridge 3 core · 12 supporting This file is the clean interface between the causal layer (the POBackdoorSystem built in Construction.lean, whose ATE E[Y(1) − Y(0)] is the genuine causal target) and the observed-data contrast ate g on which the minimax ★ causalATE_eq_ate
Causal Grounding of the Minimax ATE Model
This file is the clean interface between the causal layer (the
POBackdoorSystem built in Construction.lean, whose ATE E[Y(1) − Y(0)] is
the genuine causal target) 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 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.
Obligation status
* dgp_consistency — proved (FREE from POSystem.ofSCM_consistency).
* dgp_unconfoundedness and dgp_adjustedCE_eq_g prove the genuine
causal-layer obligations: the d-separation lift and the outcome-regression
conditional-mean computation of the constructed SCM law.
* dgp_propScore_eq_m, dgp_overlap, dgp_assumptions, dgp_P_X_eq_covLaw,
and dgpBES assemble the backdoor-estimation-system interface needed for the
final bridge theorem.
def causalATE reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
The causal average treatment effect of the constructed finite backdoor system, namely (dgpBackdoor m g).ATE. The theorem causalATE_eq_ate later identifies this potential-outcome estimand with the finite observed-data contrast ate g under validity and strict overlap.
Definition (Lean source)
def dgpBES reviewed
⚑ flagged
Causalean.Estimation.MinimaxATE.Causal
This is the backdoor estimation system whose value-space regression and propensity are the supplied functions.
Definition (Lean source)
noncomputable def dgpBES (hv : ValidDGP m g) (hso : ∀ x, m x ∈ Ioo (0 : ℝ) 1) :
BackdoorEstimationSystem (dgpPO m g) C where
toPOBackdoorSystem := dgpBackdoor m g
μ_val := g
μ_meas := fun _ => measurable_of_finite _
e_val := m
e_meas := measurable_of_finite _
e_pos := fun x => (hso x).1
e_lt_one := fun x => (hso x).2
μ_reg_compat := fun d => (dgp_adjustedCE_eq_g hv hso d).symm
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
12 supporting declarations (lemmas, instances)
-
dgpPO_isProbinstance — The constructed potential-outcome system has a probability measure as its population law.instance dgpPO_isProb : IsProbabilityMeasure (dgpPO m g).μ := by change IsProbabilityMeasure (SCM.latentProduct (dgpSCM m g)) infer_instance -
dgpPO_boreltheorem — The constructed potential-outcome system has a standard Borel sample space.conclusionStandardBorelSpace (dgpPO m g).Ω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 — The standard Borel structure for the constructed potential-outcome system is available as an instance. -
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).conclusion(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 ?hDisj_XY ?hDisj_XZ ?hDisj_YZ ?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] · native_decide · native_decide · native_decide · 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)) native_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 = SCM.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 ((SCM.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 (SCM.singletonValues (α := swigΩ (WΩ C)) (v := SWIGNode.random WNode.Xc) ∘ (RegimedVar.ofFactual (dgpBackdoor m g).xVar).value) inferInstance) inferInstance (SCM.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 (SCM.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 (SCM.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.hypotheseshv :ValidDGP m gconclusion=ᵐ[(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).μ,Proof (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.conclusionProof (Lean source)
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.conclusionProof (Lean source)
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.conclusionProof (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
Causal-centered minimax miss probability. This mirrors minimaxMiss, but centers each DGP's miss event at the potential-outcome estimand causalATE m g of the concrete backdoor system.
Definition (Lean source)
noncomputable def 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|}
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). For the outcome-dominant cell-varying construction P, 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 Case-1 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 Case-1 bound be re-centered onto the genuine causal estimand.
Formal statement
hypotheses
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.hypothesesconclusion≤ minimaxMissCausal mhat ghat εg εm n est sProof (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.hypothesesconclusionProof (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.Proof (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. -
mPertV_strictOverlaptheorem — The perturbed VaryingCenterCase1 witness has strict propensity overlap.hypothesesProof (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.Proof (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.hypothesesProof (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). For the propensity-dominant cell-varying construction, a strictly positive treated-arm bump and strict perturbed-propensity overlap imply that every measurable estimator has causal-centered miss probability at least 1/4 at half of the displayed strictly positive ATE separation.hypothesesP :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 Finset.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