PO.ID.Partial.Lee

lemma integrableY (hA : S.BaseAssumptions) : Integrable S.factualY P.μ := by have hY1_ind : Integrable (fun ω => S.YofA true ω * S.aVar.indicator true ω) P.μ := S.aVar.integrable_mul_indicator true (measurableSet_singleton _) hA.integrableY1 have hY0_ind : Integrable (fun ω => S.YofA false ω * S.aVar.indicator false ω) P.μ := S.aVar.integrable_mul_indicator false (measurableSet_singleton _) hA.integrableY0 refine (hY1_ind.add hY0_ind).congr ?_ filter_upwards with ω have htrue := congr_fun (POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn hA.consistency S.yVar S.aVar true (Ne.symm S.hAY)) ω have hfalse := congr_fun (POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn hA.consistency S.yVar S.aVar false (Ne.symm S.hAY)) ω have htrue' : S.YofA true ω * S.aVar.indicator true ω = S.factualY ω * S.aVar.indicator true ω := by simpa [POLeeSystem.YofA, POLeeSystem.factualY] using htrue.symm have hfalse' : S.YofA false ω * S.aVar.indicator false ω = S.factualY ω * S.aVar.indicator false ω := by simpa [POLeeSystem.YofA, POLeeSystem.factualY] using hfalse.symm have hsum := S.aVar.indicator_add_indicator_not ω calc S.YofA true ω * S.aVar.indicator true ω + S.YofA false ω * S.aVar.indicator false ω = S.factualY ω * S.aVar.indicator true ω + S.factualY ω * S.aVar.indicator false ω := by rw [htrue', hfalse'] _ = S.factualY ω * (S.aVar.indicator true ω + S.aVar.indicator false ω) := by ring _ = S.factualY ω := by rw [hsum, mul_one]

lemma harmedSelected_ae_empty (hMono : ∀ᵐ ω ∂P.μ, S.SelOfA false ω ≤ S.SelOfA true ω) : P.μ S.harmedSelected = 0 := by -- Monotonicity says that on a co-null set, SelOfA false ω ≤ SelOfA true ω -- (with ≤ on Bool meaning false ≤ true and false ≤ false and true ≤ true, -- but NOT true ≤ false). On harmedSelected, SelOfA false = true and -- SelOfA true = false, contradicting the inequality. So -- harmedSelected ⊆ {ω | ¬(SelOfA false ω ≤ SelOfA true ω)} which is null. -- Use `measure_mono_null` against the complement of the a.s. set, plus -- `Bool.not_le` (or a direct case split) to discharge the implication. have hNull : P.μ {ω | ¬ S.SelOfA false ω ≤ S.SelOfA true ω} = 0 := by rwa [ae_iff] at hMono exact MeasureTheory.measure_mono_null (by intro ω hω rcases hω with ⟨h0, h1⟩ simp [h0, h1]) hNull

lemma m0_eq_eventCondExp_Y0_alwaysSelected (hA : S.BaseAssumptions) (hMono : S.MonotoneSelection) : S.m0 = eventCondExp P.μ S.alwaysSelected (S.YofA false) := by have hy_on_selectedControl : ∀ ω ∈ S.selectedControl, S.factualY ω = S.YofA false ω := by intro ω hω have hcf : S.YofA false ω = S.factualY ω := POVar.cf_eq_factual_on_event hA.consistency S.yVar S.aVar false S.hAY.symm hω.1 exact hcf.symm have hY : eventCondExp P.μ S.selectedControl S.factualY = eventCondExp P.μ S.selectedControl (S.YofA false) := eventCondExp_congr_on P.μ S.measurableSet_selectedControl hy_on_selectedControl have hSelectedControl : S.selectedControl = S.aEvent false ∩ S.selOfAFalseSet := by ext ω constructor · intro hω have hsel_cf : S.SelOfA false ω = S.factualSel ω := POVar.cf_eq_factual_on_event hA.consistency S.selVar S.aVar false S.hASel.symm hω.1 exact ⟨hω.1, by simpa [selOfAFalseSet, selEvent, POVar.event, factualSel, hsel_cf] using hω.2⟩ · intro hω have hsel_cf : S.SelOfA false ω = S.factualSel ω := POVar.cf_eq_factual_on_event hA.consistency S.selVar S.aVar false S.hASel.symm hω.1 exact ⟨hω.1, by simpa [selOfAFalseSet, selEvent, POVar.event, factualSel, hsel_cf] using hω.2⟩ have hdrop : eventCondExp P.μ (S.aEvent false ∩ S.selOfAFalseSet) (S.YofA false) = eventCondExp P.μ S.selOfAFalseSet (S.YofA false) := by have hpair_meas : Measurable (fun ω => (S.YofA false ω, S.SelOfA false ω)) := prodMk (S.measurable_YofA false) (S.measurable_SelOfA false) have hselSet_pair : MeasurableSet {p : ℝ × Bool | p.2 = true} := measurable_snd (measurableSet_singleton true) have hφ_meas : Measurable (fun p : ℝ × Bool => if p.2 = true then p.1 else (0 : ℝ)) := by exact Measurable.ite hselSet_pair measurable_fst measurable_const have hφ_indicator : (fun ω => if S.SelOfA false ω = true then S.YofA false ω else (0 : ℝ)) = S.selOfAFalseSet.indicator (S.YofA false) := by funext ω by_cases hω : S.SelOfA false ω = true · simp [selOfAFalseSet, hω] · simp [selOfAFalseSet, hω] have hraw_num : ∫ ω in S.aEvent false, S.selOfAFalseSet.indicator (S.YofA false) ω ∂P.μ = (P.μ (S.aEvent false)).toReal * ∫ ω, S.selOfAFalseSet.indicator (S.YofA false) ω ∂P.μ := by have hraw := (hA.randAssign false).integral_restrict_preimage_eq_mul S.measurable_factualA.aemeasurable hpair_meas.aemeasurable (measurableSet_singleton false) (S.measurable_factualA (measurableSet_singleton false)) hφ_meas.aestronglyMeasurable simpa [aEvent, factualA, POVar.event, hφ_indicator] using hraw have hnum : ∫ ω in S.aEvent false ∩ S.selOfAFalseSet, S.YofA false ω ∂P.μ = (P.μ (S.aEvent false)).toReal * ∫ ω in S.selOfAFalseSet, S.YofA false ω ∂P.μ := by rw [← MeasureTheory.setIntegral_indicator S.measurableSet_selOfAFalseSet, ← MeasureTheory.integral_indicator S.measurableSet_selOfAFalseSet] exact hraw_num have hden_enn : P.μ (S.aEvent false ∩ S.selOfAFalseSet) = P.μ (S.aEvent false) * P.μ S.selOfAFalseSet := by have hraw := (hA.randAssign false).measure_inter_preimage_eq_mul {false} {p : ℝ × Bool | p.2 = true} (measurableSet_singleton false) hselSet_pair simpa [aEvent, factualA, selOfAFalseSet, POVar.event] using hraw have hden : (P.μ (S.aEvent false ∩ S.selOfAFalseSet)).toReal = (P.μ (S.aEvent false)).toReal * (P.μ S.selOfAFalseSet).toReal := by rw [hden_enn, ENNReal.toReal_mul] have hAfalse_ne_zero : (P.μ (S.aEvent false)).toReal ≠ 0 := by rw [ENNReal.toReal_ne_zero] exact ⟨hA.posAFalse, measure_ne_top _ _⟩ unfold eventCondExp rw [hnum, hden] exact mul_div_mul_left _ _ hAfalse_ne_zero have hAS : eventCondExp P.μ S.selOfAFalseSet (S.YofA false) = eventCondExp P.μ S.alwaysSelected (S.YofA false) := by unfold eventCondExp have hset := S.selOfAFalseSet_ae_eq_alwaysSelected hMono.monotone rw [MeasureTheory.setIntegral_congr_set hset, measure_congr hset] unfold m0 rw [hY, hSelectedControl, hdrop, hAS]

lemma YofA_true_in_finset_ae_alwaysSelected (hA : S.BaseAssumptions) (𝒴 : Finset ℝ) (hSupp : ∀ᵐ ω ∂(P.μ.restrict S.selectedTreated), S.factualY ω ∈ 𝒴) : (∀ᵐ ω ∂(P.μ.restrict S.alwaysSelected), S.YofA true ω ∈ 𝒴) ∧ (∀ᵐ ω ∂(P.μ.restrict S.helpedSelected), S.YofA true ω ∈ 𝒴) := by classical have hSelectedTreated : S.selectedTreated = S.aEvent true ∩ S.selOfATrueSet := by ext ω constructor · intro hω have hsel_cf : S.SelOfA true ω = S.factualSel ω := POVar.cf_eq_factual_on_event hA.consistency S.selVar S.aVar true S.hASel.symm hω.1 exact ⟨hω.1, by simpa [selOfATrueSet, selEvent, POVar.event, factualSel, hsel_cf] using hω.2⟩ · intro hω have hsel_cf : S.SelOfA true ω = S.factualSel ω := POVar.cf_eq_factual_on_event hA.consistency S.selVar S.aVar true S.hASel.symm hω.1 exact ⟨hω.1, by simpa [selOfATrueSet, selEvent, POVar.event, factualSel, hsel_cf] using hω.2⟩ have hFactBad_meas : MeasurableSet {ω | S.factualY ω ∉ 𝒴} := ((S.measurable_factualY) ((𝒴.finite_toSet).measurableSet)).compl have hSupp_null_restrict : (P.μ.restrict S.selectedTreated) {ω | S.factualY ω ∉ 𝒴} = 0 := by simpa using (MeasureTheory.ae_iff.mp hSupp) have hFactBad_selected : P.μ ({ω | S.factualY ω ∉ 𝒴} ∩ S.selectedTreated) = 0 := by rw [← MeasureTheory.Measure.restrict_apply hFactBad_meas] exact hSupp_null_restrict have hBad_selected : P.μ ({ω | S.YofA true ω ∉ 𝒴} ∩ S.selectedTreated) = 0 := by refine MeasureTheory.measure_mono_null ?_ hFactBad_selected intro ω hω rcases hω with ⟨hbad, hst⟩ have hcf : S.YofA true ω = S.factualY ω := POVar.cf_eq_factual_on_event hA.consistency S.yVar S.aVar true S.hAY.symm hst.1 exact ⟨by simpa [← hcf] using hbad, hst⟩ have hBad_selected' : P.μ (S.aEvent true ∩ ({ω | S.YofA true ω ∉ 𝒴} ∩ S.selOfATrueSet)) = 0 := by rw [hSelectedTreated] at hBad_selected simpa [Set.inter_assoc, Set.inter_left_comm, Set.inter_comm] using hBad_selected have hpair_meas : Measurable (fun ω => (S.YofA true ω, S.SelOfA true ω)) := prodMk (S.measurable_YofA true) (S.measurable_SelOfA true) have hbadPair_meas : MeasurableSet {p : ℝ × Bool | p.1 ∉ 𝒴 ∧ p.2 = true} := (((measurable_fst) ((𝒴.finite_toSet).measurableSet)).compl).inter (measurable_snd (measurableSet_singleton true)) have hprod : P.μ (S.aEvent true ∩ ({ω | S.YofA true ω ∉ 𝒴} ∩ S.selOfATrueSet)) = P.μ (S.aEvent true) * P.μ ({ω | S.YofA true ω ∉ 𝒴} ∩ S.selOfATrueSet) := by have hraw := (hA.randAssign true).measure_inter_preimage_eq_mul {true} {p : ℝ × Bool | p.1 ∉ 𝒴 ∧ p.2 = true} (measurableSet_singleton true) hbadPair_meas exact hraw have hBad_selOfATrue : P.μ ({ω | S.YofA true ω ∉ 𝒴} ∩ S.selOfATrueSet) = 0 := by have hmul_zero : P.μ (S.aEvent true) * P.μ ({ω | S.YofA true ω ∉ 𝒴} ∩ S.selOfATrueSet) = 0 := by rw [← hprod] exact hBad_selected' rcases mul_eq_zero.mp hmul_zero with hA_zero | hbad_zero · exact elim (hA.posATrue hA_zero) · exact hbad_zero have hBad_alwaysSelected : P.μ ({ω | S.YofA true ω ∉ 𝒴} ∩ S.alwaysSelected) = 0 := by refine MeasureTheory.measure_mono_null ?_ hBad_selOfATrue intro ω hω exact ⟨hω.1, hω.2.2⟩ have hBad_helpedSelected : P.μ ({ω | S.YofA true ω ∉ 𝒴} ∩ S.helpedSelected) = 0 := by refine MeasureTheory.measure_mono_null ?_ hBad_selOfATrue intro ω hω exact ⟨hω.1, hω.2.2⟩ constructor · apply (MeasureTheory.ae_restrict_iff' S.measurableSet_alwaysSelected).mpr rw [MeasureTheory.ae_iff] refine MeasureTheory.measure_mono_null (fun ω hω => ?_) hBad_alwaysSelected have hω' : ¬ (ω ∈ S.alwaysSelected → S.YofA true ω ∈ 𝒴) := hω obtain ⟨hmem, hbad⟩ := Classical.not_imp.mp hω' exact ⟨hbad, hmem⟩ · apply (MeasureTheory.ae_restrict_iff' S.measurableSet_helpedSelected).mpr rw [MeasureTheory.ae_iff] refine MeasureTheory.measure_mono_null (fun ω hω => ?_) hBad_helpedSelected have hω' : ¬ (ω ∈ S.helpedSelected → S.YofA true ω ∈ 𝒴) := hω obtain ⟨hmem, hbad⟩ := Classical.not_imp.mp hω' exact ⟨hbad, hmem⟩

theorem lee_bounds_ATT_AS [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMono : S.MonotoneSelection) (𝒴 : Finset ℝ) (hSupp : ∀ᵐ ω ∂(P.μ.restrict S.selectedTreated), S.factualY ω ∈ 𝒴) : S.lowerTrimMean 𝒴 - S.m0 ≤ eventCondExp P.μ S.alwaysSelected (fun ω => S.YofA true ω - S.YofA false ω) ∧ eventCondExp P.μ S.alwaysSelected (fun ω => S.YofA true ω - S.YofA false ω) ≤ S.upperTrimMean 𝒴 - S.m0 := by have hStepA := S.m0_eq_eventCondExp_Y0_alwaysSelected hA hMono have hStepC := S.trimmed_bounds_condExp_Y1_AS hA hMono 𝒴 hSupp have hSub : eventCondExp P.μ S.alwaysSelected (fun ω => S.YofA true ω - S.YofA false ω) = eventCondExp P.μ S.alwaysSelected (S.YofA true) - eventCondExp P.μ S.alwaysSelected (S.YofA false) := by exact (eventCondExp_sub P.μ S.alwaysSelected (g₁ := S.YofA true) (g₂ := S.YofA false) hA.integrableY1.integrableOn hA.integrableY0.integrableOn) constructor · rw [hSub, hStepA] exact sub_le_sub_right hStepC.1 _ · rw [hSub, hStepA] exact sub_le_sub_right hStepC.2 _

lemma selectedTreated_measure_split (hA : S.BaseAssumptions) : (P.μ S.selectedTreated).toReal = (P.μ (S.aEvent true)).toReal * ((P.μ S.alwaysSelected).toReal + (P.μ S.helpedSelected).toReal) := by have hSelectedTreated : S.selectedTreated = S.aEvent true ∩ S.selOfATrueSet := by ext ω constructor · intro hω have hsel_cf : S.SelOfA true ω = S.factualSel ω := POVar.cf_eq_factual_on_event hA.consistency S.selVar S.aVar true S.hASel.symm hω.1 exact ⟨hω.1, by simpa [selOfATrueSet, selEvent, POVar.event, factualSel, hsel_cf] using hω.2⟩ · intro hω have hsel_cf : S.SelOfA true ω = S.factualSel ω := POVar.cf_eq_factual_on_event hA.consistency S.selVar S.aVar true S.hASel.symm hω.1 exact ⟨hω.1, by simpa [selOfATrueSet, selEvent, POVar.event, factualSel, hsel_cf] using hω.2⟩ have hpair_meas : Measurable (fun ω => (S.YofA true ω, S.SelOfA true ω)) := prodMk (S.measurable_YofA true) (S.measurable_SelOfA true) have hselSet_pair : MeasurableSet {p : ℝ × Bool | p.2 = true} := measurable_snd (measurableSet_singleton true) have hden_enn : P.μ (S.aEvent true ∩ S.selOfATrueSet) = P.μ (S.aEvent true) * P.μ S.selOfATrueSet := by have hraw := (hA.randAssign true).measure_inter_preimage_eq_mul {true} {p : ℝ × Bool | p.2 = true} (measurableSet_singleton true) hselSet_pair simpa [aEvent, factualA, selOfATrueSet, POVar.event] using hraw have hsplit_enn : P.μ S.selOfATrueSet = P.μ S.alwaysSelected + P.μ S.helpedSelected := by rw [S.selOfATrueSet_eq_alwaysSelected_union_helpedSelected] exact MeasureTheory.measure_union S.disjoint_alwaysSelected_helpedSelected S.measurableSet_helpedSelected calc (P.μ S.selectedTreated).toReal = (P.μ (S.aEvent true ∩ S.selOfATrueSet)).toReal := by rw [hSelectedTreated] _ = (P.μ (S.aEvent true)).toReal * (P.μ S.selOfATrueSet).toReal := by rw [hden_enn, ENNReal.toReal_mul] _ = (P.μ (S.aEvent true)).toReal * ((P.μ S.alwaysSelected).toReal + (P.μ S.helpedSelected).toReal) := by rw [hsplit_enn, ENNReal.toReal_add (measure_ne_top P.μ S.alwaysSelected) (measure_ne_top P.μ S.helpedSelected)]

lemma trimmed_bounds_condExp_Y1_AS (hA : S.BaseAssumptions) (hMono : S.MonotoneSelection) (𝒴 : Finset ℝ) (hSupp : ∀ᵐ ω ∂(P.μ.restrict S.selectedTreated), S.factualY ω ∈ 𝒴) : S.lowerTrimMean 𝒴 ≤ eventCondExp P.μ S.alwaysSelected (S.YofA true) ∧ eventCondExp P.μ S.alwaysSelected (S.YofA true) ≤ S.upperTrimMean 𝒴 := by classical have hMw := S.Mw_alwaysSelectedTrimWeight_eq_condExp_Y1_AS hA hMono 𝒴 hSupp have hmem : S.Mw (S.alwaysSelectedTrimWeight hA hMono 𝒴 hSupp) ∈ range (fun wt : S.LeeTrimWeight 𝒴 => S.Mw wt) := by exact ⟨S.alwaysSelectedTrimWeight hA hMono 𝒴 hSupp, rfl⟩ have hf1_nonneg : ∀ y, 0 ≤ S.f1 y := by intro y unfold f1 eventCondExp exact div_nonneg (MeasureTheory.setIntegral_nonneg S.measurableSet_selectedTreated (fun ω _ => by by_cases h : S.factualY ω = y <;> simp [h])) ENNReal.toReal_nonneg let K := |(S.rho)⁻¹| * ∑ y ∈ 𝒴, |y| * S.f1 y have hBddBelow : BddBelow (range (fun wt : S.LeeTrimWeight 𝒴 => S.Mw wt)) := by refine ⟨-K, ?_⟩ rintro z ⟨wt, rfl⟩ unfold Mw have hsum_abs : |∑ y ∈ 𝒴, y * wt.w y * S.f1 y| ≤ ∑ y ∈ 𝒴, |y| * S.f1 y := by calc |∑ y ∈ 𝒴, y * wt.w y * S.f1 y| ≤ ∑ y ∈ 𝒴, |y * wt.w y * S.f1 y| := by exact Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ y ∈ 𝒴, |y| * S.f1 y := by refine Finset.sum_le_sum ?_ intro y hy have hw0 := wt.nonneg y have hw1 := wt.le_one y have hf0 := hf1_nonneg y rw [abs_mul, abs_mul] have habsw : |wt.w y| = wt.w y := abs_of_nonneg hw0 have habsf : |S.f1 y| = S.f1 y := abs_of_nonneg hf0 rw [habsw, habsf] have hinner : wt.w y * S.f1 y ≤ S.f1 y := by nlinarith [mul_le_mul_of_nonneg_right hw1 hf0] simpa [mul_assoc] using mul_le_mul_of_nonneg_left hinner (abs_nonneg y) have habs : |(S.rho)⁻¹ * ∑ y ∈ 𝒴, y * wt.w y * S.f1 y| ≤ K := by rw [abs_mul] exact mul_le_mul_of_nonneg_left hsum_abs (abs_nonneg _) nlinarith [neg_le_abs ((S.rho)⁻¹ * ∑ y ∈ 𝒴, y * wt.w y * S.f1 y)] have hBddAbove : BddAbove (range (fun wt : S.LeeTrimWeight 𝒴 => S.Mw wt)) := by refine ⟨K, ?_⟩ rintro z ⟨wt, rfl⟩ unfold Mw have hsum_abs : |∑ y ∈ 𝒴, y * wt.w y * S.f1 y| ≤ ∑ y ∈ 𝒴, |y| * S.f1 y := by calc |∑ y ∈ 𝒴, y * wt.w y * S.f1 y| ≤ ∑ y ∈ 𝒴, |y * wt.w y * S.f1 y| := by exact Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ y ∈ 𝒴, |y| * S.f1 y := by refine Finset.sum_le_sum ?_ intro y hy have hw0 := wt.nonneg y have hw1 := wt.le_one y have hf0 := hf1_nonneg y rw [abs_mul, abs_mul] have habsw : |wt.w y| = wt.w y := abs_of_nonneg hw0 have habsf : |S.f1 y| = S.f1 y := abs_of_nonneg hf0 rw [habsw, habsf] have hinner : wt.w y * S.f1 y ≤ S.f1 y := by nlinarith [mul_le_mul_of_nonneg_right hw1 hf0] simpa [mul_assoc] using mul_le_mul_of_nonneg_left hinner (abs_nonneg y) have habs : |(S.rho)⁻¹ * ∑ y ∈ 𝒴, y * wt.w y * S.f1 y| ≤ K := by rw [abs_mul] exact mul_le_mul_of_nonneg_left hsum_abs (abs_nonneg _) exact le_trans (le_abs_self _) habs -- The trimmed-mean endpoints are the inf/sup of `Mw` over the unidentified -- trim-weight nuisance, and the always-selected witness is one feasible value; -- the sandwich is then the engine bridge `mem_Icc_csInf_csSup`. have hbridge := mem_Icc_csInf_csSup hBddBelow hBddAbove hmem constructor · rw [← hMw, lowerTrimMean] exact hbridge.1 · rw [← hMw, upperTrimMean] exact hbridge.2

lemma Mw_alwaysSelectedTrimWeight_eq_condExp_Y1_AS (hA : S.BaseAssumptions) (hMono : S.MonotoneSelection) (𝒴 : Finset ℝ) (hSupp : ∀ᵐ ω ∂(P.μ.restrict S.selectedTreated), S.factualY ω ∈ 𝒴) : S.Mw (S.alwaysSelectedTrimWeight hA hMono 𝒴 hSupp) = eventCondExp P.μ S.alwaysSelected (S.YofA true) := by classical have h_f1AS_nonneg : ∀ y, 0 ≤ S.f1AS y := by intro y unfold f1AS eventCondExp exact div_nonneg (MeasureTheory.setIntegral_nonneg S.measurableSet_alwaysSelected (fun ω _ => by by_cases h : S.YofA true ω = y <;> simp [h])) ENNReal.toReal_nonneg have h_rho_nonneg : 0 ≤ S.rho := by have hp0 : 0 ≤ S.p0 := by unfold p0 pSelGivenA eventCondExp refine div_nonneg ?_ ENNReal.toReal_nonneg exact MeasureTheory.setIntegral_nonneg (S.measurableSet_aEvent false) (fun ω _ => by unfold POVar.indicator by_cases h : ω ∈ S.selVar.event true <;> simp [Set.indicator_of_mem, Set.indicator_of_notMem, h]) have hp1 : 0 ≤ S.p1 := by unfold p1 pSelGivenA eventCondExp refine div_nonneg ?_ ENNReal.toReal_nonneg exact MeasureTheory.setIntegral_nonneg (S.measurableSet_aEvent true) (fun ω _ => by unfold POVar.indicator by_cases h : ω ∈ S.selVar.event true <;> simp [Set.indicator_of_mem, Set.indicator_of_notMem, h]) exact div_nonneg hp0 hp1 have hSelectedControl : S.selectedControl = S.aEvent false ∩ S.selOfAFalseSet := by ext ω constructor · intro hω have hsel_cf : S.SelOfA false ω = S.factualSel ω := POVar.cf_eq_factual_on_event hA.consistency S.selVar S.aVar false S.hASel.symm hω.1 exact ⟨hω.1, by simpa [selOfAFalseSet, selEvent, POVar.event, factualSel, hsel_cf] using hω.2⟩ · intro hω have hsel_cf : S.SelOfA false ω = S.factualSel ω := POVar.cf_eq_factual_on_event hA.consistency S.selVar S.aVar false S.hASel.symm hω.1 exact ⟨hω.1, by simpa [selOfAFalseSet, selEvent, POVar.event, factualSel, hsel_cf] using hω.2⟩ have hSelFalseMass : (P.μ S.selectedControl).toReal = (P.μ (S.aEvent false)).toReal * (P.μ S.alwaysSelected).toReal := by have hselSet_pair : MeasurableSet {p : ℝ × Bool | p.2 = true} := measurable_snd (measurableSet_singleton true) have hden_enn : P.μ (S.aEvent false ∩ S.selOfAFalseSet) = P.μ (S.aEvent false) * P.μ S.selOfAFalseSet := by have hraw := (hA.randAssign false).measure_inter_preimage_eq_mul {false} {p : ℝ × Bool | p.2 = true} (measurableSet_singleton false) hselSet_pair simpa [aEvent, factualA, selOfAFalseSet, POVar.event] using hraw have hAS : (P.μ S.selOfAFalseSet).toReal = (P.μ S.alwaysSelected).toReal := by exact congrArg toReal (measure_congr (S.selOfAFalseSet_ae_eq_alwaysSelected hMono.monotone)) rw [hSelectedControl, hden_enn, ENNReal.toReal_mul, hAS] have hIntControl : ∫ ω in S.aEvent false, S.selVar.indicator true ω ∂P.μ = (P.μ S.selectedControl).toReal := by rw [show S.selectedControl = S.aEvent false ∩ S.selEvent true by rfl] unfold POVar.indicator selEvent rw [MeasureTheory.setIntegral_indicator (show MeasurableSet (S.selVar.event true) from S.selVar.measurableSet_event true (measurableSet_singleton _))] simp rfl have hAfalse_ne : (P.μ (S.aEvent false)).toReal ≠ 0 := by rw [ENNReal.toReal_ne_zero] exact ⟨hA.posAFalse, measure_ne_top _ _⟩ have hAS_ne : (P.μ S.alwaysSelected).toReal ≠ 0 := by intro hzero have hsel_zero : (P.μ S.selectedControl).toReal = 0 := by rw [hSelFalseMass, hzero, mul_zero] have hsel_ne : (P.μ S.selectedControl).toReal ≠ 0 := by rw [ENNReal.toReal_ne_zero] exact ⟨hA.posSelectedControl, hA.posSelCtFinite⟩ exact hsel_ne hsel_zero have hp0_eq : S.p0 = (P.μ S.alwaysSelected).toReal := by unfold p0 pSelGivenA eventCondExp rw [hIntControl, hSelFalseMass] field_simp [hAfalse_ne] have hp1_eq : S.p1 = (P.μ S.alwaysSelected).toReal + (P.μ S.helpedSelected).toReal := by have hInt : ∫ ω in S.aEvent true, S.selVar.indicator true ω ∂P.μ = (P.μ S.selectedTreated).toReal := by rw [show S.selectedTreated = S.aEvent true ∩ S.selEvent true by rfl] unfold POVar.indicator selEvent rw [MeasureTheory.setIntegral_indicator (show MeasurableSet (S.selVar.event true) from S.selVar.measurableSet_event true (measurableSet_singleton _))] simp rfl have hsplit := S.selectedTreated_measure_split hA have hAtrue_ne : (P.μ (S.aEvent true)).toReal ≠ 0 := by rw [ENNReal.toReal_ne_zero] exact ⟨hA.posATrue, measure_ne_top _ _⟩ unfold p1 pSelGivenA eventCondExp rw [hInt, hsplit] field_simp [hAtrue_ne] have hdom : ∀ y, S.rho * S.f1AS y ≤ S.f1 y := by intro y let a := (P.μ (S.aEvent true)).toReal let b := (P.μ S.alwaysSelected).toReal let c := (P.μ S.helpedSelected).toReal let iH := ∫ ω in S.helpedSelected, (if S.YofA true ω = y then (1 : ℝ) else 0) ∂P.μ have hF1Split : S.f1 y * (P.μ S.selectedTreated).toReal = a * (S.f1AS y * b + iH) := by have hraw : S.f1 y * (P.μ S.selectedTreated).toReal = a * (∫ ω in S.alwaysSelected, (if S.YofA true ω = y then (1 : ℝ) else 0) ∂P.μ + iH) := by have hden_ne : (P.μ S.selectedTreated).toReal ≠ 0 := by rw [ENNReal.toReal_ne_zero] exact ⟨hA.posSelectedTreated, hA.posSelTrFinite⟩ unfold f1 eventCondExp rw [S.selectedTreated_integral_split_indicator hA y] field_simp [hden_ne] simp [a, iH] have hASrel : S.f1AS y * b = ∫ ω in S.alwaysSelected, (if S.YofA true ω = y then (1 : ℝ) else 0) ∂P.μ := by subst b unfold f1AS eventCondExp field_simp [hAS_ne] rw [← hASrel] at hraw exact hraw have hMeasureSplit : (P.μ S.selectedTreated).toReal = a * (b + c) := by simpa [a, b, c] using S.selectedTreated_measure_split hA have ha_ne : a ≠ 0 := by subst a rw [ENNReal.toReal_ne_zero] exact ⟨hA.posATrue, measure_ne_top _ _⟩ have hbc_ne : b + c ≠ 0 := by intro hzero have hst_zero : (P.μ S.selectedTreated).toReal = 0 := by rw [hMeasureSplit, hzero, mul_zero] have hst_ne : (P.μ S.selectedTreated).toReal ≠ 0 := by rw [ENNReal.toReal_ne_zero] exact ⟨hA.posSelectedTreated, hA.posSelTrFinite⟩ exact hst_ne hst_zero have hbc_pos : 0 < b + c := by have hb : 0 ≤ b := ENNReal.toReal_nonneg have hc : 0 ≤ c := ENNReal.toReal_nonneg exact lt_of_le_of_ne' (add_nonneg hb hc) hbc_ne have hiH_nonneg : 0 ≤ iH := MeasureTheory.setIntegral_nonneg S.measurableSet_helpedSelected (fun ω _ => by by_cases h : S.YofA true ω = y <;> simp [h]) have heq : S.f1 y * (b + c) = S.f1AS y * b + iH := by have h : a * (S.f1 y * (b + c)) = a * (S.f1AS y * b + iH) := by have h' := hF1Split rw [hMeasureSplit] at h' nlinarith [h'] exact mul_left_cancel₀ ha_ne h have hrho_eq : S.rho = b / (b + c) := by unfold rho rw [hp0_eq, hp1_eq] rw [hrho_eq] have hmul_le : b * S.f1AS y ≤ S.f1 y * (b + c) := by rw [heq] nlinarith [hiH_nonneg] rw [div_mul_eq_mul_div] exact (div_le_iff₀ hbc_pos).mpr hmul_le have hrho_ne : S.rho ≠ 0 := by let b := (P.μ S.alwaysSelected).toReal let c := (P.μ S.helpedSelected).toReal have hb_pos : 0 < b := by have hb_nonneg : 0 ≤ b := ENNReal.toReal_nonneg exact lt_of_le_of_ne' hb_nonneg (by simpa [b] using hAS_ne) have hbc_pos : 0 < b + c := by have hc : 0 ≤ c := ENNReal.toReal_nonneg nlinarith have hrho_eq : S.rho = b / (b + c) := by unfold rho rw [hp0_eq, hp1_eq] rw [hrho_eq] exact div_ne_zero (ne_of_gt hb_pos) (ne_of_gt hbc_pos) have hweighted_f1AS : ∑ y ∈ 𝒴, y * S.f1AS y = eventCondExp P.μ S.alwaysSelected (S.YofA true) := by have hASrel : ∀ y, S.f1AS y * (P.μ S.alwaysSelected).toReal = ∫ ω in S.alwaysSelected, (if S.YofA true ω = y then (1 : ℝ) else 0) ∂P.μ := by intro y unfold f1AS eventCondExp field_simp [hAS_ne] have hweighted_mul : (∑ y ∈ 𝒴, y * S.f1AS y) * (P.μ S.alwaysSelected).toReal = ∫ ω in S.alwaysSelected, (∑ y ∈ 𝒴, y * (if S.YofA true ω = y then (1 : ℝ) else 0)) ∂P.μ := by have hInd_int : ∀ y, Integrable (fun ω => y * (if S.YofA true ω = y then (1 : ℝ) else 0)) (P.μ.restrict S.alwaysSelected) := by intro y have hbase : Integrable (fun ω => if S.YofA true ω = y then (1 : ℝ) else 0) (P.μ.restrict S.alwaysSelected) := by refine MeasureTheory.Integrable.of_bound ((Measurable.ite ((S.measurable_YofA true) (measurableSet_singleton y)) measurable_const measurable_const).aestronglyMeasurable) 1 (Filter.Eventually.of_forall ?_) intro ω by_cases hω : S.YofA true ω = y · simp [hω] · simp [hω] simpa only [Pi.smul_apply, smul_eq_mul] using hbase.const_mul y rw [Finset.sum_mul] rw [MeasureTheory.integral_finset_sum 𝒴 (fun y _ => hInd_int y)] refine Finset.sum_congr rfl ?_ intro y hy rw [MeasureTheory.integral_const_mul] rw [← hASrel y] ring have hIntY : ∫ ω in S.alwaysSelected, (∑ y ∈ 𝒴, y * (if S.YofA true ω = y then (1 : ℝ) else 0)) ∂P.μ = ∫ ω in S.alwaysSelected, S.YofA true ω ∂P.μ := by have hASsupp := (S.YofA_true_in_finset_ae_alwaysSelected hA 𝒴 hSupp).1 have hfun : -- … truncated; follow the source link for the rest …