PO.ID.Partial.Sensitivity.MSM.Cutoff­Construct

theorem treatedSurv_const_eq (t : ℝ) : P.μ[fun ω => S.dVar.indicator true ω * (if t < S.factualY ω then (1 : ℝ) else 0) | S.sigmaX] =ᵐ[P.μ] fun ω => S.propScore true ω * (1 - S.treatedCondCDF ω t) := by classical have hpoint : (fun ω => S.dVar.indicator true ω * (if t < S.factualY ω then (1 : ℝ) else 0)) =ᵐ[P.μ] (fun ω => S.dVar.indicator true ω - S.dVar.indicator true ω * (if S.factualY ω ≤ t then (1 : ℝ) else 0)) := by exact Filter.Eventually.of_forall fun ω => by by_cases hle : S.factualY ω ≤ t · have hnot : ¬ t < S.factualY ω := not_lt.mpr hle simp [hle, hnot] · have hlt : t < S.factualY ω := lt_of_not_ge hle simp [hle, hlt] refine (MeasureTheory.condExp_congr_ae (m := S.sigmaX) (μ := P.μ) hpoint).trans ?_ have hsub := MeasureTheory.condExp_sub (μ := P.μ) (m := S.sigmaX) (f := S.dVar.indicator true) (g := fun ω => S.dVar.indicator true ω * (if S.factualY ω ≤ t then (1 : ℝ) else 0)) (S.dVar.integrable_indicator true (MeasurableSet.singleton true)) (S.integrable_treated_le_indicator t) have hle_bridge := S.treatedLe_const_eq t filter_upwards [hsub, hle_bridge] with ω hsubω hleω change P.μ[S.dVar.indicator true - (fun ω => S.dVar.indicator true ω * (if S.factualY ω ≤ t then (1 : ℝ) else 0)) | S.sigmaX] ω = S.propScore true ω * (1 - S.treatedCondCDF ω t) rw [hsubω] change S.propScore true ω - P.μ[fun ω => S.dVar.indicator true ω * (if S.factualY ω ≤ t then (1 : ℝ) else 0) | S.sigmaX] ω = S.propScore true ω * (1 - S.treatedCondCDF ω t) rw [hleω] ring

theorem exists_calibrating_cutoff (Λ : ℝ) (hoverlap : ∀ᵐ ω ∂P.μ, 0 < S.propScore true ω ∧ S.propScore true ω < 1) (hatomless : ∀ a : γ, Continuous (condCDF S.treatedXYLaw a)) (hlevel : ∀ᵐ ω ∂P.μ, 0 < S.calibLevel Λ ω ∧ S.calibLevel Λ ω < 1) : ∃ c : P.Ω → ℝ, Measurable[S.sigmaX] c ∧ S.treatedSurv c =ᵐ[P.μ] S.survTarget Λ := by classical have hprop_meas : Measurable[S.sigmaX] (S.propScore true) := by unfold POBackdoorSystem.propScore exact stronglyMeasurable_condExp.measurable have hwMin_meas : Measurable[S.sigmaX] (S.wMin Λ) := by unfold POBackdoorSystem.wMin exact measurable_const.add ((measurable_const.sub hprop_meas).div (measurable_const.mul hprop_meas)) have hwMax_meas : Measurable[S.sigmaX] (S.wMax Λ) := by unfold POBackdoorSystem.wMax exact measurable_const.add ((measurable_const.mul (measurable_const.sub hprop_meas)).div hprop_meas) have hsurvTarget_meas : Measurable[S.sigmaX] (S.survTarget Λ) := by unfold POBackdoorSystem.survTarget exact (measurable_const.sub (hwMin_meas.mul hprop_meas)).div (hwMax_meas.sub hwMin_meas) have hlevel_meas : Measurable[S.sigmaX] (S.calibLevel Λ) := by unfold POBackdoorSystem.calibLevel exact measurable_const.sub (hsurvTarget_meas.div hprop_meas) obtain ⟨g, hg, hg_eq⟩ := S.exists_factor_through_factualX hlevel_meas let τ : γ → ℝ := fun a => if 0 < g a ∧ g a < 1 then g a else (1 / 2 : ℝ) have hτ_meas : Measurable τ := by dsimp [τ] refine Measurable.ite ?_ hg measurable_const exact (measurableSet_lt measurable_const hg).inter (measurableSet_lt hg measurable_const) have hτ0 : ∀ a, 0 < τ a := by intro a dsimp [τ] by_cases ha : 0 < g a ∧ g a < 1 · simpa [ha] using ha.1 · simp [ha] have hτ1 : ∀ a, τ a < 1 := by intro a dsimp [τ] by_cases ha : 0 < g a ∧ g a < 1 · simpa [ha] using ha.2 · simp only [ha, ↓reduceIte] norm_num haveI : IsFiniteMeasure S.treatedXYLaw := by unfold POBackdoorSystem.treatedXYLaw infer_instance obtain ⟨hq_meas, hq_attain⟩ := measurable_condQuantile_and_attains S.treatedXYLaw τ hτ_meas hτ0 hτ1 (fun a => (hatomless a).continuousAt) let c : P.Ω → ℝ := fun ω => condQuantile S.treatedXYLaw τ (S.factualX ω) have hc_meas : Measurable[S.sigmaX] c := by rw [POBackdoorSystem.sigmaX] exact hq_meas.comp (comap_measurable S.factualX) refine ⟨c, hc_meas, ?_⟩ have hτ_eq_level : ∀ᵐ ω ∂P.μ, τ (S.factualX ω) = S.calibLevel Λ ω := by filter_upwards [hlevel] with ω hω have hgx : g (S.factualX ω) = S.calibLevel Λ ω := by exact (congrFun hg_eq ω).symm dsimp [τ] rw [hgx] simp [hω] have hsurv := S.treatedSurv_eq c hc_meas filter_upwards [hsurv, hτ_eq_level, hoverlap] with ω hsurvω hτω hoverlapω rw [hsurvω] have hcdf : S.treatedCondCDF ω (c ω) = τ (S.factualX ω) := by unfold POBackdoorSystem.treatedCondCDF c exact hq_attain (S.factualX ω) rw [hcdf, hτω] unfold POBackdoorSystem.calibLevel have hpos : S.propScore true ω ≠ 0 := ne_of_gt hoverlapω.1 field_simp [hpos] ring

theorem msmUpperCalib_eq_cutoff_of_calibrating_cutoff_integrability (Λ : ℝ) (hΛ : 1 < Λ) (hoverlap : ∀ᵐ ω ∂P.μ, 0 < S.propScore true ω ∧ S.propScore true ω < 1) (hatomless : ∀ a : γ, Continuous (condCDF S.treatedXYLaw a)) (hreg : ∀ c : P.Ω → ℝ, Measurable[S.sigmaX] c → S.treatedSurv c =ᵐ[P.μ] S.survTarget Λ → Integrable c P.μ ∧ Integrable (fun ω => |c ω| * S.dVar.indicator true ω * S.wMax Λ ω) P.μ) (henv : Integrable (fun ω => S.dVar.indicator true ω * |S.factualY ω| * S.wMax Λ ω) P.μ) (hweight_env : Integrable (fun ω => S.dVar.indicator true ω * S.wMax Λ ω) P.μ) : ∃ c : P.Ω → ℝ, Measurable[S.sigmaX] c ∧ S.cutoffProp Λ c ∈ S.MSMSetCalib true Λ ∧ S.msmUpperCalib true Λ = S.candMean true (S.cutoffProp Λ c) := by obtain ⟨c, hc_meas, hsurv⟩ := S.exists_calibrating_cutoff Λ hoverlap hatomless (S.calibLevel_mem_Ioo Λ hΛ hoverlap) obtain ⟨hc_int, hc_env⟩ := hreg c hc_meas hsurv have hc_amb : Measurable c := hc_meas.mono S.sigmaX_le le_rfl have hint1 := S.integrable_treated_gt_cutoff c hc_amb have hdiff_int := S.integrable_wDiff_mul_treated_gt_cutoff Λ (le_of_lt hΛ) hoverlap c hc_amb hweight_env have hmin_int := S.integrable_treated_wMin_of_wMax Λ (le_of_lt hΛ) hoverlap hweight_env have hcut_mem : S.cutoffProp Λ c ∈ S.MSMSetCalib true Λ := S.cutoffProp_mem_MSMSetCalib_of_survival Λ hΛ hoverlap c hint1 hmin_int hdiff_int hsurv have heq : S.msmUpperCalib true Λ = S.candMean true (S.cutoffProp Λ c) := S.msmUpperCalib_eq_cutoff Λ (le_of_lt hΛ) hoverlap c hc_meas hc_int hcut_mem henv hweight_env hc_env exact ⟨c, hc_meas, hcut_mem, heq⟩