Panel.EstimandCharacterization.OLSWeightDecomposition
Sloczynski's characterization: the OLS coefficient as a convex combination of group-specific effects with reversed weights.
FinitePartition 18 core · 5 supporting This file formalizes the finite-cell algebra behind Słoczyński's saturated ordinary least squares weights with heterogeneous treatment effects. ★ finite_weights_eq_sum★ equal_groups_collapses★ homogeneous_collapses★ perTreatedWeight_antitone★ perUntreatedWeight_monotone★ represents★ equal_groups_eq_ATE★ homogeneous_eq_constant
Słoczyński Finite Partition Algebra
This file formalizes the finite-cell algebra behind Słoczyński's saturated
ordinary least squares weights with heterogeneous treatment effects. It defines
FinitePartition, cellOverlap, overlapWeight, and
overlapWeightedATE, proves the normalized-weight identity
finite_weights_eq_sum, and records the equal-share and homogeneous-effect
collapses. It also defines perTreatedWeight and perUntreatedWeight for the
per-observation leverage interpretation, and OppositeGroupRepr for the
separate ATT/ATU opposite-group representation with the derived theorem
represents.
structure FinitePartition reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition
A finite covariate partition for Słoczyński's saturated-OLS weight decomposition, carrying cell probabilities, within-cell treated shares, and within-cell conditional treatment effects, together with the side conditions used by the saturated-OLS algebra: the cell probabilities are nonnegative and sum to one, the treated shares lie in the unit interval, and the overlap denominator Σ π_g p_g (1−p_g) is strictly positive.
Definition (Lean source)
parameters
𝒢 :
Type*
Fintype 𝒢
fields
Cell probability `π_g = ℙ(G=g)`.
π :
𝒢 → ℝ
Within-cell treated share `p_g = ℙ(D=1 ∣ G=g)`.
p :
𝒢 → ℝ
Within-cell conditional treatment effect `τ_g = E[Y(1)−Y(0) ∣ G=g]`.
τ :
𝒢 → ℝ
`π` takes nonnegative values.
π_nonneg :
∀ g, 0 ≤ π g
`π` sums to 1.
π_sum_one :
∑ g, π g = 1
Treatment shares are nonnegative.
p_nonneg :
∀ g, 0 ≤ p g
Treatment shares are at most 1.
p_le_one :
∀ g, p g ≤ 1
Saturated-overlap relevance: `Σ π_g p_g (1−p_g) > 0`.
overlap_pos :
0 < ∑ g, π g * (p g * (1 - p g))
def cellOverlap reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Within-cell treatment variance p_g (1 − p_g).
Definition (Lean source)
def overlapNumerator reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Numerator Σ_g π_g · p_g (1−p_g) · τ_g of the saturated-OLS estimand in finite-cell form.
Definition (Lean source)
def overlapNumerator {𝒢 : Type*} [Fintype 𝒢] (P : FinitePartition 𝒢) : ℝ :=
∑ g, P.π g * P.cellOverlap g * P.τ g
def overlapDenominator reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Denominator Σ_g π_g · p_g (1−p_g) of the saturated-OLS estimand in finite-cell form. Positive by overlap_pos.
Definition (Lean source)
def overlapDenominator {𝒢 : Type*} [Fintype 𝒢] (P : FinitePartition 𝒢) : ℝ :=
∑ g, P.π g * P.cellOverlap g
def overlapWeight reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Normalized weight ω_g = π_g p_g (1−p_g) / Σ_h π_h p_h (1−p_h).
Definition (Lean source)
noncomputable def overlapWeight {𝒢 : Type*} [Fintype 𝒢]
(P : FinitePartition 𝒢) (g : 𝒢) : ℝ :=
(P.π g * P.cellOverlap g) / P.overlapDenominator
def overlapWeightedATE reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Saturated-OLS estimand in finite-cell form, β_sat = (Σ π·p(1−p)·τ) / (Σ π·p(1−p)).
Definition (Lean source)
noncomputable def overlapWeightedATE {𝒢 : Type*} [Fintype 𝒢]
(P : FinitePartition 𝒢) : ℝ :=
P.overlapNumerator / P.overlapDenominator
theorem finite_weights_eq_sum reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Finite-partition OLS weights (prop:po-estimand-sloczynski-ols-finite-weights). The saturated-OLS estimand equals the sum of normalized overlap weights times cell effects, Σ_g ω_g τ_g.
Formal statement
conclusion
P.overlapWeightedATE = ∑ g, P.overlapWeight g * P.τ g
Proof (Lean source)
theorem finite_weights_eq_sum :
P.overlapWeightedATE = ∑ g, P.overlapWeight g * P.τ g := by
simp only [overlapWeightedATE, overlapNumerator, overlapWeight, Finset.sum_div]
refine Finset.sum_congr rfl (fun g _ => ?_)
ring
theorem equal_groups_collapses reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Equal-cell-share collapse to unweighted average (finite half of prop:po-estimand-sloczynski-ols-equal-groups). If every cell has an equal treated share p_g = 1/2, then the saturated-OLS estimand β_sat equals the probability-weighted average of the cell treatment effects Σ π_g τ_g.
Formal statement
hypotheses
h :
∀ g, P.p g = 1 / 2
conclusion
P.overlapWeightedATE = ∑ g, P.π g * P.τ g
Proof (Lean source)
theorem equal_groups_collapses
(h : ∀ g, P.p g = 1 / 2) :
P.overlapWeightedATE = ∑ g, P.π g * P.τ g := by
rw [P.finite_weights_eq_sum]
refine Finset.sum_congr rfl (fun g _ => ?_)
rw [P.equal_groups_weight_eq_pi h g]
theorem homogeneous_collapses reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Homogeneous-effect collapse (saturated half of prop:po-estimand-sloczynski-ols-homogeneous). If the cell-level treatment effect equals a common constant τ₀ in every cell, then the saturated-OLS estimand β_sat equals τ₀.
Formal statement
hypotheses
τ₀ :
ℝ
h :
∀ g, P.τ g = τ₀
conclusion
P.overlapWeightedATE = τ₀
Proof (Lean source)
theorem homogeneous_collapses
{τ₀ : ℝ} (h : ∀ g, P.τ g = τ₀) :
P.overlapWeightedATE = τ₀ := by
have hD : P.overlapDenominator ≠ 0 := P.overlapDenominator_pos.ne'
have hnum : P.overlapNumerator = τ₀ * P.overlapDenominator := by
simp only [overlapNumerator, overlapDenominator, Finset.mul_sum]
refine Finset.sum_congr rfl (fun g _ => ?_)
rw [h g]; ring
rw [overlapWeightedATE, hnum, mul_div_assoc, div_self hD, mul_one]
def perTreatedWeight reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Per-treated-observation leverage factor in cell g.
Definition (Lean source)
noncomputable def perTreatedWeight {𝒢 : Type*} [Fintype 𝒢]
(P : FinitePartition 𝒢) (g : 𝒢) : ℝ := 1 - P.p g
def perUntreatedWeight reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Per-untreated-observation leverage factor in cell g.
Definition (Lean source)
noncomputable def perUntreatedWeight {𝒢 : Type*} [Fintype 𝒢]
(P : FinitePartition 𝒢) (g : 𝒢) : ℝ := P.p g
theorem perTreatedWeight_antitone reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Headline monotonicity — smaller treated group gets larger per-treated weight (rem:po-estimand-sloczynski-ols-group-size). The per-treated-observation leverage factor 1 − p_g is antitone in the treated share: if cell g has a treated share no larger than cell h's, then g's per-treated-observation leverage factor is at least h's: perTreatedWeight P h ≤ perTreatedWeight P g.
Formal statement
hypotheses
conclusion
P.perTreatedWeight h ≤ P.perTreatedWeight g
Proof (Lean source)
theorem perTreatedWeight_antitone {𝒢 : Type*} [Fintype 𝒢]
(P : FinitePartition 𝒢) {g h : 𝒢}
(hph : P.p g ≤ P.p h) :
P.perTreatedWeight h ≤ P.perTreatedWeight g := by
simp only [perTreatedWeight]
linarith
theorem perUntreatedWeight_monotone reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.FinitePartition
Monotonicity — larger treated group gives larger per-untreated weight (rem:po-estimand-sloczynski-ols-group-size, untreated side). The per-untreated-observation leverage factor p_g is monotone in the treated share: if cell g has a treated share no larger than cell h's, then h's per-untreated-observation leverage factor is at least g's: perUntreatedWeight P g ≤ perUntreatedWeight P h.
Formal statement
hypotheses
conclusion
P.perUntreatedWeight g ≤ P.perUntreatedWeight h
Proof (Lean source)
theorem perUntreatedWeight_monotone {𝒢 : Type*} [Fintype 𝒢]
(P : FinitePartition 𝒢) {g h : 𝒢}
(hph : P.p g ≤ P.p h) :
P.perUntreatedWeight g ≤ P.perUntreatedWeight h := by
simp only [perUntreatedWeight]
exact hph
structure OppositeGroupRepr reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition
Słoczyński's two-component ATT/ATU representation (ass:po-estimand-sloczynski-ols-opposite-group).
Definition (Lean source)
fields
Treated share `ρ = ℙ(D=1)`.
ρ :
ℝ
ATT, `τ_ATT = E[Y(1)−Y(0) | D=1]`.
τ_ATT :
ℝ
ATU, `τ_ATU = E[Y(1)−Y(0) | D=0]`.
τ_ATU :
ℝ
OLS coefficient on `D`.
β_ols :
ℝ
General two-component weight on `τ_ATT`.
w₁ :
ℝ
General two-component weight on `τ_ATU`.
w₀ :
ℝ
`ρ` is a probability — nonnegative side.
ρ_nonneg :
0 ≤ ρ
`ρ` is a probability — `≤ 1` side.
ρ_le_one :
ρ ≤ 1
**Structural assumption** (Słoczyński two-component representation,
`ass:po-estimand-sloczynski-ols-opposite-group`): the OLS coefficient is a
convex-style combination of the group-status effects. This is genuinely
weaker than the opposite-group conclusion — it does not fix the weights.
twoComponent :
β_ols = w₁ * τ_ATT + w₀ * τ_ATU
The two weights sum to one.
weights_sum_one :
w₁ + w₀ = 1
**Equal-dispersion specialization**: the ATT weight equals the untreated
share `1 − ρ` (`ass:po-estimand-sloczynski-ols-opposite-group`).
equalDispersion :
w₁ = 1 - ρ
def tau_ATE reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.OppositeGroupRepr
ATE expressed as ρ τ_ATT + (1−ρ) τ_ATU (def:po-estimand-sloczynski-ols-att-atu).
Definition (Lean source)
def tau_ATE (R : OppositeGroupRepr) : ℝ := R.ρ * R.τ_ATT + (1 - R.ρ) * R.τ_ATU
theorem represents reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.OppositeGroupRepr
Słoczyński opposite-group identity (prop:po-estimand-sloczynski-ols-opposite-group) — derived rather than assumed. Substituting the equal-dispersion weights into the two-component representation shows that the OLS coefficient equals (1−ρ)·τ_ATT + ρ·τ_ATU: the treated-group effect receives the untreated share as its weight, and vice versa.
Formal statement
conclusion
R.β_ols = (1 - R.ρ) * R.τ_ATT + R.ρ * R.τ_ATU
Proof (Lean source)
theorem represents : R.β_ols = (1 - R.ρ) * R.τ_ATT + R.ρ * R.τ_ATU := by
rw [R.twoComponent, R.equalDispersion, R.w0_eq_rho]
theorem equal_groups_eq_ATE reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.OppositeGroupRepr
Equal-group-size collapse to the ATE (top half of prop:po-estimand-sloczynski-ols-equal-groups). If the treated share ρ equals one half, then the opposite-group OLS coefficient β_ols equals the ATE τ_ATE = ρ·τ_ATT + (1−ρ)·τ_ATU.
Formal statement
hypotheses
h :
R.ρ = 1 / 2
conclusion
R.β_ols = R.tau_ATE
Proof (Lean source)
theorem equal_groups_eq_ATE (h : R.ρ = 1 / 2) :
R.β_ols = R.tau_ATE := by
rw [R.represents, tau_ATE, h]; ring
theorem homogeneous_eq_constant reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition.OppositeGroupRepr
Homogeneous-effect collapse for the opposite-group representation (ATT/ATU half of prop:po-estimand-sloczynski-ols-homogeneous). If the ATT equals a common constant τ₀ and the ATU equals that same constant τ₀, then the opposite-group OLS coefficient β_ols equals τ₀, regardless of the treated share ρ.
Formal statement
hypotheses
τ₀ :
ℝ
hT :
R.τ_ATT = τ₀
hU :
R.τ_ATU = τ₀
conclusion
R.β_ols = τ₀
Proof (Lean source)
theorem homogeneous_eq_constant
{τ₀ : ℝ} (hT : R.τ_ATT = τ₀) (hU : R.τ_ATU = τ₀) :
R.β_ols = τ₀ := by
rw [R.represents, hT, hU]; ring
5 supporting declarations (lemmas, instances)
-
overlapDenominator_postheorem — The denominator is positive. Restated from overlap_pos.conclusion0 < P.overlapDenominatorProof (Lean source)
theorem overlapDenominator_pos : 0 < P.overlapDenominator := by simpa [overlapDenominator, cellOverlap, mul_assoc] using P.overlap_pos -
omega_sum_eq_onetheorem — The overlap weights sum to one. Direct from positivity of the denominator and pulling the common denominator out of the sum.conclusion∑ g, P.overlapWeight g = 1Proof (Lean source)
theorem omega_sum_eq_one : ∑ g, P.overlapWeight g = 1 := by have hD : P.overlapDenominator ≠ 0 := P.overlapDenominator_pos.ne' have hsum : ∑ g, P.overlapWeight g = P.overlapDenominator / P.overlapDenominator := by simp [overlapWeight, overlapDenominator, Finset.sum_div] rw [hsum, div_self hD] -
equal_groups_weight_eq_pitheorem — Equal-cell-share weight collapse: if p_g = 1/2 for every cell, the normalized overlap weight reduces to the cell probability π_g.hypothesesh :∀ g, P.p g = 1 / 2g :𝒢conclusionP.overlapWeight g = P.π gProof (Lean source)
theorem equal_groups_weight_eq_pi (h : ∀ g, P.p g = 1 / 2) (g : 𝒢) : P.overlapWeight g = P.π g := by have hcell : ∀ g', P.cellOverlap g' = (1 : ℝ) / 4 := by intro g' simp [cellOverlap, h g'] ring have hden : P.overlapDenominator = (1 : ℝ) / 4 := by have hsum : ∑ g', P.π g' * P.cellOverlap g' = ∑ g', P.π g' * ((1 : ℝ)/4) := by refine Finset.sum_congr rfl (fun g' _ => ?_) rw [hcell g'] rw [overlapDenominator, hsum, ← Finset.sum_mul, P.π_sum_one, one_mul] simp [overlapWeight, hcell, hden] -
cellOverlap_eq_perWeights_multheorem — The cell overlap variance is the product of the two per-observation leverage factors: p_g (1−p_g) = perUntreatedWeight_g · perTreatedWeight_g. This links the finite-cell denominator directly to the paper's per-unit weight interpretation.hypothesesconclusionP.cellOverlap g = P.perUntreatedWeight g * P.perTreatedWeight gProof (Lean source)
theorem cellOverlap_eq_perWeights_mul {𝒢 : Type*} [Fintype 𝒢] (P : FinitePartition 𝒢) (g : 𝒢) : P.cellOverlap g = P.perUntreatedWeight g * P.perTreatedWeight g := by unfold cellOverlap perUntreatedWeight perTreatedWeight ring -
w0_eq_rhotheorem — The untreated weight in the equal-dispersion case is the treated share ρ, forced by w₁ + w₀ = 1 and w₁ = 1 − ρ.conclusionR.w₀ = R.ρProof (Lean source)
theorem w0_eq_rho : R.w₀ = R.ρ := by have h := R.weights_sum_one rw [R.equalDispersion] at h; linarith
GeneralCondExp 1 core · 6 supporting This file proves the continuous-covariate saturated ordinary least squares ratio identity using conditional expectation with respect to an arbitrary covariate σ-algebra. ★ saturated_ols_overlap_weighted_ate
Słoczyński General Conditional Expectation
This file proves the continuous-covariate saturated ordinary least squares
ratio identity using conditional expectation with respect to an arbitrary
covariate σ-algebra. The helper lemmas denom_identity and numer_identity
identify the Frisch-Waugh-Lovell denominator and numerator after residualizing
treatment on m. The headline theorem saturated_ols_overlap_weighted_ate
then shows that, under binary treatment, consistency, integrability, factored
conditional-mean-independence, and strictly positive integrated overlap, the
residualized treatment ratio equals the corresponding overlap-weighted
conditional-treatment-effect ratio.
theorem saturated_ols_overlap_weighted_ate reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition
Saturated-control OLS overlap-weighted ATE identity. Fix a covariate σ-algebra m at most as fine as the ambient one, and outcome, treatment, and potential-outcome functions D, Y, Y0, Y1. Suppose treatment is binary almost everywhere, D is integrable, D·Y1 is integrable, and (1−D)·Y0 is integrable. Suppose also consistency: the observed outcome equals D·Y1 + (1−D)·Y0 almost everywhere, and the factored conditional-mean-independence conditions μ[D·Y1 ∣ m] equals μ[D∣m]·μ[Y1∣m] almost everywhere and μ[(1−D)·Y0 ∣ m] equals μ[1−D∣m]·μ[Y0∣m] almost everywhere. Then the saturated-control OLS residualized treatment-outcome ratio E[(D−μ[D∣m])·Y] / E[(D−μ[D∣m])²] equals the overlap-weighted average of conditional treatment effects E[μ[D∣m]·(1−μ[D∣m])·(μ[Y1∣m]−μ[Y0∣m])] / E[μ[D∣m]·(1−μ[D∣m])], using Lean's totalized division convention so the identity also covers the zero-denominator case. This is the paper-facing statement corresponding to LaTeX thm:po-estimand-sloczynski-ols-overlap-weighted-ate.
Formal statement
hypotheses
hm :
m ≤ mΩ
D Y Y0 Y1 :
Ω → ℝ
hDbin :
∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1
hD_int :
Integrable D μ
hDY1_int :
Integrable (fun ω => D ω * Y1 ω) μ
h1DY0_int :
Integrable (fun ω => (1 - D ω) * Y0 ω) μ
hcons :
Y =ᵐ[μ] fun ω => D ω * Y1 ω + (1 - D ω) * Y0 ω
hCMI1 :
μ[(fun ω => D ω * Y1 ω) | m] =ᵐ[μ] fun ω => (μ[D | m]) ω * (μ[Y1 | m]) ω
hCMI0 :
μ[(fun ω => (1 - D ω) * Y0 ω) | m]
=ᵐ[μ] fun ω => (μ[(fun ω => 1 - D ω) | m]) ω * (μ[Y0 | m]) ω
conclusion
(∫ ω, (D ω - (μ[D | m]) ω) * Y ω ∂μ) / (∫ ω, (D ω - (μ[D | m]) ω) ^ 2 ∂μ)
= (∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) * ((μ[Y1 | m]) ω - (μ[Y0 | m]) ω) ∂μ) / (∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) ∂μ)
Proof (Lean source)
theorem saturated_ols_overlap_weighted_ate (hm : m ≤ mΩ)
(D Y Y0 Y1 : Ω → ℝ) (hDbin : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1)
(hD_int : Integrable D μ)
(hDY1_int : Integrable (fun ω => D ω * Y1 ω) μ)
(h1DY0_int : Integrable (fun ω => (1 - D ω) * Y0 ω) μ)
(hcons : Y =ᵐ[μ] fun ω => D ω * Y1 ω + (1 - D ω) * Y0 ω)
(hCMI1 : μ[(fun ω => D ω * Y1 ω) | m] =ᵐ[μ] fun ω => (μ[D | m]) ω * (μ[Y1 | m]) ω)
(hCMI0 : μ[(fun ω => (1 - D ω) * Y0 ω) | m]
=ᵐ[μ] fun ω => (μ[(fun ω => 1 - D ω) | m]) ω * (μ[Y0 | m]) ω) :
(∫ ω, (D ω - (μ[D | m]) ω) * Y ω ∂μ) / (∫ ω, (D ω - (μ[D | m]) ω) ^ 2 ∂μ)
= (∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) * ((μ[Y1 | m]) ω - (μ[Y0 | m]) ω) ∂μ)
/ (∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) ∂μ) := by
exact saturated_ols_overlap_weighted_ate_core μ hm D Y Y0 Y1 hDbin hD_int
hDY1_int h1DY0_int hcons hCMI1 hCMI0
6 supporting declarations (lemmas, instances)
-
condExp_one_sublemma — The conditional expectation of one minus an integrable real-valued variable, given a sub-σ-algebra, equals one minus that variable's conditional expectation almost surely.hypothesesconclusionμ[(fun ω => 1 - D ω) | m] =ᵐ[μ] fun ω => 1 - (μ[D | m]) ωProof (Lean source)
lemma condExp_one_sub (hm : m ≤ mΩ) {D : Ω → ℝ} (hD_int : Integrable D μ) : μ[(fun ω => 1 - D ω) | m] =ᵐ[μ] fun ω => 1 - (μ[D | m]) ω := by have hone : (fun ω : Ω => 1 - D ω) = (fun _ : Ω => (1 : ℝ)) - D := by funext ω; simp [Pi.sub_apply] rw [hone] have hsub := condExp_sub (μ := μ) (integrable_const (1 : ℝ)) hD_int m refine hsub.trans ?_ have hc : μ[(fun _ : Ω => (1 : ℝ)) | m] = fun _ => (1 : ℝ) := condExp_const hm (1 : ℝ) filter_upwards [] with ω simp [Pi.sub_apply, hc] -
condExp_D_boundslemma — A real-valued variable that is zero or one almost surely has conditional expectation, given a sub-σ-algebra, between zero and one almost surely.hypothesesconclusion(∀ᵐ ω ∂μ, 0 ≤ (μ[D | m]) ω) ∧ (∀ᵐ ω ∂μ, (μ[D | m]) ω ≤ 1)Proof (Lean source)
lemma condExp_D_bounds (hm : m ≤ mΩ) {D : Ω → ℝ} (hD_int : Integrable D μ) (hDbin : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1) : (∀ᵐ ω ∂μ, 0 ≤ (μ[D | m]) ω) ∧ (∀ᵐ ω ∂μ, (μ[D | m]) ω ≤ 1) := by have h0 : (0 : Ω → ℝ) ≤ᵐ[μ] D := by filter_upwards [hDbin] with ω hω; rcases hω with h | h <;> simp [h] have h1 : D ≤ᵐ[μ] fun _ => (1 : ℝ) := by filter_upwards [hDbin] with ω hω; rcases hω with h | h <;> simp [h] refine ⟨condExp_nonneg h0, ?_⟩ have hmono := condExp_mono (m := m) hD_int (integrable_const (1 : ℝ)) h1 have hc : μ[(fun _ : Ω => (1 : ℝ)) | m] = fun _ => (1 : ℝ) := condExp_const hm (1 : ℝ) filter_upwards [hmono] with ω hω rwa [hc] at hω -
condExp_D_norm_lelemma — The conditional expectation of a real-valued variable that is zero or one almost surely has absolute value at most one almost surely.hypothesesconclusion∀ᵐ ω ∂μ, ‖(μ[D | m]) ω‖ ≤ 1Proof (Lean source)
lemma condExp_D_norm_le (hm : m ≤ mΩ) {D : Ω → ℝ} (hD_int : Integrable D μ) (hDbin : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1) : ∀ᵐ ω ∂μ, ‖(μ[D | m]) ω‖ ≤ 1 := by obtain ⟨hlo, hhi⟩ := condExp_D_bounds μ hm hD_int hDbin filter_upwards [hlo, hhi] with ω h0 h1 rw [Real.norm_eq_abs, abs_le]; exact ⟨by linarith, h1⟩ -
denom_identitylemma — Denominator identity (A). For binary D, ∫ (D − μ[D | m])² ∂μ = ∫ μ[D | m]·(1 − μ[D | m]) ∂μ.hypothesesconclusion(∫ ω, (D ω - (μ[D | m]) ω) ^ 2 ∂μ) = ∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) ∂μProof (Lean source)
lemma denom_identity (hm : m ≤ mΩ) (D : Ω → ℝ) (hDbin : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1) (hD_int : Integrable D μ) : (∫ ω, (D ω - (μ[D | m]) ω) ^ 2 ∂μ) = ∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) ∂μ := by haveI : IsFiniteMeasure (μ.trim hm) := isFiniteMeasure_trim hm set p : Ω → ℝ := μ[D | m] with hp have hp_sm : StronglyMeasurable[m] p := stronglyMeasurable_condExp have hp_int : Integrable p μ := integrable_condExp have hp_bound : ∀ᵐ ω ∂μ, ‖p ω‖ ≤ 1 := condExp_D_norm_le μ hm hD_int hDbin have hp_aesm : AEStronglyMeasurable p μ := (hp_sm.mono hm).aestronglyMeasurable -- Integrabilities of the products (`p` is a.e. bounded by 1). have hpD_int : Integrable (fun ω => p ω * D ω) μ := hD_int.bdd_mul hp_aesm hp_bound have hp2_int : Integrable (fun ω => p ω * p ω) μ := hp_int.bdd_mul hp_aesm hp_bound -- Expand `(D-p)² =ᵐ D - 2*(p*D) + p*p` (using `D² =ᵐ D`). have hexp : (fun ω => (D ω - p ω) ^ 2) =ᵐ[μ] fun ω => D ω - 2 * (p ω * D ω) + p ω * p ω := by filter_upwards [hDbin] with ω hω rcases hω with h | h <;> rw [h] <;> ring -- `∫ p*D = ∫ p*p`, via pull-out of the m-measurable `p` and `integral_condExp`. have hpullout : μ[(fun ω => p ω * D ω) | m] =ᵐ[μ] fun ω => p ω * (μ[D | m]) ω := condExp_mul_of_stronglyMeasurable_left hp_sm hpD_int hD_int have hpD_eq_pp : (∫ ω, p ω * D ω ∂μ) = ∫ ω, p ω * p ω ∂μ := by rw [← integral_condExp hm (f := fun ω => p ω * D ω)] refine integral_congr_ae ?_ filter_upwards [hpullout] with ω hω; rw [hω] -- `∫ D = ∫ p`. have hD_eq_p : (∫ ω, D ω ∂μ) = ∫ ω, p ω ∂μ := by rw [hp]; exact (integral_condExp hm).symm -- Integral of the expansion via linearity (`∫ (f + g) = ∫ f + ∫ g` etc.). have h2pD_int : Integrable (fun ω => 2 * (p ω * D ω)) μ := hpD_int.const_mul 2 have hint_exp : (∫ ω, (D ω - 2 * (p ω * D ω) + p ω * p ω) ∂μ) = (∫ ω, D ω ∂μ) - 2 * (∫ ω, p ω * D ω ∂μ) + ∫ ω, p ω * p ω ∂μ := by rw [integral_add (μ := μ) (f := fun ω => D ω - 2 * (p ω * D ω)) (g := fun ω => p ω * p ω) (hD_int.sub h2pD_int) hp2_int, integral_sub (μ := μ) (f := D) (g := fun ω => 2 * (p ω * D ω)) hD_int h2pD_int, integral_const_mul] -- Compute both sides via integral linearity. calc (∫ ω, (D ω - p ω) ^ 2 ∂μ) = ∫ ω, (D ω - 2 * (p ω * D ω) + p ω * p ω) ∂μ := integral_congr_ae hexp _ = (∫ ω, D ω ∂μ) - 2 * (∫ ω, p ω * D ω ∂μ) + ∫ ω, p ω * p ω ∂μ := hint_exp _ = (∫ ω, p ω ∂μ) - 2 * (∫ ω, p ω * p ω ∂μ) + ∫ ω, p ω * p ω ∂μ := by rw [hD_eq_p, hpD_eq_pp] _ = (∫ ω, p ω ∂μ) - ∫ ω, p ω * p ω ∂μ := by ring _ = ∫ ω, p ω * (1 - p ω) ∂μ := by rw [← integral_sub hp_int hp2_int] refine integral_congr_ae ?_ filter_upwards [] with ω; ring -
numer_identitylemma — Numerator identity (B). Under consistency and the factored conditional-mean-independence hypotheses, ∫ (D − μ[D | m])·Y ∂μ = ∫ μ[D | m]·(1 − μ[D | m])·(μ[Y1 | m] − μ[Y0 | m]) ∂μ.hypotheseshm :m ≤ mΩD Y Y0 Y1 :Ω → ℝhDbin :∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1hD_int :Integrable D μhDY1_int :Integrable (fun ω => D ω * Y1 ω) μh1DY0_int :Integrable (fun ω => (1 - D ω) * Y0 ω) μhcons :Y =ᵐ[μ] fun ω => D ω * Y1 ω + (1 - D ω) * Y0 ωhCMI1 :μ[(fun ω => D ω * Y1 ω) | m] =ᵐ[μ] fun ω => (μ[D | m]) ω * (μ[Y1 | m]) ωhCMI0 :μ[(fun ω => (1 - D ω) * Y0 ω) | m]=ᵐ[μ] fun ω => (μ[(fun ω => 1 - D ω) | m]) ω * (μ[Y0 | m]) ωconclusion(∫ ω, (D ω - (μ[D | m]) ω) * Y ω ∂μ)= ∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) * ((μ[Y1 | m]) ω - (μ[Y0 | m]) ω) ∂μProof (Lean source)
lemma numer_identity (hm : m ≤ mΩ) (D Y Y0 Y1 : Ω → ℝ) (hDbin : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1) (hD_int : Integrable D μ) (hDY1_int : Integrable (fun ω => D ω * Y1 ω) μ) (h1DY0_int : Integrable (fun ω => (1 - D ω) * Y0 ω) μ) (hcons : Y =ᵐ[μ] fun ω => D ω * Y1 ω + (1 - D ω) * Y0 ω) (hCMI1 : μ[(fun ω => D ω * Y1 ω) | m] =ᵐ[μ] fun ω => (μ[D | m]) ω * (μ[Y1 | m]) ω) (hCMI0 : μ[(fun ω => (1 - D ω) * Y0 ω) | m] =ᵐ[μ] fun ω => (μ[(fun ω => 1 - D ω) | m]) ω * (μ[Y0 | m]) ω) : (∫ ω, (D ω - (μ[D | m]) ω) * Y ω ∂μ) = ∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) * ((μ[Y1 | m]) ω - (μ[Y0 | m]) ω) ∂μ := by haveI : IsFiniteMeasure (μ.trim hm) := isFiniteMeasure_trim hm set p : Ω → ℝ := μ[D | m] with hp set M1 : Ω → ℝ := μ[Y1 | m] with hM1 set M0 : Ω → ℝ := μ[Y0 | m] with hM0 have hp_sm : StronglyMeasurable[m] p := stronglyMeasurable_condExp have hp_bound : ∀ᵐ ω ∂μ, ‖p ω‖ ≤ 1 := condExp_D_norm_le μ hm hD_int hDbin have hp_aesm : AEStronglyMeasurable p μ := (hp_sm.mono hm).aestronglyMeasurable -- `1 - p` is `m`-strongly measurable and a.e. bounded by `2`. have h1p_sm : StronglyMeasurable[m] (fun ω => 1 - p ω) := stronglyMeasurable_const.sub hp_sm have h1p_aesm : AEStronglyMeasurable (fun ω => 1 - p ω) μ := (h1p_sm.mono hm).aestronglyMeasurable have h1p_bound : ∀ᵐ ω ∂μ, ‖1 - p ω‖ ≤ 2 := by filter_upwards [hp_bound] with ω hω calc ‖1 - p ω‖ ≤ ‖(1 : ℝ)‖ + ‖p ω‖ := norm_sub_le _ _ _ ≤ 1 + 1 := by rw [norm_one]; linarith [hω] _ = 2 := by norm_num -- Integrabilities. have ha_int : Integrable (fun ω => (1 - p ω) * (D ω * Y1 ω)) μ := hDY1_int.bdd_mul h1p_aesm h1p_bound have hb_int : Integrable (fun ω => p ω * ((1 - D ω) * Y0 ω)) μ := h1DY0_int.bdd_mul hp_aesm hp_bound -- Consistency + binary `D`: `(D-p)·Y =ᵐ (1-p)·(D·Y1) - p·((1-D)·Y0)`. have hsplit : (fun ω => (D ω - p ω) * Y ω) =ᵐ[μ] fun ω => (1 - p ω) * (D ω * Y1 ω) - p ω * ((1 - D ω) * Y0 ω) := by filter_upwards [hcons, hDbin] with ω hY hD rw [hY]; rcases hD with h | h <;> rw [h] <;> ring -- `μ[1-D | m] =ᵐ 1 - p`. have h1D : μ[(fun ω => 1 - D ω) | m] =ᵐ[μ] fun ω => 1 - p ω := condExp_one_sub μ hm hD_int -- Term A: `∫ (1-p)(D·Y1) = ∫ (1-p)·p·M1`. have hpullA : μ[(fun ω => (1 - p ω) * (D ω * Y1 ω)) | m] =ᵐ[μ] fun ω => (1 - p ω) * (μ[(fun ω => D ω * Y1 ω) | m]) ω := condExp_mul_of_stronglyMeasurable_left h1p_sm ha_int hDY1_int have hA : (∫ ω, (1 - p ω) * (D ω * Y1 ω) ∂μ) = ∫ ω, (1 - p ω) * (p ω * M1 ω) ∂μ := by rw [← integral_condExp hm (f := fun ω => (1 - p ω) * (D ω * Y1 ω))] refine integral_congr_ae ?_ filter_upwards [hpullA, hCMI1] with ω h1 h2; rw [h1, h2] -- Term B: `∫ p((1-D)Y0) = ∫ p·(1-p)·M0`. have hpullB : μ[(fun ω => p ω * ((1 - D ω) * Y0 ω)) | m] =ᵐ[μ] fun ω => p ω * (μ[(fun ω => (1 - D ω) * Y0 ω) | m]) ω := condExp_mul_of_stronglyMeasurable_left hp_sm hb_int h1DY0_int have hB : (∫ ω, p ω * ((1 - D ω) * Y0 ω) ∂μ) = ∫ ω, p ω * ((1 - p ω) * M0 ω) ∂μ := by rw [← integral_condExp hm (f := fun ω => p ω * ((1 - D ω) * Y0 ω))] refine integral_congr_ae ?_ filter_upwards [hpullB, hCMI0, h1D] with ω h1 h2 h3 rw [h1, h2, h3] -- Assemble. calc (∫ ω, (D ω - p ω) * Y ω ∂μ) = ∫ ω, ((1 - p ω) * (D ω * Y1 ω) - p ω * ((1 - D ω) * Y0 ω)) ∂μ := integral_congr_ae hsplit _ = (∫ ω, (1 - p ω) * (D ω * Y1 ω) ∂μ) - ∫ ω, p ω * ((1 - D ω) * Y0 ω) ∂μ := by simp only [integral_sub ha_int hb_int] _ = (∫ ω, (1 - p ω) * (p ω * M1 ω) ∂μ) - ∫ ω, p ω * ((1 - p ω) * M0 ω) ∂μ := by rw [hA, hB] _ = ∫ ω, p ω * (1 - p ω) * (M1 ω - M0 ω) ∂μ := by -- `1-p` bounded by 2, `p` bounded by 1, so the coefficients are bounded by 2. have hM1_int : Integrable M1 μ := integrable_condExp have hM0_int : Integrable M0 μ := integrable_condExp have hcoeff_bound : ∀ᵐ ω ∂μ, ‖(1 - p ω) * p ω‖ ≤ 2 := by filter_upwards [hp_bound, h1p_bound] with ω hp1 h1p calc ‖(1 - p ω) * p ω‖ = ‖1 - p ω‖ * ‖p ω‖ := by rw [norm_mul] _ ≤ 2 * 1 := mul_le_mul h1p hp1 (norm_nonneg _) (by norm_num) _ = 2 := by norm_num have hA_int : Integrable (fun ω => (1 - p ω) * (p ω * M1 ω)) μ := by have : (fun ω => (1 - p ω) * (p ω * M1 ω)) = (fun ω => ((1 - p ω) * p ω) * M1 ω) := by funext ω; ring rw [this] exact hM1_int.bdd_mul ((h1p_aesm.mul hp_aesm)) hcoeff_bound have hB_int : Integrable (fun ω => p ω * ((1 - p ω) * M0 ω)) μ := by have : (fun ω => p ω * ((1 - p ω) * M0 ω)) = (fun ω => ((1 - p ω) * p ω) * M0 ω) := by funext ω; ring rw [this] exact hM0_int.bdd_mul ((h1p_aesm.mul hp_aesm)) hcoeff_bound rw [← integral_sub hA_int hB_int] refine integral_congr_ae ?_ filter_upwards [] with ω; ring -
saturated_ols_overlap_weighted_ate_coretheorem — Positivity-free core of the saturated-control OLS overlap-weighted ratio identity. Both ratios are totalized, so the algebraic equality also holds when the common denominator is zero.hypotheseshm :m ≤ mΩD Y Y0 Y1 :Ω → ℝhDbin :∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1hD_int :Integrable D μhDY1_int :Integrable (fun ω => D ω * Y1 ω) μh1DY0_int :Integrable (fun ω => (1 - D ω) * Y0 ω) μhcons :Y =ᵐ[μ] fun ω => D ω * Y1 ω + (1 - D ω) * Y0 ωhCMI1 :μ[(fun ω => D ω * Y1 ω) | m] =ᵐ[μ] fun ω => (μ[D | m]) ω * (μ[Y1 | m]) ωhCMI0 :μ[(fun ω => (1 - D ω) * Y0 ω) | m]=ᵐ[μ] fun ω => (μ[(fun ω => 1 - D ω) | m]) ω * (μ[Y0 | m]) ωconclusion(∫ ω, (D ω - (μ[D | m]) ω) * Y ω ∂μ) / (∫ ω, (D ω - (μ[D | m]) ω) ^ 2 ∂μ)= (∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) * ((μ[Y1 | m]) ω - (μ[Y0 | m]) ω) ∂μ) / (∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) ∂μ)Proof (Lean source)
theorem saturated_ols_overlap_weighted_ate_core (hm : m ≤ mΩ) (D Y Y0 Y1 : Ω → ℝ) (hDbin : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1) (hD_int : Integrable D μ) (hDY1_int : Integrable (fun ω => D ω * Y1 ω) μ) (h1DY0_int : Integrable (fun ω => (1 - D ω) * Y0 ω) μ) (hcons : Y =ᵐ[μ] fun ω => D ω * Y1 ω + (1 - D ω) * Y0 ω) (hCMI1 : μ[(fun ω => D ω * Y1 ω) | m] =ᵐ[μ] fun ω => (μ[D | m]) ω * (μ[Y1 | m]) ω) (hCMI0 : μ[(fun ω => (1 - D ω) * Y0 ω) | m] =ᵐ[μ] fun ω => (μ[(fun ω => 1 - D ω) | m]) ω * (μ[Y0 | m]) ω) : (∫ ω, (D ω - (μ[D | m]) ω) * Y ω ∂μ) / (∫ ω, (D ω - (μ[D | m]) ω) ^ 2 ∂μ) = (∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) * ((μ[Y1 | m]) ω - (μ[Y0 | m]) ω) ∂μ) / (∫ ω, (μ[D | m]) ω * (1 - (μ[D | m]) ω) ∂μ) := by rw [denom_identity μ hm D hDbin hD_int, numer_identity μ hm D Y Y0 Y1 hDbin hD_int hDY1_int h1DY0_int hcons hCMI1 hCMI0]
OverlapWeightedATE 1 core · 0 supporting This file holds the finite-cell headline theorem of the module: starting from a probability space with a binary treatment, potential outcomes, and a finite covariate G, the saturated-OLS residualized coefficient is ident ★ bridge_finite_residualized_eq_overlap
Słoczyński finite-cell overlap-weighted ATE (headline)
This file holds the finite-cell headline theorem of the module: starting
from a probability space with a binary treatment, potential outcomes, and a
finite covariate G, the saturated-OLS residualized coefficient is identified
with the overlap-weighted average treatment effect
Σ ω_g · E[Y(1)−Y(0) ∣ G=g]. This is where the abstract FinitePartition
algebra acquires its causal content; the Support/ files provide the
per-cell measure-theoretic machinery. The continuous-covariate counterpart is
GeneralCondExp.lean.
theorem bridge_finite_residualized_eq_overlap reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.OLSWeightDecomposition
Finite-cell saturated-OLS bridge to the overlap-weighted average treatment effect. For a probability space (Ω, μ) with a measurable binary treatment D, an outcome Y, square-integrable potential outcomes Y0, Y1, and a measurable finite covariate G, suppose treatment is binary almost everywhere, the observed outcome is consistent — Y equals D·Y1 + (1−D)·Y0 almost everywhere, the integrated-indicator finite-cell bridge condition holds, a finite-cell operational substitute for full conditional-mean independence of the potential outcomes given treatment and the covariate, and the covariate cells have nondegenerate treatment overlap. Then the saturated-OLS residualized coefficient of Y on D given G equals the overlap-weighted average treatment effect Σ_g ω_g · E[Y(1)−Y(0) ∣ G=g] built from the potential outcomes Y0, Y1:
Formal statement
hypotheses
Ω 𝒢 :
μ :
D Y Y0 Y1 :
Ω → ℝ
G :
Ω → 𝒢
B_meas_G :
B_meas_D :
B_binary :
∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1
B_Y0_L2 :
MemLp Y0 2 μ
B_Y1_L2 :
MemLp Y1 2 μ
B_consis :
Y =ᵐ[μ] fun ω => D ω * Y1 ω + (1 - D ω) * Y0 ω
Finite-cell bridge condition implied by the usual CMI clause `E[Y(d) | D, G] = E[Y(d) | G]`; this integrated-indicator form is used directly in the cell algebra and is not stated as an equivalence to CMI.
B_CMI :
∀ (d : ℝ) (g : 𝒢)
if
d = 0 ∨ d = 1
conclusion
residualizedCoefficient μ (saturatedClass μ G B_meas_G) (residWitnessY μ Y G B_meas_G (Y_memLp_of_consistency μ B_meas_D B_binary B_Y0_L2 B_Y1_L2 B_consis)) (residWitnessD μ D G B_meas_G B_meas_D B_binary)
= FinitePartition.overlapWeightedATE (partitionOf μ D Y0 Y1 G B_meas_G B_binary B_overlap)
Proof (Lean source)
theorem bridge_finite_residualized_eq_overlap
{Ω 𝒢 : Type*} [MeasurableSpace Ω] [Fintype 𝒢]
[DecidableEq 𝒢] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢]
(μ : Measure Ω) [IsProbabilityMeasure μ]
(D Y Y0 Y1 : Ω → ℝ) (G : Ω → 𝒢)
(B_meas_G : Measurable G)
(B_meas_D : Measurable D)
(B_binary : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1)
(B_Y0_L2 : MemLp Y0 2 μ)
(B_Y1_L2 : MemLp Y1 2 μ)
(B_consis : Y =ᵐ[μ] fun ω => D ω * Y1 ω + (1 - D ω) * Y0 ω)
-- Finite-cell bridge condition implied by the usual CMI clause
-- `E[Y(d) | D, G] = E[Y(d) | G]`; this integrated-indicator form is used
-- directly in the cell algebra and is not stated as an equivalence to CMI.
(B_CMI : ∀ (d : ℝ) (g : 𝒢), d = 0 ∨ d = 1 →
∫ ω, (if d = 1 then Y1 ω else Y0 ω)
* indicator {ω' | D ω' = d} (fun _ => (1 : ℝ)) ω
* indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ
= (∫ ω, (if d = 1 then Y1 ω else Y0 ω)
* indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ)
* (if d = 1 then cellShare μ D G g else 1 - cellShare μ D G g))
(B_overlap : 0 < ∑ g, cellMass μ G g
* (cellShare μ D G g * (1 - cellShare μ D G g))) :
residualizedCoefficient μ (saturatedClass μ G B_meas_G)
(residWitnessY μ Y G B_meas_G
-- `Y_memLp` is derived from consistency, binary treatment, and the two
-- potential-outcome square-integrability assumptions.
(Y_memLp_of_consistency μ B_meas_D B_binary B_Y0_L2 B_Y1_L2 B_consis))
(residWitnessD μ D G B_meas_G B_meas_D B_binary)
= FinitePartition.overlapWeightedATE
(partitionOf μ D Y0 Y1 G B_meas_G B_binary B_overlap) := by
-- Bring derived Y_memLp into scope by name for readability.
have Y_memLp : MemLp Y 2 μ :=
Y_memLp_of_consistency μ B_meas_D B_binary B_Y0_L2 B_Y1_L2 B_consis
let H := saturatedClass μ G B_meas_G
let wY := residWitnessY μ Y G B_meas_G Y_memLp
let wD := residWitnessD μ D G B_meas_G B_meas_D B_binary
let P := partitionOf μ D Y0 Y1 G B_meas_G B_binary B_overlap
have hMeanReg_mem : H.mem (meanReg μ Y G) :=
meanReg_mem_saturatedClass μ Y G B_meas_G
have hNum_tilde :
∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ =
∫ ω, wD.Vtilde ω * Y ω ∂μ := by
have hDY_int : Integrable (fun ω => wD.Vtilde ω * Y ω) μ :=
wD.Vtilde_memLp.integrable_mul Y_memLp
have hDM_int : Integrable (fun ω => wD.Vtilde ω * meanReg μ Y G ω) μ :=
wD.Vtilde_memLp.integrable_mul (H.memLp hMeanReg_mem)
calc
∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ =
∫ ω, wD.Vtilde ω * Y ω
- wD.Vtilde ω * meanReg μ Y G ω ∂μ := by
refine integral_congr_ae ?_
filter_upwards [] with ω
simp [wY, residWitnessY]
ring
_ = ∫ ω, wD.Vtilde ω * Y ω ∂μ
- ∫ ω, wD.Vtilde ω * meanReg μ Y G ω ∂μ :=
integral_sub hDY_int hDM_int
_ = ∫ ω, wD.Vtilde ω * Y ω ∂μ := by
rw [wD.orthogonal hMeanReg_mem]
ring
have hDen_sum :
∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ =
∑ g, cellMass μ G g
* (cellShare μ D G g * (1 - cellShare μ D G g)) := by
have hF_int : Integrable (fun ω => wD.Vtilde ω * wD.Vtilde ω) μ :=
wD.Vtilde_memLp.integrable_mul wD.Vtilde_memLp
calc
∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ =
∑ g, ∫ ω, (wD.Vtilde ω * wD.Vtilde ω)
* indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ :=
integral_eq_sum_cell μ (fun ω => wD.Vtilde ω * wD.Vtilde ω)
G B_meas_G hF_int
_ = ∑ g, cellMass μ G g
* (cellShare μ D G g * (1 - cellShare μ D G g)) := by
refine Finset.sum_congr rfl (fun g _ => ?_)
simpa [wD, residWitnessD, mul_assoc] using
denom_per_cell μ D G B_meas_G B_meas_D B_binary g
have hNum_sum :
∫ ω, wD.Vtilde ω * Y ω ∂μ =
∑ g, cellMass μ G g
* (cellShare μ D G g * (1 - cellShare μ D G g))
* cellTau μ Y0 Y1 G g := by
have hF_int : Integrable (fun ω => wD.Vtilde ω * Y ω) μ :=
wD.Vtilde_memLp.integrable_mul Y_memLp
calc
∫ ω, wD.Vtilde ω * Y ω ∂μ =
∑ g, ∫ ω, (wD.Vtilde ω * Y ω)
* indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ :=
integral_eq_sum_cell μ (fun ω => wD.Vtilde ω * Y ω)
G B_meas_G hF_int
_ = ∑ g, cellMass μ G g
* (cellShare μ D G g * (1 - cellShare μ D G g))
* cellTau μ Y0 Y1 G g := by
refine Finset.sum_congr rfl (fun g _ => ?_)
simpa [wD, residWitnessD, mul_assoc] using
num_per_cell μ D Y Y0 Y1 G B_meas_G B_meas_D B_binary
B_Y0_L2 B_Y1_L2 B_consis B_CMI g
-- Derive residual-variation positivity from overlap via `hDen_sum`.
-- `hDen_sum` rewrites `∫ wD.Vtilde^2 dμ` to the cell-sum form, which
-- equals B_overlap. No separate B_Dtilde_pos hypothesis needed.
have hOverlapDen_ne :
(∑ g, cellMass μ G g
* (cellShare μ D G g * (1 - cellShare μ D G g))) ≠ 0 :=
B_overlap.ne'
have hP :
FinitePartition.overlapWeightedATE P =
(∑ g, cellMass μ G g
* (cellShare μ D G g * (1 - cellShare μ D G g))
* cellTau μ Y0 Y1 G g)
/ (∑ g, cellMass μ G g
* (cellShare μ D G g * (1 - cellShare μ D G g))) := by
simp [P, partitionOf, FinitePartition.overlapWeightedATE,
FinitePartition.overlapNumerator, FinitePartition.overlapDenominator,
FinitePartition.cellOverlap, mul_assoc]
have _ := hOverlapDen_ne
calc
residualizedCoefficient μ (saturatedClass μ G B_meas_G)
(residWitnessY μ Y G B_meas_G Y_memLp)
(residWitnessD μ D G B_meas_G B_meas_D B_binary)
= (∫ ω, wD.Vtilde ω * wY.Vtilde ω ∂μ)
/ (∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ) := by
rfl
_ = (∫ ω, wD.Vtilde ω * Y ω ∂μ)
/ (∫ ω, wD.Vtilde ω * wD.Vtilde ω ∂μ) := by
rw [hNum_tilde]
_ = (∑ g, cellMass μ G g
* (cellShare μ D G g * (1 - cellShare μ D G g))
* cellTau μ Y0 Y1 G g)
/ (∑ g, cellMass μ G g
* (cellShare μ D G g * (1 - cellShare μ D G g))) := by
rw [hNum_sum, hDen_sum]
_ = FinitePartition.overlapWeightedATE
(partitionOf μ D Y0 Y1 G B_meas_G B_binary B_overlap) := by
rw [hP]