PO.ID.Exact.Proximal

lemma integrable_Y (HA : Assumptions S μ) (hAY : S.Avar.v ≠ S.Yvar.v) : Integrable S.Y μ := by have htrue_int : Integrable (fun ω => S.YofA true ω * S.Avar.indicator true ω) μ := integrable_mul_indicator S.Avar true HA.integrable_YofA1 (S.measurable_YofA true) have hfalse_int : Integrable (fun ω => S.YofA false ω * S.Avar.indicator false ω) μ := integrable_mul_indicator S.Avar false HA.integrable_YofA0 (S.measurable_YofA false) have hsum_int : Integrable ((fun ω => S.YofA true ω * S.Avar.indicator true ω) + fun ω => S.YofA false ω * S.Avar.indicator false ω) μ := htrue_int.add hfalse_int refine hsum_int.congr (Filter.Eventually.of_forall ?_) intro ω by_cases hω : S.A ω = true · have hcf : S.YofA true ω = S.Y ω := by simpa [YofA, Y, A] using POVar.cf_eq_factual_on_event HA.consistency S.Yvar S.Avar true hAY.symm hω have hind_true : S.Avar.indicator true ω = 1 := S.Avar.indicator_apply_eq_one hω have hfalse : S.A ω ≠ false := by rw [hω] decide have hind_false : S.Avar.indicator false ω = 0 := S.Avar.indicator_apply_eq_zero hfalse simp [Pi.add_apply, hcf, hind_true, hind_false] · have hω_false : S.A ω = false := by cases hA : S.A ω <;> simp_all have hcf : S.YofA false ω = S.Y ω := by simpa [YofA, Y, A] using POVar.cf_eq_factual_on_event HA.consistency S.Yvar S.Avar false hAY.symm hω_false have hind_true : S.Avar.indicator true ω = 0 := S.Avar.indicator_apply_eq_zero hω have hind_false : S.Avar.indicator false ω = 1 := S.Avar.indicator_apply_eq_one hω_false simp [Pi.add_apply, hcf, hind_true, hind_false]

lemma consistency_event (HA : Assumptions S μ) (a : Bool) (hAY : S.Avar.v ≠ S.Yvar.v) : μ[S.Y | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[S.YofA a | S.σ_AUX] := by have hYaInt : Integrable (S.YofA a) μ := by cases a · exact HA.integrable_YofA0 · exact HA.integrable_YofA1 exact consistency_event' HA.consistency a hAY (HA.integrable_Y hAY) hYaInt

theorem Eofyofa_eq_Eh (HA : Assumptions S μ) (a : Bool) (hAY : S.Avar.v ≠ S.Yvar.v) : ∫ ω, S.YofA a ω ∂μ = ∫ ω, HA.h (a, S.W ω, S.X ω) ∂μ := by -- Set s = {A = a}; needed throughout. set s : Set P.Ω := {ω | S.A ω = a} with hs_def have hs_meas : MeasurableSet s := S.measurable_A (measurableSet_singleton a) -- Integrability shortcuts. have hYInt : Integrable S.Y μ := HA.integrable_Y hAY have hYaInt : Integrable (S.YofA a) μ := by cases a · exact HA.integrable_YofA0 · exact HA.integrable_YofA1 have hhInt : Integrable (fun ω => HA.h (a, S.W ω, S.X ω)) μ := by fun_prop have hhAInt : Integrable (fun ω => HA.h (S.A ω, S.W ω, S.X ω)) μ := by fun_prop have h_meas_haWX : Measurable (fun ω => HA.h (a, S.W ω, S.X ω)) := by fun_prop -- ============================================================ -- Step 1: Construct g_a : γ_U × γ_X → ℝ via Doob–Dynkin. -- ============================================================ -- μ[Y | σ_AUX] is σ_AUX = comap S.AUX-measurable, so factors through S.AUX. have hCEY_meas : Measurable[S.σ_AUX] (μ[S.Y | S.σ_AUX]) := by fun_prop have hCEY_meas' : Measurable[comap S.AUX inferInstance] (μ[S.Y | S.σ_AUX]) := by fun_prop obtain ⟨f_Y, hf_Y_meas, hf_Y_eq⟩ := Measurable.exists_eq_measurable_comp (f := S.AUX) (Z := ℝ) hCEY_meas' -- μ[h(a,W,X) | σ_AUX] is also σ_AUX-measurable. have hCEh_meas : Measurable[S.σ_AUX] (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) := by fun_prop have hCEh_meas' : Measurable[comap S.AUX inferInstance] (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) := by fun_prop obtain ⟨f_h, hf_h_meas, hf_h_eq⟩ := Measurable.exists_eq_measurable_comp (f := S.AUX) (Z := ℝ) hCEh_meas' -- Define g_a (u, x) := f_Y (a, u, x) - f_h (a, u, x). let g_a : γ_U × γ_X → ℝ := fun p => f_Y (a, p.1, p.2) - f_h (a, p.1, p.2) have g_a_meas : Measurable g_a := by fun_prop -- g_a ∘ S.UX is integrable on the restriction to s = {A = a}. -- On s, S.AUX ω = (a, S.U ω, S.X ω), so g_a ∘ UX = (μ[Y|σ_AUX]) - (μ[h|σ_AUX]) -- pointwise. Both condExps are integrable globally, hence on restrict, and -- their difference is integrable; congr lifts to g_a ∘ UX. have g_a_UX_int : Integrable (fun ω => g_a (S.UX ω)) (μ.restrict s) := by have hCEY_int : Integrable (μ[S.Y | S.σ_AUX]) μ := by fun_prop have hCEh_int : Integrable (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) μ := by fun_prop have hCEY_int_r : Integrable (μ[S.Y | S.σ_AUX]) (μ.restrict s) := hCEY_int.restrict have hCEh_int_r : Integrable (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) (μ.restrict s) := hCEh_int.restrict have hdiff_int : Integrable (fun ω => (μ[S.Y | S.σ_AUX]) ω - (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω) (μ.restrict s) := by fun_prop -- Show on s: g_a (S.UX ω) = (μ[Y|σ_AUX]) ω - (μ[h|σ_AUX]) ω. have hae : (fun ω => (μ[S.Y | S.σ_AUX]) ω - (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω) =ᵐ[μ.restrict s] (fun ω => g_a (S.UX ω)) := by filter_upwards [ae_restrict_mem hs_meas] with ω hω_s have hAa : S.A ω = a := hω_s have hAUX_eq : S.AUX ω = (a, S.U ω, S.X ω) := by change (S.A ω, S.U ω, S.X ω) = (a, S.U ω, S.X ω); rw [hAa] have hY : (μ[S.Y | S.σ_AUX]) ω = f_Y (a, S.U ω, S.X ω) := by have h1 := congrFun hf_Y_eq ω change (μ[S.Y | S.σ_AUX]) ω = f_Y (a, S.U ω, S.X ω) rw [h1]; change f_Y (S.AUX ω) = f_Y (a, S.U ω, S.X ω); rw [hAUX_eq] have hh : (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω = f_h (a, S.U ω, S.X ω) := by have h1 := congrFun hf_h_eq ω change (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω = f_h (a, S.U ω, S.X ω) rw [h1]; change f_h (S.AUX ω) = f_h (a, S.U ω, S.X ω); rw [hAUX_eq] have hUX : S.UX ω = (S.U ω, S.X ω) := rfl simp [hY, hh, g_a, hUX] exact hdiff_int.congr hae -- ============================================================ -- Step 2: μ[Y - h(a,W,X) | σ_AZUX] =ᵐ[μ.restrict s] g_a ∘ S.UX. -- ============================================================ -- By linearity + helpers 1, 2: -- μ[Y - h(a,W,X) | σ_AZUX] -- =ᵐ μ[Y | σ_AZUX] - μ[h(a,W,X) | σ_AZUX] (linearity) -- =ᵐ μ[Y | σ_AUX] - μ[h(a,W,X) | σ_AUX] (helpers 1, 2) -- = (f_Y ∘ S.AUX) - (f_h ∘ S.AUX) (Doob–Dynkin) -- On s = {A=a}, S.AUX ω = (a, S.U ω, S.X ω), so this evaluates to -- f_Y(a, S.U ω, S.X ω) - f_h(a, S.U ω, S.X ω) = g_a (S.UX ω). have step2 : (μ[fun ω => S.Y ω - HA.h (a, S.W ω, S.X ω) | S.σ_AZUX]) =ᵐ[μ.restrict s] (fun ω => g_a (S.UX ω)) := by -- Linearity: μ[Y - h(a,W,X)|σ_AZUX] =ᵐ μ[Y|σ_AZUX] - μ[h(a,W,X)|σ_AZUX]. have hlin : μ[fun ω => S.Y ω - HA.h (a, S.W ω, S.X ω) | S.σ_AZUX] =ᵐ[μ] μ[S.Y | S.σ_AZUX] - μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AZUX] := by condexp_linearity -- Helpers 1, 2: drop Z. have h1 : μ[S.Y | S.σ_AZUX] =ᵐ[μ] μ[S.Y | S.σ_AUX] := condExp_drop_Z HA hAY have h2 : μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AZUX] =ᵐ[μ] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] := condExp_h_drop_Z HA a -- Combine globally: -- μ[Y-h|σ_AZUX] =ᵐ μ[Y|σ_AUX] - μ[h|σ_AUX]. have hglobal : μ[fun ω => S.Y ω - HA.h (a, S.W ω, S.X ω) | S.σ_AZUX] =ᵐ[μ] μ[S.Y | S.σ_AUX] - μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] := by refine hlin.trans ?_ filter_upwards [h1, h2] with ω hω1 hω2 simp [Pi.sub_apply, hω1, hω2] -- Now restrict to s. have hrestrict : μ[fun ω => S.Y ω - HA.h (a, S.W ω, S.X ω) | S.σ_AZUX] =ᵐ[μ.restrict s] μ[S.Y | S.σ_AUX] - μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] := ae_restrict_of_ae hglobal -- On s, the RHS = g_a ∘ S.UX (Doob–Dynkin substitution, same as step 5). refine hrestrict.trans ?_ filter_upwards [ae_restrict_mem hs_meas] with ω hω_s have hAa : S.A ω = a := hω_s have hAUX_eq : S.AUX ω = (a, S.U ω, S.X ω) := by change (S.A ω, S.U ω, S.X ω) = (a, S.U ω, S.X ω); rw [hAa] have hY : (μ[S.Y | S.σ_AUX]) ω = f_Y (a, S.U ω, S.X ω) := by have h1 := congrFun hf_Y_eq ω change (μ[S.Y | S.σ_AUX]) ω = f_Y (a, S.U ω, S.X ω) rw [h1]; change f_Y (S.AUX ω) = f_Y (a, S.U ω, S.X ω); rw [hAUX_eq] have hh : (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω = f_h (a, S.U ω, S.X ω) := by have h1 := congrFun hf_h_eq ω change (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω = f_h (a, S.U ω, S.X ω) rw [h1]; change f_h (S.AUX ω) = f_h (a, S.U ω, S.X ω); rw [hAUX_eq] show (μ[S.Y | S.σ_AUX] - μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω = g_a (S.UX ω) have hUX : S.UX ω = (S.U ω, S.X ω) := rfl simp [Pi.sub_apply, hY, hh, g_a, hUX] -- ============================================================ -- Step 3: μ[g_a ∘ S.UX | σ_AZX] =ᵐ[μ.restrict s] 0. -- ============================================================ -- σ_AZX ≤ σ_AZUX (σ_AZUX includes U), so by tower: -- μ[Y - h(A,W,X) | σ_AZX] =ᵐ μ[μ[Y - h(A,W,X) | σ_AZUX] | σ_AZX]. -- Bridge gives LHS =ᵐ 0; on s, h(A,W,X) =ᵐ h(a,W,X) (since A=a on s), and -- s ∈ σ_AZX, so we can swap to get -- μ[μ[Y - h(a,W,X) | σ_AZUX] | σ_AZX] =ᵐ[restrict s] 0. -- Combining with step2: μ[g_a ∘ S.UX | σ_AZX] =ᵐ[restrict s] 0. have step3 : (μ[fun ω => g_a (S.UX ω) | S.σ_AZX]) =ᵐ[μ.restrict s] 0 := by -- Strategy: -- 1. Tower: σ_AZX ≤ σ_AZUX. Get -- μ[g_a∘UX | σ_AZX] =ᵐ μ[μ[g_a∘UX | σ_AZUX] | σ_AZX]. -- 2. Step 2 says μ[Y - h(a,W,X) | σ_AZUX] =ᵐ[restrict s] g_a∘UX. -- Lift LHS to global: bridge gives μ[Y - h(A,W,X) | σ_AZX] =ᵐ 0, -- so condExp through indicator on {A=a} (where h(A,W,X)=h(a,W,X)) -- gives the goal. -- σ_AZX ≤ σ_AZUX (since AZUX projects onto AZX measurably). have hAZX_le_AZUX : S.σ_AZX ≤ S.σ_AZUX := by -- Show S.AZX is σ_AZUX-measurable. have hAZX_meas : Measurable[S.σ_AZUX] S.AZX := by fun_prop exact hAZX_meas.comap_le -- s = {A=a} ∈ σ_AZX (use comap of (A,Z,X) on the first coordinate). have hs_in_AZX : MeasurableSet[S.σ_AZX] s := by refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩ · exact measurable_fst (measurableSet_singleton a) · ext ω; rfl -- Difference function and integrability. let h : P.Ω → ℝ := fun ω => S.Y ω - HA.h (S.A ω, S.W ω, S.X ω) let h' : P.Ω → ℝ := fun ω => S.Y ω - HA.h (a, S.W ω, S.X ω) have hint : Integrable h μ := by fun_prop have hint' : Integrable h' μ := by fun_prop -- On s, h = h' pointwise. have hh_eq_on_s : ∀ᵐ ω ∂(μ.restrict s), h ω = h' ω := by filter_upwards [ae_restrict_mem hs_meas] with ω hω_s have hAa : S.A ω = a := hω_s show S.Y ω - HA.h (S.A ω, S.W ω, S.X ω) = S.Y ω - HA.h (a, S.W ω, S.X ω) rw [hAa] -- Tower step 2 to σ_AZX: -- μ[h' | σ_AZX] =ᵐ μ[μ[h' | σ_AZUX] | σ_AZX]. have h_tower : μ[h' | S.σ_AZX] =ᵐ[μ] μ[μ[h' | S.σ_AZUX] | S.σ_AZX] := (MeasureTheory.condExp_condExp_of_le hAZX_le_AZUX S.σ_AZUX_le).symm -- step2 (restricted) lifts: μ[μ[h' | σ_AZUX] | σ_AZX] =ᵐ[restrict s] μ[g_a∘UX | σ_AZX]. -- Use indicator technique: 1_s · μ[h' | σ_AZUX] =ᵐ 1_s · g_a∘UX (both globally). -- Then condExp_indicator with s ∈ σ_AZX. -- Actually simpler: condExp_congr on restrict requires inner =ᵐ on restrict, -- which doesn't directly give condExp =ᵐ on restrict. -- We use: indicator s · μ[h'|σ_AZUX] =ᵐ[μ] indicator s · g_a∘UX. have hCEh'_AZUX_int : Integrable (μ[h' | S.σ_AZUX]) μ := by fun_prop -- Case split: if g_a ∘ UX is not globally integrable, μ[g_a∘UX|σ_AZX] = 0 -- everywhere, so the goal is trivial. Otherwise, use original argument. by_cases hg_a_int : Integrable (fun ω => g_a (S.UX ω)) μ case neg => -- μ[g_a∘UX|σ_AZX] = 0 globally, so a.e. zero on restrict s. have h0 : (μ[fun ω => g_a (S.UX ω) | S.σ_AZX]) = 0 := MeasureTheory.condExp_of_not_integrable hg_a_int rw [h0] -- pos branch: hg_a_int : Integrable (fun ω => g_a (S.UX ω)) μ holds. -- 1_s · μ[h'|σ_AZUX] =ᵐ[μ] 1_s · g_a∘UX (from step2 restricted to s). have hind_eq : s.indicator (μ[h' | S.σ_AZUX]) =ᵐ[μ] s.indicator (fun ω => g_a (S.UX ω)) := by exact indicator_aeEq_of_aeEq_restrict hs_meas step2 -- Apply condExp to both sides and use condExp_indicator. have hCE_ind_h' := MeasureTheory.condExp_indicator (m := S.σ_AZX) hCEh'_AZUX_int hs_in_AZX have hCE_ind_g := MeasureTheory.condExp_indicator (m := S.σ_AZX) hg_a_int hs_in_AZX -- μ[1_s · μ[h'|σ_AZUX] | σ_AZX] =ᵐ μ[1_s · g_a∘UX | σ_AZX] (by hind_eq + condExp_congr). have hCE_eq : μ[s.indicator (μ[h' | S.σ_AZUX]) | S.σ_AZX] =ᵐ[μ] μ[s.indicator (fun ω => g_a (S.UX ω)) | S.σ_AZX] := MeasureTheory.condExp_congr_ae hind_eq -- Combine: 1_s · μ[μ[h'|σ_AZUX] | σ_AZX] =ᵐ 1_s · μ[g_a∘UX | σ_AZX]. have hind_CE : s.indicator (μ[μ[h' | S.σ_AZUX] | S.σ_AZX]) =ᵐ[μ] s.indicator (μ[fun ω => g_a (S.UX ω) | S.σ_AZX]) := hCE_ind_h'.symm.trans (hCE_eq.trans hCE_ind_g) -- Now we need: 1_s · μ[μ[h'|σ_AZUX] | σ_AZX] =ᵐ 0, since by tower -- μ[μ[h'|σ_AZUX] | σ_AZX] =ᵐ μ[h' | σ_AZX] -- and on s (since {A=a} ∈ σ_AZX), μ[h'|σ_AZX] =ᵐ μ[h|σ_AZX] =ᵐ 0 (bridge). -- We prove 1_s · μ[h'|σ_AZX] =ᵐ 0 using bridge. -- Step (a): μ[h'|σ_AZX] =ᵐ[restrict s] 0. -- Use indicator technique: 1_s · h =ᵐ 1_s · h' globally (both pointwise on s). have hind_h_h' : s.indicator h =ᵐ[μ] s.indicator h' := by exact indicator_aeEq_of_aeEq_restrict hs_meas hh_eq_on_s -- Apply condExp_indicator to both: have hCE_ind_h := MeasureTheory.condExp_indicator (m := S.σ_AZX) hint hs_in_AZX have hCE_ind_h'_AZX := MeasureTheory.condExp_indicator (m := S.σ_AZX) hint' hs_in_AZX -- μ[1_s · h | σ_AZX] =ᵐ μ[1_s · h' | σ_AZX] (by hind_h_h'). have hCE_eq2 : μ[s.indicator h | S.σ_AZX] =ᵐ[μ] μ[s.indicator h' | S.σ_AZX] := MeasureTheory.condExp_congr_ae hind_h_h' have hind_CE_h : s.indicator (μ[h | S.σ_AZX]) =ᵐ[μ] s.indicator (μ[h' | S.σ_AZX]) := hCE_ind_h.symm.trans (hCE_eq2.trans hCE_ind_h'_AZX) -- Bridge: μ[h | σ_AZX] =ᵐ 0, so 1_s · μ[h|σ_AZX] =ᵐ 0. have hbridge : (μ[h | S.σ_AZX]) =ᵐ[μ] 0 := HA.bridge have hind_h_zero : s.indicator (μ[h | S.σ_AZX]) =ᵐ[μ] 0 := by filter_upwards [hbridge] with ω hω by_cases hωs : ω ∈ s · rw [Set.indicator_of_mem hωs, hω] · rw [Set.indicator_of_notMem hωs]; rfl -- So 1_s · μ[h'|σ_AZX] =ᵐ 0, hence μ[h'|σ_AZX] =ᵐ[restrict s] 0. have hind_h'_zero : s.indicator (μ[h' | S.σ_AZX]) =ᵐ[μ] 0 := hind_CE_h.symm.trans hind_h_zero have hh'_AZX_zero : (μ[h' | S.σ_AZX]) =ᵐ[μ.restrict s] 0 := by have hind_h'_zero' : s.indicator (μ[h' | S.σ_AZX]) =ᵐ[μ] s.indicator (0 : P.Ω → ℝ) := by simpa using hind_h'_zero simpa using aeEq_restrict_of_indicator_aeEq hs_meas hind_h'_zero' -- Tower h_tower says μ[h'|σ_AZX] =ᵐ μ[μ[h'|σ_AZUX]|σ_AZX]. Restrict to s: have h_tower_s : μ[h' | S.σ_AZX] =ᵐ[μ.restrict s] μ[μ[h' | S.σ_AZUX] | S.σ_AZX] := ae_restrict_of_ae h_tower -- So μ[μ[h'|σ_AZUX]|σ_AZX] =ᵐ[restrict s] 0. have hinner_zero : (μ[μ[h' | S.σ_AZUX] | S.σ_AZX]) =ᵐ[μ.restrict s] 0 := h_tower_s.symm.trans hh'_AZX_zero -- 1_s · μ[μ[h'|σ_AZUX]|σ_AZX] =ᵐ 0 globally. have hind_inner_zero : s.indicator (μ[μ[h' | S.σ_AZUX] | S.σ_AZX]) =ᵐ[μ] 0 := by simpa using indicator_aeEq_of_aeEq_restrict hs_meas hinner_zero -- So 1_s · μ[g_a∘UX | σ_AZX] =ᵐ 0, hence the goal. have hind_g_zero : s.indicator (μ[fun ω => g_a (S.UX ω) | S.σ_AZX]) =ᵐ[μ] 0 := hind_CE.symm.trans hind_inner_zero rw [EventuallyEq, ae_restrict_iff' hs_meas] -- … truncated; follow the source link for the rest …

theorem ate_proximal (HA : Assumptions S μ) (hAY : S.Avar.v ≠ S.Yvar.v) : ∫ ω, S.YofA true ω ∂μ - ∫ ω, S.YofA false ω ∂μ = ∫ ω, HA.h (true, S.W ω, S.X ω) ∂μ - ∫ ω, HA.h (false, S.W ω, S.X ω) ∂μ := by rw [Eofyofa_eq_Eh HA true hAY, Eofyofa_eq_Eh HA false hAY]