PO.ID.Partial.Sensitivity.MSM

theorem candMean_completeProp_eq_Ymean [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (d : Bool) (hcons : P.Consistency) (hpos : ∀ᵐ ω ∂P.μ, 0 < S.completeProp d ω) (hcand_int : Integrable (fun ω => S.dVar.indicator d ω * S.factualY ω / S.completeProp d ω) P.μ) : S.candMean d (S.completeProp d) = S.Ymean d := by classical -- Abbreviations. set f : P.Ω → ℝ := S.dVar.indicator d with hf_def set e : P.Ω → ℝ := S.completeProp d with he_def set g : P.Ω → ℝ := fun ω => S.YofD d ω / e ω with hg_def -- (1) Consistency: `f ω * factualY ω = f ω * YofD d ω` pointwise. have hcons_fn : (fun ω => S.factualY ω * f ω) = (fun ω => S.YofD d ω * f ω) := by have h := POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn hcons S.yVar S.dVar d (Ne.symm S.hDY) funext ω have := congr_fun h ω simpa [POBackdoorSystem.YofD, POBackdoorSystem.factualY, hf_def] using this -- `candMean e = ∫ g ω * f ω`. have hcandMean_eq : S.candMean d e = ∫ ω, g ω * f ω ∂P.μ := by unfold POBackdoorSystem.candMean refine integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω have hcw : S.factualY ω * f ω = S.YofD d ω * f ω := congr_fun hcons_fn ω -- `f ω * factualY ω / e ω = (YofD d ω / e ω) * f ω`. simp only [hg_def, hf_def] at hcw ⊢ rw [div_eq_mul_inv, div_eq_mul_inv] linear_combination (e ω)⁻¹ * hcw -- (2) `g` is `sigmaXY d`-strongly measurable. have hY1_meas : Measurable[S.sigmaXY d] (S.YofD d) := by have hle : comap (S.YofD d) inferInstance ≤ S.sigmaXY d := le_sup_right exact (comap_measurable (S.YofD d)).mono hle le_rfl have he_smeas : StronglyMeasurable[S.sigmaXY d] e := by rw [he_def] exact stronglyMeasurable_condExp have hg_smeas : StronglyMeasurable[S.sigmaXY d] g := by have he_meas : Measurable[S.sigmaXY d] e := he_smeas.measurable exact (hY1_meas.div he_meas).stronglyMeasurable -- Integrability of `f` and `g * f`. have hf_int : Integrable f P.μ := S.dVar.integrable_indicator d (measurableSet_singleton d) have hgf_int : Integrable (fun ω => g ω * f ω) P.μ := by refine hcand_int.congr (Filter.Eventually.of_forall ?_) intro ω have hcw : S.factualY ω * f ω = S.YofD d ω * f ω := congr_fun hcons_fn ω simp only [hg_def, hf_def] at hcw ⊢ rw [div_eq_mul_inv, div_eq_mul_inv] linear_combination (e ω)⁻¹ * hcw -- (3) Pull-out + tower: `∫ g * f = ∫ g * e`. have hpull : P.μ[fun ω => g ω * f ω | S.sigmaXY d] =ᵐ[P.μ] (fun ω => g ω * e ω) := by have h := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (m := S.sigmaXY d) (μ := P.μ) hg_smeas hgf_int hf_int -- `μ[g * f | m] =ᵐ g * μ[f | m]`, and `μ[f | m] = e`. have he_cond : (P.μ[f | S.sigmaXY d]) = e := by rw [hf_def, he_def]; rfl refine h.trans ?_ rw [he_cond] rfl have htower : ∫ ω, g ω * f ω ∂P.μ = ∫ ω, g ω * e ω ∂P.μ := by have h1 : ∫ ω, P.μ[fun ω => g ω * f ω | S.sigmaXY d] ω ∂P.μ = ∫ ω, g ω * f ω ∂P.μ := MeasureTheory.integral_condExp (S.sigmaXY_le d) rw [← h1] exact integral_congr_ae hpull -- (4) Cancel: `∫ g * e = ∫ YofD d = Ymean d`. have hcancel : ∫ ω, g ω * e ω ∂P.μ = S.Ymean d := by unfold POBackdoorSystem.Ymean refine integral_congr_ae ?_ filter_upwards [hpos] with ω hω rw [hg_def] field_simp rw [hcandMean_eq, htower, hcancel]

theorem Ymean_mem_Icc (d : Bool) (Λ : ℝ) (hmem : S.completeProp d ∈ S.MSMSet d Λ) (hbridge : S.candMean d (S.completeProp d) = S.Ymean d) (hbdd : BddBelow (S.candMean d '' S.MSMSet d Λ)) (hbdd' : BddAbove (S.candMean d '' S.MSMSet d Λ)) : S.Ymean d ∈ Icc (S.msmLower d Λ) (S.msmUpper d Λ) := by have hmemImg : S.candMean d (S.completeProp d) ∈ S.candMean d '' S.MSMSet d Λ := Set.mem_image_of_mem _ hmem rw [Set.mem_Icc, ← hbridge] refine ⟨?_, ?_⟩ · exact csInf_le hbdd hmemImg · exact le_csSup hbdd' hmemImg

theorem MSMSet_one_eq (d : Bool) (etilde : P.Ω → ℝ) (hprop : ∀ᵐ ω ∂P.μ, 0 < S.propScore d ω ∧ S.propScore d ω < 1) (hmem : etilde ∈ S.MSMSet d 1) : ∀ᵐ ω ∂P.μ, etilde ω = S.propScore d ω := by obtain ⟨hint, hor⟩ := hmem filter_upwards [hprop, hint, hor] with ω hq hp hOR obtain ⟨hqpos, hqlt⟩ := hq obtain ⟨hppos, hplt⟩ := hp obtain ⟨hlo, hhi⟩ := hOR -- At Λ = 1, the odds-ratio window is {1}. rw [one_div, inv_one] at hlo have hOReq : OR (etilde ω) (S.propScore d ω) = 1 := le_antisymm hhi hlo -- Unfold OR and clear denominators. set p := etilde ω with hpdef set q := S.propScore d ω with hqdef have h1p : (0:ℝ) < 1 - p := by linarith have h1q : (0:ℝ) < 1 - q := by linarith have hqratio : q / (1 - q) ≠ 0 := by apply div_ne_zero · exact ne_of_gt hqpos · exact ne_of_gt h1q rw [OR, div_eq_one_iff_eq hqratio] at hOReq -- hOReq : p/(1-p) = q/(1-q); conclude p = q. field_simp at hOReq nlinarith [hOReq]

theorem Ymean_mem_Icc_calib (d : Bool) (Λ : ℝ) (hmem : S.completeProp d ∈ S.MSMSetCalib d Λ) (hbridge : S.candMean d (S.completeProp d) = S.Ymean d) (hbdd : BddBelow (S.candMean d '' S.MSMSetCalib d Λ)) (hbdd' : BddAbove (S.candMean d '' S.MSMSetCalib d Λ)) : S.Ymean d ∈ Icc (S.msmLowerCalib d Λ) (S.msmUpperCalib d Λ) := by have hmemImg : S.candMean d (S.completeProp d) ∈ S.candMean d '' S.MSMSetCalib d Λ := Set.mem_image_of_mem _ hmem rw [Set.mem_Icc, ← hbridge] refine ⟨?_, ?_⟩ · exact csInf_le hbdd hmemImg · exact le_csSup hbdd' hmemImg

theorem msmUpperCalib_le_msmUpper (d : Bool) (Λ : ℝ) (hne : (S.candMean d '' S.MSMSetCalib d Λ).Nonempty) (hbdd : BddAbove (S.candMean d '' S.MSMSet d Λ)) : S.msmUpperCalib d Λ ≤ S.msmUpper d Λ := by have hsub : S.MSMSetCalib d Λ ⊆ S.MSMSet d Λ := S.MSMSetCalib_subset d Λ have himg : S.candMean d '' S.MSMSetCalib d Λ ⊆ S.candMean d '' S.MSMSet d Λ := Set.image_mono hsub exact csSup_le_csSup hbdd hne himg

theorem msmUpper_eq (Λ : ℝ) (hΛ : 1 ≤ Λ) (hoverlap : ∀ᵐ ω ∂P.μ, 0 < S.propScore true ω ∧ S.propScore true ω < 1) (hmeas : ∀ etilde ∈ S.MSMSet true Λ, AEMeasurable etilde P.μ) (henv : Integrable (fun ω => S.dVar.indicator true ω * |S.factualY ω| * S.wMax Λ ω) P.μ) : S.msmUpper true Λ = S.msmUpperForm Λ := by classical have hΛ0 : (0:ℝ) < Λ := lt_of_lt_of_le one_pos hΛ -- Abbreviations. set A : P.Ω → ℝ := S.dVar.indicator true with hA_def set Y : P.Ω → ℝ := S.factualY with hY_def set e : P.Ω → ℝ := S.propScore true with he_def -- Measurability. have hAm : Measurable A := S.dVar.measurable_indicator true (measurableSet_singleton true) have hYm : Measurable Y := S.measurable_factualY have hem : Measurable e := by rw [he_def]; unfold POBackdoorSystem.propScore exact (stronglyMeasurable_condExp.mono S.sigmaX_le).measurable have hwMaxm : Measurable (S.wMax Λ) := by unfold POBackdoorSystem.wMax exact (measurable_const.add ((measurable_const.mul (measurable_const.sub hem)).div hem)) have hwMinm : Measurable (S.wMin Λ) := by unfold POBackdoorSystem.wMin exact (measurable_const.add ((measurable_const.sub hem).div (measurable_const.mul hem))) -- `A` is in `[0,1]`. have hA0 : ∀ ω, 0 ≤ A ω := fun ω => by rcases S.dVar.indicator_eq_one_or_zero true ω with h | h <;> simp [hA_def, h] have hA1 : ∀ ω, A ω ≤ 1 := fun ω => by rcases S.dVar.indicator_eq_one_or_zero true ω with h | h <;> simp [hA_def, h] -- The optimal weight and candidate propensity. set wstar : P.Ω → ℝ := fun ω => if 0 ≤ Y ω then S.wMax Λ ω else S.wMin Λ ω with hwstar_def set estar : P.Ω → ℝ := fun ω => 1 / wstar ω with hestar_def -- a.e. positivity / ordering of the weights from overlap. have hae : ∀ᵐ ω ∂P.μ, (1:ℝ) < S.wMin Λ ω ∧ S.wMin Λ ω ≤ S.wMax Λ ω := by filter_upwards [hoverlap] with ω hω obtain ⟨he0, he1⟩ := hω have h1e : 0 < 1 - e ω := by rw [he_def] at *; linarith have he0' : 0 < e ω := by rw [he_def] at *; exact he0 refine ⟨?_, ?_⟩ · have : 0 < (1 - e ω) / (Λ * e ω) := by positivity simp only [POBackdoorSystem.wMin, ← he_def]; linarith · simp only [POBackdoorSystem.wMin, POBackdoorSystem.wMax, ← he_def] have hd1 : (1 - e ω) / (Λ * e ω) ≤ Λ * (1 - e ω) / e ω := by rw [div_le_div_iff₀ (by positivity) he0'] nlinarith [hΛ, mul_pos h1e he0', mul_pos hΛ0 he0', mul_nonneg (mul_nonneg (le_of_lt h1e) (le_of_lt he0')) (sub_nonneg.mpr hΛ)] linarith -- Measurability and a.e. bounds of the optimal weight. have hwstar_m : Measurable wstar := by rw [hwstar_def] exact Measurable.ite (measurableSet_le measurable_const hYm) hwMaxm hwMinm have hwstar_ae : ∀ᵐ ω ∂P.μ, S.wMin Λ ω ≤ wstar ω ∧ wstar ω ≤ S.wMax Λ ω ∧ 0 < wstar ω := by filter_upwards [hae] with ω hω obtain ⟨hwm1, hwmle⟩ := hω rw [hwstar_def] by_cases hy : 0 ≤ Y ω · simp only [if_pos hy]; exact ⟨hwmle, le_rfl, by linarith⟩ · simp only [if_neg hy]; exact ⟨le_rfl, hwmle, by linarith⟩ -- `A*Y*wstar` is dominated by the envelope, hence integrable. have hform_int : Integrable (fun ω => A ω * Y ω * wstar ω) P.μ := by refine Integrable.mono' henv ((hAm.mul hYm).mul hwstar_m).aestronglyMeasurable ?_ filter_upwards [hwstar_ae] with ω hω obtain ⟨_, hle, hpos⟩ := hω rw [Real.norm_eq_abs, abs_mul, abs_mul, abs_of_nonneg (hA0 ω)] have hwabs : |wstar ω| = wstar ω := abs_of_nonneg (le_of_lt hpos) rw [hwabs, mul_assoc, mul_assoc] apply mul_le_mul_of_nonneg_left _ (hA0 ω) exact mul_le_mul_of_nonneg_left hle (abs_nonneg _) -- `msmUpperForm = ∫ A*Y*wstar`. have hform_eq : S.msmUpperForm Λ = ∫ ω, A ω * Y ω * wstar ω ∂P.μ := by rfl -- Witness: `estar = 1/wstar ∈ MSMSet Λ` with `candMean estar = msmUpperForm`. have hestar_candMean : S.candMean true estar = S.msmUpperForm Λ := by rw [hform_eq] unfold POBackdoorSystem.candMean refine integral_congr_ae ?_ filter_upwards [hwstar_ae] with ω hω obtain ⟨_, _, hpos⟩ := hω change A ω * Y ω / (1 / wstar ω) = A ω * Y ω * wstar ω rw [div_div_eq_mul_div, div_one] -- a.e. `wstar > 1` (since `wstar ∈ {wMin, wMax}`, `wMin > 1`, `wMax ≥ wMin`). have hwstar_gt1 : ∀ᵐ ω ∂P.μ, 1 < wstar ω := by filter_upwards [hae] with ω hω obtain ⟨hwm1, hwmle⟩ := hω rw [hwstar_def] by_cases hy : 0 ≤ Y ω · simp only [if_pos hy]; linarith · simp only [if_neg hy]; exact hwm1 have hestar_mem : estar ∈ S.MSMSet true Λ := by refine ⟨?_, ?_⟩ · filter_upwards [hwstar_gt1] with ω hω rw [hestar_def] constructor · positivity · rw [div_lt_one (by linarith)]; linarith · filter_upwards [hoverlap, hwstar_ae, hwstar_gt1] with ω hov hw hwgt obtain ⟨he0, he1⟩ := hov obtain ⟨hmin, hmax, hpos⟩ := hw have het0 : 0 < estar ω := by rw [hestar_def]; positivity have het1 : estar ω < 1 := by rw [hestar_def, div_lt_one (by linarith)]; linarith rw [OR_box_iff hΛ0 he0 he1 het0 het1] have hinv : 1 / estar ω = wstar ω := by rw [hestar_def, one_div_one_div] rw [hinv] exact ⟨hmin, hmax⟩ -- Every candidate mean is `≤ msmUpperForm`. have hcand_le : ∀ etilde ∈ S.MSMSet true Λ, S.candMean true etilde ≤ S.msmUpperForm Λ := by intro et hmem obtain ⟨hint, hor⟩ := hmem have hetm : AEMeasurable et P.μ := hmeas et ⟨hint, hor⟩ -- a.e. box bound on `w = 1/et`. have hbox : ∀ᵐ ω ∂P.μ, S.wMin Λ ω ≤ 1 / et ω ∧ 1 / et ω ≤ S.wMax Λ ω := by filter_upwards [hoverlap, hint, hor] with ω hov het hOR obtain ⟨he0, he1⟩ := hov obtain ⟨het0, het1⟩ := het have := (OR_box_iff hΛ0 he0 he1 het0 het1).mp hOR exact this -- `A*Y/et = A*Y*(1/et)` a.e.; integrable by domination. have hcandmean_int : Integrable (fun ω => A ω * Y ω / et ω) P.μ := by refine Integrable.mono' henv (((hAm.mul hYm).aemeasurable.div hetm).aestronglyMeasurable) ?_ filter_upwards [hbox, hoverlap, hint] with ω hb hov het obtain ⟨hmin, hmax⟩ := hb obtain ⟨he0, he1⟩ := hov obtain ⟨het0, het1⟩ := het rw [Real.norm_eq_abs, mul_div_assoc, abs_mul, abs_of_nonneg (hA0 ω), mul_assoc] apply mul_le_mul_of_nonneg_left _ (hA0 ω) have hYdiv : |Y ω / et ω| = |Y ω| * (1 / et ω) := by rw [abs_div, abs_of_nonneg (le_of_lt het0), mul_one_div] rw [hYdiv] exact mul_le_mul_of_nonneg_left hmax (abs_nonneg _) have heq_w : (fun ω => A ω * Y ω / et ω) =ᵐ[P.μ] (fun ω => A ω * Y ω * (1 / et ω)) := by filter_upwards with ω rw [mul_one_div] -- `candMean et = ∫ A*Y*(1/et) ≤ ∫ A*Y*wstar = form`. rw [show S.candMean true et = ∫ ω, A ω * Y ω / et ω ∂P.μ from rfl, hform_eq] rw [integral_congr_ae heq_w] apply integral_mono_ae (hcandmean_int.congr heq_w) hform_int filter_upwards [hbox] with ω hb obtain ⟨hmin, hmax⟩ := hb exact weight_mul_le_upper (hA0 ω) hmin hmax -- Assemble: `msmUpper = sSup (candMean '' MSMSet) = msmUpperForm`. have hne : (S.candMean true '' S.MSMSet true Λ).Nonempty := ⟨S.candMean true estar, Set.mem_image_of_mem _ hestar_mem⟩ have hbdd : BddAbove (S.candMean true '' S.MSMSet true Λ) := by refine ⟨S.msmUpperForm Λ, ?_⟩ rintro x ⟨et, hmem, rfl⟩ exact hcand_le et hmem refine le_antisymm ?_ ?_ · apply csSup_le hne rintro x ⟨et, hmem, rfl⟩ exact hcand_le et hmem · rw [← hestar_candMean] exact le_csSup hbdd (Set.mem_image_of_mem _ hestar_mem)

theorem msmLower_eq (Λ : ℝ) (hΛ : 1 ≤ Λ) (hoverlap : ∀ᵐ ω ∂P.μ, 0 < S.propScore true ω ∧ S.propScore true ω < 1) (hmeas : ∀ etilde ∈ S.MSMSet true Λ, AEMeasurable etilde P.μ) (henv : Integrable (fun ω => S.dVar.indicator true ω * |S.factualY ω| * S.wMax Λ ω) P.μ) : S.msmLower true Λ = S.msmLowerForm Λ := by classical have hΛ0 : (0:ℝ) < Λ := lt_of_lt_of_le one_pos hΛ set A : P.Ω → ℝ := S.dVar.indicator true with hA_def set Y : P.Ω → ℝ := S.factualY with hY_def set e : P.Ω → ℝ := S.propScore true with he_def have hAm : Measurable A := S.dVar.measurable_indicator true (measurableSet_singleton true) have hYm : Measurable Y := S.measurable_factualY have hem : Measurable e := by rw [he_def]; unfold POBackdoorSystem.propScore exact (stronglyMeasurable_condExp.mono S.sigmaX_le).measurable have hwMaxm : Measurable (S.wMax Λ) := by unfold POBackdoorSystem.wMax exact (measurable_const.add ((measurable_const.mul (measurable_const.sub hem)).div hem)) have hwMinm : Measurable (S.wMin Λ) := by unfold POBackdoorSystem.wMin exact (measurable_const.add ((measurable_const.sub hem).div (measurable_const.mul hem))) have hA0 : ∀ ω, 0 ≤ A ω := fun ω => by rcases S.dVar.indicator_eq_one_or_zero true ω with h | h <;> simp [hA_def, h] -- Lower-bound optimal weight: `wMin` where `Y ≥ 0`, `wMax` where `Y < 0`. set wstar : P.Ω → ℝ := fun ω => if 0 ≤ Y ω then S.wMin Λ ω else S.wMax Λ ω with hwstar_def set estar : P.Ω → ℝ := fun ω => 1 / wstar ω with hestar_def have hae : ∀ᵐ ω ∂P.μ, (1:ℝ) < S.wMin Λ ω ∧ S.wMin Λ ω ≤ S.wMax Λ ω := by filter_upwards [hoverlap] with ω hω obtain ⟨he0, he1⟩ := hω have h1e : 0 < 1 - e ω := by rw [he_def] at *; linarith have he0' : 0 < e ω := by rw [he_def] at *; exact he0 refine ⟨?_, ?_⟩ · have : 0 < (1 - e ω) / (Λ * e ω) := by positivity simp only [POBackdoorSystem.wMin, ← he_def]; linarith · simp only [POBackdoorSystem.wMin, POBackdoorSystem.wMax, ← he_def] have hd1 : (1 - e ω) / (Λ * e ω) ≤ Λ * (1 - e ω) / e ω := by rw [div_le_div_iff₀ (by positivity) he0'] nlinarith [hΛ, mul_pos h1e he0', mul_pos hΛ0 he0', mul_nonneg (mul_nonneg (le_of_lt h1e) (le_of_lt he0')) (sub_nonneg.mpr hΛ)] linarith have hwstar_m : Measurable wstar := by rw [hwstar_def] exact Measurable.ite (measurableSet_le measurable_const hYm) hwMinm hwMaxm have hwstar_ae : ∀ᵐ ω ∂P.μ, S.wMin Λ ω ≤ wstar ω ∧ wstar ω ≤ S.wMax Λ ω ∧ 0 < wstar ω := by filter_upwards [hae] with ω hω obtain ⟨hwm1, hwmle⟩ := hω rw [hwstar_def] by_cases hy : 0 ≤ Y ω · simp only [if_pos hy]; exact ⟨le_rfl, hwmle, by linarith⟩ · simp only [if_neg hy]; exact ⟨hwmle, le_rfl, by linarith⟩ have hwstar_gt1 : ∀ᵐ ω ∂P.μ, 1 < wstar ω := by filter_upwards [hae] with ω hω obtain ⟨hwm1, hwmle⟩ := hω rw [hwstar_def] by_cases hy : 0 ≤ Y ω · simp only [if_pos hy]; exact hwm1 · simp only [if_neg hy]; linarith -- `A*Y*wstar` integrable (dominated by envelope). have hform_int : Integrable (fun ω => A ω * Y ω * wstar ω) P.μ := by refine Integrable.mono' henv ((hAm.mul hYm).mul hwstar_m).aestronglyMeasurable ?_ filter_upwards [hwstar_ae] with ω hω obtain ⟨_, hle, hpos⟩ := hω rw [Real.norm_eq_abs, abs_mul, abs_mul, abs_of_nonneg (hA0 ω)] have hwabs : |wstar ω| = wstar ω := abs_of_nonneg (le_of_lt hpos) rw [hwabs, mul_assoc, mul_assoc] apply mul_le_mul_of_nonneg_left _ (hA0 ω) exact mul_le_mul_of_nonneg_left hle (abs_nonneg _) have hform_eq : S.msmLowerForm Λ = ∫ ω, A ω * Y ω * wstar ω ∂P.μ := by rfl -- Witness `estar = 1/wstar ∈ MSMSet`, `candMean estar = msmLowerForm`. have hestar_candMean : S.candMean true estar = S.msmLowerForm Λ := by rw [hform_eq] unfold POBackdoorSystem.candMean refine integral_congr_ae ?_ filter_upwards [hwstar_ae] with ω hω obtain ⟨_, _, hpos⟩ := hω change A ω * Y ω / (1 / wstar ω) = A ω * Y ω * wstar ω rw [div_div_eq_mul_div, div_one] have hestar_mem : estar ∈ S.MSMSet true Λ := by refine ⟨?_, ?_⟩ · filter_upwards [hwstar_gt1] with ω hω rw [hestar_def] exact ⟨by positivity, by rw [div_lt_one (by linarith)]; linarith⟩ · filter_upwards [hoverlap, hwstar_ae, hwstar_gt1] with ω hov hw hwgt obtain ⟨he0, he1⟩ := hov obtain ⟨hmin, hmax, hpos⟩ := hw have het0 : 0 < estar ω := by rw [hestar_def]; positivity have het1 : estar ω < 1 := by rw [hestar_def, div_lt_one (by linarith)]; linarith rw [OR_box_iff hΛ0 he0 he1 het0 het1] have hinv : 1 / estar ω = wstar ω := by rw [hestar_def, one_div_one_div] rw [hinv]; exact ⟨hmin, hmax⟩ -- Every candidate mean is `≥ msmLowerForm`. have hcand_ge : ∀ etilde ∈ S.MSMSet true Λ, S.msmLowerForm Λ ≤ S.candMean true etilde := by intro et hmem obtain ⟨hint, hor⟩ := hmem have hetm : AEMeasurable et P.μ := hmeas et ⟨hint, hor⟩ have hbox : ∀ᵐ ω ∂P.μ, S.wMin Λ ω ≤ 1 / et ω ∧ 1 / et ω ≤ S.wMax Λ ω := by filter_upwards [hoverlap, hint, hor] with ω hov het hOR obtain ⟨he0, he1⟩ := hov obtain ⟨het0, het1⟩ := het exact (OR_box_iff hΛ0 he0 he1 het0 het1).mp hOR have hcandmean_int : Integrable (fun ω => A ω * Y ω / et ω) P.μ := by refine Integrable.mono' henv (((hAm.mul hYm).aemeasurable.div hetm).aestronglyMeasurable) ?_ filter_upwards [hbox, hoverlap, hint] with ω hb hov het obtain ⟨hmin, hmax⟩ := hb obtain ⟨he0, he1⟩ := hov obtain ⟨het0, het1⟩ := het rw [Real.norm_eq_abs, mul_div_assoc, abs_mul, abs_of_nonneg (hA0 ω), mul_assoc] apply mul_le_mul_of_nonneg_left _ (hA0 ω) have hYdiv : |Y ω / et ω| = |Y ω| * (1 / et ω) := by rw [abs_div, abs_of_nonneg (le_of_lt het0), mul_one_div] rw [hYdiv] exact mul_le_mul_of_nonneg_left hmax (abs_nonneg _) have heq_w : (fun ω => A ω * Y ω / et ω) =ᵐ[P.μ] (fun ω => A ω * Y ω * (1 / et ω)) := by filter_upwards with ω; rw [mul_one_div] rw [show S.candMean true et = ∫ ω, A ω * Y ω / et ω ∂P.μ from rfl, hform_eq] rw [integral_congr_ae heq_w] apply integral_mono_ae hform_int (hcandmean_int.congr heq_w) filter_upwards [hbox] with ω hb obtain ⟨hmin, hmax⟩ := hb exact weight_mul_ge_lower (hA0 ω) hmin hmax -- Assemble via `sInf`. have hne : (S.candMean true '' S.MSMSet true Λ).Nonempty := ⟨S.candMean true estar, Set.mem_image_of_mem _ hestar_mem⟩ have hbdd : BddBelow (S.candMean true '' S.MSMSet true Λ) := by refine ⟨S.msmLowerForm Λ, ?_⟩ rintro x ⟨et, hmem, rfl⟩ exact hcand_ge et hmem refine le_antisymm ?_ ?_ · rw [← hestar_candMean] exact csInf_le hbdd (Set.mem_image_of_mem _ hestar_mem) · apply le_csInf hne rintro x ⟨et, hmem, rfl⟩ exact hcand_ge et hmem

theorem cutoff_optimal (Λ : ℝ) (hΛ : 1 ≤ Λ) (hoverlap : ∀ᵐ ω ∂P.μ, 0 < S.propScore true ω ∧ S.propScore true ω < 1) (c : P.Ω → ℝ) (hc_meas : Measurable[S.sigmaX] c) (hc_int : Integrable c P.μ) (hcut_mem : S.cutoffProp Λ c ∈ S.MSMSetCalib true Λ) (henv : Integrable (fun ω => S.dVar.indicator true ω * |S.factualY ω| * S.wMax Λ ω) P.μ) (hweight_env : Integrable (fun ω => S.dVar.indicator true ω * S.wMax Λ ω) P.μ) (hc_env : Integrable (fun ω => |c ω| * S.dVar.indicator true ω * S.wMax Λ ω) P.μ) {etilde : P.Ω → ℝ} (hmem : etilde ∈ S.MSMSetCalib true Λ) : S.candMean true etilde ≤ S.candMean true (S.cutoffProp Λ c) := by classical have _ : Integrable c P.μ := hc_int have hΛ0 : (0 : ℝ) < Λ := lt_of_lt_of_le one_pos hΛ set A : P.Ω → ℝ := S.dVar.indicator true with hA_def set Y : P.Ω → ℝ := S.factualY with hY_def set e : P.Ω → ℝ := S.propScore true with he_def set wE : P.Ω → ℝ := fun ω => 1 / etilde ω with hwE_def set wC : P.Ω → ℝ := fun ω => if c ω < Y ω then S.wMax Λ ω else S.wMin Λ ω with hwC_def have hOR_box : ∀ {e et : ℝ}, 0 < e → e < 1 → 0 < et → et < 1 → ((1 / Λ ≤ OR et e ∧ OR et e ≤ Λ) ↔ (1 + (1 - e) / (Λ * e) ≤ 1 / et ∧ 1 / et ≤ 1 + Λ * (1 - e) / e)) := by intro e0 et he0 he1 het0 het1 have h1e : 0 < 1 - e0 := by linarith have h1et : 0 < 1 - et := by linarith have hOReq : OR et e0 = et * (1 - e0) / ((1 - et) * e0) := by rw [OR, div_div_eq_mul_div, div_mul_eq_mul_div, mul_comm, mul_div_mul_comm] ring_nf rw [hOReq] have hMax : (1 / Λ ≤ et * (1 - e0) / ((1 - et) * e0)) ↔ (1 / et ≤ 1 + Λ * (1 - e0) / e0) := by rw [div_le_div_iff₀ hΛ0 (by positivity : (0 : ℝ) < (1 - et) * e0), show (1 : ℝ) + Λ * (1 - e0) / e0 = (e0 + Λ * (1 - e0)) / e0 by field_simp, div_le_div_iff₀ het0 he0] constructor <;> intro h <;> nlinarith [h, mul_pos hΛ0 he0] have hMin : (et * (1 - e0) / ((1 - et) * e0) ≤ Λ) ↔ (1 + (1 - e0) / (Λ * e0) ≤ 1 / et) := by rw [div_le_iff₀ (by positivity : (0 : ℝ) < (1 - et) * e0), show (1 : ℝ) + (1 - e0) / (Λ * e0) = (Λ * e0 + (1 - e0)) / (Λ * e0) by field_simp, div_le_div_iff₀ (by positivity : (0 : ℝ) < Λ * e0) het0] constructor <;> intro h <;> nlinarith [h, mul_pos hΛ0 he0] rw [hMax, hMin, and_comm] have hAm : Measurable A := by rw [hA_def] exact S.dVar.measurable_indicator true (MeasurableSet.singleton true) have hYm : Measurable Y := by rw [hY_def] exact S.measurable_factualY have hem : Measurable e := by rw [he_def] unfold POBackdoorSystem.propScore exact (stronglyMeasurable_condExp.mono S.sigmaX_le).measurable have hwMaxm : Measurable (S.wMax Λ) := by unfold POBackdoorSystem.wMax exact (measurable_const.add ((measurable_const.mul (measurable_const.sub hem)).div hem)) have hwMinm : Measurable (S.wMin Λ) := by unfold POBackdoorSystem.wMin exact (measurable_const.add ((measurable_const.sub hem).div (measurable_const.mul hem))) have hwCm : Measurable wC := by rw [hwC_def] exact Measurable.ite (measurableSet_lt (hc_meas.mono S.sigmaX_le le_rfl) hYm) hwMaxm hwMinm have hA0 : ∀ ω, 0 ≤ A ω := fun ω => by rcases S.dVar.indicator_eq_one_or_zero true ω with h | h <;> simp [hA_def, h] have hae : ∀ᵐ ω ∂P.μ, (1 : ℝ) < S.wMin Λ ω ∧ S.wMin Λ ω ≤ S.wMax Λ ω := by filter_upwards [hoverlap] with ω hω obtain ⟨he0ω, he1ω⟩ := hω have h1e : 0 < 1 - e ω := by rw [he_def] at *; linarith have he0' : 0 < e ω := by rw [he_def] at *; exact he0ω refine ⟨?_, ?_⟩ · have : 0 < (1 - e ω) / (Λ * e ω) := by positivity simp only [POBackdoorSystem.wMin, ← he_def] linarith · simp only [POBackdoorSystem.wMin, POBackdoorSystem.wMax, ← he_def] have hd1 : (1 - e ω) / (Λ * e ω) ≤ Λ * (1 - e ω) / e ω := by rw [div_le_div_iff₀ (by positivity) he0'] nlinarith [hΛ, mul_pos h1e he0', mul_pos hΛ0 he0', mul_nonneg (mul_nonneg (le_of_lt h1e) (le_of_lt he0')) (sub_nonneg.mpr hΛ)] linarith have hboxE : ∀ᵐ ω ∂P.μ, S.wMin Λ ω ≤ wE ω ∧ wE ω ≤ S.wMax Λ ω := by obtain ⟨hinterior, hor⟩ := hmem.1 filter_upwards [hoverlap, hinterior, hor] with ω hov het hOR obtain ⟨he0ω, he1ω⟩ := hov obtain ⟨het0, het1⟩ := het have hbox := (hOR_box he0ω he1ω het0 het1).mp hOR simpa [POBackdoorSystem.wMin, POBackdoorSystem.wMax, he_def, hwE_def] using hbox have hboxC : ∀ᵐ ω ∂P.μ, S.wMin Λ ω ≤ wC ω ∧ wC ω ≤ S.wMax Λ ω ∧ 0 < wC ω := by filter_upwards [hae] with ω hω obtain ⟨hmin1, hminmax⟩ := hω rw [hwC_def] by_cases hcy : c ω < Y ω · simp only [if_pos hcy] exact ⟨hminmax, le_rfl, lt_of_lt_of_le (by linarith) hminmax⟩ · simp only [if_neg hcy] exact ⟨le_rfl, hminmax, by linarith⟩ have hXE_int : Integrable (fun ω => A ω / etilde ω) P.μ := by simpa [hA_def] using S.calibrated_weight_integrable true etilde hmem.2 have hAwE_int : Integrable (fun ω => A ω * wE ω) P.μ := by refine hXE_int.congr (Filter.Eventually.of_forall ?_) intro ω simp [hwE_def, div_eq_mul_inv] have hYE_int : Integrable (fun ω => A ω * Y ω * wE ω) P.μ := by have hmeas : AEStronglyMeasurable (fun ω => A ω * Y ω * wE ω) P.μ := by refine (hYm.aestronglyMeasurable.mul hAwE_int.aestronglyMeasurable).congr ?_ filter_upwards [] with ω simp only [Pi.mul_apply] ring refine Integrable.mono' henv hmeas ?_ filter_upwards [hboxE, hmem.1.1] with ω hbox hint obtain ⟨_, hmax⟩ := hbox obtain ⟨het0, _⟩ := hint rw [Real.norm_eq_abs, abs_mul, abs_mul, abs_of_nonneg (hA0 ω), hwE_def, abs_of_nonneg (by positivity : 0 ≤ 1 / etilde ω), mul_assoc, mul_assoc] apply mul_le_mul_of_nonneg_left _ (hA0 ω) exact mul_le_mul_of_nonneg_left hmax (abs_nonneg _) have hYC_int : Integrable (fun ω => A ω * Y ω * wC ω) P.μ := by refine Integrable.mono' henv (((hAm.mul hYm).mul hwCm).aestronglyMeasurable) ?_ filter_upwards [hboxC] with ω hbox obtain ⟨_, hmax, hpos⟩ := hbox rw [Real.norm_eq_abs, abs_mul, abs_mul, abs_of_nonneg (hA0 ω), abs_of_nonneg (le_of_lt hpos), mul_assoc, mul_assoc] apply mul_le_mul_of_nonneg_left _ (hA0 ω) exact mul_le_mul_of_nonneg_left hmax (abs_nonneg _) have hXC_int : Integrable (fun ω => A ω / S.cutoffProp Λ c ω) P.μ := by have hAwC_int : Integrable (fun ω => A ω * wC ω) P.μ := by refine Integrable.mono' hweight_env ((hAm.mul hwCm).aestronglyMeasurable) ?_ filter_upwards [hboxC] with ω hbox obtain ⟨_, hmax, hpos⟩ := hbox rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (hA0 ω), abs_of_nonneg (le_of_lt hpos)] exact mul_le_mul_of_nonneg_left hmax (hA0 ω) refine hAwC_int.congr ?_ filter_upwards [hboxC] with ω hbox change A ω * wC ω = A ω / (1 / (if c ω < S.factualY ω then S.wMax Λ ω else S.wMin Λ ω)) rw [hwC_def, hY_def, div_div_eq_mul_div, div_one] have hcE_int : Integrable (fun ω => c ω * A ω * wE ω) P.μ := by have hmeas : AEStronglyMeasurable (fun ω => c ω * A ω * wE ω) P.μ := by refine ((hc_meas.mono S.sigmaX_le le_rfl).aestronglyMeasurable.mul hAwE_int.aestronglyMeasurable).congr ?_ filter_upwards [] with ω simp only [Pi.mul_apply] ring refine Integrable.mono' hc_env hmeas ?_ filter_upwards [hboxE, hmem.1.1] with ω hbox hint obtain ⟨_, hmax⟩ := hbox obtain ⟨het0, _⟩ := hint rw [Real.norm_eq_abs, abs_mul, abs_mul, abs_of_nonneg (hA0 ω), hwE_def, abs_of_nonneg (by positivity : 0 ≤ 1 / etilde ω), mul_assoc, mul_assoc] simpa [mul_assoc, hwE_def, one_div] using mul_le_mul_of_nonneg_left hmax (mul_nonneg (abs_nonneg (c ω)) (hA0 ω)) have hcC_int : Integrable (fun ω => c ω * A ω * wC ω) P.μ := by refine Integrable.mono' hc_env (((hc_meas.mono S.sigmaX_le le_rfl).mul hAm).mul hwCm).aestronglyMeasurable ?_ filter_upwards [hboxC] with ω hbox obtain ⟨_, hmax, hpos⟩ := hbox rw [Real.norm_eq_abs, abs_mul, abs_mul, abs_of_nonneg (hA0 ω), abs_of_nonneg (le_of_lt hpos), mul_assoc, mul_assoc] simpa [mul_assoc] using mul_le_mul_of_nonneg_left hmax (mul_nonneg (abs_nonneg (c ω)) (hA0 ω)) have hfirstE_int : Integrable (fun ω => A ω * (Y ω - c ω) * wE ω) P.μ := by refine (hYE_int.sub hcE_int).congr (Filter.Eventually.of_forall ?_) intro ω change A ω * Y ω * wE ω - c ω * A ω * wE ω = A ω * (Y ω - c ω) * wE ω ring have hfirstC_int : Integrable (fun ω => A ω * (Y ω - c ω) * wC ω) P.μ := by refine (hYC_int.sub hcC_int).congr (Filter.Eventually.of_forall ?_) intro ω change A ω * Y ω * wC ω - c ω * A ω * wC ω = A ω * (Y ω - c ω) * wC ω ring have hctermE_eq : ∫ ω, c ω * A ω * wE ω ∂P.μ = ∫ ω, c ω ∂P.μ := by have hprod_int : Integrable (fun ω => c ω * (A ω / etilde ω)) P.μ := by refine hcE_int.congr (Filter.Eventually.of_forall ?_) intro ω change c ω * A ω * (1 / etilde ω) = c ω * (A ω / etilde ω) rw [div_eq_mul_inv] ring have hpull : P.μ[fun ω => c ω * (A ω / etilde ω) | S.sigmaX] =ᵐ[P.μ] (fun ω => c ω * P.μ[fun ω => A ω / etilde ω | S.sigmaX] ω) := by exact MeasureTheory.condExp_mul_of_stronglyMeasurable_left (m := S.sigmaX) (μ := P.μ) hc_meas.stronglyMeasurable hprod_int hXE_int have hcal : P.μ[fun ω => A ω / etilde ω | S.sigmaX] =ᵐ[P.μ] (fun _ => (1 : ℝ)) := by simpa [POBackdoorSystem.Calibrated, hA_def] using hmem.2 have hmain : ∫ ω, c ω * (A ω / etilde ω) ∂P.μ = ∫ ω, c ω ∂P.μ := by have hcond : ∫ ω, P.μ[fun ω => c ω * (A ω / etilde ω) | S.sigmaX] ω ∂P.μ = ∫ ω, c ω * (A ω / etilde ω) ∂P.μ := MeasureTheory.integral_condExp S.sigmaX_le rw [← hcond] calc ∫ ω, P.μ[fun ω => c ω * (A ω / etilde ω) | S.sigmaX] ω ∂P.μ = ∫ ω, c ω * P.μ[fun ω => A ω / etilde ω | S.sigmaX] ω ∂P.μ := integral_congr_ae hpull _ = ∫ ω, c ω * 1 ∂P.μ := by refine integral_congr_ae ?_ filter_upwards [hcal] with ω hω rw [hω] _ = ∫ ω, c ω ∂P.μ := by simp rw [← hmain] refine integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω change c ω * A ω * (1 / etilde ω) = c ω * (A ω / etilde ω) rw [div_eq_mul_inv] ring have hctermC_eq : ∫ ω, c ω * A ω * wC ω ∂P.μ = ∫ ω, c ω ∂P.μ := by have hprod_int : Integrable (fun ω => c ω * (A ω / S.cutoffProp Λ c ω)) P.μ := by refine hcC_int.congr ?_ filter_upwards [hboxC] with ω hbox change c ω * A ω * wC ω = c ω * (A ω / (1 / (if c ω < S.factualY ω then S.wMax Λ ω else S.wMin Λ ω))) rw [hwC_def, hY_def, div_div_eq_mul_div, div_one] ring have hpull : P.μ[fun ω => c ω * (A ω / S.cutoffProp Λ c ω) | S.sigmaX] =ᵐ[P.μ] (fun ω => c ω * P.μ[fun ω => A ω / S.cutoffProp Λ c ω | S.sigmaX] ω) := by exact MeasureTheory.condExp_mul_of_stronglyMeasurable_left (m := S.sigmaX) (μ := P.μ) hc_meas.stronglyMeasurable hprod_int hXC_int have hcal : P.μ[fun ω => A ω / S.cutoffProp Λ c ω | S.sigmaX] =ᵐ[P.μ] (fun _ => (1 : ℝ)) := by simpa [POBackdoorSystem.Calibrated, hA_def] using hcut_mem.2 have hmain : ∫ ω, c ω * (A ω / S.cutoffProp Λ c ω) ∂P.μ = ∫ ω, c ω ∂P.μ := by have hcond : ∫ ω, P.μ[fun ω => c ω * (A ω / S.cutoffProp Λ c ω) | S.sigmaX] ω ∂P.μ = ∫ ω, c ω * (A ω / S.cutoffProp Λ c ω) ∂P.μ := MeasureTheory.integral_condExp S.sigmaX_le rw [← hcond] calc ∫ ω, P.μ[fun ω => c ω * (A ω / S.cutoffProp Λ c ω) | S.sigmaX] ω ∂P.μ -- … truncated; follow the source link for the rest …

theorem msmUpperCalib_eq_cutoff (Λ : ℝ) (hΛ : 1 ≤ Λ) (hoverlap : ∀ᵐ ω ∂P.μ, 0 < S.propScore true ω ∧ S.propScore true ω < 1) (c : P.Ω → ℝ) (hc_meas : Measurable[S.sigmaX] c) (hc_int : Integrable c P.μ) (hcut_mem : S.cutoffProp Λ c ∈ S.MSMSetCalib true Λ) (henv : Integrable (fun ω => S.dVar.indicator true ω * |S.factualY ω| * S.wMax Λ ω) P.μ) (hweight_env : Integrable (fun ω => S.dVar.indicator true ω * S.wMax Λ ω) P.μ) (hc_env : Integrable (fun ω => |c ω| * S.dVar.indicator true ω * S.wMax Λ ω) P.μ) : S.msmUpperCalib true Λ = S.candMean true (S.cutoffProp Λ c) := by classical have hne : (S.candMean true '' S.MSMSetCalib true Λ).Nonempty := ⟨S.candMean true (S.cutoffProp Λ c), Set.mem_image_of_mem _ hcut_mem⟩ have hle_all : ∀ x ∈ S.candMean true '' S.MSMSetCalib true Λ, x ≤ S.candMean true (S.cutoffProp Λ c) := by rintro x ⟨etilde, hmem, rfl⟩ exact S.cutoff_optimal Λ hΛ hoverlap c hc_meas hc_int hcut_mem henv hweight_env hc_env hmem have hbdd : BddAbove (S.candMean true '' S.MSMSetCalib true Λ) := ⟨S.candMean true (S.cutoffProp Λ c), hle_all⟩ refine le_antisymm ?_ ?_ · unfold POBackdoorSystem.msmUpperCalib exact csSup_le hne hle_all · unfold POBackdoorSystem.msmUpperCalib exact le_csSup hbdd (Set.mem_image_of_mem _ hcut_mem)

theorem wMin0_mul_propScore_le_one (Λ : ℝ) (hΛ : 1 ≤ Λ) (hoverlap : ∀ᵐ ω ∂P.μ, 0 < S.propScore false ω ∧ S.propScore false ω < 1) : ∀ᵐ ω ∂P.μ, S.wMin0 Λ ω * S.propScore false ω ≤ 1 := by have hΛ0 : 0 < Λ := lt_of_lt_of_le zero_lt_one hΛ filter_upwards [hoverlap] with ω hω set e : ℝ := S.propScore false ω with he_def have he0 : 0 < e := by simpa [he_def] using hω.1 have he1 : e < 1 := by simpa [he_def] using hω.2 have hw : S.wMin0 Λ ω * S.propScore false ω = e + (1 - e) / Λ := by simp only [POBackdoorSystem.wMin0, ← he_def] field_simp [hΛ0.ne', he0.ne'] have hdiv : (1 - e) / Λ ≤ 1 - e := by rw [div_le_iff₀ hΛ0] nlinarith [hΛ, le_of_lt he1] calc S.wMin0 Λ ω * S.propScore false ω = e + (1 - e) / Λ := hw _ ≤ e + (1 - e) := by linarith _ = 1 := by ring

theorem controlCutoffProp_calibrated_of_survival (Λ : ℝ) (hΛ : 1 < Λ) (hoverlap : ∀ᵐ ω ∂P.μ, 0 < S.propScore false ω ∧ S.propScore false ω < 1) (c : P.Ω → ℝ) (hint1 : Integrable (fun ω => S.dVar.indicator false ω * (if c ω < S.factualY ω then (1 : ℝ) else 0)) P.μ) (hmin_int : Integrable (fun ω => S.dVar.indicator false ω * S.wMin0 Λ ω) P.μ) (hdiff_int : Integrable (fun ω => (S.wMax0 Λ ω - S.wMin0 Λ ω) * (S.dVar.indicator false ω * (if c ω < S.factualY ω then (1 : ℝ) else 0))) P.μ) (hsurv : S.controlSurv c =ᵐ[P.μ] S.survTarget0 Λ) : S.Calibrated false (S.cutoffProp0 Λ c) := by have hΛ0 : 0 < Λ := lt_trans zero_lt_one hΛ refine (S.control_calibValue_eq Λ c hint1 hmin_int hdiff_int).trans ?_ filter_upwards [hoverlap, hsurv] with ω hω hsurvω rw [hsurvω] set e : ℝ := S.propScore false ω with he_def have he0 : 0 < e := by simpa [he_def] using hω.1 have he1 : e < 1 := by simpa [he_def] using hω.2 have hdiff_pos : 0 < S.wMax0 Λ ω - S.wMin0 Λ ω := by simp only [POBackdoorSystem.wMax0, POBackdoorSystem.wMin0, ← he_def] have h1e : 0 < 1 - e := by linarith have hΛsq : 0 < Λ * Λ - 1 := by nlinarith field_simp [hΛ0.ne', he0.ne'] nlinarith [h1e, hΛsq, hΛ0, he0] have hdiff_ne : S.wMax0 Λ ω - S.wMin0 Λ ω ≠ 0 := hdiff_pos.ne' unfold POBackdoorSystem.survTarget0 field_simp [hdiff_ne] ring

theorem cutoffProp0_mem_MSMSetCalib0_of_survival (Λ : ℝ) (hΛ : 1 < Λ) (hoverlap : ∀ᵐ ω ∂P.μ, 0 < S.propScore false ω ∧ S.propScore false ω < 1) (c : P.Ω → ℝ) (hint1 : Integrable (fun ω => S.dVar.indicator false ω * (if c ω < S.factualY ω then (1 : ℝ) else 0)) P.μ) (hmin_int : Integrable (fun ω => S.dVar.indicator false ω * S.wMin0 Λ ω) P.μ) (hdiff_int : Integrable (fun ω => (S.wMax0 Λ ω - S.wMin0 Λ ω) * (S.dVar.indicator false ω * (if c ω < S.factualY ω then (1 : ℝ) else 0))) P.μ) (hsurv : S.controlSurv c =ᵐ[P.μ] S.survTarget0 Λ) : S.cutoffProp0 Λ c ∈ S.MSMSetCalib false Λ := ⟨S.cutoffProp0_mem_MSMSet0 Λ (le_of_lt hΛ) hoverlap c, S.controlCutoffProp_calibrated_of_survival Λ hΛ hoverlap c hint1 hmin_int hdiff_int hsurv⟩

theorem cutoff_calibValue_eq (Λ : ℝ) (c : P.Ω → ℝ) (hint1 : Integrable (fun ω => S.dVar.indicator true ω * (if c ω < S.factualY ω then (1 : ℝ) else 0)) P.μ) (hmin_int : Integrable (fun ω => S.dVar.indicator true ω * S.wMin Λ ω) P.μ) (hdiff_int : Integrable (fun ω => (S.wMax Λ ω - S.wMin Λ ω) * (S.dVar.indicator true ω * (if c ω < S.factualY ω then (1 : ℝ) else 0))) P.μ) : P.μ[fun ω => S.dVar.indicator true ω / S.cutoffProp Λ c ω | S.sigmaX] =ᵐ[P.μ] (fun ω => S.wMin Λ ω * S.propScore true ω + (S.wMax Λ ω - S.wMin Λ ω) * S.treatedSurv c ω) := by classical set A : P.Ω → ℝ := S.dVar.indicator true with hA_def set I : P.Ω → ℝ := fun ω => if c ω < S.factualY ω then (1 : ℝ) else 0 with hI_def have hprop_meas : Measurable[S.sigmaX] (S.propScore true) := by unfold POBackdoorSystem.propScore exact stronglyMeasurable_condExp.measurable have hwMin_smeas : StronglyMeasurable[S.sigmaX] (S.wMin Λ) := by unfold POBackdoorSystem.wMin exact (measurable_const.add ((measurable_const.sub hprop_meas).div (measurable_const.mul hprop_meas))).stronglyMeasurable have hwMax_smeas : StronglyMeasurable[S.sigmaX] (S.wMax Λ) := by unfold POBackdoorSystem.wMax exact (measurable_const.add ((measurable_const.mul (measurable_const.sub hprop_meas)).div hprop_meas)).stronglyMeasurable have hdiff_smeas : StronglyMeasurable[S.sigmaX] (fun ω => S.wMax Λ ω - S.wMin Λ ω) := (hwMax_smeas.measurable.sub hwMin_smeas.measurable).stronglyMeasurable have hA_int : Integrable A P.μ := by rw [hA_def] exact S.dVar.integrable_indicator true (measurableSet_singleton true) have hI_int : Integrable (fun ω => A ω * I ω) P.μ := by rw [hA_def, hI_def] exact hint1 have hmin_int' : Integrable (fun ω => S.wMin Λ ω * A ω) P.μ := by refine hmin_int.congr (Filter.Eventually.of_forall ?_) intro ω rw [hA_def] exact mul_comm _ _ have hpoint : (fun ω => S.dVar.indicator true ω / S.cutoffProp Λ c ω) =ᵐ[P.μ] (fun ω => S.wMin Λ ω * A ω + (S.wMax Λ ω - S.wMin Λ ω) * (A ω * I ω)) := by refine Filter.Eventually.of_forall ?_ intro ω rw [hA_def, hI_def] by_cases hcy : c ω < S.factualY ω · simp only [POBackdoorSystem.cutoffProp, if_pos hcy] rw [div_div_eq_mul_div, div_one] ring · simp only [POBackdoorSystem.cutoffProp, if_neg hcy] rw [div_div_eq_mul_div, div_one] ring refine (MeasureTheory.condExp_congr_ae (m := S.sigmaX) (μ := P.μ) hpoint).trans ?_ have hsplit : P.μ[fun ω => S.wMin Λ ω * A ω + (S.wMax Λ ω - S.wMin Λ ω) * (A ω * I ω) | S.sigmaX] =ᵐ[P.μ] P.μ[fun ω => S.wMin Λ ω * A ω | S.sigmaX] + P.μ[fun ω => (S.wMax Λ ω - S.wMin Λ ω) * (A ω * I ω) | S.sigmaX] := MeasureTheory.condExp_add hmin_int' hdiff_int S.sigmaX have hpullMin : P.μ[fun ω => S.wMin Λ ω * A ω | S.sigmaX] =ᵐ[P.μ] (fun ω => S.wMin Λ ω * S.propScore true ω) := by have h := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (m := S.sigmaX) (μ := P.μ) hwMin_smeas hmin_int' hA_int exact h.trans (Filter.EventuallyEq.of_eq (by funext ω rfl)) have hpullDiff : P.μ[fun ω => (S.wMax Λ ω - S.wMin Λ ω) * (A ω * I ω) | S.sigmaX] =ᵐ[P.μ] (fun ω => (S.wMax Λ ω - S.wMin Λ ω) * S.treatedSurv c ω) := by have h := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (m := S.sigmaX) (μ := P.μ) hdiff_smeas hdiff_int hI_int exact h.trans (Filter.EventuallyEq.of_eq (by funext ω rfl)) filter_upwards [hsplit, hpullMin, hpullDiff] with ω hsplitω hminω hdiffω rw [hsplitω] change P.μ[fun ω => S.wMin Λ ω * A ω | S.sigmaX] ω + P.μ[fun ω => (S.wMax Λ ω - S.wMin Λ ω) * (A ω * I ω) | S.sigmaX] ω = S.wMin Λ ω * S.propScore true ω + (S.wMax Λ ω - S.wMin Λ ω) * S.treatedSurv c ω rw [hminω, hdiffω]

theorem cutoffProp_mem_MSMSet (Λ : ℝ) (hΛ : 1 ≤ Λ) (hoverlap : ∀ᵐ ω ∂P.μ, 0 < S.propScore true ω ∧ S.propScore true ω < 1) (c : P.Ω → ℝ) : S.cutoffProp Λ c ∈ S.MSMSet true Λ := by classical have hΛ0 : (0 : ℝ) < Λ := lt_of_lt_of_le zero_lt_one hΛ have hOR_box : ∀ {e et : ℝ}, 0 < e → e < 1 → 0 < et → et < 1 → ((1 / Λ ≤ OR et e ∧ OR et e ≤ Λ) ↔ (1 + (1 - e) / (Λ * e) ≤ 1 / et ∧ 1 / et ≤ 1 + Λ * (1 - e) / e)) := by intro e et he0 he1 het0 het1 have h1e : 0 < 1 - e := by linarith have h1et : 0 < 1 - et := by linarith have hOReq : OR et e = et * (1 - e) / ((1 - et) * e) := by rw [OR, div_div_eq_mul_div, div_mul_eq_mul_div, mul_comm, mul_div_mul_comm] ring_nf rw [hOReq] have hMax : (1 / Λ ≤ et * (1 - e) / ((1 - et) * e)) ↔ (1 / et ≤ 1 + Λ * (1 - e) / e) := by rw [div_le_div_iff₀ hΛ0 (by positivity : (0 : ℝ) < (1 - et) * e), show (1 : ℝ) + Λ * (1 - e) / e = (e + Λ * (1 - e)) / e by field_simp, div_le_div_iff₀ het0 he0] constructor <;> intro h <;> nlinarith [h, mul_pos hΛ0 he0] have hMin : (et * (1 - e) / ((1 - et) * e) ≤ Λ) ↔ (1 + (1 - e) / (Λ * e) ≤ 1 / et) := by rw [div_le_iff₀ (by positivity : (0 : ℝ) < (1 - et) * e), show (1 : ℝ) + (1 - e) / (Λ * e) = (Λ * e + (1 - e)) / (Λ * e) by field_simp, div_le_div_iff₀ (by positivity : (0 : ℝ) < Λ * e) het0] constructor <;> intro h <;> nlinarith [h, mul_pos hΛ0 he0] rw [hMax, hMin, and_comm] have hae : ∀ᵐ ω ∂P.μ, (1 : ℝ) < S.wMin Λ ω ∧ S.wMin Λ ω ≤ S.wMax Λ ω := by filter_upwards [hoverlap] with ω hω set e : ℝ := S.propScore true ω with he_def have he0 : 0 < e := by simpa [he_def] using hω.1 have he1 : e < 1 := by simpa [he_def] using hω.2 have h1e : 0 < 1 - e := by linarith refine ⟨?_, ?_⟩ · have : 0 < (1 - e) / (Λ * e) := by positivity simp only [POBackdoorSystem.wMin, ← he_def] linarith · simp only [POBackdoorSystem.wMin, POBackdoorSystem.wMax, ← he_def] have hd1 : (1 - e) / (Λ * e) ≤ Λ * (1 - e) / e := by rw [div_le_div_iff₀ (by positivity) he0] nlinarith [hΛ, mul_pos h1e he0, mul_pos hΛ0 he0, mul_nonneg (mul_nonneg (le_of_lt h1e) (le_of_lt he0)) (sub_nonneg.mpr hΛ)] linarith have hboxC : ∀ᵐ ω ∂P.μ, S.wMin Λ ω ≤ (if c ω < S.factualY ω then S.wMax Λ ω else S.wMin Λ ω) ∧ (if c ω < S.factualY ω then S.wMax Λ ω else S.wMin Λ ω) ≤ S.wMax Λ ω ∧ 1 < (if c ω < S.factualY ω then S.wMax Λ ω else S.wMin Λ ω) := by filter_upwards [hae] with ω hω obtain ⟨hmin1, hminmax⟩ := hω by_cases hcy : c ω < S.factualY ω · simp only [if_pos hcy] exact ⟨hminmax, le_rfl, lt_of_lt_of_le hmin1 hminmax⟩ · simp only [if_neg hcy] exact ⟨le_rfl, hminmax, hmin1⟩ refine ⟨?_, ?_⟩ · filter_upwards [hboxC] with ω hω obtain ⟨_, _, hwgt⟩ := hω unfold POBackdoorSystem.cutoffProp constructor · positivity · rw [div_lt_one (by linarith)] linarith · filter_upwards [hoverlap, hboxC] with ω hov hw obtain ⟨he0, he1⟩ := hov obtain ⟨hmin, hmax, hwgt⟩ := hw set wC : ℝ := if c ω < S.factualY ω then S.wMax Λ ω else S.wMin Λ ω with hwC_def have hcut : S.cutoffProp Λ c ω = 1 / wC := by rw [POBackdoorSystem.cutoffProp, hwC_def] have het0 : 0 < S.cutoffProp Λ c ω := by rw [hcut] positivity have het1 : S.cutoffProp Λ c ω < 1 := by rw [hcut, div_lt_one (by linarith)] linarith rw [(hOR_box he0 he1 het0 het1)] have hinv : 1 / S.cutoffProp Λ c ω = wC := by rw [hcut, one_div_one_div] rw [hinv] simpa [POBackdoorSystem.wMin, POBackdoorSystem.wMax, hwC_def] using ⟨hmin, hmax⟩

theorem condExp_treatmentIndicator_eq_xyPropensity : M.Q[M.treatmentIndicator | M.sigmaXY1] =ᵐ[M.Q] M.xyPropensity := by let mFull : MeasurableSpace M.Ω := M.sigmaXU ⊔ MeasurableSpace.comap M.Y1 inferInstance have hmFull : mFull ≤ M.measurableSpace := sup_le M.sigmaXU_le M.measurable_Y1.comap_le have hXYFull : M.sigmaXY1 ≤ mFull := by unfold sigmaXY1 mFull sigmaXU exact sup_le (le_trans le_sup_left le_sup_left) le_sup_right have hdrop : M.Q[M.treatmentIndicator | mFull] =ᵐ[M.Q] M.Q[M.treatmentIndicator | M.sigmaXU] := by let mark : Bool → ℝ := fun z => if z then 1 else 0 have hmark : Measurable mark := by fun_prop have htreat : M.treatmentIndicator = mark ∘ M.Z := by rfl rw [htreat] exact condExp_sup_comap_eq_of_condIndep M.sigmaXU_le M.measurable_Y1 M.measurable_Z M.latentUnconfounded hmark M.integrable_treatmentIndicator have htower : M.Q[M.treatmentIndicator | M.sigmaXY1] =ᵐ[M.Q] M.Q[M.Q[M.treatmentIndicator | mFull] | M.sigmaXY1] := (condExp_condExp_of_le (μ := M.Q) (f := M.treatmentIndicator) hXYFull hmFull).symm have hinner : M.Q[M.Q[M.treatmentIndicator | mFull] | M.sigmaXY1] =ᵐ[M.Q] M.Q[M.completePropensity | M.sigmaXY1] := by apply condExp_congr_ae refine hdrop.trans ?_ rw [M.propensity_eq] rfl exact htower.trans hinner