Panel.EstimandCharacterization.StaggeredTWFEDecomposition.Support
Support layer for the Goodman-Bacon decomposition: saturated cohort-period classes, cell-mass identities, orthogonality lemmas, residualization witnesses, and per-cell numerator and denominator formulas.
Basic 11 core · 4 supporting Defines basic bridge objects for the staggered-TWFE decomposition. ★ panelPropensity_mem_panelClass★ panelMeanReg_mem_panelClass
Defines basic bridge objects for the staggered-TWFE decomposition. The module packages saturated cohort-period classes and finite panel support used to connect algebraic weighted panels to population integrals.
def panelClass reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Given a finite measure, a cohort classifier, a period classifier, a measurable cohort classifier, and a measurable period classifier, the saturated cohort-and-period function class consists of functions that agree almost everywhere with a linear combination of cohort and period indicator functions.
Definition (Lean source)
parameters
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
def
given by
CellBridge.twoAxisIndicatorSpan μ G T_rv G_meas T_meas
def cellMass reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measure, a cohort classifier, a period classifier, a cohort, and a period, the cohort-period cell mass is the real-valued mass of observations classified in that cohort-period cell.
def cohortMass reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measure, a cohort classifier, and a cohort, the cohort mass is the real-valued mass of observations classified in that cohort.
Definition (Lean source)
parameters
def
cohortMass μ G g :
ℝ
given by
CellBridge.cellMass μ G g
def periodMass reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measure, a period classifier, and a period, the period mass is the real-valued mass of observations classified in that period.
def cellMean reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measure, an outcome variable, a cohort classifier, a period classifier, a cohort, and a period, the cohort-period cell mean is the outcome integral over that cell divided by its mass, and is zero when the cell has zero mass.
def cohortBarD reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measure, a treatment variable, a cohort classifier, and a cohort, the cohort mean treatment share is the treatment integral over that cohort's cell divided by its mass, and is zero when the cell has zero mass.
Definition (Lean source)
parameters
def
cohortBarD μ D G g :
ℝ
given by
(∫ ω, D ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ) / cohortMass μ G g
def panelOf reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Given a measure, an outcome variable, a cohort classifier, a period classifier, an adoption-date schedule, a positive number of periods, strictly positive cohort masses, and cohort masses summing to one, the cohort panel constructed from the law has those cohort masses as shares, the supplied adoption dates, and cohort-period outcome means.
Definition (Lean source)
parameters
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
Measure Ω
Y :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
hT_pos :
0 < T
hp_pos :
∀ g, 0 < cohortMass μ G g
hp_sum :
∑ g, cohortMass μ G g = 1
def
given by
{ p := cohortMass μ G , A := A , Y := cellMean μ Y G T_rv , T_pos := hT_pos , p_pos := hp_pos , p_sum_one := hp_sum }
def panelPropensity reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measure, a treatment variable, a cohort classifier, and a period classifier, the saturated cohort-and-period propensity regression assigns each observation its cohort mean treatment plus its period mean treatment minus the overall mean treatment.
Definition (Lean source)
parameters
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
Measure Ω
D :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
def
panelPropensity μ D G T_rv :
Ω → ℝ
given by
fun ω
=> (∑ g, cohortBarD μ D G g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω)
+ (∑ t, ((∫ ω', D ω' * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ) / periodMass μ T_rv t - ∫ ω', D ω' ∂μ) * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω)
def panelMeanReg reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measure, an outcome variable, a cohort classifier, and a period classifier, the saturated cohort-and-period outcome regression assigns each observation its cohort mean outcome plus its period mean outcome minus the overall mean outcome.
Definition (Lean source)
parameters
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
Measure Ω
Y :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
def
panelMeanReg μ Y G T_rv :
Ω → ℝ
given by
fun ω
=> (∑ g, ((∫ ω', Y ω' * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω' ∂μ) / cohortMass μ G g) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω)
+ (∑ t, ((∫ ω', Y ω' * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ) / periodMass μ T_rv t - ∫ ω', Y ω' ∂μ) * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω)
theorem panelPropensity_mem_panelClass reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a finite measure μ, a treatment variable D, a measurable cohort map G, and a measurable period map T_rv, the pointwise saturated cohort-and-period propensity regression of D belongs to the two-axis additive (cohort-plus-period) function class.
Formal statement
hypotheses
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
D :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
conclusion
Proof (Lean source)
theorem panelPropensity_mem_panelClass
(μ : Measure Ω) [IsFiniteMeasure μ]
(D : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T)
(G_meas : Measurable G) (T_meas : Measurable T_rv) :
(panelClass μ G T_rv G_meas T_meas).mem (panelPropensity μ D G T_rv) := by
unfold panelClass CellBridge.twoAxisIndicatorSpan
refine ⟨fun g => cohortBarD μ D G g,
fun t => (∫ ω', D ω'
* indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ)
/ periodMass μ T_rv t
- ∫ ω', D ω' ∂μ, ?_⟩
filter_upwards [] with ω
rfl
theorem panelMeanReg_mem_panelClass reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a finite measure μ, an outcome variable Y, a measurable cohort map G, and a measurable period map T_rv, the pointwise saturated cohort-and-period mean regression of Y belongs to the two-axis additive (cohort-plus-period) function class.
Formal statement
hypotheses
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
Y :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
conclusion
Proof (Lean source)
theorem panelMeanReg_mem_panelClass
(μ : Measure Ω) [IsFiniteMeasure μ]
(Y : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T)
(G_meas : Measurable G) (T_meas : Measurable T_rv) :
(panelClass μ G T_rv G_meas T_meas).mem (panelMeanReg μ Y G T_rv) := by
unfold panelClass CellBridge.twoAxisIndicatorSpan
refine ⟨fun g => (∫ ω', Y ω'
* indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω' ∂μ)
/ cohortMass μ G g,
fun t => (∫ ω', Y ω'
* indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ)
/ periodMass μ T_rv t
- ∫ ω', Y ω' ∂μ, ?_⟩
filter_upwards [] with ω
rfl
4 supporting declarations (lemmas, instances)
-
cellMean_eq_cellBridgetheorem — The panel cell mean for a cohort and period equals the generic cell-mean operator applied to the joint cohort-period cell.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :Measure ΩY :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin Tg :𝒢t :Fin TconclusioncellMean μ Y G T_rv g t = CellBridge.cellMean μ Y (fun ω => (G ω, T_rv ω)) (g, t)Proof (Lean source)
theorem cellMean_eq_cellBridge (μ : Measure Ω) (Y : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) (g : 𝒢) (t : Fin T) : cellMean μ Y G T_rv g t = CellBridge.cellMean μ Y (fun ω => (G ω, T_rv ω)) (g, t) := by classical unfold cellMean CellBridge.cellMean cellMass CellBridge.jointCellMass CellBridge.cellMass congr 2 · ext ω simp · congr 1 ext ω simp -
cohortMass_nonnegtheorem — Cohort mass is nonnegative.hypothesesconclusion0 ≤ cohortMass μ G gProof (Lean source)
theorem cohortMass_nonneg (μ : Measure Ω) (G : Ω → 𝒢) (g : 𝒢) : 0 ≤ cohortMass μ G g := ENNReal.toReal_nonneg -
periodMass_nonnegtheorem — Period mass is nonnegative.hypothesesconclusion0 ≤ periodMass μ T_rv tProof (Lean source)
theorem periodMass_nonneg (μ : Measure Ω) (T_rv : Ω → Fin T) (t : Fin T) : 0 ≤ periodMass μ T_rv t := ENNReal.toReal_nonneg
Orthogonality 2 core · 8 supporting This file proves the cohort-axis and period-axis orthogonality conditions needed for the measure-theoretic Goodman-Bacon bridge. ★ residD_cohort_orthogonal
Goodman-Bacon Bridge Orthogonality
This file proves the cohort-axis and period-axis orthogonality conditions needed for the measure-theoretic Goodman-Bacon bridge. Under the balanced cell-mass product condition, residuals from the panel propensity and mean regressions are orthogonal to the saturated cohort and period indicator class.
def IsBalancedPanelLaw reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measure, a cohort classifier, and a period classifier, the balanced-panel-law condition states that every cohort-period cell has mass equal to the product of its cohort marginal mass and its period marginal mass.
Definition (Lean source)
parameters
def
IsBalancedPanelLaw μ G T_rv :
Prop
given by
cellMass μ G T_rv g t = cohortMass μ G g * periodMass μ T_rv t
theorem residD_cohort_orthogonal reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a treatment indicator D that is binary almost everywhere, the residual between D and its cohort-period propensity score panelPropensity is orthogonal, in the L²(μ) sense, to every cohort indicator 𝟙{G = g}.
Formal statement
hypotheses
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
D :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
D_meas :
D_binary :
∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1
B_balanced :
IsBalancedPanelLaw μ G T_rv
g :
𝒢
conclusion
∫ ω, (D ω - panelPropensity μ D G T_rv ω) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ
= 0
Proof (Lean source)
theorem residD_cohort_orthogonal
(μ : Measure Ω) [IsProbabilityMeasure μ]
(D : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T)
(G_meas : Measurable G) (T_meas : Measurable T_rv)
(D_meas : Measurable D)
(D_binary : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1)
(B_balanced : IsBalancedPanelLaw μ G T_rv) (g : 𝒢) :
∫ ω, (D ω - panelPropensity μ D G T_rv ω)
* indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = 0 := by
classical
have hD_mem : MemLp D 2 μ :=
memLp_two_of_binary μ D D_meas D_binary
have hproj : panelPropensity μ D G T_rv = panelMeanReg μ D G T_rv := by
funext ω
simp [panelPropensity, panelMeanReg, cohortBarD]
simpa [hproj] using
panelMeanReg_cohort_axis_orthogonal μ D G T_rv G_meas T_meas
hD_mem B_balanced g
8 supporting declarations (lemmas, instances)
-
memLp_two_of_binarytheorem — Under a probability measure, a measurable real-valued variable that equals either zero or one almost surely has a finite second moment.hypothesesΩ :sharedType u_1μ :D :Ω → ℝD_meas :D_binary :∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1conclusionMemLp D 2 μProof (Lean source)
theorem memLp_two_of_binary (μ : Measure Ω) [IsProbabilityMeasure μ] (D : Ω → ℝ) (D_meas : Measurable D) (D_binary : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1) : MemLp D 2 μ := by have hD_bounded : ∀ᵐ ω ∂μ, D ω ∈ Icc (-1 : ℝ) 1 := by filter_upwards [D_binary] with ω hD rcases hD with hD0 | hD1 · simp [hD0] · simp [hD1] exact memLp_of_bounded (f := D) hD_bounded D_meas.aestronglyMeasurable (2 : ENNReal) -
sum_periodMass_eq_onetheorem — Under a probability distribution, the probabilities assigned to every period by a measurable finite-valued period variable sum to one.hypothesesconclusion∑ t, periodMass μ T_rv t = 1Proof (Lean source)
theorem sum_periodMass_eq_one (μ : Measure Ω) [IsProbabilityMeasure μ] (T_rv : Ω → Fin T) (T_meas : Measurable T_rv) : ∑ t, periodMass μ T_rv t = 1 := by have hOneInt : Integrable (fun _ : Ω => (1 : ℝ)) μ := integrable_const (1 : ℝ) calc ∑ t, periodMass μ T_rv t = ∑ t, ∫ ω, (fun _ : Ω => (1 : ℝ)) ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ := by refine Finset.sum_congr rfl ?_ intro t _ simpa [periodMass] using (CellBridge.integral_cell_indicator_one_eq_cellMass μ T_rv T_meas t).symm _ = ∫ ω, (1 : ℝ) ∂μ := by rw [CellBridge.integral_eq_sum_cell μ (fun _ : Ω => (1 : ℝ)) T_rv T_meas hOneInt] _ = 1 := by simp -
period_centered_sum_eq_zerotheorem — Under a probability distribution, period-specific means of an integrable outcome, centered by the overall mean and weighted by their period probabilities, sum to zero.hypothesesΩ :sharedType u_1T :sharedℕμ :F :Ω → ℝT_rv :Ω → Fin TT_meas :Measurable T_rvF_int :Integrable F μconclusion∑ t, (((∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ) / periodMass μ T_rv t) - ∫ ω, F ω ∂μ) * periodMass μ T_rv t= 0Proof (Lean source)
theorem period_centered_sum_eq_zero (μ : Measure Ω) [IsProbabilityMeasure μ] (F : Ω → ℝ) (T_rv : Ω → Fin T) (T_meas : Measurable T_rv) (F_int : Integrable F μ) : ∑ t, (((∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ) / periodMass μ T_rv t) - ∫ ω, F ω ∂μ) * periodMass μ T_rv t = 0 := by have hdiv : ∀ t, ((∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ) / periodMass μ T_rv t) * periodMass μ T_rv t = ∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ := fun t => period_integral_div_mul_periodMass μ F T_rv t calc ∑ t, (((∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ) / periodMass μ T_rv t) - ∫ ω, F ω ∂μ) * periodMass μ T_rv t = (∑ t, ∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ) - (∫ ω, F ω ∂μ) * ∑ t, periodMass μ T_rv t := by simp only [sub_mul, Finset.sum_sub_distrib, Finset.mul_sum] congr 1 exact Finset.sum_congr rfl (fun t _ => hdiv t) _ = (∫ ω, F ω ∂μ) - (∫ ω, F ω ∂μ) * 1 := by rw [← integral_eq_sum_period μ F T_rv T_meas F_int, sum_periodMass_eq_one μ T_rv T_meas] _ = 0 := by ring -
panelMeanReg_cohort_axis_orthogonaltheorem — Under a balanced panel law, the residual from the panel mean regression has zero average product with the indicator of any fixed cohort.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :F :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin TG_meas :T_meas :Measurable T_rvF_memLp :MemLp F 2 μB_balanced :IsBalancedPanelLaw μ G T_rvg :𝒢conclusion∫ ω, (F ω - panelMeanReg μ F G T_rv ω) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ= 0Proof (Lean source)
theorem panelMeanReg_cohort_axis_orthogonal (μ : Measure Ω) [IsProbabilityMeasure μ] (F : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) (G_meas : Measurable G) (T_meas : Measurable T_rv) (F_memLp : MemLp F 2 μ) (B_balanced : IsBalancedPanelLaw μ G T_rv) (g : 𝒢) : ∫ ω, (F ω - panelMeanReg μ F G T_rv ω) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = 0 := by classical let IG : 𝒢 → Ω → ℝ := fun g ω => indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω let IT : Fin T → Ω → ℝ := fun t ω => indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω let a : 𝒢 → ℝ := fun g => (∫ ω, F ω * IG g ω ∂μ) / cohortMass μ G g let b : Fin T → ℝ := fun t => (∫ ω, F ω * IT t ω ∂μ) / periodMass μ T_rv t - ∫ ω, F ω ∂μ have hF_int : Integrable F μ := F_memLp.integrable (by norm_num : (1 : ENNReal) ≤ 2) have hIG : MemLp (IG g) 2 μ := by simpa [IG] using indicator_cohort_memLp μ G G_meas g have hFI_int : Integrable (fun ω => F ω * IG g ω) μ := F_memLp.integrable_mul hIG have hPanel_mem : MemLp (panelMeanReg μ F G T_rv) 2 μ := (panelClass μ G T_rv G_meas T_meas).memLp (panelMeanReg_mem_panelClass μ F G T_rv G_meas T_meas) have hPanelI_int : Integrable (fun ω => panelMeanReg μ F G T_rv ω * IG g ω) μ := hPanel_mem.integrable_mul hIG have hsumG_mem : MemLp (fun ω => ∑ g', a g' * IG g' ω) 2 μ := (panelClass μ G T_rv G_meas T_meas).memLp ⟨a, fun _ => 0, by filter_upwards [] with ω; simp [IG]⟩ have hsumT_mem : MemLp (fun ω => ∑ t, b t * IT t ω) 2 μ := (panelClass μ G T_rv G_meas T_meas).memLp ⟨fun _ => 0, b, by filter_upwards [] with ω; simp [IT]⟩ have hsumGI_int : Integrable (fun ω => (∑ g', a g' * IG g' ω) * IG g ω) μ := hsumG_mem.integrable_mul hIG have hsumTI_int : Integrable (fun ω => (∑ t, b t * IT t ω) * IG g ω) μ := hsumT_mem.integrable_mul hIG have hcohort : ∫ ω, (∑ g', a g' * IG g' ω) * IG g ω ∂μ = ∫ ω, F ω * IG g ω ∂μ := by calc ∫ ω, (∑ g', a g' * IG g' ω) * IG g ω ∂μ = a g * cohortMass μ G g := by simpa [IG, a] using integral_cohort_sum_mul_cohort_indicator μ G G_meas a g _ = ∫ ω, F ω * IG g ω ∂μ := by simpa [a, IG, mul_comm] using (cohort_integral_div_mul_cohortMass μ F G g) have hperiod : ∫ ω, (∑ t, b t * IT t ω) * IG g ω ∂μ = 0 := by calc ∫ ω, (∑ t, b t * IT t ω) * IG g ω ∂μ = ∑ t, b t * cellMass μ G T_rv g t := by simpa [IG, IT, b] using integral_period_sum_mul_cohort_indicator μ G T_rv G_meas T_meas b g _ = cohortMass μ G g * ∑ t, b t * periodMass μ T_rv t := by calc ∑ t, b t * cellMass μ G T_rv g t = ∑ t, b t * (cohortMass μ G g * periodMass μ T_rv t) := by refine Finset.sum_congr rfl ?_ intro t _ rw [B_balanced g t] _ = cohortMass μ G g * ∑ t, b t * periodMass μ T_rv t := by rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro t _ ring _ = 0 := by rw [period_centered_sum_eq_zero μ F T_rv T_meas hF_int] ring have hpanel : ∫ ω, panelMeanReg μ F G T_rv ω * IG g ω ∂μ = ∫ ω, F ω * IG g ω ∂μ := by calc ∫ ω, panelMeanReg μ F G T_rv ω * IG g ω ∂μ = ∫ ω, ((∑ g', a g' * IG g' ω) + (∑ t, b t * IT t ω)) * IG g ω ∂μ := by simp [panelMeanReg, IG, IT, a, b] _ = ∫ ω, (∑ g', a g' * IG g' ω) * IG g ω + (∑ t, b t * IT t ω) * IG g ω ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω ring _ = ∫ ω, (∑ g', a g' * IG g' ω) * IG g ω ∂μ + ∫ ω, (∑ t, b t * IT t ω) * IG g ω ∂μ := by integral_linearity _ = ∫ ω, F ω * IG g ω ∂μ := by rw [hcohort, hperiod] ring calc ∫ ω, (F ω - panelMeanReg μ F G T_rv ω) * IG g ω ∂μ = ∫ ω, F ω * IG g ω ∂μ - ∫ ω, panelMeanReg μ F G T_rv ω * IG g ω ∂μ := by calc ∫ ω, (F ω - panelMeanReg μ F G T_rv ω) * IG g ω ∂μ = ∫ ω, F ω * IG g ω - panelMeanReg μ F G T_rv ω * IG g ω ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω ring _ = ∫ ω, F ω * IG g ω ∂μ - ∫ ω, panelMeanReg μ F G T_rv ω * IG g ω ∂μ := by integral_linearity _ = 0 := by rw [hpanel]; ring -
panelMeanReg_period_axis_orthogonaltheorem — Under a balanced panel law, the residual from the panel mean regression has zero average product with the indicator of any fixed period.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :F :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin TG_meas :T_meas :Measurable T_rvF_memLp :MemLp F 2 μB_balanced :IsBalancedPanelLaw μ G T_rvt :Fin Tconclusion∫ ω, (F ω - panelMeanReg μ F G T_rv ω) * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ= 0Proof (Lean source)
theorem panelMeanReg_period_axis_orthogonal (μ : Measure Ω) [IsProbabilityMeasure μ] (F : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) (G_meas : Measurable G) (T_meas : Measurable T_rv) (F_memLp : MemLp F 2 μ) (B_balanced : IsBalancedPanelLaw μ G T_rv) (t : Fin T) : ∫ ω, (F ω - panelMeanReg μ F G T_rv ω) * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = 0 := by classical let IG : 𝒢 → Ω → ℝ := fun g ω => indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω let IT : Fin T → Ω → ℝ := fun t ω => indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω let a : 𝒢 → ℝ := fun g => (∫ ω, F ω * IG g ω ∂μ) / cohortMass μ G g let b : Fin T → ℝ := fun t => (∫ ω, F ω * IT t ω ∂μ) / periodMass μ T_rv t - ∫ ω, F ω ∂μ have hF_int : Integrable F μ := F_memLp.integrable (by norm_num : (1 : ENNReal) ≤ 2) have hIT : MemLp (IT t) 2 μ := by simpa [IT] using indicator_period_memLp μ T_rv T_meas t have hFI_int : Integrable (fun ω => F ω * IT t ω) μ := F_memLp.integrable_mul hIT have hPanel_mem : MemLp (panelMeanReg μ F G T_rv) 2 μ := (panelClass μ G T_rv G_meas T_meas).memLp (panelMeanReg_mem_panelClass μ F G T_rv G_meas T_meas) have hPanelI_int : Integrable (fun ω => panelMeanReg μ F G T_rv ω * IT t ω) μ := hPanel_mem.integrable_mul hIT have hsumG_mem : MemLp (fun ω => ∑ g, a g * IG g ω) 2 μ := (panelClass μ G T_rv G_meas T_meas).memLp ⟨a, fun _ => 0, by filter_upwards [] with ω; simp [IG]⟩ have hsumT_mem : MemLp (fun ω => ∑ t', b t' * IT t' ω) 2 μ := (panelClass μ G T_rv G_meas T_meas).memLp ⟨fun _ => 0, b, by filter_upwards [] with ω; simp [IT]⟩ have hsumGI_int : Integrable (fun ω => (∑ g, a g * IG g ω) * IT t ω) μ := hsumG_mem.integrable_mul hIT have hsumTI_int : Integrable (fun ω => (∑ t', b t' * IT t' ω) * IT t ω) μ := hsumT_mem.integrable_mul hIT have hcohort : ∫ ω, (∑ g, a g * IG g ω) * IT t ω ∂μ = (∫ ω, F ω ∂μ) * periodMass μ T_rv t := by calc ∫ ω, (∑ g, a g * IG g ω) * IT t ω ∂μ = ∑ g, a g * cellMass μ G T_rv g t := by simpa [IG, IT, a] using integral_cohort_sum_mul_period_indicator μ G T_rv G_meas T_meas a t _ = (∑ g, a g * cohortMass μ G g) * periodMass μ T_rv t := by calc ∑ g, a g * cellMass μ G T_rv g t = ∑ g, a g * (cohortMass μ G g * periodMass μ T_rv t) := by refine Finset.sum_congr rfl ?_ intro g _ rw [B_balanced g t] _ = (∑ g, a g * cohortMass μ G g) * periodMass μ T_rv t := by rw [Finset.sum_mul] refine Finset.sum_congr rfl ?_ intro g _ ring _ = (∫ ω, F ω ∂μ) * periodMass μ T_rv t := by congr 1 calc ∑ g, a g * cohortMass μ G g = ∑ g, ∫ ω, F ω * IG g ω ∂μ := by refine Finset.sum_congr rfl ?_ intro g _ simpa [a, IG, mul_comm] using (cohort_integral_div_mul_cohortMass μ F G g) _ = ∫ ω, F ω ∂μ := by rw [integral_eq_sum_cohort μ F G G_meas hF_int] have hperiod : ∫ ω, (∑ t', b t' * IT t' ω) * IT t ω ∂μ = ∫ ω, F ω * IT t ω ∂μ - (∫ ω, F ω ∂μ) * periodMass μ T_rv t := by calc ∫ ω, (∑ t', b t' * IT t' ω) * IT t ω ∂μ = b t * periodMass μ T_rv t := by simpa [IT, b] using integral_period_sum_mul_period_indicator μ T_rv T_meas b t _ = ∫ ω, F ω * IT t ω ∂μ - (∫ ω, F ω ∂μ) * periodMass μ T_rv t := by have hdiv : ((∫ ω, F ω * IT t ω ∂μ) / periodMass μ T_rv t) * periodMass μ T_rv t = ∫ ω, F ω * IT t ω ∂μ := by simpa [IT] using period_integral_div_mul_periodMass μ F T_rv t dsimp [b] calc ((∫ ω, F ω * IT t ω ∂μ) / periodMass μ T_rv t - ∫ ω, F ω ∂μ) * periodMass μ T_rv t = ((∫ ω, F ω * IT t ω ∂μ) / periodMass μ T_rv t) * periodMass μ T_rv t - (∫ ω, F ω ∂μ) * periodMass μ T_rv t := by ring _ = ∫ ω, F ω * IT t ω ∂μ - (∫ ω, F ω ∂μ) * periodMass μ T_rv t := by rw [hdiv] have hpanel : ∫ ω, panelMeanReg μ F G T_rv ω * IT t ω ∂μ = ∫ ω, F ω * IT t ω ∂μ := by calc ∫ ω, panelMeanReg μ F G T_rv ω * IT t ω ∂μ = ∫ ω, ((∑ g, a g * IG g ω) + (∑ t', b t' * IT t' ω)) * IT t ω ∂μ := by simp [panelMeanReg, IG, IT, a, b] _ = ∫ ω, (∑ g, a g * IG g ω) * IT t ω + (∑ t', b t' * IT t' ω) * IT t ω ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω ring _ = ∫ ω, (∑ g, a g * IG g ω) * IT t ω ∂μ + ∫ ω, (∑ t', b t' * IT t' ω) * IT t ω ∂μ := by integral_linearity _ = ∫ ω, F ω * IT t ω ∂μ := by rw [hcohort, hperiod] ring calc ∫ ω, (F ω - panelMeanReg μ F G T_rv ω) * IT t ω ∂μ = ∫ ω, F ω * IT t ω ∂μ - ∫ ω, panelMeanReg μ F G T_rv ω * IT t ω ∂μ := by calc ∫ ω, (F ω - panelMeanReg μ F G T_rv ω) * IT t ω ∂μ = ∫ ω, F ω * IT t ω - panelMeanReg μ F G T_rv ω * IT t ω ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω ring _ = ∫ ω, F ω * IT t ω ∂μ - ∫ ω, panelMeanReg μ F G T_rv ω * IT t ω ∂μ := by integral_linearity _ = 0 := by rw [hpanel]; ring -
residY_cohort_orthogonaltheorem — The outcome residual is orthogonal to every cohort indicator.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :Y :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin TG_meas :T_meas :Measurable T_rvY_memLp :MemLp Y 2 μB_balanced :IsBalancedPanelLaw μ G T_rvg :𝒢conclusion∫ ω, (Y ω - panelMeanReg μ Y G T_rv ω) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ= 0Proof (Lean source)
theorem residY_cohort_orthogonal (μ : Measure Ω) [IsProbabilityMeasure μ] (Y : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) (G_meas : Measurable G) (T_meas : Measurable T_rv) (Y_memLp : MemLp Y 2 μ) (B_balanced : IsBalancedPanelLaw μ G T_rv) (g : 𝒢) : ∫ ω, (Y ω - panelMeanReg μ Y G T_rv ω) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = 0 := by classical exact panelMeanReg_cohort_axis_orthogonal μ Y G T_rv G_meas T_meas Y_memLp B_balanced g -
residD_period_orthogonaltheorem — The treatment residual is orthogonal to every period indicator 𝟙{T_rv = t}. Requires B_balanced to make the cross-cohort sum cancel.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :D :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin TG_meas :T_meas :Measurable T_rvD_meas :D_binary :∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1B_balanced :IsBalancedPanelLaw μ G T_rvt :Fin Tconclusion∫ ω, (D ω - panelPropensity μ D G T_rv ω) * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ= 0Proof (Lean source)
theorem residD_period_orthogonal (μ : Measure Ω) [IsProbabilityMeasure μ] (D : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) (G_meas : Measurable G) (T_meas : Measurable T_rv) (D_meas : Measurable D) (D_binary : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1) (B_balanced : IsBalancedPanelLaw μ G T_rv) (t : Fin T) : ∫ ω, (D ω - panelPropensity μ D G T_rv ω) * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = 0 := by classical have hD_mem : MemLp D 2 μ := memLp_two_of_binary μ D D_meas D_binary have hproj : panelPropensity μ D G T_rv = panelMeanReg μ D G T_rv := by funext ω simp [panelPropensity, panelMeanReg, cohortBarD] simpa [hproj] using panelMeanReg_period_axis_orthogonal μ D G T_rv G_meas T_meas hD_mem B_balanced t -
residY_period_orthogonaltheorem — The outcome residual is orthogonal to every period indicator.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :Y :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin TG_meas :T_meas :Measurable T_rvY_memLp :MemLp Y 2 μB_balanced :IsBalancedPanelLaw μ G T_rvt :Fin Tconclusion∫ ω, (Y ω - panelMeanReg μ Y G T_rv ω) * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ= 0Proof (Lean source)
theorem residY_period_orthogonal (μ : Measure Ω) [IsProbabilityMeasure μ] (Y : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) (G_meas : Measurable G) (T_meas : Measurable T_rv) (Y_memLp : MemLp Y 2 μ) (B_balanced : IsBalancedPanelLaw μ G T_rv) (t : Fin T) : ∫ ω, (Y ω - panelMeanReg μ Y G T_rv ω) * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = 0 := by classical exact panelMeanReg_period_axis_orthogonal μ Y G T_rv G_meas T_meas Y_memLp B_balanced t
Integrals 3 core · 15 supporting Proves integral identities for the staggered-TWFE bridge. ★ integral_mul_panelClass_eq_zero_of_axes
Proves integral identities for the staggered-TWFE bridge. The module supplies MemLp, indicator, and orthogonality facts used to transport finite weighted decompositions into the population setting.
def panelPropensityHat reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measurable sample space, a finite cohort label space whose members can be compared for equality and whose singleton sets are measurable, a natural-number panel length, a measure, a treatment variable, a cohort variable, a period variable, a cohort label, and a period, the cell-specific additive treatment fit is the cohort-specific mean treatment plus the period-specific mean treatment minus the overall mean treatment.
Definition (Lean source)
parameters
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
Measure Ω
D :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
g :
𝒢
t :
Fin T
def
panelPropensityHat μ D G T_rv g t :
ℝ
given by
cohortBarD μ D G g
+ ((∫ ω', D ω' * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ) / periodMass μ T_rv t - ∫ ω', D ω' ∂μ)
def panelMeanRegHat reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measurable sample space, a finite cohort label space whose members can be compared for equality and whose singleton sets are measurable, a natural-number panel length, a measure, an outcome variable, a cohort variable, a period variable, a cohort label, and a period, the cell-specific additive outcome fit is the cohort-specific mean outcome plus the period-specific mean outcome minus the overall mean outcome.
Definition (Lean source)
parameters
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
Measure Ω
Y :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
g :
𝒢
t :
Fin T
def
panelMeanRegHat μ Y G T_rv g t :
ℝ
given by
((∫ ω', Y ω' * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω' ∂μ) / cohortMass μ G g)
+ ((∫ ω', Y ω' * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ) / periodMass μ T_rv t - ∫ ω', Y ω' ∂μ)
theorem integral_mul_panelClass_eq_zero_of_axes reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
If a square-integrable random variable V has zero mean product against every cohort indicator 𝟙{G = g} and zero mean product against every period indicator 𝟙{T_rv = t}, then V is orthogonal, in the L²(μ) sense, to every unit/period-additive combination ∑_g cG(g)·𝟙{G = g} + ∑_t cT(t)·𝟙{T_rv = t}, i.e. to every member of the additive nuisance class panelClass.
Formal statement
hypotheses
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
V :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
V_memLp :
MemLp V 2 μ
cG :
𝒢 → ℝ
cT :
Fin T → ℝ
hCohort :
∀ g, ∫ ω, V ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = 0
hPeriod :
∀ t, ∫ ω, V ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = 0
Proof (Lean source)
theorem integral_mul_panelClass_eq_zero_of_axes
(μ : Measure Ω) [IsFiniteMeasure μ]
(V : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T)
(G_meas : Measurable G) (T_meas : Measurable T_rv)
(V_memLp : MemLp V 2 μ)
(cG : 𝒢 → ℝ) (cT : Fin T → ℝ)
(hCohort : ∀ g,
∫ ω, V ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = 0)
(hPeriod : ∀ t,
∫ ω, V ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = 0) :
∫ ω, V ω
* ((∑ g, cG g
* indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω)
+ (∑ t, cT t
* indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω)) ∂μ
= 0 := by
classical
exact CellBridge.integral_mul_twoAxisIndicatorSpan_eq_zero_of_axes
μ V G T_rv G_meas T_meas V_memLp cG cT hCohort hPeriod
15 supporting declarations (lemmas, instances)
-
indicator_cohort_memLptheorem — Cohort indicator 𝟙{G = g} is in MemLp 2 μ (bounded + finite measure).hypothesesΩ :sharedType u_1𝒢 :sharedType u_2μ :G :Ω → 𝒢G_meas :g :𝒢Proof (Lean source)
theorem indicator_cohort_memLp (μ : Measure Ω) [IsFiniteMeasure μ] (G : Ω → 𝒢) (G_meas : Measurable G) (g : 𝒢) : MemLp (fun ω => indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) 2 μ := by exact CellBridge.indicator_cell_memLp μ G G_meas g -
indicator_period_memLptheorem — Period indicator 𝟙{T_rv = t} is in MemLp 2 μ.hypothesesProof (Lean source)
theorem indicator_period_memLp (μ : Measure Ω) [IsFiniteMeasure μ] (T_rv : Ω → Fin T) (T_meas : Measurable T_rv) (t : Fin T) : MemLp (fun ω => indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω) 2 μ := by exact CellBridge.indicator_cell_memLp μ T_rv T_meas t -
indicator_panel_cell_memLptheorem — Joint cell indicator 𝟙{G=g ∧ T_rv=t} is in MemLp 2 μ.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :G :Ω → 𝒢T_rv :Ω → Fin TG_meas :T_meas :Measurable T_rvg :𝒢t :Fin TProof (Lean source)
theorem indicator_panel_cell_memLp (μ : Measure Ω) [IsFiniteMeasure μ] (G : Ω → 𝒢) (T_rv : Ω → Fin T) (G_meas : Measurable G) (T_meas : Measurable T_rv) (g : 𝒢) (t : Fin T) : MemLp (fun ω => indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω) 2 μ := by -- The cell `{G = g ∧ T_rv = t}` is the intersection of two measurable sets. let sG : Set Ω := {ω | G ω = g} let sT : Set Ω := {ω | T_rv ω = t} have hG : MeasurableSet sG := G_meas (measurableSet_singleton g) have hT : MeasurableSet sT := T_meas (measurableSet_singleton t) have hcell : MeasurableSet (sG ∩ sT) := hG.inter hT have hEq : ({ω | G ω = g ∧ T_rv ω = t} : Set Ω) = sG ∩ sT := by ext ω; simp [sG, sT] rw [hEq] exact (memLp_const (μ := μ) (1 : ℝ)).indicator hcell -
integral_cohort_indicator_one_eq_cohortMasstheorem — ∫ 𝟙{G = g} dμ = cohortMass μ G g.hypothesesconclusion∫ ω, indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = cohortMass μ G gProof (Lean source)
theorem integral_cohort_indicator_one_eq_cohortMass (μ : Measure Ω) (G : Ω → 𝒢) (G_meas : Measurable G) (g : 𝒢) : ∫ ω, indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = cohortMass μ G g := by simpa [cohortMass] using (CellBridge.integral_cell_indicator_one_eq_cellMass μ G G_meas g) -
integral_period_indicator_one_eq_periodMasstheorem — ∫ 𝟙{T_rv = t} dμ = periodMass μ T_rv t.hypothesesconclusion∫ ω, indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = periodMass μ T_rv tProof (Lean source)
theorem integral_period_indicator_one_eq_periodMass (μ : Measure Ω) (T_rv : Ω → Fin T) (T_meas : Measurable T_rv) (t : Fin T) : ∫ ω, indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = periodMass μ T_rv t := by simpa [periodMass] using (CellBridge.integral_cell_indicator_one_eq_cellMass μ T_rv T_meas t) -
integral_panel_cell_indicator_one_eq_cellMasstheorem — ∫ 𝟙{G = g ∧ T_rv = t} dμ = cellMass μ G T_rv g t.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :Measure ΩG :Ω → 𝒢T_rv :Ω → Fin TG_meas :T_meas :Measurable T_rvg :𝒢t :Fin Tconclusion∫ ω, indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ= cellMass μ G T_rv g tProof (Lean source)
theorem integral_panel_cell_indicator_one_eq_cellMass (μ : Measure Ω) (G : Ω → 𝒢) (T_rv : Ω → Fin T) (G_meas : Measurable G) (T_meas : Measurable T_rv) (g : 𝒢) (t : Fin T) : ∫ ω, indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = cellMass μ G T_rv g t := by let sG : Set Ω := {ω | G ω = g} let sT : Set Ω := {ω | T_rv ω = t} have hG : MeasurableSet sG := G_meas (measurableSet_singleton g) have hT : MeasurableSet sT := T_meas (measurableSet_singleton t) have hcell : MeasurableSet (sG ∩ sT) := hG.inter hT have hEq : ({ω | G ω = g ∧ T_rv ω = t} : Set Ω) = sG ∩ sT := by ext ω; simp [sG, sT] change (∫ ω, indicator (sG ∩ sT) (1 : Ω → ℝ) ω ∂μ) = cellMass μ G T_rv g t rw [MeasureTheory.integral_indicator_one hcell] rw [← hEq] simp [Measure.real, cellMass, CellBridge.jointCellMass] -
cohort_integral_div_mul_cohortMasstheorem — Defining identity for cohortBarD: dividing by cohort mass and multiplying back recovers the cohort-indicator-weighted integral. On zero-mass cohorts both sides are zero (a.e.-vanishing indicator).hypothesesconclusion((∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ) / cohortMass μ G g) * cohortMass μ G g= ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μProof (Lean source)
theorem cohort_integral_div_mul_cohortMass (μ : Measure Ω) [IsFiniteMeasure μ] (F : Ω → ℝ) (G : Ω → 𝒢) (g : 𝒢) : ((∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ) / cohortMass μ G g) * cohortMass μ G g = ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ := by simpa [cohortMass] using (CellBridge.cell_integral_div_mul_cellMass μ F G g) -
period_integral_div_mul_periodMasstheorem — Period analogue.hypothesesconclusion((∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ) / periodMass μ T_rv t) * periodMass μ T_rv t= ∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μProof (Lean source)
theorem period_integral_div_mul_periodMass (μ : Measure Ω) [IsFiniteMeasure μ] (F : Ω → ℝ) (T_rv : Ω → Fin T) (t : Fin T) : ((∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ) / periodMass μ T_rv t) * periodMass μ T_rv t = ∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ := by simpa [periodMass] using (CellBridge.cell_integral_div_mul_cellMass μ F T_rv t) -
panel_cell_integral_div_mul_cellMasstheorem — Cell analogue (joint cohort × period cell).hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :F :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin TG_meas :T_meas :Measurable T_rvg :𝒢t :Fin TProof (Lean source)
theorem panel_cell_integral_div_mul_cellMass (μ : Measure Ω) [IsFiniteMeasure μ] (F : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) (G_meas : Measurable G) (T_meas : Measurable T_rv) (g : 𝒢) (t : Fin T) : ((∫ ω, F ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ) / cellMass μ G T_rv g t) * cellMass μ G T_rv g t = ∫ ω, F ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ := by let s : Set Ω := {ω | G ω = g ∧ T_rv ω = t} let A : ℝ := ∫ ω, F ω * indicator s (fun _ => (1 : ℝ)) ω ∂μ have _hs_meas : MeasurableSet s := by have hG : MeasurableSet {ω : Ω | G ω = g} := G_meas (measurableSet_singleton g) have hT : MeasurableSet {ω : Ω | T_rv ω = t} := T_meas (measurableSet_singleton t) simpa [s, Set.inter_def] using hG.inter hT have hs_top : μ s ≠ ⊤ := by exact ne_of_lt <| lt_of_le_of_lt (measure_mono (Set.subset_univ s)) (by simp) by_cases hmass : cellMass μ G T_rv g t = 0 · have hs_zero : μ s = 0 := by have hzero : (μ s).toReal = 0 := by simpa [cellMass, CellBridge.jointCellMass, s] using hmass rcases (ENNReal.toReal_eq_zero_iff (μ s)).1 hzero with h0 | htop · exact h0 · exact elim (hs_top htop) have h_not_mem : ∀ᵐ ω ∂μ, ω ∉ s := by rw [MeasureTheory.ae_iff] simpa using hs_zero have h_ae : (fun ω => F ω * indicator s (fun _ => (1 : ℝ)) ω) =ᵐ[μ] 0 := by filter_upwards [h_not_mem] with ω hω simp [indicator, hω] have hA : A = 0 := by simpa [A] using (integral_eq_zero_of_ae h_ae) simp [cellMass, s, A, hA] · have hAdef : A = ∫ ω, F ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ := by simp [A, s] rw [hAdef.symm] field_simp [hmass] -
cohortBarD_mul_cohortMasstheorem — cohortBarD g · cohortMass g = ∫ D · 𝟙{G=g} dμ.hypothesesconclusioncohortBarD μ D G g * cohortMass μ G g= ∫ ω, D ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μProof (Lean source)
theorem cohortBarD_mul_cohortMass (μ : Measure Ω) [IsFiniteMeasure μ] (D : Ω → ℝ) (G : Ω → 𝒢) (g : 𝒢) : cohortBarD μ D G g * cohortMass μ G g = ∫ ω, D ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ := by simpa [cohortBarD] using (cohort_integral_div_mul_cohortMass μ D G g) -
panelPropensity_eq_hat_of_memtheorem — On the cell {G = g ∧ T_rv = t}, panelPropensity evaluates to panelPropensityHat g t. Pointwise (no a.e. needed) by single-cell membership selecting one term in each finite sum.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :Measure ΩD :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin Tg :𝒢t :Fin Tω :ΩhG :G ω = ghT :T_rv ω = tconclusionpanelPropensity μ D G T_rv ω = panelPropensityHat μ D G T_rv g tProof (Lean source)
theorem panelPropensity_eq_hat_of_mem (μ : Measure Ω) (D : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) {g : 𝒢} {t : Fin T} {ω : Ω} (hG : G ω = g) (hT : T_rv ω = t) : panelPropensity μ D G T_rv ω = panelPropensityHat μ D G T_rv g t := by classical unfold panelPropensity panelPropensityHat rw [Finset.sum_eq_single g] · rw [Finset.sum_eq_single t] · simp [hG, hT] · intro b _ hbt simp [indicator, hT, hbt.symm] · intro ht simp at ht · intro b _ hbg simp [indicator, hG, hbg.symm] · intro hg simp at hg -
panelMeanReg_eq_hat_of_memtheorem — On the cell {G = g ∧ T_rv = t}, panelMeanReg evaluates to panelMeanRegHat g t.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :Measure ΩY :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin Tg :𝒢t :Fin Tω :ΩhG :G ω = ghT :T_rv ω = tconclusionpanelMeanReg μ Y G T_rv ω = panelMeanRegHat μ Y G T_rv g tProof (Lean source)
theorem panelMeanReg_eq_hat_of_mem (μ : Measure Ω) (Y : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) {g : 𝒢} {t : Fin T} {ω : Ω} (hG : G ω = g) (hT : T_rv ω = t) : panelMeanReg μ Y G T_rv ω = panelMeanRegHat μ Y G T_rv g t := by classical unfold panelMeanReg panelMeanRegHat rw [Finset.sum_eq_single g] · rw [Finset.sum_eq_single t] · simp [hG, hT] · intro b _ hbt simp [indicator, hT, hbt.symm] · intro ht simp at ht · intro b _ hbg simp [indicator, hG, hbg.symm] · intro hg simp at hg -
integral_eq_sum_cohorttheorem — Integrate by summing over cohort cells: ∫ F dμ = ∑_g ∫ F · 𝟙{G = g} dμ.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2μ :Measure ΩF :Ω → ℝG :Ω → 𝒢G_meas :F_int :Integrable F μconclusion∫ ω, F ω ∂μ = ∑ g, ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μProof (Lean source)
theorem integral_eq_sum_cohort (μ : Measure Ω) (F : Ω → ℝ) (G : Ω → 𝒢) (G_meas : Measurable G) (F_int : Integrable F μ) : ∫ ω, F ω ∂μ = ∑ g, ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ := by classical exact CellBridge.integral_eq_sum_cell μ F G G_meas F_int -
integral_eq_sum_periodtheorem — Integrate by summing over period cells.hypothesesΩ :sharedType u_1T :sharedℕμ :Measure ΩF :Ω → ℝT_rv :Ω → Fin TT_meas :Measurable T_rvF_int :Integrable F μconclusion∫ ω, F ω ∂μ = ∑ t, ∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μProof (Lean source)
theorem integral_eq_sum_period (μ : Measure Ω) (F : Ω → ℝ) (T_rv : Ω → Fin T) (T_meas : Measurable T_rv) (F_int : Integrable F μ) : ∫ ω, F ω ∂μ = ∑ t, ∫ ω, F ω * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ := by exact CellBridge.integral_eq_sum_cell μ F T_rv T_meas F_int -
integral_eq_sum_panel_celltheorem — Integrate by summing over cohort × period cells.hypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :Measure ΩF :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin TG_meas :T_meas :Measurable T_rvF_int :Integrable F μconclusion∫ ω, F ω ∂μ= ∑ g, ∑ t, ∫ ω, F ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μProof (Lean source)
theorem integral_eq_sum_panel_cell (μ : Measure Ω) (F : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) (G_meas : Measurable G) (T_meas : Measurable T_rv) (F_int : Integrable F μ) : ∫ ω, F ω ∂μ = ∑ g, ∑ t, ∫ ω, F ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ := by let term : 𝒢 × Fin T → Ω → ℝ := fun gt ω => F ω * indicator {ω' | G ω' = gt.1 ∧ T_rv ω' = gt.2} (fun _ => (1 : ℝ)) ω have hterm_int : ∀ gt ∈ ((Finset.univ : Finset 𝒢).product (Finset.univ : Finset (Fin T))), Integrable (term gt) μ := by intro gt _ have hG : MeasurableSet {ω : Ω | G ω = gt.1} := G_meas (measurableSet_singleton gt.1) have hT : MeasurableSet {ω : Ω | T_rv ω = gt.2} := T_meas (measurableSet_singleton gt.2) have hcell : MeasurableSet ({ω : Ω | G ω = gt.1} ∩ {ω : Ω | T_rv ω = gt.2}) := hG.inter hT have hEq : term gt = fun ω => indicator {ω' | G ω' = gt.1 ∧ T_rv ω' = gt.2} F ω := by funext ω by_cases hω : G ω = gt.1 ∧ T_rv ω = gt.2 · simp [term, indicator, hω] · simp [term, indicator, hω] rw [hEq] have hcellSet : MeasurableSet {ω : Ω | G ω = gt.1 ∧ T_rv ω = gt.2} := by simpa [Set.inter_def] using hcell exact F_int.indicator hcellSet have hsum_ind : ∀ ω, (∑ g, ∑ t, indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω) = 1 := by intro ω rw [Finset.sum_eq_single (G ω)] · rw [Finset.sum_eq_single (T_rv ω)] · simp · intro b _ hb have hne : ¬ T_rv ω = b := fun h => hb h.symm simp [indicator, hne] · intro hnot exact elim (hnot (Finset.mem_univ _)) · intro b _ hb have hne : ¬ G ω = b := fun h => hb h.symm simp [indicator, hne] · intro hnot exact elim (hnot (Finset.mem_univ _)) have hsum_product : ∀ ω, ((Finset.univ : Finset 𝒢).product (Finset.univ : Finset (Fin T))).sum (fun gt => term gt ω) = ∑ g, ∑ t, F ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω := by intro ω simpa [term] using (Finset.sum_product' (Finset.univ : Finset 𝒢) (Finset.univ : Finset (Fin T)) (fun g t => F ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω)) calc ∫ ω, F ω ∂μ = ∫ ω, F ω * (∑ g, ∑ t, indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω) ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω simp [hsum_ind ω] _ = ∫ ω, ((Finset.univ : Finset 𝒢).product (Finset.univ : Finset (Fin T))).sum (fun gt => term gt ω) ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω rw [hsum_product] simp [Finset.mul_sum] _ = ((Finset.univ : Finset 𝒢).product (Finset.univ : Finset (Fin T))).sum (fun gt => ∫ ω, term gt ω ∂μ) := by simpa using (MeasureTheory.integral_finsetSum ((Finset.univ : Finset 𝒢).product (Finset.univ : Finset (Fin T))) (f := term) hterm_int) _ = ∑ g, ∑ t, ∫ ω, F ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ := by simpa [term] using (Finset.sum_product' (Finset.univ : Finset 𝒢) (Finset.univ : Finset (Fin T)) (fun g t => ∫ ω, F ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ))
Partition 2 core · 0 supporting This file constructs the residualization witnesses for treatment and outcome after projecting on cohort and period cells in a balanced panel.
Goodman-Bacon Residualization Witnesses
This file constructs the residualization witnesses for treatment and outcome after projecting on cohort and period cells in a balanced panel. These witnesses package the fitted component, the residual component, square integrability, decomposition, and orthogonality conditions used by the Goodman-Bacon bridge.
def residWitnessD_panel reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
On a measurable sample space with a finite cohort label space whose members can be compared for equality and whose singleton sets are measurable and a natural-number panel length, let the probability measure, the treatment variable, the cohort variable, and the period variable be given. If the cohort variable is measurable, the period variable is measurable, the treatment variable is measurable, the treatment variable equals either zero or one almost everywhere, and each cohort-period cell has probability equal to the product of its cohort and period marginal probabilities, then the additive cohort-and-period treatment fit and its residual constitute a residualization witness for treatment with respect to the class of additive cohort-and-period functions.
Definition (Lean source)
parameters
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
D :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
D_meas :
D_binary :
∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1
B_balanced :
IsBalancedPanelLaw μ G T_rv
def
residWitnessD_panel μ D G T_rv G_meas T_meas D_meas D_binary B_balanced :
ResidualizationWitness μ (panelClass μ G T_rv G_meas T_meas) D
given by
by let H := panelClass μ G T_rv G_meas T_meas have hVH_mem : H.mem (panelPropensity μ D G T_rv) := panelPropensity_mem_panelClass μ D G T_rv G_meas T_meas have hD_mem : MemLp D 2 μ := by have hD_bounded : ∀ᵐ ω ∂μ, D ω ∈ Icc (-1 : ℝ) 1 := by filter_upwards [D_binary] with ω hD rcases hD with hD0 | hD1 · simp [hD0] · simp [hD1] exact memLp_of_bounded (f := D) hD_bounded (D_meas.aestronglyMeasurable) (2 : ENNReal) have hVtilde_memLp : MemLp (fun ω => D ω - panelPropensity μ D G T_rv ω) 2 μ := hD_mem.sub (H.memLp hVH_mem) refine { VH := panelPropensity μ D G T_rv , Vtilde := fun ω => D ω - panelPropensity μ D G T_rv ω , VH_mem := hVH_mem , Vtilde_memLp := hVtilde_memLp , decomp := by filter_upwards [] with ω change D ω = panelPropensity μ D G T_rv ω + (D ω - panelPropensity μ D G T_rv ω) ring , orthogonal := by intro h hh rcases hh with ⟨cG, cT, hh_eq⟩ have hVtilde := hVtilde_memLp calc ∫ ω, (D ω - panelPropensity μ D G T_rv ω) * h ω ∂μ = ∫ ω, (D ω - panelPropensity μ D G T_rv ω) * ((∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, cT t * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω)) ∂μ := by refine integral_congr_ae ?_ filter_upwards [hh_eq] with ω hω rw [hω] _ = 0 := integral_mul_panelClass_eq_zero_of_axes μ (fun ω => D ω - panelPropensity μ D G T_rv ω) G T_rv G_meas T_meas hVtilde cG cT (fun g => residD_cohort_orthogonal μ D G T_rv G_meas T_meas D_meas D_binary B_balanced g) (fun t => residD_period_orthogonal μ D G T_rv G_meas T_meas D_meas D_binary B_balanced t) }
def residWitnessY_panel reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
On a measurable sample space with a finite cohort label space whose members can be compared for equality and whose singleton sets are measurable and a natural-number panel length, let the probability measure, the outcome variable, the cohort variable, and the period variable be given. If the cohort variable is measurable, the period variable is measurable, the outcome has a finite second moment, and each cohort-period cell has probability equal to the product of its cohort and period marginal probabilities, then the additive cohort-and-period outcome fit and its residual constitute a residualization witness for the outcome with respect to the class of additive cohort-and-period functions.
Definition (Lean source)
parameters
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
Y :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
Y_memLp :
MemLp Y 2 μ
B_balanced :
IsBalancedPanelLaw μ G T_rv
def
residWitnessY_panel μ Y G T_rv G_meas T_meas Y_memLp B_balanced :
ResidualizationWitness μ (panelClass μ G T_rv G_meas T_meas) Y
given by
by let H := panelClass μ G T_rv G_meas T_meas have hVH_mem : H.mem (panelMeanReg μ Y G T_rv) := panelMeanReg_mem_panelClass μ Y G T_rv G_meas T_meas have hVtilde_memLp : MemLp (fun ω => Y ω - panelMeanReg μ Y G T_rv ω) 2 μ := Y_memLp.sub (H.memLp hVH_mem) refine { VH := panelMeanReg μ Y G T_rv , Vtilde := fun ω => Y ω - panelMeanReg μ Y G T_rv ω , VH_mem := hVH_mem , Vtilde_memLp := hVtilde_memLp , decomp := by filter_upwards [] with ω change Y ω = panelMeanReg μ Y G T_rv ω + (Y ω - panelMeanReg μ Y G T_rv ω) ring , orthogonal := by intro h hh rcases hh with ⟨cG, cT, hh_eq⟩ have hVtilde := hVtilde_memLp calc ∫ ω, (Y ω - panelMeanReg μ Y G T_rv ω) * h ω ∂μ = ∫ ω, (Y ω - panelMeanReg μ Y G T_rv ω) * ((∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, cT t * indicator {ω' | T_rv ω' = t} (fun _ => (1 : ℝ)) ω)) ∂μ := by refine integral_congr_ae ?_ filter_upwards [hh_eq] with ω hω rw [hω] _ = 0 := integral_mul_panelClass_eq_zero_of_axes μ (fun ω => Y ω - panelMeanReg μ Y G T_rv ω) G T_rv G_meas T_meas hVtilde cG cT (fun g => residY_cohort_orthogonal μ Y G T_rv G_meas T_meas Y_memLp B_balanced g) (fun t => residY_period_orthogonal μ Y G T_rv G_meas T_meas Y_memLp B_balanced t) }
PerCell 2 core · 1 supporting This file proves the cell-level integral identities that express the residualized-treatment denominator and the residualized-outcome numerator in terms of cohort-period panel statistics. ★ num_per_cell_panel
Goodman-Bacon Per-Cell Bridge Identities
This file proves the cell-level integral identities that express the residualized-treatment denominator and the residualized-outcome numerator in terms of cohort-period panel statistics. These identities supply the local algebra needed to connect the measure-theoretic bridge with the finite Goodman-Bacon decomposition.
def panelDtilde reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
For a measurable sample space, a finite cohort label space whose members can be compared for equality and whose singleton sets are measurable, a natural-number panel length, a measure on that sample space, a treatment variable, a cohort variable, a period variable, a cohort label, and a period, the cell-specific residualized treatment value is the treatment integral over the cohort-period cell divided by that cell's mass, minus the additive cohort-and-period fitted treatment value for that cell.
Definition (Lean source)
parameters
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
Measure Ω
D :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
g :
𝒢
t :
Fin T
def
panelDtilde μ D G T_rv g t :
ℝ
given by
((∫ ω, D ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ) / cellMass μ G T_rv g t)
- panelPropensityHat μ D G T_rv g t
theorem num_per_cell_panel reviewed
⚑ flagged
Causalean.Panel.EstimandCharacterization.StaggeredTWFEDecomposition
Per-cell numerator identity. On the cohort-period cell (g, t), if the treatment D is almost-everywhere equal, on that cell, to its own cell mean (cell-measurability of D), then the integral of the propensity-residual D - panelPropensity times the outcome Y over the cell equals the cell mass times the cell's residualized treatment panelDtilde times the outcome's cell mean:
Formal statement
hypotheses
Ω :
Type u_1
𝒢 :
Type u_2
T :
ℕ
μ :
D Y :
Ω → ℝ
G :
Ω → 𝒢
T_rv :
Ω → Fin T
G_meas :
T_meas :
Measurable T_rv
g :
𝒢
t :
Fin T
hD_cell :
∀ᵐ ω ∂μ.restrict {ω' | G ω' = g ∧ T_rv ω' = t}, D ω
= (∫ ω', D ω' * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ) / cellMass μ G T_rv g t
conclusion
∫ ω, (D ω - panelPropensity μ D G T_rv ω) * Y ω * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ
= cellMass μ G T_rv g t * panelDtilde μ D G T_rv g t * cellMean μ Y G T_rv g t
Proof (Lean source)
theorem num_per_cell_panel
(μ : Measure Ω) [IsFiniteMeasure μ]
(D Y : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T)
(G_meas : Measurable G) (T_meas : Measurable T_rv)
(g : 𝒢) (t : Fin T)
(hD_cell : ∀ᵐ ω ∂μ.restrict {ω' | G ω' = g ∧ T_rv ω' = t},
D ω = (∫ ω', D ω' * indicator {ω' | G ω' = g ∧ T_rv ω' = t}
(fun _ => (1 : ℝ)) ω' ∂μ) / cellMass μ G T_rv g t) :
∫ ω, (D ω - panelPropensity μ D G T_rv ω) * Y ω
* indicator {ω' | G ω' = g ∧ T_rv ω' = t}
(fun _ => (1 : ℝ)) ω ∂μ
= cellMass μ G T_rv g t * panelDtilde μ D G T_rv g t
* cellMean μ Y G T_rv g t := by
classical
let s : Set Ω := {ω | G ω = g ∧ T_rv ω = t}
let I : Ω → ℝ := fun ω => indicator s (fun _ => (1 : ℝ)) ω
let q : ℝ := panelDtilde μ D G T_rv g t
let mY : ℝ := cellMean μ Y G T_rv g t
have hs : MeasurableSet s := by
have hG : MeasurableSet {ω : Ω | G ω = g} :=
G_meas (measurableSet_singleton g)
have hT : MeasurableSet {ω : Ω | T_rv ω = t} :=
T_meas (measurableSet_singleton t)
simpa [s, Set.inter_def] using hG.inter hT
change ∫ ω, (D ω - panelPropensity μ D G T_rv ω) * Y ω * I ω ∂μ
= cellMass μ G T_rv g t * q * mY
have h_on :
(fun ω => (D ω - panelPropensity μ D G T_rv ω) * Y ω * I ω)
=ᵐ[μ.restrict s] (fun ω => q * (Y ω * I ω)) := by
filter_upwards [hD_cell, MeasureTheory.ae_restrict_mem hs] with ω hDω hωs
rcases hωs with ⟨hGω, hTω⟩
have hpω :
panelPropensity μ D G T_rv ω = panelPropensityHat μ D G T_rv g t :=
panelPropensity_eq_hat_of_mem μ D G T_rv hGω hTω
have hres : D ω - panelPropensity μ D G T_rv ω = q := by
rw [hDω, hpω]
simp [q, panelDtilde]
simp [I, s, hGω, hTω, hres]
have h_off :
(fun ω => (D ω - panelPropensity μ D G T_rv ω) * Y ω * I ω)
=ᵐ[μ.restrict sᶜ] (fun ω => q * (Y ω * I ω)) := by
rw [EventuallyEq, MeasureTheory.ae_restrict_iff' hs.compl]
filter_upwards with ω hωs
have hω_not_s : ω ∉ s := by simpa using hωs
simp [I, indicator, hω_not_s]
have h_ae :
(fun ω => (D ω - panelPropensity μ D G T_rv ω) * Y ω * I ω)
=ᵐ[μ] (fun ω => q * (Y ω * I ω)) :=
MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl s h_on h_off
have hmean :
mY * cellMass μ G T_rv g t =
∫ ω, Y ω * I ω ∂μ := by
simpa [mY, cellMean, I, s] using
(panel_cell_integral_div_mul_cellMass μ Y G T_rv G_meas T_meas g t)
calc
∫ ω, (D ω - panelPropensity μ D G T_rv ω) * Y ω * I ω ∂μ
= ∫ ω, q * (Y ω * I ω) ∂μ := integral_congr_ae h_ae
_ = q * ∫ ω, Y ω * I ω ∂μ := integral_const_mul q (fun ω => Y ω * I ω)
_ = q * (mY * cellMass μ G T_rv g t) := by rw [hmean]
_ = cellMass μ G T_rv g t * q * mY := by ring
1 supporting declaration (lemmas, instances)
-
denom_per_cell_paneltheorem — Per-cell denominator identity. On the cell {G = g ∧ T_rv = t}, (D - panelPropensity)(ω) = panelDtilde μ D G T_rv g t; squaring and integrating over the cell giveshypothesesΩ :sharedType u_1𝒢 :sharedType u_2T :sharedℕμ :D :Ω → ℝG :Ω → 𝒢T_rv :Ω → Fin TG_meas :T_meas :Measurable T_rvg :𝒢t :Fin ThD_cell :∀ᵐ ω ∂μ.restrict {ω' | G ω' = g ∧ T_rv ω' = t}, D ω= (∫ ω', D ω' * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ) / cellMass μ G T_rv g tconclusion∫ ω, (D ω - panelPropensity μ D G T_rv ω) * (D ω - panelPropensity μ D G T_rv ω) * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ= cellMass μ G T_rv g t * (panelDtilde μ D G T_rv g t)^2Proof (Lean source)
theorem denom_per_cell_panel (μ : Measure Ω) [IsFiniteMeasure μ] (D : Ω → ℝ) (G : Ω → 𝒢) (T_rv : Ω → Fin T) (G_meas : Measurable G) (T_meas : Measurable T_rv) (g : 𝒢) (t : Fin T) (hD_cell : ∀ᵐ ω ∂μ.restrict {ω' | G ω' = g ∧ T_rv ω' = t}, D ω = (∫ ω', D ω' * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω' ∂μ) / cellMass μ G T_rv g t) : ∫ ω, (D ω - panelPropensity μ D G T_rv ω) * (D ω - panelPropensity μ D G T_rv ω) * indicator {ω' | G ω' = g ∧ T_rv ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = cellMass μ G T_rv g t * (panelDtilde μ D G T_rv g t)^2 := by classical let s : Set Ω := {ω | G ω = g ∧ T_rv ω = t} let I : Ω → ℝ := fun ω => indicator s (fun _ => (1 : ℝ)) ω let q : ℝ := panelDtilde μ D G T_rv g t have hs : MeasurableSet s := by have hG : MeasurableSet {ω : Ω | G ω = g} := G_meas (measurableSet_singleton g) have hT : MeasurableSet {ω : Ω | T_rv ω = t} := T_meas (measurableSet_singleton t) simpa [s, Set.inter_def] using hG.inter hT change ∫ ω, (D ω - panelPropensity μ D G T_rv ω) * (D ω - panelPropensity μ D G T_rv ω) * I ω ∂μ = cellMass μ G T_rv g t * q^2 have h_on : (fun ω => (D ω - panelPropensity μ D G T_rv ω) * (D ω - panelPropensity μ D G T_rv ω) * I ω) =ᵐ[μ.restrict s] (fun ω => q^2 * I ω) := by filter_upwards [hD_cell, MeasureTheory.ae_restrict_mem hs] with ω hDω hωs rcases hωs with ⟨hGω, hTω⟩ have hpω : panelPropensity μ D G T_rv ω = panelPropensityHat μ D G T_rv g t := panelPropensity_eq_hat_of_mem μ D G T_rv hGω hTω have hres : D ω - panelPropensity μ D G T_rv ω = q := by rw [hDω, hpω] simp [q, panelDtilde] simp [I, s, hGω, hTω, hres, pow_two] have h_off : (fun ω => (D ω - panelPropensity μ D G T_rv ω) * (D ω - panelPropensity μ D G T_rv ω) * I ω) =ᵐ[μ.restrict sᶜ] (fun ω => q^2 * I ω) := by rw [EventuallyEq, MeasureTheory.ae_restrict_iff' hs.compl] filter_upwards with ω hωs have hω_not_s : ω ∉ s := by simpa using hωs simp [I, indicator, hω_not_s] have h_ae : (fun ω => (D ω - panelPropensity μ D G T_rv ω) * (D ω - panelPropensity μ D G T_rv ω) * I ω) =ᵐ[μ] (fun ω => q^2 * I ω) := MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl s h_on h_off calc ∫ ω, (D ω - panelPropensity μ D G T_rv ω) * (D ω - panelPropensity μ D G T_rv ω) * I ω ∂μ = ∫ ω, q^2 * I ω ∂μ := integral_congr_ae h_ae _ = q^2 * ∫ ω, I ω ∂μ := integral_const_mul (q^2) I _ = q^2 * cellMass μ G T_rv g t := by rw [integral_panel_cell_indicator_one_eq_cellMass μ G T_rv G_meas T_meas g t] _ = cellMass μ G T_rv g t * q^2 := by ring