Panel.Estimand­Characterization.Staggered­TWFEDecomposition.Support

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

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)

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

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

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 exact integral_add hsumGI_int hsumTI_int _ = ∫ ω, 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 ω ∂μ := integral_sub hFI_int hPanelI_int _ = 0 := by rw [hpanel]; ring

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 exact integral_add hsumGI_int hsumTI_int _ = ∫ ω, 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 ω ∂μ := integral_sub hFI_int hPanelI_int _ = 0 := by rw [hpanel]; ring

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

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

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

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

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

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

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)

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)

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]

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)

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)

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]

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)

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

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

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

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

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 : ℝ)) ω ∂μ))

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