PO.ID.Exact.DTR

@[fun_prop] lemma measurable_indD (S : PODTRSystem P n δ γ) (dbar : Fin n → δ) : ∀ k : ℕ, Measurable (S.indD dbar k) | 0 => measurable_const | k + 1 => by unfold indD by_cases hk : k < n · simp only [hk, ↓reduceDIte] exact (S.measurable_indD dbar k).mul ((S.dVar ⟨k, hk⟩).measurable_indicator (dbar ⟨k, hk⟩) (measurableSet_singleton _)) · simp only [hk, ↓reduceDIte] exact S.measurable_indD dbar k

@[fun_prop] lemma measurable_hb_step_proj (S : PODTRSystem P n δ γ) (k : ℕ) (h : k + 1 < n) : Measurable (S.hb_step_proj k h) := by apply measurable_pi_lambda intro j -- Instance search no longer unfolds `historyBundle (k+1)` to see that its -- index type is `Fin (… + 1 + 1)`, so supply the coordinate measurable-space -- family explicitly. let _ : ∀ i : Fin ((S.historyBundle k (lt_of_succ_lt h)).n + 1 + 1), MeasurableSpace ((S.historyBundle (k + 1) h).type i) := fun i => (S.historyBundle (k + 1) h).inst i exact measurable_pi_apply j.succ.succ

lemma hb_jointValue_step_eq (S : PODTRSystem P n δ γ) (k : ℕ) (h : k + 1 < n) : (S.historyBundle k (lt_of_succ_lt h)).jointValue = S.hb_step_proj k h ∘ (S.historyBundle (k+1) h).jointValue := by funext ω j rfl

lemma historyBundle_sigma_mono_step (S : PODTRSystem P n δ γ) (k : ℕ) (h : k + 1 < n) : (S.historyBundle k (lt_of_succ_lt h)).sigma ≤ (S.historyBundle (k+1) h).sigma := by change comap (S.historyBundle k (lt_of_succ_lt h)).jointValue inferInstance ≤ comap (S.historyBundle (k+1) h).jointValue inferInstance rw [S.hb_jointValue_step_eq k h, ← MeasurableSpace.comap_comp] exact comap_mono (S.measurable_hb_step_proj k h).comap_le

lemma historyBundle_sigma_mono (S : PODTRSystem P n δ γ) (j k : ℕ) (hjk : j ≤ k) (hk : k < n) : (S.historyBundle j (lt_of_le_of_lt hjk hk)).sigma ≤ (S.historyBundle k hk).sigma := by induction k with | zero => interval_cases j exact le_refl _ | succ k ih => rcases Nat.lt_or_ge j (k + 1) with hlt | hge · have hjk' : j ≤ k := Nat.lt_succ_iff.mp hlt have hkn : k < n := lt_of_succ_lt hk exact (ih hjk' hkn).trans (S.historyBundle_sigma_mono_step k hk) · have hjeq : j = k + 1 := le_antisymm hjk hge subst hjeq exact le_refl _

lemma indD_eq_zero_or_one (S : PODTRSystem P n δ γ) (dbar : Fin n → δ) : ∀ (k : ℕ) (ω : P.Ω), S.indD dbar k ω = 0 ∨ S.indD dbar k ω = 1 | 0, _ => inr rfl | k + 1, ω => by unfold indD by_cases hk : k < n · simp only [hk, ↓reduceDIte] rcases indD_eq_zero_or_one S dbar k ω with h | h · left; simp [h] · rcases (S.dVar ⟨k, hk⟩).indicator_eq_one_or_zero (dbar ⟨k, hk⟩) ω with h' | h' · right; simp [h, h'] · left; simp [h, h'] · simp only [hk, ↓reduceDIte] exact indD_eq_zero_or_one S dbar k ω

@[fun_prop] lemma indD_integrable (S : PODTRSystem P n δ γ) (dbar : Fin n → δ) (k : ℕ) [IsFiniteMeasure P.μ] : Integrable (S.indD dbar k) P.μ := by refine Integrable.of_bound (S.measurable_indD dbar k).aestronglyMeasurable 1 (Filter.Eventually.of_forall ?_) intro ω rcases S.indD_eq_zero_or_one dbar k ω with h | h <;> simp [h]

lemma indD_eq_indicator_event (S : PODTRSystem P n δ γ) (dbar : Fin n → δ) : ∀ (k : ℕ) (_ : k ≤ n), S.indD dbar k = ({ω | ∀ i : Fin n, i.val < k → S.factualD i ω = dbar i}).indicator (fun _ => (1 : ℝ)) | 0, _ => by funext ω simp [indD] | k + 1, h => by have hk : k < n := h funext ω have hrec := indD_eq_indicator_event S dbar k (le_of_lt hk) -- Rewrite indD dbar (k+1) ω in terms of indD dbar k ω * indicator. have hstep : S.indD dbar (k+1) ω = S.indD dbar k ω * (S.dVar ⟨k, hk⟩).indicator (dbar ⟨k, hk⟩) ω := by change (if h' : k < n then S.indD dbar k ω * (S.dVar ⟨k, h'⟩).indicator (dbar ⟨k, h'⟩) ω else S.indD dbar k ω) = _ simp [hk] rw [hstep] rw [show S.indD dbar k = _ from hrec] by_cases hall : ∀ i : Fin n, i.val < k + 1 → S.factualD i ω = dbar i · have hprefix : ∀ i : Fin n, i.val < k → S.factualD i ω = dbar i := fun i hi => hall i (Nat.lt_succ_of_lt hi) have hnew : S.factualD ⟨k, hk⟩ ω = dbar ⟨k, hk⟩ := hall ⟨k, hk⟩ (Nat.lt_succ_self _) have hmem : ω ∈ {ω | ∀ i : Fin n, i.val < k → S.factualD i ω = dbar i} := hprefix have hmem' : ω ∈ {ω | ∀ i : Fin n, i.val < k + 1 → S.factualD i ω = dbar i} := hall rw [Set.indicator_of_mem hmem, Set.indicator_of_mem hmem'] rw [(S.dVar ⟨k, hk⟩).indicator_apply_eq_one hnew] ring · have hnmem' : ω ∉ {ω | ∀ i : Fin n, i.val < k + 1 → S.factualD i ω = dbar i} := hall rw [Set.indicator_of_notMem hnmem'] by_cases hprefix : ∀ i : Fin n, i.val < k → S.factualD i ω = dbar i · have hnew : S.factualD ⟨k, hk⟩ ω ≠ dbar ⟨k, hk⟩ := by intro hn apply hall intro i hi rcases Nat.lt_succ_iff_lt_or_eq.mp hi with hi' | hi' · exact hprefix i hi' · have : i = ⟨k, hk⟩ := Fin.ext (by simpa using hi') rw [this]; exact hn have hmem : ω ∈ {ω | ∀ i : Fin n, i.val < k → S.factualD i ω = dbar i} := hprefix rw [Set.indicator_of_mem hmem] rw [(S.dVar ⟨k, hk⟩).indicator_apply_eq_zero hnew] ring · have hnmem : ω ∉ {ω | ∀ i : Fin n, i.val < k → S.factualD i ω = dbar i} := hprefix rw [Set.indicator_of_notMem hnmem] ring

lemma measurable_factualS_sigma_history (S : PODTRSystem P n δ γ) (m : ℕ) (hm : m < n) (k' : Fin n) (hk' : k'.val ≤ m) : Measurable[(S.historyBundle m hm).sigma] (S.factualS k') := by induction m with | zero => have hkv : k'.val = 0 := Nat.le_zero.mp hk' have hkeq : k' = ⟨0, hm⟩ := Fin.ext (by simp [hkv]) subst hkeq intro s hs refine ⟨(fun f : ∀ i, (S.historyBundle 0 hm).type i => f ⟨0, zero_lt_succ 0⟩) ⁻¹' s, ?_, ?_⟩ · exact measurable_pi_apply _ hs · rfl | succ m ih => rcases Nat.lt_or_ge k'.val (m + 1) with hlt | hge · have hkm : k'.val ≤ m := Nat.lt_succ_iff.mp hlt have hmn : m < n := lt_of_succ_lt hm have hrec := ih hmn hkm -- Upgrade via σ-algebra monotonicity. intro s hs exact S.historyBundle_sigma_mono_step m hm _ (hrec hs) · have hkeq : k'.val = m + 1 := le_antisymm hk' hge have hkfin : k' = ⟨m + 1, hm⟩ := Fin.ext hkeq subst hkfin intro s hs refine ⟨(fun f : ∀ i, (S.historyBundle (m+1) hm).type i => f ⟨0, zero_lt_succ _⟩) ⁻¹' s, ?_, ?_⟩ · exact measurable_pi_apply _ hs · rfl

lemma measurable_factualD_sigma_history (S : PODTRSystem P n δ γ) (m : ℕ) (hm : m < n) (k' : Fin n) (hk' : k'.val < m) : Measurable[(S.historyBundle m hm).sigma] (S.factualD k') := by induction m with | zero => exact absurd hk' (Nat.not_lt_zero _) | succ m ih => rcases Nat.lt_or_ge k'.val m with hlt | hge · have hmn : m < n := Nat.lt_of_succ_lt hm intro s hs exact S.historyBundle_sigma_mono_step m hm _ ((ih hmn hlt) hs) · have hkeq : k'.val = m := by omega have hmlt : m < n := Nat.lt_of_succ_lt hm have hkfin : k' = ⟨m, hmlt⟩ := Fin.ext hkeq intro s hs -- index 1 in historyBundle (m+1) — use a Fin literal. let i1 : Fin ((S.historyBundle (m+1) hm).n) := ⟨1, by -- The length of historyBundle (m+1) is (historyBundle m).n + 1 + 1 ≥ 2. change 1 < (S.historyBundle m hmlt).n + 1 + 1 omega⟩ refine ⟨(fun f : ∀ i, (S.historyBundle (m+1) hm).type i => f i1) ⁻¹' s, ?_, ?_⟩ · exact measurable_pi_apply _ hs · rw [hkfin]; rfl

lemma stronglyMeasurable_indicator_dVar_sigma_history (S : PODTRSystem P n δ γ) (m : ℕ) (hm : m < n) (k' : Fin n) (hk' : k'.val < m) (x : δ) : StronglyMeasurable[(S.historyBundle m hm).sigma] ((S.dVar k').indicator x) := by have hfmeas := S.measurable_factualD_sigma_history m hm k' hk' have hev : MeasurableSet[(S.historyBundle m hm).sigma] ((S.dVar k').event x) := hfmeas (MeasurableSet.singleton x) have hmeas : Measurable[(S.historyBundle m hm).sigma] ((S.dVar k').indicator x) := by unfold POVar.indicator exact measurable_const.indicator hev exact hmeas.stronglyMeasurable

@[fun_prop] lemma measurable_factualS_sigma_history_last (S : PODTRSystem P n δ γ) (m : ℕ) (hm : m < n) : Measurable[(S.historyBundle m hm).sigma] (S.factualS ⟨m, hm⟩) := S.measurable_factualS_sigma_history m hm ⟨m, hm⟩ (le_refl m)

@[fun_prop] lemma measurable_factualS_sigma_history_pred (S : PODTRSystem P n δ γ) (m : ℕ) (hm : m + 1 < n) : Measurable[(S.historyBundle (m + 1) hm).sigma] (S.factualS ⟨m, lt_of_succ_lt hm⟩) := S.measurable_factualS_sigma_history (m + 1) hm ⟨m, lt_of_succ_lt hm⟩ (Nat.le_succ m)

@[fun_prop] lemma measurable_factualD_sigma_history_last (S : PODTRSystem P n δ γ) (m : ℕ) (hm : m + 1 < n) : Measurable[(S.historyBundle (m + 1) hm).sigma] (S.factualD ⟨m, lt_of_succ_lt hm⟩) := S.measurable_factualD_sigma_history (m + 1) hm ⟨m, lt_of_succ_lt hm⟩ (Nat.lt_succ_self m)

@[fun_prop] lemma stronglyMeasurable_indicator_dVar_sigma_history_last (S : PODTRSystem P n δ γ) (m : ℕ) (hm : m + 1 < n) (x : δ) : StronglyMeasurable[(S.historyBundle (m + 1) hm).sigma] ((S.dVar ⟨m, lt_of_succ_lt hm⟩).indicator x) := S.stronglyMeasurable_indicator_dVar_sigma_history (m + 1) hm ⟨m, lt_of_succ_lt hm⟩ (Nat.lt_succ_self m) x

lemma stronglyMeasurable_indD_sigma_history (S : PODTRSystem P n δ γ) (m : ℕ) (hm : m < n) (dbar : Fin n → δ) : ∀ (m' : ℕ) (_ : m' ≤ m), StronglyMeasurable[(S.historyBundle m hm).sigma] (S.indD dbar m') | 0, _ => by unfold indD exact stronglyMeasurable_const | m' + 1, h => by have hm' : m' < n := lt_of_lt_of_le h (le_of_lt hm) have hrec := stronglyMeasurable_indD_sigma_history S m hm dbar m' (le_of_succ_le h) have hmlt : m' < m := h have hind := S.stronglyMeasurable_indicator_dVar_sigma_history m hm ⟨m', hm'⟩ hmlt (dbar ⟨m', hm'⟩) -- `indD (m'+1) = indD m' * indicator`. have heq : S.indD dbar (m' + 1) = fun ω => S.indD dbar m' ω * (S.dVar ⟨m', hm'⟩).indicator (dbar ⟨m', hm'⟩) ω := S.indD_factor_split dbar m' hm' rw [heq] -- `StronglyMeasurable` closed under mul. exact hrec.mul hind

lemma factualAgrees_regimeUpTo (S : PODTRSystem P n δ γ) (dbar : Fin n → δ) : ∀ (k : ℕ) (h : k ≤ n) (ω : P.Ω), (∀ i : Fin n, i.val < k → S.factualD i ω = dbar i) → P.FactualAgrees (S.regimeUpTo dbar k h) ω | 0, _, ω, _ => by change P.FactualAgrees (S.regimeUpToAux dbar 0 (by exact zero_le n)).1 ω unfold regimeUpToAux exact POSystem.factualAgrees_empty ω | k + 1, h, ω, hall => by have hk : k < n := h have hprefix : ∀ i : Fin n, i.val < k → S.factualD i ω = dbar i := fun i hi => hall i (Nat.lt_succ_of_lt hi) have hnew : S.factualD ⟨k, hk⟩ ω = dbar ⟨k, hk⟩ := hall ⟨k, hk⟩ (Nat.lt_succ_self _) have hrec := factualAgrees_regimeUpTo S dbar k (le_of_lt hk) ω hprefix -- Unfold regimeUpTo at k+1 to a sqcup. change P.FactualAgrees (S.regimeUpToAux dbar (k+1) h).1 ω unfold regimeUpToAux simp only apply POSystem.factualAgrees_sqcup · exact (S.dVar ⟨k, hk⟩).factualAgrees_single (dbar ⟨k, hk⟩) hnew · -- hrec is about S.regimeUpTo dbar k _ = (S.regimeUpToAux dbar k _).1. exact hrec

lemma factualAgrees_regime (S : PODTRSystem P n δ γ) (dbar : Fin n → δ) : ∀ ω ∈ {ω | ∀ i : Fin n, S.factualD i ω = dbar i}, P.FactualAgrees (S.regime dbar) ω := by intro ω hω exact S.factualAgrees_regimeUpTo dbar n (le_refl n) ω (fun i _ => hω i)

lemma indD_mul_Y_integrable (S : PODTRSystem P n δ γ) (dbar : Fin n → δ) (k : ℕ) (hY : Integrable (S.Y_of dbar) P.μ) : Integrable (fun ω => S.indD dbar k ω * S.Y_of dbar ω) P.μ := by refine hY.mono ((S.measurable_indD dbar k).mul (S.measurable_Y_of dbar)).aestronglyMeasurable ?_ refine Filter.Eventually.of_forall (fun ω => ?_) rcases S.indD_eq_zero_or_one dbar k ω with h | h <;> simp [h]

@[fun_prop] lemma measurable_innerReg (S : PODTRSystem P n δ γ) (dbar : Fin n → δ) : ∀ j : ℕ, Measurable (S.innerReg dbar j) | 0 => by unfold innerReg by_cases hn : 0 < n · simp only [hn, ↓reduceDIte] set B := S.historyBundle (n-1) (sub_lt hn one_pos) have hN := (B.stronglyMeasurable_condExpGiven (μ := P.μ) (fun ω' => S.factualY ω' * S.indD dbar n ω')).measurable have hD := (B.stronglyMeasurable_condExpGiven (μ := P.μ) (S.indD dbar n)).measurable exact hN.div hD · simp only [hn, ↓reduceDIte] exact measurable_const | j + 1 => by unfold innerReg by_cases hj : j + 1 < n · simp only [hj, ↓reduceDIte] have hkk : n - j - 2 < n := by omega set kFin : Fin n := ⟨n - j - 2, hkk⟩ set ind_k : P.Ω → ℝ := (S.dVar kFin).indicator (dbar kFin) set B := S.historyBundle (n - j - 2) hkk have hN := (B.stronglyMeasurable_condExpGiven (μ := P.μ) (fun ω' => S.innerReg dbar j ω' * ind_k ω')).measurable have hD := (B.stronglyMeasurable_condExpGiven (μ := P.μ) ind_k).measurable exact hN.div hD · simp only [hj, ↓reduceDIte] exact S.measurable_innerReg dbar j

lemma yVar_notMem_regime (S : PODTRSystem P n δ γ) (dbar : Fin n → δ) : S.yVar.v ∉ (S.regime dbar).target := by intro hmem have hmem' : S.yVar.v ∈ S.regimeTarget n := by rw [← S.regimeUpTo_target_eq dbar n (le_refl n)] exact hmem rcases (S.regimeTarget_mem_iff n (le_refl n) S.yVar.v).mp hmem' with ⟨i, _, heq⟩ exact (S.distinctDY i) heq.symm

theorem cdtr_step [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (S : PODTRSystem P n δ γ) (hA : S.Assumptions) (dbar : Fin n → δ) (j : ℕ) (hj : j + 1 < n) (hk : n - j - 2 < n) (hIH_int : Integrable (S.innerReg dbar j) P.μ) (IH : (fun ω => S.innerReg dbar j ω * S.indD dbar (n - j - 1) ω) =ᵐ[P.μ] (fun ω => S.indD dbar (n - j - 1) ω * (S.historyBundle (n - j - 1) (by omega)).condExpGiven (S.Y_of dbar) P.μ ω)) : (fun ω => S.innerReg dbar (j + 1) ω * S.indD dbar (n - j - 2) ω) =ᵐ[P.μ] (fun ω => S.indD dbar (n - j - 2) ω * (S.historyBundle (n - j - 2) hk).condExpGiven (S.Y_of dbar) P.μ ω) := by -- Abbreviations. set k : ℕ := n - j - 2 with hk_def have hk1 : k + 1 < n := by omega set kFin : Fin n := ⟨k, hk⟩ with hkFin_def set ind_k : P.Ω → ℝ := (S.dVar kFin).indicator (dbar kFin) with hind_k_def -- σ-algebra inclusion σ_k ≤ σ_{k+1}. have hσk_le : (S.historyBundle k hk).sigma ≤ (inferInstance : MeasurableSpace P.Ω) := (S.historyBundle k hk).sigma_le have hσ_step : (S.historyBundle k hk).sigma ≤ (S.historyBundle (k+1) hk1).sigma := S.historyBundle_sigma_mono_step k hk1 -- Strong-measurability of `indD k` (σ_k) and `ind_k` (σ_{k+1}). have hindDk_sm : StronglyMeasurable[(S.historyBundle k hk).sigma] (S.indD dbar k) := S.stronglyMeasurable_indD_sigma_history k hk dbar k (le_refl k) have hindk_sm_k1 : StronglyMeasurable[(S.historyBundle (k+1) hk1).sigma] ind_k := S.stronglyMeasurable_indicator_dVar_sigma_history (k+1) hk1 kFin (Nat.lt_succ_self _) (dbar kFin) -- Integrability prerequisites. have hYof_int : Integrable (S.Y_of dbar) P.μ := hA.integrable_Y dbar have hindk_int : Integrable ind_k P.μ := (S.dVar kFin).integrable_indicator (dbar kFin) (measurableSet_singleton _) have hindDk1_int : Integrable (S.indD dbar (k+1)) P.μ := S.indD_integrable dbar (k+1) have hYof_indk_int : Integrable (fun ω => S.Y_of dbar ω * ind_k ω) P.μ := by dsimp [ind_k] exact (S.dVar kFin).integrable_mul_indicator (dbar kFin) (measurableSet_singleton _) hYof_int have hindk_Yof_int : Integrable (fun ω => ind_k ω * S.Y_of dbar ω) P.μ := hYof_indk_int.congr (Filter.Eventually.of_forall (fun ω => by ring)) -- `n - j - 1 = k + 1`. have hk1_idx : n - j - 1 = k + 1 := by omega -- Pointwise factor split: indD (k+1) = indD k · ind_k. have hFactor : S.indD dbar (k+1) = fun ω => S.indD dbar k ω * ind_k ω := S.indD_factor_split dbar k hk -- Integrability of `innerReg j · indD (k+1)`: derived from IH RHS being integrable. have hCondExpY_k1_int : Integrable ((S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ) P.μ := (S.historyBundle (k+1) hk1).integrable_condExpGiven _ have hRHS_IH_int : Integrable (fun ω => S.indD dbar (k+1) ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω) P.μ := by refine hCondExpY_k1_int.mono ((S.measurable_indD dbar (k+1)).mul ((S.historyBundle (k+1) hk1).stronglyMeasurable_condExpGiven _).measurable ).aestronglyMeasurable ?_ refine Filter.Eventually.of_forall (fun ω => ?_) rcases S.indD_eq_zero_or_one dbar (k+1) ω with h | h <;> simp [h] -- Cast IH from `n - j - 1` to `k + 1`. have IH' : (fun ω => S.innerReg dbar j ω * S.indD dbar (k+1) ω) =ᵐ[P.μ] (fun ω => S.indD dbar (k+1) ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω) := by -- The indices `n - j - 1` and `k + 1` are equal (`hk1_idx`); rewrite via -- a heterogeneous-eq cast on the historyBundle. have hHB_eq : HEq ((S.historyBundle (n - j - 1) (by omega : n - j - 1 < n)).condExpGiven (S.Y_of dbar) P.μ) ((S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ) := by congr 1 simp [hk1_idx] have hHB_eq' : (S.historyBundle (n - j - 1) (by omega : n - j - 1 < n)).condExpGiven (S.Y_of dbar) P.μ = (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ := eq_of_heq hHB_eq have hindDeq : S.indD dbar (n - j - 1) = S.indD dbar (k + 1) := by rw [hk1_idx] have := IH rw [hindDeq] at this refine this.trans ?_ refine Filter.Eventually.of_forall (fun ω => ?_) rw [hHB_eq'] have hinnerReg_indD_int : Integrable (fun ω => S.innerReg dbar j ω * S.indD dbar (k+1) ω) P.μ := hRHS_IH_int.congr IH'.symm -- ====== Master identity ===================================================== -- Prove: μ[innerReg j · indD (k+1) | σ_k] =ᵐ -- indD k · μ[ind_k | σ_k] · μ[Y_of | σ_k]. -- Path: -- (a) condExpGiven_congr_ae of IH'. -- (b) Rewrite RHS integrand: indD (k+1) · μ[Y|σ_{k+1}] = indD k · (ind_k · μ[Y|σ_{k+1}]). -- (c) Pull indD k (σ_k-meas, bounded) out. -- (d) Reverse pullout of ind_k on σ_{k+1}. -- (e) Tower σ_k ≤ σ_{k+1}. -- (f) Stage-k exch. -- ============================================================================ -- (a) Apply σ_k-CE to both sides of IH'. have hStepA : (S.historyBundle k hk).condExpGiven (fun ω => S.innerReg dbar j ω * S.indD dbar (k+1) ω) P.μ =ᵐ[P.μ] (S.historyBundle k hk).condExpGiven (fun ω => S.indD dbar (k+1) ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω) P.μ := (S.historyBundle k hk).condExpGiven_congr_ae IH' -- (b) Rewrite: indD (k+1) · X = indD k · (ind_k · X). have hRewriteRHS : (fun ω => S.indD dbar (k+1) ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω) = (fun ω => S.indD dbar k ω * (ind_k ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω)) := by funext ω rw [show S.indD dbar (k+1) ω = S.indD dbar k ω * ind_k ω from congr_fun hFactor ω] ring -- (c) Pull indD k (σ_k-meas) out of σ_k-CE. have hindk_CE_int : Integrable (fun ω => ind_k ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω) P.μ := by dsimp [ind_k] have hmul := (S.dVar kFin).integrable_mul_indicator (dbar kFin) (measurableSet_singleton _) hCondExpY_k1_int exact hmul.congr (Filter.Eventually.of_forall (fun ω => by ring)) have hindDk_indk_CE_int : Integrable (S.indD dbar k * fun ω => ind_k ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω) P.μ := by have hrw : (S.indD dbar k * fun ω => ind_k ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω) = fun ω => S.indD dbar (k+1) ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω := by funext ω change S.indD dbar k ω * (ind_k ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω) = _ rw [show S.indD dbar (k+1) ω = S.indD dbar k ω * ind_k ω from congr_fun hFactor ω] ring rw [hrw]; exact hRHS_IH_int have hPullIndDk : (S.historyBundle k hk).condExpGiven (fun ω => S.indD dbar k ω * (ind_k ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω)) P.μ =ᵐ[P.μ] (fun ω => S.indD dbar k ω * (S.historyBundle k hk).condExpGiven (fun ω' => ind_k ω' * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω') P.μ ω) := by have hpull := (S.historyBundle k hk).condExpGiven_mul_of_stronglyMeasurable_left (f := S.indD dbar k) (g := fun ω => ind_k ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω) hindDk_sm hindDk_indk_CE_int hindk_CE_int filter_upwards [hpull] with ω hω exact hω -- (d) Reverse pullout of ind_k on σ_{k+1}. have hRevPull : (fun ω => ind_k ω * (S.historyBundle (k+1) hk1).condExpGiven (S.Y_of dbar) P.μ ω) =ᵐ[P.μ] (S.historyBundle (k+1) hk1).condExpGiven (fun ω => ind_k ω * S.Y_of dbar ω) P.μ := by have hfwd := (S.historyBundle (k+1) hk1).condExpGiven_mul_of_stronglyMeasurable_left (f := ind_k) (g := S.Y_of dbar) hindk_sm_k1 hindk_Yof_int hYof_int filter_upwards [hfwd] with ω hω exact hω.symm -- (e) Tower σ_k ≤ σ_{k+1}. haveI : IsFiniteMeasure (P.μ.trim (S.historyBundle (k+1) hk1).sigma_le) := isFiniteMeasure_trim _ have hTower : (S.historyBundle k hk).condExpGiven ((S.historyBundle (k+1) hk1).condExpGiven (fun ω => ind_k ω * S.Y_of dbar ω) P.μ) P.μ =ᵐ[P.μ] (S.historyBundle k hk).condExpGiven (fun ω => ind_k ω * S.Y_of dbar ω) P.μ := by have h := (S.historyBundle (k+1) hk1).condExpGiven_tower_of_le (g := fun ω => ind_k ω * S.Y_of dbar ω) (μ := P.μ) (m := (S.historyBundle k hk).sigma) hσ_step simpa [POCFBundle.condExpGiven] using h -- (f) Stage-k exchangeability. have hcfY_n : (S.cfYBundle dbar).n = 1 := rfl let i0 : Fin (S.cfYBundle dbar).n := ⟨0, by rw [hcfY_n]; exact Nat.one_pos⟩ let ψ : (∀ i : Fin (S.cfYBundle dbar).n, (S.cfYBundle dbar).type i) → ℝ := fun f => (f i0 : ℝ) have hψ_meas : Measurable ψ := by change Measurable (fun f : (∀ i, (S.cfYBundle dbar).type i) => (f i0 : ℝ)) exact measurable_pi_apply i0 have hYof_eq_proj : S.Y_of dbar = ψ ∘ (S.cfYBundle dbar).jointValue := by funext ω; rfl have hCI : CondIndepFun (S.historyBundle k hk).sigma hσk_le (S.factualD kFin) (S.Y_of dbar) P.μ := by have hproj := (hA.exch dbar kFin).project (ψ := ψ) hψ_meas rw [hYof_eq_proj]; exact hproj let u : δ → ℝ := ({dbar kFin} : Set δ).indicator (fun _ => (1 : ℝ)) have hu_meas : Measurable u := measurable_const.indicator (MeasurableSet.singleton _) have hu_eq : (fun ω => u (S.factualD kFin ω)) = ind_k := by funext ω show u (S.factualD kFin ω) = ind_k ω by_cases h : S.factualD kFin ω = dbar kFin · have h1 : S.factualD kFin ω ∈ ({dbar kFin} : Set δ) := h have h2 : ω ∈ (S.dVar kFin).event (dbar kFin) := h rw [show u (S.factualD kFin ω) = (1 : ℝ) from Set.indicator_of_mem h1 _, show ind_k ω = (1 : ℝ) from (S.dVar kFin).indicator_apply_eq_one h2] · have h1 : S.factualD kFin ω ∉ ({dbar kFin} : Set δ) := h have h2 : ω ∉ (S.dVar kFin).event (dbar kFin) := h rw [show u (S.factualD kFin ω) = (0 : ℝ) from Set.indicator_of_notMem h1 _, show ind_k ω = (0 : ℝ) from (S.dVar kFin).indicator_apply_eq_zero h2] have huv_int : Integrable (fun ω => u (S.factualD kFin ω) * S.Y_of dbar ω) P.μ := by have hEq : (fun ω => u (S.factualD kFin ω) * S.Y_of dbar ω) = (fun ω => ind_k ω * S.Y_of dbar ω) := by funext ω; rw [congr_fun hu_eq ω] rw [hEq]; exact hindk_Yof_int have hfact : P.μ[fun ω => u (S.factualD kFin ω) * S.Y_of dbar ω | (S.historyBundle k hk).sigma] =ᵐ[P.μ] P.μ[fun ω => u (S.factualD kFin ω) | (S.historyBundle k hk).sigma] * P.μ[fun ω => S.Y_of dbar ω | (S.historyBundle k hk).sigma] := condExp_mul_of_condIndep (μ := P.μ) (m := (S.historyBundle k hk).sigma) hσk_le (f := S.factualD kFin) (g := S.Y_of dbar) (S.measurable_factualD kFin) (S.measurable_Y_of dbar) hCI (u := u) (v := id) hu_meas measurable_id (by rw [hu_eq]; exact hindk_int) hYof_int huv_int have hExch : (S.historyBundle k hk).condExpGiven (fun ω => ind_k ω * S.Y_of dbar ω) P.μ -- … truncated; follow the source link for the rest …

theorem cdtr_iter [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (S : PODTRSystem P n δ γ) (hA : S.Assumptions) (dbar : Fin n → δ) (hn : 0 < n) : ∀ j : ℕ, j < n → (fun ω => S.innerReg dbar j ω * S.indD dbar (n - 1 - j) ω) =ᵐ[P.μ] (fun ω => S.indD dbar (n - 1 - j) ω * (S.historyBundle (n - 1 - j) (by omega)).condExpGiven (S.Y_of dbar) P.μ ω) := by intro j hj induction j with | zero => have h := S.cdtr_base hA dbar hn -- `cdtr_base` produces the j = 0 case with `n - 1` on the indD side; -- `n - 1 - 0 = n - 1`, so the two statements coincide. have heq : n - 1 - 0 = n - 1 := by omega simp only [heq] convert h using 3 | succ j ih => have hj' : j < n := Nat.lt_of_succ_lt hj have ih' := ih hj' -- `cdtr_step` consumes IH at depth j (with index `n - j - 1` on indD) -- and produces depth j+1 (with index `n - j - 2`). Bridge `n - 1 - j` -- ↔ `n - j - 1` and `n - 1 - (j + 1)` ↔ `n - j - 2`. have heq1 : n - 1 - j = n - j - 1 := by omega have heq2 : n - 1 - (j + 1) = n - j - 2 := by omega have hk : n - j - 2 < n := by omega -- Reshape ih' to match cdtr_step's IH-shape. have ihStep : (fun ω => S.innerReg dbar j ω * S.indD dbar (n - j - 1) ω) =ᵐ[P.μ] (fun ω => S.indD dbar (n - j - 1) ω * (S.historyBundle (n - j - 1) (by omega)).condExpGiven (S.Y_of dbar) P.μ ω) := by have := ih' simp only [heq1] at this convert this using 2 have hjlt : j < n := Nat.lt_of_succ_lt hj have hIH_int : Integrable (S.innerReg dbar j) P.μ := (S.cdtr_strong hA dbar hn j hjlt).2 have hStep := S.cdtr_step hA dbar j hj hk hIH_int ihStep -- Reshape `hStep`'s conclusion to the goal indices. simp only [heq2] convert hStep using 2

lemma innerReg_integrable [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (S : PODTRSystem P n δ γ) (hA : S.Assumptions) (dbar : Fin n → δ) (j : ℕ) (hj : j < n) : Integrable (S.innerReg dbar j) P.μ := by have hn : 0 < n := lt_of_le_of_lt (zero_le _) hj exact (S.cdtr_strong hA dbar hn j hj).2