Estimation.DTR.Mean­Zero

theorem seqDR_mean_zero (S : DTREstimationSystem P δ γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOLongitudinalPathSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOLongitudinalPathSystem.factualY ω) ^ 2) P.μ) : (∫ z, S.ψ_seqDR z ∂(S.P_Z)) = 0 := by rw [DTREstimationSystem.P_Z] rw [MeasureTheory.integral_map S.measurable_factualZ.aemeasurable (S.measurable_ψ_seqDR).aestronglyMeasurable] exact seqDR_factualZ_integral_zero S h_overlap hA h_y2

lemma cond_exp_residual_zero_stage1 (S : DTREstimationSystem P δ γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOLongitudinalPathSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOLongitudinalPathSystem.factualY ω) ^ 2) P.μ) : (S.toPOLongitudinalPathSystem.historyBundle 1 (by decide)).condExpGiven (fun ω => (S.toPOLongitudinalPathSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * ((S.toPOLongitudinalPathSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω * (S.toPOLongitudinalPathSystem.factualY ω - S.μ₁_val (S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)))) P.μ =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by let B1 := S.toPOLongitudinalPathSystem.historyBundle 1 (by decide) let I0 : P.Ω → ℝ := (S.toPOLongitudinalPathSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) let I1 : P.Ω → ℝ := (S.toPOLongitudinalPathSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) let Y : P.Ω → ℝ := S.toPOLongitudinalPathSystem.Y_of S.dbar let Yf : P.Ω → ℝ := S.toPOLongitudinalPathSystem.factualY let M1 : P.Ω → ℝ := fun ω => S.μ₁_val (S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) have hY_int : Integrable Y P.μ := by simpa [Y] using hA.integrable_Y S.dbar have hYf_int : Integrable Yf P.μ := by simpa [Yf] using hA.integrable_factualY have hI0_int : Integrable I0 P.μ := by fun_prop have hI1_int : Integrable I1 P.μ := by fun_prop have hM1_int : Integrable M1 P.μ := by have hM1_L2 : MemLp M1 2 P.μ := by simpa [M1] using (S.stageOneReg_memLp h_overlap h_y2).ae_eq (S.μ₁_val_comp_eq_stageOneReg).symm exact hM1_L2.integrable (by norm_num) have hM1_meas : Measurable M1 := by fun_prop have hI1Y_int : Integrable (fun ω => I1 ω * Y ω) P.μ := by fun_prop have hI1Yf_int : Integrable (fun ω => I1 ω * Yf ω) P.μ := by fun_prop have hI1M1_int : Integrable (fun ω => I1 ω * M1 ω) P.μ := by fun_prop have hI0I1Y_int : Integrable (fun ω => I0 ω * (I1 ω * Y ω)) P.μ := by fun_prop have hI0I1Yf_int : Integrable (fun ω => I0 ω * (I1 ω * Yf ω)) P.μ := by fun_prop have hI0I1M1_int : Integrable (fun ω => I0 ω * (I1 ω * M1 ω)) P.μ := by fun_prop have hres_eq : (fun ω => I0 ω * (I1 ω * (Yf ω - M1 ω))) = (fun ω => I0 ω * (I1 ω * Yf ω) - I0 ω * (I1 ω * M1 ω)) := by funext ω ring have hsub : B1.condExpGiven (fun ω => I0 ω * (I1 ω * Yf ω) - I0 ω * (I1 ω * M1 ω)) P.μ =ᵐ[P.μ] B1.condExpGiven (fun ω => I0 ω * (I1 ω * Yf ω)) P.μ - B1.condExpGiven (fun ω => I0 ω * (I1 ω * M1 ω)) P.μ := by condexp_linearity have hConsistency : (fun ω => Yf ω * S.toPOLongitudinalPathSystem.indD S.dbar 2 ω) = (fun ω => Y ω * S.toPOLongitudinalPathSystem.indD S.dbar 2 ω) := by have h := POVar.factual_mul_indicator_eq_cf_mul_indicator hA.consistency S.toPOLongitudinalPathSystem.yVar (S.toPOLongitudinalPathSystem.regime S.dbar) (S.toPOLongitudinalPathSystem.yVar_notMem_regime S.dbar) {ω | ∀ i : Fin 2, S.toPOLongitudinalPathSystem.factualD i ω = S.dbar i} (S.toPOLongitudinalPathSystem.factualAgrees_regime S.dbar) have hrewrite : S.toPOLongitudinalPathSystem.indD S.dbar 2 = ({ω | ∀ i : Fin 2, S.toPOLongitudinalPathSystem.factualD i ω = S.dbar i}).indicator (fun _ => (1 : ℝ)) := by have h0 := S.toPOLongitudinalPathSystem.indD_eq_indicator_event S.dbar 2 (le_refl 2) have h_set_eq : ({ω | ∀ i : Fin 2, i.val < 2 → S.toPOLongitudinalPathSystem.factualD i ω = S.dbar i}) = {ω | ∀ i : Fin 2, S.toPOLongitudinalPathSystem.factualD i ω = S.dbar i} := by ext ω refine ⟨fun hω i => hω i i.isLt, fun hω i _ => hω i⟩ rw [h0, h_set_eq] change (fun ω => S.toPOLongitudinalPathSystem.factualY ω * S.toPOLongitudinalPathSystem.indD S.dbar 2 ω) = (fun ω => S.toPOLongitudinalPathSystem.Y_of S.dbar ω * S.toPOLongitudinalPathSystem.indD S.dbar 2 ω) rw [hrewrite] exact h have hIndD2_factor : S.toPOLongitudinalPathSystem.indD S.dbar 2 = fun ω => I0 ω * I1 ω := by funext ω have hsplit1 := congr_fun (S.toPOLongitudinalPathSystem.indD_factor_split S.dbar 1 (by decide)) ω have hsplit0 := congr_fun (S.toPOLongitudinalPathSystem.indD_factor_split S.dbar 0 (by decide)) ω rw [hsplit1, hsplit0] have hzero : S.toPOLongitudinalPathSystem.indD S.dbar 0 ω = 1 := rfl rw [hzero] ring have hFact_to_cf : (fun ω => I0 ω * (I1 ω * Yf ω)) =ᵐ[P.μ] (fun ω => I0 ω * (I1 ω * Y ω)) := by exact Filter.Eventually.of_forall (fun ω => by have hc := congr_fun hConsistency ω rw [hIndD2_factor] at hc change Yf ω * (I0 ω * I1 ω) = Y ω * (I0 ω * I1 ω) at hc nlinarith [hc]) have hCE_fact_to_cf : B1.condExpGiven (fun ω => I0 ω * (I1 ω * Yf ω)) P.μ =ᵐ[P.μ] B1.condExpGiven (fun ω => I0 ω * (I1 ω * Y ω)) P.μ := B1.condExpGiven_congr_ae hFact_to_cf have hI0_sm_B1 : StronglyMeasurable[B1.sigma] I0 := by fun_prop have hM1_sm_B1 : StronglyMeasurable[B1.sigma] M1 := by fun_prop have hI0M1_sm_B1 : StronglyMeasurable[B1.sigma] (fun ω => I0 ω * M1 ω) := by fun_prop have hcfY_n : (S.toPOLongitudinalPathSystem.cfYBundle S.dbar).n = 1 := rfl let i0 : Fin (S.toPOLongitudinalPathSystem.cfYBundle S.dbar).n := ⟨0, by rw [hcfY_n]; exact Nat.one_pos⟩ let ψ : (∀ i : Fin (S.toPOLongitudinalPathSystem.cfYBundle S.dbar).n, (S.toPOLongitudinalPathSystem.cfYBundle S.dbar).type i) → ℝ := fun f => (f i0 : ℝ) have hψ_meas : Measurable ψ := by fun_prop have hYof_eq_proj : S.toPOLongitudinalPathSystem.Y_of S.dbar = ψ ∘ (S.toPOLongitudinalPathSystem.cfYBundle S.dbar).jointValue := by funext ω rfl have hCI : CondIndepFun B1.sigma B1.sigma_le (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩) Y P.μ := by have hproj := (hA.exch S.dbar ⟨1, by decide⟩).project (ψ := ψ) hψ_meas change CondIndepFun B1.sigma B1.sigma_le (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩) (S.toPOLongitudinalPathSystem.Y_of S.dbar) P.μ rw [hYof_eq_proj] exact hproj let u : δ → ℝ := ({S.dbar ⟨1, by decide⟩} : Set δ).indicator (fun _ => (1 : ℝ)) have hu_meas : Measurable u := by fun_prop (disch := measurability) have hu_eq : (fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω)) = I1 := by funext ω by_cases h : S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω = S.dbar ⟨1, by decide⟩ · have h1 : S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω ∈ ({S.dbar ⟨1, by decide⟩} : Set δ) := h have h2 : ω ∈ (S.toPOLongitudinalPathSystem.dVar ⟨1, by decide⟩).event (S.dbar ⟨1, by decide⟩) := h rw [show u (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω) = (1 : ℝ) from Set.indicator_of_mem h1 _, show I1 ω = (1 : ℝ) from by simpa [I1] using (S.toPOLongitudinalPathSystem.dVar ⟨1, by decide⟩).indicator_apply_eq_one h2] · have h1 : S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω ∉ ({S.dbar ⟨1, by decide⟩} : Set δ) := h have h2 : ω ∉ (S.toPOLongitudinalPathSystem.dVar ⟨1, by decide⟩).event (S.dbar ⟨1, by decide⟩) := h rw [show u (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω) = (0 : ℝ) from Set.indicator_of_notMem h1 _, show I1 ω = (0 : ℝ) from by simpa [I1] using (S.toPOLongitudinalPathSystem.dVar ⟨1, by decide⟩).indicator_apply_eq_zero h2] have hfact : P.μ[fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω) * Y ω | B1.sigma] =ᵐ[P.μ] P.μ[fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω) | B1.sigma] * P.μ[Y | B1.sigma] := condExp_mul_of_condIndep (μ := P.μ) (m := B1.sigma) B1.sigma_le (f := S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩) (g := Y) (S.toPOLongitudinalPathSystem.measurable_factualD ⟨1, by decide⟩) (by simpa [Y] using S.toPOLongitudinalPathSystem.measurable_Y_of S.dbar) hCI (u := u) (v := id) hu_meas measurable_id (by rw [hu_eq]; exact hI1_int) hY_int (by have heq : (fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω) * Y ω) = (fun ω => I1 ω * Y ω) := by funext ω rw [congr_fun hu_eq ω] change Integrable (fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω) * Y ω) P.μ rw [heq] exact hI1Y_int) have hExch : B1.condExpGiven (fun ω => I1 ω * Y ω) P.μ =ᵐ[P.μ] (fun ω => B1.condExpGiven I1 P.μ ω * B1.condExpGiven Y P.μ ω) := by unfold POCFBundle.condExpGiven have hprod_rw : (fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω) * Y ω) = (fun ω => I1 ω * Y ω) := by funext ω rw [congr_fun hu_eq ω] rw [hprod_rw, hu_eq] at hfact filter_upwards [hfact] with ω hω simpa [Pi.mul_apply] using hω have hpull_I0Y := B1.condExpGiven_mul_of_stronglyMeasurable_left (f := I0) (g := fun ω => I1 ω * Y ω) hI0_sm_B1 hI0I1Y_int hI1Y_int have hCE_fact : B1.condExpGiven (fun ω => I0 ω * (I1 ω * Yf ω)) P.μ =ᵐ[P.μ] (fun ω => I0 ω * (S.e₁_val (S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) * M1 ω)) := by refine hCE_fact_to_cf.trans ?_ have hI0_eq_indD : I0 = S.toPOLongitudinalPathSystem.indD S.dbar 1 := by funext ω have hsplit := congr_fun (S.toPOLongitudinalPathSystem.indD_factor_split S.dbar 0 (by decide)) ω simp [I0, POLongitudinalPathSystem.indD] at hsplit ⊢ filter_upwards [hpull_I0Y, hExch, S.e₁_compat, S.indD_mul_μ₁_val_comp_eq hA] with ω hp hE he hμ have hp' : B1.condExpGiven (fun ω => I0 ω * (I1 ω * Y ω)) P.μ ω = I0 ω * B1.condExpGiven (fun ω => I1 ω * Y ω) P.μ ω := by exact hp have hμ_local : I0 ω * M1 ω = I0 ω * B1.condExpGiven Y P.μ ω := by have hμ' : S.toPOLongitudinalPathSystem.indD S.dbar 1 ω * M1 ω = S.toPOLongitudinalPathSystem.indD S.dbar 1 ω * B1.condExpGiven Y P.μ ω := hμ rw [hI0_eq_indD] exact hμ' rw [hp', hE, he] calc I0 ω * (S.e₁_val (S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) * B1.condExpGiven Y P.μ ω) -- … truncated; follow the source link for the rest …

lemma cond_exp_residual_zero_stage0 (S : DTREstimationSystem P δ γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOLongitudinalPathSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOLongitudinalPathSystem.factualY ω) ^ 2) P.μ) : (S.toPOLongitudinalPathSystem.historyBundle 0 (by decide)).condExpGiven (fun ω => (S.toPOLongitudinalPathSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * (S.μ₁_val (S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) - S.μ₀_val (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))) P.μ =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by let B0 := S.toPOLongitudinalPathSystem.historyBundle 0 (by decide) let B1 := S.toPOLongitudinalPathSystem.historyBundle 1 (by decide) let I0 : P.Ω → ℝ := (S.toPOLongitudinalPathSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) let Y : P.Ω → ℝ := S.toPOLongitudinalPathSystem.Y_of S.dbar let M0 : P.Ω → ℝ := fun ω => S.μ₀_val (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) let M1 : P.Ω → ℝ := fun ω => S.μ₁_val (S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) have hY_int : Integrable Y P.μ := by simpa [Y] using hA.integrable_Y S.dbar have hI0_int : Integrable I0 P.μ := by fun_prop have hI0Y_int : Integrable (fun ω => I0 ω * Y ω) P.μ := by fun_prop have hM0_int : Integrable M0 P.μ := by exact (B0.integrable_condExpGiven (S.toPOLongitudinalPathSystem.Y_of S.dbar)).congr (by simpa [B0, M0] using S.μ₀_compat hA) have hM1_int : Integrable M1 P.μ := by have hM1_L2 : MemLp M1 2 P.μ := by simpa [M1] using (S.stageOneReg_memLp h_overlap h_y2).ae_eq (S.μ₁_val_comp_eq_stageOneReg).symm exact hM1_L2.integrable (by norm_num) have hM0_meas : Measurable M0 := by fun_prop have hM1_meas : Measurable M1 := by fun_prop have hI0M0_int : Integrable (fun ω => I0 ω * M0 ω) P.μ := by fun_prop have hI0M1_int : Integrable (fun ω => I0 ω * M1 ω) P.μ := by fun_prop have hres_eq : (fun ω => I0 ω * (M1 ω - M0 ω)) = (fun ω => I0 ω * M1 ω - I0 ω * M0 ω) := by funext ω ring have hsub : B0.condExpGiven (fun ω => I0 ω * M1 ω - I0 ω * M0 ω) P.μ =ᵐ[P.μ] B0.condExpGiven (fun ω => I0 ω * M1 ω) P.μ - B0.condExpGiven (fun ω => I0 ω * M0 ω) P.μ := by condexp_linearity have hI0_sm_B1 : StronglyMeasurable[B1.sigma] I0 := by fun_prop have hrev_B1 : (fun ω => I0 ω * M1 ω) =ᵐ[P.μ] B1.condExpGiven (fun ω => I0 ω * Y ω) P.μ := by have hI0_eq_indD : I0 = S.toPOLongitudinalPathSystem.indD S.dbar 1 := by funext ω have hsplit := congr_fun (S.toPOLongitudinalPathSystem.indD_factor_split S.dbar 0 (by decide)) ω simp [I0, POLongitudinalPathSystem.indD] at hsplit ⊢ have hpull := B1.condExpGiven_mul_of_stronglyMeasurable_left (f := I0) (g := Y) hI0_sm_B1 hI0Y_int hY_int filter_upwards [hpull, S.indD_mul_μ₁_val_comp_eq hA] with ω hp hμ1 have hp' : B1.condExpGiven (fun ω => I0 ω * Y ω) P.μ ω = I0 ω * B1.condExpGiven Y P.μ ω := by exact hp have hμ1_local : I0 ω * M1 ω = I0 ω * B1.condExpGiven Y P.μ ω := by have hμ1' : S.toPOLongitudinalPathSystem.indD S.dbar 1 ω * M1 ω = S.toPOLongitudinalPathSystem.indD S.dbar 1 ω * B1.condExpGiven Y P.μ ω := hμ1 rw [hI0_eq_indD] exact hμ1' rw [hp'] exact hμ1_local haveI : IsFiniteMeasure (P.μ.trim B1.sigma_le) := isFiniteMeasure_trim _ have hB0_le_B1 : B0.sigma ≤ B1.sigma := by simpa [B0, B1] using S.toPOLongitudinalPathSystem.historyBundle_sigma_mono 0 1 (by decide) (by decide) have htower : B0.condExpGiven (B1.condExpGiven (fun ω => I0 ω * Y ω) P.μ) P.μ =ᵐ[P.μ] B0.condExpGiven (fun ω => I0 ω * Y ω) P.μ := by have h := B1.condExpGiven_tower_of_le (g := fun ω => I0 ω * Y ω) (μ := P.μ) (m := B0.sigma) hB0_le_B1 simpa [POCFBundle.condExpGiven] using h have hCE_I0M1_to_Y : B0.condExpGiven (fun ω => I0 ω * M1 ω) P.μ =ᵐ[P.μ] B0.condExpGiven (fun ω => I0 ω * Y ω) P.μ := by exact (B0.condExpGiven_congr_ae hrev_B1).trans htower have hcfY_n : (S.toPOLongitudinalPathSystem.cfYBundle S.dbar).n = 1 := rfl let i0 : Fin (S.toPOLongitudinalPathSystem.cfYBundle S.dbar).n := ⟨0, by rw [hcfY_n]; exact Nat.one_pos⟩ let ψ : (∀ i : Fin (S.toPOLongitudinalPathSystem.cfYBundle S.dbar).n, (S.toPOLongitudinalPathSystem.cfYBundle S.dbar).type i) → ℝ := fun f => (f i0 : ℝ) have hψ_meas : Measurable ψ := by fun_prop have hYof_eq_proj : S.toPOLongitudinalPathSystem.Y_of S.dbar = ψ ∘ (S.toPOLongitudinalPathSystem.cfYBundle S.dbar).jointValue := by funext ω rfl have hCI : CondIndepFun B0.sigma B0.sigma_le (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩) Y P.μ := by have hproj := (hA.exch S.dbar ⟨0, by decide⟩).project (ψ := ψ) hψ_meas change CondIndepFun B0.sigma B0.sigma_le (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩) (S.toPOLongitudinalPathSystem.Y_of S.dbar) P.μ rw [hYof_eq_proj] exact hproj let u : δ → ℝ := ({S.dbar ⟨0, by decide⟩} : Set δ).indicator (fun _ => (1 : ℝ)) have hu_meas : Measurable u := by fun_prop (disch := measurability) have hu_eq : (fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω)) = I0 := by funext ω by_cases h : S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω = S.dbar ⟨0, by decide⟩ · have h1 : S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω ∈ ({S.dbar ⟨0, by decide⟩} : Set δ) := h have h2 : ω ∈ (S.toPOLongitudinalPathSystem.dVar ⟨0, by decide⟩).event (S.dbar ⟨0, by decide⟩) := h rw [show u (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω) = (1 : ℝ) from Set.indicator_of_mem h1 _, show I0 ω = (1 : ℝ) from by simpa [I0] using (S.toPOLongitudinalPathSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_one h2] · have h1 : S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω ∉ ({S.dbar ⟨0, by decide⟩} : Set δ) := h have h2 : ω ∉ (S.toPOLongitudinalPathSystem.dVar ⟨0, by decide⟩).event (S.dbar ⟨0, by decide⟩) := h rw [show u (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω) = (0 : ℝ) from Set.indicator_of_notMem h1 _, show I0 ω = (0 : ℝ) from by simpa [I0] using (S.toPOLongitudinalPathSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_zero h2] have hfact : P.μ[fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω) * Y ω | B0.sigma] =ᵐ[P.μ] P.μ[fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω) | B0.sigma] * P.μ[Y | B0.sigma] := condExp_mul_of_condIndep (μ := P.μ) (m := B0.sigma) B0.sigma_le (f := S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩) (g := Y) (S.toPOLongitudinalPathSystem.measurable_factualD ⟨0, by decide⟩) (by simpa [Y] using S.toPOLongitudinalPathSystem.measurable_Y_of S.dbar) hCI (u := u) (v := id) hu_meas measurable_id (by rw [hu_eq]; exact hI0_int) hY_int (by change Integrable (fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω) * Y ω) P.μ have heq : (fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω) * Y ω) = (fun ω => I0 ω * Y ω) := by funext ω rw [congr_fun hu_eq ω] rw [heq] exact hI0Y_int) have hExch : B0.condExpGiven (fun ω => I0 ω * Y ω) P.μ =ᵐ[P.μ] (fun ω => B0.condExpGiven I0 P.μ ω * B0.condExpGiven Y P.μ ω) := by unfold POCFBundle.condExpGiven have hprod_rw : (fun ω => u (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω) * Y ω) = (fun ω => I0 ω * Y ω) := by funext ω rw [congr_fun hu_eq ω] rw [hprod_rw, hu_eq] at hfact filter_upwards [hfact] with ω hω simpa [Pi.mul_apply] using hω have hCE_I0M1 : B0.condExpGiven (fun ω => I0 ω * M1 ω) P.μ =ᵐ[P.μ] (fun ω => S.e₀_val (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) * S.μ₀_val (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)) := by refine hCE_I0M1_to_Y.trans ?_ filter_upwards [hExch, S.e₀_compat, S.μ₀_compat hA] with ω hE he hμ rw [hE, he, hμ] have hM0_sm_B0 : StronglyMeasurable[B0.sigma] M0 := by fun_prop have hpull_M0 := B0.condExpGiven_mul_of_stronglyMeasurable_right (f := I0) (g := M0) hM0_sm_B0 hI0M0_int hI0_int have hCE_I0M0 : B0.condExpGiven (fun ω => I0 ω * M0 ω) P.μ =ᵐ[P.μ] (fun ω => S.e₀_val (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) * S.μ₀_val (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)) := by filter_upwards [hpull_M0, S.e₀_compat] with ω hp he have hp' : B0.condExpGiven (fun ω => I0 ω * M0 ω) P.μ ω = B0.condExpGiven I0 P.μ ω * M0 ω := by exact hp rw [hp', he] rw [show (fun ω => (S.toPOLongitudinalPathSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * (S.μ₁_val (S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω, S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) - S.μ₀_val (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))) = (fun ω => I0 ω * (M1 ω - M0 ω)) by rfl] rw [hres_eq] refine hsub.trans ?_ filter_upwards [hCE_I0M1, hCE_I0M0] with ω h1 h0 rw [Pi.sub_apply, h1, h0] ring