Panel.Estimand­Characterization.OLSWeight­Decomposition.Support

theorem cellMean_eq_eventCondExp {Ω 𝒢 : Type*} [MeasurableSpace Ω] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] (μ : Measure Ω) (F : Ω → ℝ) (G : Ω → 𝒢) (G_meas : Measurable G) (g : 𝒢) : CellBridge.cellMean μ F G g = eventCondExp μ {ω | G ω = g} F := by have hA : MeasurableSet {ω | G ω = g} := G_meas (measurableSet_singleton g) unfold CellBridge.cellMean eventCondExp CellBridge.cellMass congr 1 rw [← MeasureTheory.integral_indicator hA] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall (fun ω => ?_)) by_cases hω : ω ∈ {ω | G ω = g} · simp [Set.indicator_of_mem hω] · simp [Set.indicator_of_notMem hω]

theorem integral_eq_sum_cell {Ω 𝒢 : Type*} [MeasurableSpace Ω] [Fintype 𝒢] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] (μ : 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 residY_cell_orthogonal {Ω 𝒢 : Type*} [MeasurableSpace Ω] [Fintype 𝒢] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] (μ : Measure Ω) [IsFiniteMeasure μ] (Y : Ω → ℝ) (G : Ω → 𝒢) (G_meas : Measurable G) (Y_memLp : MemLp Y 2 μ) (g : 𝒢) : ∫ ω, (Y ω - meanReg μ Y G ω) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = 0 := by classical let s : Set Ω := {ω | G ω = g} let I : Ω → ℝ := fun ω => indicator s (fun _ => (1 : ℝ)) ω let m : ℝ := (∫ ω, Y ω * I ω ∂μ) / cellMass μ G g have hI_mem : MemLp I 2 μ := by simpa [I, s] using indicator_cell_memLp μ G G_meas g have hYInt : Integrable (fun ω => Y ω * I ω) μ := Y_memLp.integrable_mul hI_mem have hmIInt : Integrable (fun ω => m * I ω) μ := (hI_mem.const_mul m).integrable (by norm_num : (1 : ENNReal) ≤ 2) have h_ae : (fun ω => (Y ω - meanReg μ Y G ω) * I ω) =ᵐ[μ] (fun ω => Y ω * I ω - m * I ω) := by filter_upwards [] with ω by_cases hω : ω ∈ s · have hm : meanReg μ Y G ω = m := by simpa [m, I, s] using meanReg_eq_cellMean_of_mem μ Y G hω simp [I, indicator, hω, hm, m] · simp [I, indicator, hω] have hInt : ∫ ω, (Y ω - meanReg μ Y G ω) * I ω ∂μ = ∫ ω, Y ω * I ω ∂μ - ∫ ω, m * I ω ∂μ := by calc ∫ ω, (Y ω - meanReg μ Y G ω) * I ω ∂μ = ∫ ω, Y ω * I ω - m * I ω ∂μ := integral_congr_ae h_ae _ = ∫ ω, Y ω * I ω ∂μ - ∫ ω, m * I ω ∂μ := integral_sub hYInt hmIInt have hIint : ∫ ω, I ω ∂μ = cellMass μ G g := by simpa [I, s] using integral_cell_indicator_one_eq_cellMass μ G G_meas g have hmInt : ∫ ω, m * I ω ∂μ = m * cellMass μ G g := by calc ∫ ω, m * I ω ∂μ = m * ∫ ω, I ω ∂μ := integral_const_mul m I _ = m * cellMass μ G g := by rw [hIint] have hmean : m * cellMass μ G g = ∫ ω, Y ω * I ω ∂μ := by simpa [m, I, s, cellMass, CellBridge.cellMean] using (CellBridge.cellMean_mul_cellMass μ Y G g) change ∫ ω, (Y ω - meanReg μ Y G ω) * I ω ∂μ = 0 rw [hInt, hmInt, hmean] ring

theorem partitionOf_p_eq_eventCondExp {Ω 𝒢 : Type*} [MeasurableSpace Ω] [Fintype 𝒢] [DecidableEq 𝒢] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] (μ : Measure Ω) [IsProbabilityMeasure μ] (D Y0 Y1 : Ω → ℝ) (G : Ω → 𝒢) (G_meas : Measurable G) (D_binary : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1) (overlap : 0 < ∑ g, cellMass μ G g * (cellShare μ D G g * (1 - cellShare μ D G g))) (g : 𝒢) : (partitionOf μ D Y0 Y1 G G_meas D_binary overlap).p g = eventCondExp μ {ω | G ω = g} D := cellShare_eq_eventCondExp μ D G G_meas g

theorem num_per_cell {Ω 𝒢 : Type*} [MeasurableSpace Ω] [Fintype 𝒢] [DecidableEq 𝒢] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] (μ : Measure Ω) [IsProbabilityMeasure μ] (D Y Y0 Y1 : Ω → ℝ) (G : Ω → 𝒢) (G_meas : Measurable G) (D_meas : Measurable D) (D_binary : ∀ᵐ ω ∂μ, D ω = 0 ∨ D ω = 1) (Y0_memLp : MemLp Y0 2 μ) (Y1_memLp : MemLp Y1 2 μ) (consis : Y =ᵐ[μ] fun ω => D ω * Y1 ω + (1 - D ω) * Y0 ω) (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)) (g : 𝒢) : ∫ ω, (D ω - propensity μ D G ω) * Y ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = cellMass μ G g * (cellShare μ D G g * (1 - cellShare μ D G g)) * cellTau μ Y0 Y1 G g := by let s : Set Ω := {ω | G ω = g} let I : Ω → ℝ := fun ω => indicator s (fun _ => (1 : ℝ)) ω let J1 : Ω → ℝ := fun ω => indicator {ω' | D ω' = (1 : ℝ)} (fun _ => (1 : ℝ)) ω let J0 : Ω → ℝ := fun ω => indicator {ω' | D ω' = (0 : ℝ)} (fun _ => (1 : ℝ)) ω let p : ℝ := cellShare μ D G g let M : ℝ := cellMass μ G g let τ : ℝ := cellTau μ Y0 Y1 G g let B1 : ℝ := ∫ ω, Y1 ω * I ω ∂μ let B0 : ℝ := ∫ ω, Y0 ω * I ω ∂μ have hI_mem : MemLp I 2 μ := by simpa [I, s] using indicator_cell_memLp μ G G_meas g have hY1IInt : Integrable (fun ω => Y1 ω * I ω) μ := Y1_memLp.integrable_mul hI_mem have hY0IInt : Integrable (fun ω => Y0 ω * I ω) μ := Y0_memLp.integrable_mul hI_mem have hY1J1IInt : Integrable (fun ω => Y1 ω * J1 ω * I ω) μ := by simpa [J1, I, s] using integrable_mul_indicator_D_G μ Y1 D G D_meas G_meas Y1_memLp (1 : ℝ) g have hY0J0IInt : Integrable (fun ω => Y0 ω * J0 ω * I ω) μ := by simpa [J0, I, s] using integrable_mul_indicator_D_G μ Y0 D G D_meas G_meas Y0_memLp (0 : ℝ) g have hTerm1Int : Integrable (fun ω => (1 - p) * (Y1 ω * J1 ω * I ω)) μ := hY1J1IInt.const_mul (1 - p) have hTerm0Int : Integrable (fun ω => p * (Y0 ω * J0 ω * I ω)) μ := hY0J0IInt.const_mul p have h_ae : (fun ω => (D ω - propensity μ D G ω) * Y ω * I ω) =ᵐ[μ] (fun ω => (1 - p) * (Y1 ω * J1 ω * I ω) - p * (Y0 ω * J0 ω * I ω)) := by filter_upwards [D_binary, consis] with ω hD hY by_cases hω : ω ∈ s · have hp : propensity μ D G ω = p := propensity_eq_cellShare_of_mem μ D G hω have hGω : G ω = g := hω rcases hD with hD0 | hD1 · have hY0 : Y ω = Y0 ω := by simpa [hD0] using hY simp [I, J1, J0, s, indicator, hGω, hp, p, hD0, hY0] · have hY1 : Y ω = Y1 ω := by simpa [hD1] using hY simp [I, J1, J0, s, indicator, hGω, hp, p, hD1, hY1] · have hGne : G ω ≠ g := by simpa [s] using hω simp [I, s, indicator, hGne] have hInt : ∫ ω, (D ω - propensity μ D G ω) * Y ω * I ω ∂μ = (1 - p) * (∫ ω, Y1 ω * J1 ω * I ω ∂μ) - p * (∫ ω, Y0 ω * J0 ω * I ω ∂μ) := by calc ∫ ω, (D ω - propensity μ D G ω) * Y ω * I ω ∂μ = ∫ ω, (1 - p) * (Y1 ω * J1 ω * I ω) - p * (Y0 ω * J0 ω * I ω) ∂μ := integral_congr_ae h_ae _ = ∫ ω, (1 - p) * (Y1 ω * J1 ω * I ω) ∂μ - ∫ ω, p * (Y0 ω * J0 ω * I ω) ∂μ := integral_sub hTerm1Int hTerm0Int _ = (1 - p) * (∫ ω, Y1 ω * J1 ω * I ω ∂μ) - p * (∫ ω, Y0 ω * J0 ω * I ω ∂μ) := by rw [integral_const_mul, integral_const_mul] have hA1 : ∫ ω, Y1 ω * J1 ω * I ω ∂μ = B1 * p := by simpa [J1, I, s, B1, p] using CMI (1 : ℝ) g (inr rfl) have hA0 : ∫ ω, Y0 ω * J0 ω * I ω ∂μ = B0 * (1 - p) := by simpa [J0, I, s, B0, p] using CMI (0 : ℝ) g (inl rfl) have hdiff : ∫ ω, (Y1 ω - Y0 ω) * I ω ∂μ = B1 - B0 := by calc ∫ ω, (Y1 ω - Y0 ω) * I ω ∂μ = ∫ ω, Y1 ω * I ω - Y0 ω * I ω ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω ring _ = B1 - B0 := by simpa [B1, B0] using integral_sub hY1IInt hY0IInt have hTauM : τ * M = B1 - B0 := by calc τ * M = ∫ ω, (Y1 ω - Y0 ω) * I ω ∂μ := by simpa [τ, M, I, s, cellTau, cellMass] using (CellBridge.cellMean_mul_cellMass μ (fun ω => Y1 ω - Y0 ω) G g) _ = B1 - B0 := hdiff change ∫ ω, (D ω - propensity μ D G ω) * Y ω * I ω ∂μ = M * (p * (1 - p)) * τ calc ∫ ω, (D ω - propensity μ D G ω) * Y ω * I ω ∂μ = (1 - p) * (B1 * p) - p * (B0 * (1 - p)) := by rw [hInt, hA1, hA0] _ = p * (1 - p) * (B1 - B0) := by ring _ = M * (p * (1 - p)) * τ := by rw [← hTauM] ring