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.
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)
The printable representation of a witness-graph node is its corresponding node label, with the observed covariate, treatment, outcome, the latent covariate draw, treatment noise, and outcome noise given their six respective labels.
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.
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)
Every edge of the finite backdoor witness graph points strictly forward in the chosen topological order on its nodes.
Formal statement
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.
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)
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.
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.
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.
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
Proof (Lean source)
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)
The latent-noise probability law is the uniform probability distribution on the closed unit interval of the real line.
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)
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)
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)
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.
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.
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.
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.
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.
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.
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.
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.
9 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 equipped with a measurable structure and a standard-Borel structure 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 equipped with a measurable structure, the uniform covariate law is a probability measure.
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.
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)
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)
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)
12 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_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 ?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] · decide · decide · 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)) 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.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.
For a finite nonempty covariate space, with a measurable structure in which every singleton is measurable, centered propensity and outcome-regression functions, two real radii with no sign restrictions, a sample size, an estimator based on that many observed treatment--outcome--covariate records, and a real error threshold, the causal-centered minimax miss probability is the supremum, over all valid observed-data distributions in the nuisance-function class determined by those centers and radii, of the probability that the estimator's absolute error from that distribution's average potential-outcome treatment effect is at least the threshold.
Definition (Lean source)
Two-point Le Cam witness whose realizability target is minimaxMissCausal.
Definition (Lean source)
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
Proof (Lean source)
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). 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.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 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