PO.ID.Partial.Proxy.ZBased

theorem condMeanYofA_Z_bounds (HA : POProximalSystem.ZBasedAssumptions S μ) (a : Bool) (hAY : S.Avar.v ≠ S.Yvar.v) (Lenv Uenv : Bool × γ_X → ℝ) (hL : S.IsLowerEnvZ μ a Lenv) (hU : S.IsUpperEnvZ μ a Uenv) (hLInt : Integrable (fun ω => Lenv (a, S.X ω)) μ) (hUInt : Integrable (fun ω => Uenv (a, S.X ω)) μ) (hL_q : Integrable (fun ω => Lenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ) (hU_q : Integrable (fun ω => Uenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ) (hL_L : Integrable (fun ω => Lenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ) (hU_L : Integrable (fun ω => Uenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ) (hμpos : 0 < (μ {ω | S.A ω ≠ a}).toReal) : (μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω ≠ a}, Lenv (a, S.X ω) ∂μ ≤ S.condMeanYofA μ a ∧ S.condMeanYofA μ a ≤ (μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω ≠ a}, Uenv (a, S.X ω) ∂μ := by -- Both sides are obtained from the envelope chains by multiplying through -- by the positive scalar `(μ {A ≠ a}).toReal⁻¹`. have hinv_nn : 0 ≤ (μ {ω | S.A ω ≠ a}).toReal⁻¹ := inv_nonneg.mpr hμpos.le have hL_int := S.envelope_le_condIntYofA_arm HA a hAY hL hLInt hL_q hL_L have hU_int := S.condIntYofA_le_envelope_arm HA a hAY hU hUInt hU_q hU_L refine ⟨?_, ?_⟩ · -- Lower bound: scale `hL_int` by `(μ {A ≠ a}).toReal⁻¹`. have := mul_le_mul_of_nonneg_left hL_int hinv_nn simpa [POProximalSystem.condMeanYofA] using this · -- Upper bound: scale `hU_int` by `(μ {A ≠ a}).toReal⁻¹`. have := mul_le_mul_of_nonneg_left hU_int hinv_nn simpa [POProximalSystem.condMeanYofA] using this

theorem meanYofA_Z_bounds (HA : POProximalSystem.ZBasedAssumptions S μ) (a : Bool) (hAY : S.Avar.v ≠ S.Yvar.v) (Lenv Uenv : Bool × γ_X → ℝ) (hL : S.IsLowerEnvZ μ a Lenv) (hU : S.IsUpperEnvZ μ a Uenv) (hLInt : Integrable (fun ω => Lenv (a, S.X ω)) μ) (hUInt : Integrable (fun ω => Uenv (a, S.X ω)) μ) (hL_q : Integrable (fun ω => Lenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ) (hU_q : Integrable (fun ω => Uenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ) (hL_L : Integrable (fun ω => Lenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ) (hU_L : Integrable (fun ω => Uenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ) : (∫ ω in {ω | S.A ω ≠ a}, Lenv (a, S.X ω) ∂μ) + (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ) ≤ S.meanYofA μ a ∧ S.meanYofA μ a ≤ (∫ ω in {ω | S.A ω ≠ a}, Uenv (a, S.X ω) ∂μ) + (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ) := by -- `meanYofA = ∫_{A=¬a} Y(a) + ∫_{A=a} Y` by `meanYofA_eq_strata`. -- Then sandwich the off-arm `∫_{A=¬a} Y(a)` with the envelope chains. have hsplit := POProximalSystem.meanYofA_eq_strata (S := S) (μ := μ) HA.consistency a hAY (HA.integrable_YofA a) have hL_int := S.envelope_le_condIntYofA_arm HA a hAY hL hLInt hL_q hL_L have hU_int := S.condIntYofA_le_envelope_arm HA a hAY hU hUInt hU_q hU_L refine ⟨?_, ?_⟩ · rw [hsplit]; linarith · rw [hsplit]; linarith

lemma condIntYofA_le_envelope_arm (HA : POProximalSystem.ZBasedAssumptions S μ) (a : Bool) (hAY : S.Avar.v ≠ S.Yvar.v) {Uenv : Bool × γ_X → ℝ} (hU : S.IsUpperEnvZ μ a Uenv) (hUInt : Integrable (fun ω => Uenv (a, S.X ω)) μ) (hU_int : Integrable (fun ω => Uenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ) (hU_int_L : Integrable (fun ω => Uenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ) : (∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ) ≤ (∫ ω in {ω | S.A ω ≠ a}, Uenv (a, S.X ω) ∂μ) := by -- Implements the chain in the docstring (paper Thm 2 Appendix). -- We materialise each line as a `have` and chain them together. set s' : Set P.Ω := {ω | S.A ω ≠ a} with hs'_def set s : Set P.Ω := {ω | S.A ω = a} with hs_def have hs_meas : MeasurableSet s := S.measurable_A (measurableSet_singleton a) have hs'_meas : MeasurableSet s' := by have h_compl : s' = sᶜ := by ext ω; simp [s', s] rw [h_compl]; exact hs_meas.compl have hs'_in_AUX : MeasurableSet[S.σ_AUX] s' := by refine ⟨Prod.fst ⁻¹' {b : Bool | b ≠ a}, ?_, ?_⟩ · exact measurable_fst (MeasurableSet.compl (measurableSet_singleton a)) · ext ω; rfl have hs_in_AUX_set : MeasurableSet[S.σ_AUX] s := by refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩ · exact measurable_fst (measurableSet_singleton a) · ext ω; rfl -- Integrability shortcuts. have hYInt : Integrable S.Y μ := HA.integrable_Y have hYaInt : Integrable (S.YofA a) μ := HA.integrable_YofA a have hqInt : Integrable (fun ω => HA.q (S.Z ω, a, S.X ω)) μ := HA.integrable_q a -- σ_AUX-version of latent_exch and consistency. have hLatent : μ[S.YofA a | S.σ_AUX] =ᵐ[μ] μ[S.YofA a | S.σ_UX] := POProximalSystem.latent_exch_to_condExp' a (HA.latent_exch a) hYaInt have hConsist : μ[S.Y | S.σ_AUX] =ᵐ[μ.restrict s] μ[S.YofA a | S.σ_AUX] := POProximalSystem.consistency_event' HA.consistency a hAY hYInt hYaInt -- ============================================================ -- (1) ∫_{A≠a} Y(a) dμ = ∫_{A≠a} E[Y(a) | σ_AUX] dμ -- ============================================================ have hStep1 : (∫ ω in s', S.YofA a ω ∂μ) = (∫ ω in s', (μ[S.YofA a | S.σ_AUX]) ω ∂μ) := by have := MeasureTheory.setIntegral_condExp (μ := μ) (m := S.σ_AUX) S.σ_AUX_le hYaInt hs'_in_AUX exact this.symm -- ============================================================ -- (2) ∫_{A≠a} E[Y(a) | σ_AUX] dμ = ∫_{A≠a} E[Y(a) | σ_UX] dμ -- ============================================================ have hStep2 : (∫ ω in s', (μ[S.YofA a | S.σ_AUX]) ω ∂μ) = (∫ ω in s', (μ[S.YofA a | S.σ_UX]) ω ∂μ) := integral_congr_ae (ae_restrict_of_ae hLatent) -- ============================================================ -- (3+10) Arm-swap via the likelihood ratio (combines steps 3 and 10): -- ∫_{A≠a} f dμ = ∫_{A=a} f · L dμ for σ_UX-meas f. -- -- Justification sketch: tower against σ_UX, then apply -- `likelihoodRatio_swapA_spec` to convert E[𝟙{A≠a}|σ_UX] into -- E[𝟙{A=a}|σ_UX] · L, then collapse E[𝟙{A=a}|σ_UX] back via tower. -- The forward direction (E[𝟙_{A=a}|σ_UX] absorbing L into 𝟙_{A=a}) is -- the substantive measure-theoretic content, supplied by the likelihood-ratio -- swap specification in the assumption bundle. -- ============================================================ have hArmSwap_Y : (∫ ω in s', (μ[S.YofA a | S.σ_UX]) ω ∂μ) = (∫ ω in s, (μ[S.YofA a | S.σ_UX]) ω * HA.likelihoodRatio_swapA a ω ∂μ) := by -- Apply L2 (`setIntegral_eq_setIntegral_mul_of_likelihoodRatio_swap`). -- Setup: m = σ_UX, A = S.A, (a, a') = (a, !a), f = μ[Y(a)|σ_UX], L = LR. have hf_m : Measurable[S.σ_UX] (μ[S.YofA a | S.σ_UX] : P.Ω → ℝ) := (stronglyMeasurable_condExp).measurable have hL_m : Measurable[S.σ_UX] (HA.likelihoodRatio_swapA a) := HA.measurable_likelihoodRatio_swapA a haveI : IsFiniteMeasure (μ.trim S.σ_UX_le) := isFiniteMeasure_trim S.σ_UX_le haveI : SigmaFinite (μ.trim S.σ_UX_le) := inferInstance have hfInt : Integrable (fun ω => (μ[S.YofA a | S.σ_UX]) ω) μ := integrable_condExp -- Integrability of f * L is supplied by the bundle field below. have hfLInt : Integrable (fun ω => (μ[S.YofA a | S.σ_UX]) ω * HA.likelihoodRatio_swapA a ω) μ := HA.integrable_condExpYofA_mul_L a -- hSpec from the bundle. have hSpec := HA.likelihoodRatio_swapA_spec a -- Convert {A ω ≠ a} to {A ω = !a} using Bool decidability. have h_ne_eq : ({ω | S.A ω ≠ a} : Set P.Ω) = {ω | S.A ω = !a} := by ext ω; constructor · intro h; cases ha : S.A ω <;> cases a <;> simp_all · intro h; cases ha : S.A ω <;> cases a <;> simp_all -- Apply L2. have hL2 := setIntegral_eq_setIntegral_mul_of_likelihoodRatio_swap S.σ_UX_le {ω | S.A ω = a} {ω | S.A ω = !a} (S.measurable_A (measurableSet_singleton a)) (S.measurable_A (measurableSet_singleton (!a))) (hf_m.aestronglyMeasurable.mul hL_m.aestronglyMeasurable) hf_m.aestronglyMeasurable hfInt.integrableOn hfLInt.integrableOn (by -- Need hSpec's RHS to use (!a) instead of (≠ a). They're equal as sets. have h_ind_eq : (indicator ({ω' | S.A ω' = !a}) (fun _ => (1:ℝ))) = indicator ({ω' | S.A ω' ≠ a}) (fun _ => (1:ℝ)) := by congr 1 ext ω; constructor · intro h; cases ha : S.A ω <;> cases a <;> simp_all · intro h; cases ha : S.A ω <;> cases a <;> simp_all rw [h_ind_eq] exact hSpec) -- hL2: ∫_{S.A ω = !a} f dμ = ∫_{S.A ω = a} f * L dμ. -- Goal: ∫ in s', f dμ = ∫ in s, f * L dμ. s' = {A ≠ a}, s = {A = a}. rw [show s' = {ω | S.A ω = !a} from h_ne_eq] exact hL2 -- ============================================================ -- (4) On {A=a}: replace E[Y(a) | σ_UX] by E[Y | σ_UX]. -- -- From hConsist (on {A=a}: E[Y|σ_AUX] =ᵐ E[Y(a)|σ_AUX]) and hLatent -- (global: E[Y(a)|σ_AUX] =ᵐ E[Y(a)|σ_UX]) plus the analogous transfer -- for Y, we get E[Y|σ_UX] =ᵐ[restrict s] E[Y(a)|σ_UX]. -- ============================================================ -- Corrected step: use σ_AUX rather than σ_UX in the middle of the chain. -- This avoids requiring a separate `Y ⟂ A | σ_UX` lift; paper Theorem 2 does not bundle it. -- hCE_eq_arm_AUX : μ[Y(a)|σ_UX] =ᵐ[restrict s] μ[Y|σ_AUX]. -- Derived from: hLatent.symm (gives μ[Y(a)|σ_UX] =ᵐ μ[Y(a)|σ_AUX] globally) -- and hConsist.symm (gives μ[Y(a)|σ_AUX] =ᵐ[restrict s] μ[Y|σ_AUX]). have hCE_eq_arm_AUX : μ[S.YofA a | S.σ_UX] =ᵐ[μ.restrict s] μ[S.Y | S.σ_AUX] := by have h1 : μ[S.YofA a | S.σ_UX] =ᵐ[μ.restrict s] μ[S.YofA a | S.σ_AUX] := ae_restrict_of_ae hLatent.symm exact h1.trans hConsist.symm have hStep4 : (∫ ω in s, (μ[S.YofA a | S.σ_UX]) ω * HA.likelihoodRatio_swapA a ω ∂μ) = (∫ ω in s, (μ[S.Y | S.σ_AUX]) ω * HA.likelihoodRatio_swapA a ω ∂μ) := by refine integral_congr_ae ?_ filter_upwards [hCE_eq_arm_AUX] with ω hω rw [hω] -- ============================================================ -- (5) Substitute the bridge: on {A=a}, L = E[q(Z,a,X) | σ_AUX]. -- ============================================================ have hStep5 : (∫ ω in s, (μ[S.Y | S.σ_AUX]) ω * HA.likelihoodRatio_swapA a ω ∂μ) = (∫ ω in s, (μ[S.Y | S.σ_AUX]) ω * (μ[fun ω' => HA.q (S.Z ω', a, S.X ω') | S.σ_AUX]) ω ∂μ) := by refine integral_congr_ae ?_ have hbridge := HA.bridge_q a filter_upwards [hbridge] with ω hω rw [hω] -- ============================================================ -- (6,7) Combined factorisation step: -- ∫_{A=a} E[Y|σ_UX] · E[q|σ_AUX] dμ -- = ∫_{A=a} E[Y · q | σ_AZX] · 1 dμ -- = ∫_{A=a} (μ[Y|σ_AZX]) ω · q(Z,a,X) dμ -- This uses proxy_YZ (Y ⟂ Z | σ_AUX) and σ_AZX-measurability of q. -- The combined manipulation is the Mathlib gap. -- ============================================================ have hStep67 : (∫ ω in s, (μ[S.Y | S.σ_AUX]) ω * (μ[fun ω' => HA.q (S.Z ω', a, S.X ω') | S.σ_AUX]) ω ∂μ) = (∫ ω in s, (μ[S.Y | S.σ_AZX]) ω * HA.q (S.Z ω, a, S.X ω) ∂μ) := condIntYq_factor_arm HA a -- ============================================================ -- (8) Apply IsUpperEnvZ pointwise a.e. on {A=a}, with q ≥ 0. -- ============================================================ have hStep8 : (∫ ω in s, (μ[S.Y | S.σ_AZX]) ω * HA.q (S.Z ω, a, S.X ω) ∂μ) ≤ (∫ ω in s, Uenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω) ∂μ) := by refine MeasureTheory.setIntegral_mono_ae_restrict ?_ ?_ ?_ · -- Integrability of LHS on s, supplied by the bundle field -- `integrable_condExpY_mul_q`. exact (HA.integrable_condExpY_mul_q a).restrict · exact hU_int.restrict · -- Pointwise a.e. comparison from `hU` and `q ≥ 0`. have hUpper := hU.2 filter_upwards [hUpper] with ω hω have hqnn : 0 ≤ HA.q (S.Z ω, a, S.X ω) := HA.q_nonneg _ exact mul_le_mul_of_nonneg_right hω hqnn -- ============================================================ -- (9) Reverse the bridge: on {A=a}, E[q(Z,a,X) | σ_AUX] = L. -- ============================================================ have hStep9 : (∫ ω in s, Uenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω) ∂μ) = (∫ ω in s, Uenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω ∂μ) := by -- Apply L1 (setIntegral_mul_condExp_of_stronglyMeasurableLeft) with -- m = σ_AUX, f = Uenv(a, X) (σ_X-meas, hence σ_AUX-meas via -- σ_X_le_σ_AUX), g = q(Z, a, X), s = {A=a} ∈ σ_AUX. -- Then bridge_q substitutes μ[q|σ_AUX] for L on s. have hUmeas_X : Measurable[S.σ_X] (fun ω => Uenv (a, S.X ω)) := by have hUenv_meas : Measurable Uenv := hU.1 have hpair : Measurable[S.σ_X] (fun ω : P.Ω => (a, S.X ω)) := by refine prodMk (m := S.σ_X) (measurable_const) ?_ -- S.X is σ_X-measurable by definition. intro t ht exact ⟨t, ht, rfl⟩ exact hUenv_meas.comp hpair have hUmeas_AUX : Measurable[S.σ_AUX] (fun ω => Uenv (a, S.X ω)) := hUmeas_X.mono S.σ_X_le_σ_AUX le_rfl have hU_sm : StronglyMeasurable[S.σ_AUX] (fun ω => Uenv (a, S.X ω)) := hUmeas_AUX.stronglyMeasurable have hL1 := setIntegral_mul_condExp_of_stronglyMeasurableLeft (m := S.σ_AUX) S.σ_AUX_le hU_sm hqInt hU_int hs_in_AUX_set -- hL1: ∫_s Uenv·q dμ = ∫_s Uenv · μ[q|σ_AUX] dμ rw [hL1] refine integral_congr_ae ?_ have hbridge := HA.bridge_q a -- … truncated; follow the source link for the rest …