Mathlib.Probability.Kernel.Finite­History

theorem integral_compProd_of_law {H B : Type*} [MeasurableSpace H] [MeasurableSpace B] (μ : Measure H) (K : Kernel H B) [SFinite μ] [IsSFiniteKernel K] (ν : Measure (H × B)) (hν : ν = μ ⊗ₘ K) (f : H × B → ℝ) (hf : Integrable f ν) : ∫ z, f z ∂ν = ∫ h, ∫ b, f (h, b) ∂K h ∂μ := by subst ν exact Measure.integral_compProd hf

theorem integral_compProd_bounded {H B : Type*} [MeasurableSpace H] [MeasurableSpace B] (μ : Measure H) (K : Kernel H B) [IsProbabilityMeasure μ] [IsMarkovKernel K] (ν : Measure (H × B)) (hν : ν = μ ⊗ₘ K) (f : H × B → ℝ) (hf : Measurable f) (C : ℝ) (hbound : ∀ z, |f z| ≤ C) : ∫ z, f z ∂ν = ∫ h, ∫ b, f (h, b) ∂K h ∂μ := by subst ν have hfi : Integrable f (μ ⊗ₘ K) := Integrable.of_bound hf.aestronglyMeasurable C (Filter.Eventually.of_forall fun z => by simpa only [Real.norm_eq_abs] using hbound z) exact Measure.integral_compProd hfi

theorem covariance_compProd_of_centered_kernel_bound {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (μ : Measure X) [IsProbabilityMeasure μ] (K : Kernel X Y) [IsMarkovKernel K] (ν : Measure (X × Y)) (hν : ν = μ ⊗ₘ K) (f : X → ℝ) (hf : Measurable f) (Cf : ℝ) (hCf : 0 ≤ Cf) (hf_bound : ∀ x, |f x| ≤ Cf) (g : Y → ℝ) (hg : Measurable g) (Cg : ℝ) (hg_bound : ∀ y, |g y| ≤ Cg) (D : ℝ) (hkernel : ∀ x, |(∫ y, g y ∂K x) - (∫ z, g z.2 ∂ν)| ≤ D) : |(∫ z, f z.1 * g z.2 ∂ν) - (∫ x, f x ∂μ) * (∫ z, g z.2 ∂ν)| ≤ Cf * D := by let c : ℝ := ∫ z, g z.2 ∂ν have hkg_meas : Measurable (fun x => ∫ y, g y ∂K x) := by simpa using ((hg.comp measurable_snd).stronglyMeasurable.integral_kernel_prod_right').measurable have hkg_bound : ∀ x, |∫ y, g y ∂K x| ≤ Cg := by intro x simpa only [Real.norm_eq_abs, probReal_univ, mul_one] using (norm_integral_le_of_norm_le_const (μ := K x) (f := g) (C := Cg) (Filter.Eventually.of_forall fun y => by simpa only [Real.norm_eq_abs] using hg_bound y)) have hfg_bound : ∀ z : X × Y, |f z.1 * g z.2| ≤ Cf * Cg := by intro z rw [abs_mul] exact mul_le_mul (hf_bound z.1) (hg_bound z.2) (abs_nonneg _) hCf have hfg_meas : Measurable (fun z : X × Y => f z.1 * g z.2) := (hf.comp measurable_fst).mul (hg.comp measurable_snd) have hf_int : Integrable f μ := Integrable.of_bound hf.aestronglyMeasurable Cf (Filter.Eventually.of_forall fun x => by simpa only [Real.norm_eq_abs] using hf_bound x) have hkgf_int : Integrable (fun x => f x * ∫ y, g y ∂K x) μ := by apply Integrable.of_bound ((hf.mul hkg_meas).aestronglyMeasurable) (Cf * Cg) exact Filter.Eventually.of_forall fun x => by simpa only [Pi.mul_apply, Real.norm_eq_abs, abs_mul] using mul_le_mul (hf_bound x) (hkg_bound x) (abs_nonneg _) hCf have hfg_eq : (∫ z, f z.1 * g z.2 ∂ν) = ∫ x, f x * (∫ y, g y ∂K x) ∂μ := by rw [integral_compProd_bounded μ K ν hν _ hfg_meas (Cf * Cg) hfg_bound] congr 1 funext x simpa only [fst, snd] using integral_const_mul (μ := K x) (f x) g have hcenter_eq : (∫ x, f x * ((∫ y, g y ∂K x) - c) ∂μ) = (∫ x, f x * (∫ y, g y ∂K x) ∂μ) - (∫ x, f x ∂μ) * c := by simp_rw [mul_sub] rw [integral_sub hkgf_int (hf_int.mul_const c), integral_mul_const] rw [hfg_eq] change |(∫ x, f x * (∫ y, g y ∂K x) ∂μ) - (∫ x, f x ∂μ) * c| ≤ Cf * D rw [← hcenter_eq] simpa only [Real.norm_eq_abs, probReal_univ, mul_one] using (norm_integral_le_of_norm_le_const (μ := μ) (f := fun x => f x * ((∫ y, g y ∂K x) - c)) (C := Cf * D) (Filter.Eventually.of_forall fun x => by simpa only [Real.norm_eq_abs, abs_mul] using mul_le_mul (hf_bound x) (hkernel x) (abs_nonneg _) hCf))

theorem integral_finite_eq_sum_of_singleton_masses {S : Type*} [Fintype S] [MeasurableSpace S] (ρ : Measure S) [IsProbabilityMeasure ρ] (π : S → ℝ) (hπsum : ∑ s, π s = 1) (hπatom : ∀ s, (ρ {s}).toReal = π s) (v : S → ℝ) (hv : Measurable v) : (∫ s, v s ∂ρ) = ∑ s, π s * v s := by classical let T (A : Set S) : Finset S := Finset.univ.filter (fun s => s ∈ A) have hbound (A : Set S) : ρ.real A ≤ ∑ s ∈ T A, π s := by have hset : A = ⋃ s ∈ T A, ({s} : Set S) := by ext s simp [T] calc ρ.real A = ρ.real (⋃ s ∈ T A, ({s} : Set S)) := congrArg ρ.real hset _ ≤ ∑ s ∈ T A, ρ.real {s} := measureReal_biUnion_finset_le _ _ _ = ∑ s ∈ T A, π s := by simp [Measure.real, hπatom] have hevent (A : Set S) (hA : MeasurableSet A) : ρ.real A = ∑ s ∈ T A, π s := by have hc := hbound Aᶜ have hs : (∑ s ∈ T A, π s) + (∑ s ∈ T Aᶜ, π s) = 1 := by simpa only [T, Set.mem_compl_iff, Finset.sum_filter_add_sum_filter_not] using hπsum have hm : ρ.real A + ρ.real Aᶜ = 1 := by simpa [probReal_univ] using (measureReal_add_measureReal_compl (μ := ρ) hA) have ha := hbound A have hreverse : (∑ s ∈ T A, π s) ≤ ρ.real A := by calc (∑ s ∈ T A, π s) = 1 - (∑ s ∈ T Aᶜ, π s) := eq_sub_of_add_eq hs _ ≤ 1 - ρ.real Aᶜ := sub_le_sub_left hc 1 _ = ρ.real A := (eq_sub_of_add_eq hm).symm exact le_antisymm ha hreverse let f : SimpleFunc S ℝ := ⟨v, (fun x => hv (measurableSet_singleton x)), Set.finite_range v⟩ have hf : (f : S → ℝ) = v := rfl have hi : Integrable (f : S → ℝ) ρ := f.integrable_of_isFiniteMeasure change (∫ s, f s ∂ρ) = ∑ s, π s * v s rw [SimpleFunc.integral_eq_sum f hi] simp only [smul_eq_mul] have hfiber (x : ℝ) : ρ.real (v ⁻¹' {x}) = ∑ s ∈ Finset.univ.filter (fun s => v s = x), π s := by simpa only [T, Set.mem_preimage, Set.mem_singleton_iff] using hevent (v ⁻¹' {x}) (hv (measurableSet_singleton x)) simp only [hf] at * simp_rw [hfiber] rw [← Finset.sum_fiberwise_of_maps_to (s := univ) (t := f.range) (g := v) (f := fun s => π s * v s) (by intro s hs exact f.mem_range_self s)] congr 1 ext x rw [Finset.sum_mul] apply Finset.sum_congr rfl intro s hs have hvs : v s = x := (Finset.mem_filter.mp hs).2 rw [hvs]

theorem markovIterate_point_stationary_bound {S : Type*} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) (π : S → ℝ) (alpha : ℝ) (hP : IsStochasticMatrix P) (hπ : IsStationary P π) (hcontract : ContractsL1 P alpha) (halpha0 : 0 ≤ alpha) (gap : ℕ) (s : S) : l1Distance (markovIterate P (pointVector s) gap) π ≤ 2 * alpha ^ gap := by have hp : IsProbabilityVector (pointVector s) := by constructor · intro t unfold pointVector split <;> norm_num · simp [pointVector] have hbase : l1Distance (pointVector s) π ≤ 2 := by unfold l1Distance calc (∑ t, |pointVector s t - π t|) ≤ ∑ t, (pointVector s t + π t) := by apply Finset.sum_le_sum intro t ht apply abs_le.mpr constructor <;> have := hp.1 t <;> have := hπ.1.1 t <;> linarith _ = 2 := by rw [Finset.sum_add_distrib, hp.2, hπ.1.2]; ring induction gap with | zero => simpa [markovIterate] using hbase | succ n ih => have hn := hP.iterate_probability hp n calc l1Distance (markovIterate P (pointVector s) (n + 1)) π = l1Distance (markovStep (markovIterate P (pointVector s) n) P) (markovStep π P) := by rw [hπ.2]; rfl _ ≤ alpha * l1Distance (markovIterate P (pointVector s) n) π := hcontract _ _ hn hπ.1 _ ≤ alpha * (2 * alpha ^ n) := mul_le_mul_of_nonneg_left ih halpha0 _ = 2 * alpha ^ (n + 1) := by rw [pow_succ]; ring

theorem markov_row_score_bound {S : Type*} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) (π : S → ℝ) (alpha : ℝ) (hP : IsStochasticMatrix P) (hπ : IsStationary P π) (hcontract : ContractsL1 P alpha) (halpha0 : 0 ≤ alpha) (gap : ℕ) (s : S) (v : S → ℝ) (Cv : ℝ) (hv : ∀ t, |v t| ≤ Cv) : |(∑ t, markovIterate P (pointVector s) gap t * v t) - (∑ t, π t * v t)| ≤ 2 * Cv * alpha ^ gap := by have hCv : 0 ≤ Cv := le_trans (abs_nonneg _) (hv s) have hdist := markovIterate_point_stationary_bound P π alpha hP hπ hcontract halpha0 gap s calc |(∑ t, markovIterate P (pointVector s) gap t * v t) - (∑ t, π t * v t)| ≤ Cv * l1Distance (markovIterate P (pointVector s) gap) π := by rw [← Finset.sum_sub_distrib] calc |∑ t, (markovIterate P (pointVector s) gap t * v t - π t * v t)| = |∑ t, (markovIterate P (pointVector s) gap t - π t) * v t| := by congr 1 apply Finset.sum_congr rfl intro t ht ring _ ≤ ∑ t, |(markovIterate P (pointVector s) gap t - π t) * v t| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ t, |markovIterate P (pointVector s) gap t - π t| * Cv := by apply Finset.sum_le_sum intro t ht rw [abs_mul] exact mul_le_mul_of_nonneg_left (hv t) (abs_nonneg _) _ = Cv * l1Distance (markovIterate P (pointVector s) gap) π := by rw [l1Distance, Finset.mul_sum] apply Finset.sum_congr rfl intro t ht ring _ ≤ Cv * (2 * alpha ^ gap) := mul_le_mul_of_nonneg_left hdist hCv _ = 2 * Cv * alpha ^ gap := by ring

theorem stationary_future_window_mean {S X Y : Type*} [Fintype S] [DecidableEq S] [MeasurableSpace S] [MeasurableSpace X] [MeasurableSpace Y] (P : Matrix S S ℝ) (π : S → ℝ) (hπ : IsStationary P π) (gap : ℕ) (μ : Measure X) [IsProbabilityMeasure μ] (last : X → S) (hlast_meas : Measurable last) (hlast : ∀ s, ((μ.map last) {s}).toReal = π s) (Q : Kernel S Y) [IsMarkovKernel Q] (future : Kernel X Y) [IsMarkovKernel future] (hfuture : ∀ (g : Y → ℝ), Measurable g → (∀ y, |g y| ≤ 1) → ∀ x, (∫ y, g y ∂future x) = ∑ s, markovIterate P (pointVector (last x)) gap s * (∫ y, g y ∂Q s)) (ν : Measure (X × Y)) (hν : ν = μ ⊗ₘ future) (g : Y → ℝ) (hg : Measurable g) (hg_bound : ∀ y, |g y| ≤ 1) : (∫ z, g z.2 ∂ν) = ∑ s, π s * (∫ y, g y ∂Q s) := by -- The future kernel integral is measurable on `X`. Its finite fibers have -- masses determined by the outer singleton masses of `μ.map last`, even -- when the state singletons themselves are not measurable. The stationary -- identity then averages the finite Markov rows back to `π`. classical let ρ : Measure S := μ.map last have : IsProbabilityMeasure ρ := Measure.isProbabilityMeasure_map hlast_meas.aemeasurable let q : S → ℝ := fun s => ∫ y, g y ∂Q s let v : S → ℝ := fun s => ∑ t, markovIterate P (pointVector s) gap t * q t let F : X → ℝ := fun x => ∫ y, g y ∂future x have hF : Measurable F := ((hg.comp measurable_snd).stronglyMeasurable.integral_kernel_prod_right').measurable have hFv (x : X) : F x = v (last x) := hfuture g hg hg_bound x have hbound (B : Set S) : μ.real (last ⁻¹' B) ≤ ∑ s ∈ Finset.univ.filter (fun s => s ∈ B), π s := by have hset : B = ⋃ s ∈ Finset.univ.filter (fun s => s ∈ B), ({s} : Set S) := by ext s simp calc μ.real (last ⁻¹' B) ≤ ρ.real B := by exact ENNReal.toReal_mono (measure_ne_top ρ B) (Measure.le_map_apply hlast_meas.aemeasurable B) _ = ρ.real (⋃ s ∈ Finset.univ.filter (fun s => s ∈ B), ({s} : Set S)) := congrArg ρ.real hset _ ≤ ∑ s ∈ Finset.univ.filter (fun s => s ∈ B), ρ.real {s} := measureReal_biUnion_finset_le _ _ _ = ∑ s ∈ Finset.univ.filter (fun s => s ∈ B), π s := by simp [Measure.real, ρ, hlast] have hevent (B : Set S) (hB : MeasurableSet (last ⁻¹' B)) : μ.real (last ⁻¹' B) = ∑ s ∈ Finset.univ.filter (fun s => s ∈ B), π s := by have hc := hbound Bᶜ have hs : (∑ s ∈ Finset.univ.filter (fun s => s ∈ B), π s) + (∑ s ∈ Finset.univ.filter (fun s => s ∈ Bᶜ), π s) = 1 := by simpa only [Set.mem_compl_iff, Finset.sum_filter_add_sum_filter_not] using hπ.1.2 have hm : μ.real (last ⁻¹' B) + μ.real (last ⁻¹' Bᶜ) = 1 := by simpa [Set.preimage_compl, probReal_univ] using (measureReal_add_measureReal_compl (μ := μ) hB) have ha := hbound B have hr : (∑ s ∈ Finset.univ.filter (fun s => s ∈ B), π s) ≤ μ.real (last ⁻¹' B) := by calc (∑ s ∈ Finset.univ.filter (fun s => s ∈ B), π s) = 1 - (∑ s ∈ Finset.univ.filter (fun s => s ∈ Bᶜ), π s) := eq_sub_of_add_eq hs _ ≤ 1 - μ.real (last ⁻¹' Bᶜ) := by simpa only [Set.mem_compl_iff] using (sub_le_sub_left hc 1) _ = μ.real (last ⁻¹' B) := (eq_sub_of_add_eq hm).symm exact le_antisymm ha hr have hfr : (range F).Finite := (Set.finite_range v).subset (by rintro r ⟨x, rfl⟩ exact ⟨last x, (hFv x).symm⟩) let sf : SimpleFunc X ℝ := ⟨F, (fun r => hF (measurableSet_singleton r)), hfr⟩ have hfi : Integrable (sf : X → ℝ) μ := sf.integrable_of_isFiniteMeasure have hfiber (r : ℝ) : μ.real (F ⁻¹' {r}) = ∑ s ∈ Finset.univ.filter (fun s => v s = r), π s := by have hpre : F ⁻¹' {r} = last ⁻¹' {s | v s = r} := by ext x simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_ofPred_eq, hFv] rw [hpre] simpa only [Set.mem_ofPred_eq] using hevent {s | v s = r} (by rw [← hpre]; exact hF (measurableSet_singleton r)) have hmass : (∫ x, F x ∂μ) = ∑ s, π s * v s := by change (∫ x, sf x ∂μ) = _ rw [← SimpleFunc.integral_eq_integral sf hfi] have hsubset : {r ∈ sf.range | r ≠ 0} ⊆ Finset.univ.image v := by intro r hr obtain ⟨x, hx⟩ := (SimpleFunc.mem_range.mp (Finset.mem_filter.mp hr).1) exact Finset.mem_image.mpr ⟨last x, Finset.mem_univ _, by simpa [sf] using (hFv x).symm.trans hx⟩ rw [SimpleFunc.integral_eq_sum_of_subset hsubset] simp only [smul_eq_mul] simp_rw [show (sf : X → ℝ) = F from rfl, hfiber] rw [← Finset.sum_fiberwise_of_maps_to (s := univ) (t := Finset.univ.image v) (g := v) (f := fun s => π s * v s) (by intro s hs; exact Finset.mem_image_of_mem v hs)] congr 1 ext r rw [Finset.sum_mul] apply Finset.sum_congr rfl intro s hs rw [(Finset.mem_filter.mp hs).2] have hmix : ∀ n t, (∑ s, π s * markovIterate P (pointVector s) n t) = π t := by intro n induction n with | zero => intro t simp [markovIterate, pointVector] | succ n ih => intro t simp only [markovIterate, markovStep, Matrix.vecMul_eq_sum, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] calc (∑ s, π s * ∑ u, markovIterate P (pointVector s) n u * P u t) = ∑ u, (∑ s, π s * markovIterate P (pointVector s) n u) * P u t := by simp_rw [Finset.mul_sum] rw [Finset.sum_comm] simp_rw [← mul_assoc, ← Finset.sum_mul] _ = ∑ u, π u * P u t := by simp_rw [ih] _ = π t := by have ht := congrFun hπ.2 t simpa [markovStep, Matrix.vecMul_eq_sum] using ht have hq : Measurable q := ((hg.comp measurable_snd).stronglyMeasurable.integral_kernel_prod_right').measurable have hqmean := integral_finite_eq_sum_of_singleton_masses ρ π hπ.1.2 (by simpa [ρ] using hlast) q hq calc (∫ z, g z.2 ∂ν) = ∫ x, F x ∂μ := by exact integral_compProd_bounded μ future ν hν _ (hg.comp measurable_snd) 1 (fun z => hg_bound z.2) _ = ∑ s, π s * v s := hmass _ = ∑ t, π t * q t := by simp only [v] simp_rw [Finset.mul_sum] rw [Finset.sum_comm] simp_rw [← mul_assoc, ← Finset.sum_mul] simp_rw [hmix] _ = ∫ s, q s ∂ρ := hqmean.symm _ = ∑ s, π s * (∫ y, g y ∂Q s) := hqmean

@[fun_prop] theorem actionLikelihood_measurable {S A : Type*} [MeasurableSpace S] [MeasurableSpace A] [MeasurableSingletonClass A] [Fintype A] (behavior target : Kernel S A) : Measurable fun z : S × A => actionLikelihood behavior target z.1 z.2 := by -- Partition the finite action space into singleton cells. For fixed `a`, -- kernel evaluation on `{a}` is measurable in the state. apply measurable_from_prod_countable_left intro a unfold actionLikelihood have hb : Measurable (fun s => (behavior s) {a}) := Kernel.measurable_coe behavior (MeasurableSet.singleton a) have ht : Measurable (fun s => (target s) {a}) := Kernel.measurable_coe target (MeasurableSet.singleton a) exact Measurable.ite (hb (measurableSet_singleton 0)) measurable_const (ht.ennreal_toReal.div hb.ennreal_toReal)

theorem integral_actionLikelihood {S A : Type*} [MeasurableSpace S] [MeasurableSpace A] [MeasurableSingletonClass A] [Fintype A] (behavior target : Kernel S A) [IsMarkovKernel behavior] [IsMarkovKernel target] (hAC : ∀ s, target s ≪ behavior s) (s : S) (g : A → ℝ) : ∫ a, actionLikelihood behavior target s a * g a ∂behavior s = ∫ a, g a ∂target s := by -- Convert both integrals into finite sums of atom masses. On a behavior-null -- atom, `hAC s` makes the target atom null too; on other atoms cancel the -- denominator after converting finite ENNReal masses to real numbers. have hbint : Integrable (fun a => actionLikelihood behavior target s a * g a) (behavior s) := Integrable.of_finite have htint : Integrable g (target s) := Integrable.of_finite rw [integral_fintype hbint, integral_fintype htint] apply Finset.sum_congr rfl intro a _ simp only [Measure.real, smul_eq_mul] by_cases hb : (behavior s) {a} = 0 · have ht : (target s) {a} = 0 := hAC s hb simp [actionLikelihood, hb, ht] · have hb' : ((behavior s) {a}).toReal ≠ 0 := ENNReal.toReal_ne_zero.mpr ⟨hb, measure_ne_top _ _⟩ simp only [actionLikelihood, hb, if_false] field_simp

theorem weightedValue_measurable {H B : Type*} [MeasurableSpace H] [MeasurableSpace B] (K : Kernel H B) [IsMarkovKernel K] (append : H → B → H) (happend : Measurable fun z : H × B => append z.1 z.2) (w : H → B → ℝ) (hw : Measurable fun z : H × B => w z.1 z.2) (Cw : ℝ) (hw_bound : ∀ h b, |w h b| ≤ Cw) (f : H → ℝ) (hf : Measurable f) (Cf : ℝ) (hf_bound : ∀ h, |f h| ≤ Cf) (n : ℕ) : Measurable (weightedValue K append w n f) := by -- Induct on `n`; the bound gives integrability of each kernel section and -- Mathlib's measurable kernel integral handles the induction step. exact (weightedValue_measurable_bounded_aux K append happend w hw Cw hw_bound f hf Cf hf_bound n).1

theorem weightedValue_bounded {H B : Type*} [MeasurableSpace H] [MeasurableSpace B] (K : Kernel H B) [IsMarkovKernel K] (append : H → B → H) (happend : Measurable fun z : H × B => append z.1 z.2) (w : H → B → ℝ) (hw : Measurable fun z : H × B => w z.1 z.2) (Cw : ℝ) (hw_bound : ∀ h b, |w h b| ≤ Cw) (f : H → ℝ) (hf : Measurable f) (Cf : ℝ) (hf_bound : ∀ h, |f h| ≤ Cf) (n : ℕ) : ∃ C : ℝ, ∀ h, |weightedValue K append w n f h| ≤ C := by -- The bound `Cf * max 1 Cw ^ n` suffices; use the Markov integral bound. exact (weightedValue_measurable_bounded_aux K append happend w hw Cw hw_bound f hf Cf hf_bound n).2

theorem integral_weighted_history {H B : Type*} [MeasurableSpace H] [MeasurableSpace B] (K : Kernel H B) [IsMarkovKernel K] (append : H → B → H) (happend : Measurable fun z : H × B => append z.1 z.2) (w : H → B → ℝ) (hw : Measurable fun z : H × B => w z.1 z.2) (Cw : ℝ) (hw_bound : ∀ h b, |w h b| ≤ Cw) (μ : ℕ → Measure H) (hμprob : ∀ n, IsProbabilityMeasure (μ n)) (hμ : ∀ n, μ (n + 1) = (μ n ⊗ₘ K).map (fun z => append z.1 z.2)) (weight : ℕ → H → ℝ) (hweight_meas : ∀ n, Measurable (weight n)) (hweight_bound : ∀ n, ∃ C : ℝ, ∀ h, |weight n h| ≤ C) (hweight0 : ∀ h, weight 0 h = 1) (hweight_step : ∀ n h b, weight (n + 1) (append h b) = weight n h * w h b) (f : H → ℝ) (hf : Measurable f) (Cf : ℝ) (hf_bound : ∀ h, |f h| ≤ Cf) (n : ℕ) : ∫ h, weight n h * f h ∂μ n = ∫ h, weightedValue K append w n f h ∂μ 0 := by -- Prove the stronger induction statement starting at an arbitrary time `k`. -- At a successor use `integral_map` and `integral_compProd_bounded`, then -- `hweight_step`. The resulting operator is `T f := weightedValue ... 1 f`. -- Its powers satisfy `T ^ (n+1) f = T ^ n (T f)`; this semigroup fact needs -- a separate induction because `weightedValue` recurses on the left. have hmain : ∀ m k (g : H → ℝ), Measurable g → ∀ Cg : ℝ, (∀ h, |g h| ≤ Cg) → ∫ h, weight (k + m) h * g h ∂μ (k + m) = ∫ h, weight k h * weightedValue K append w m g h ∂μ k := by intro m induction m with | zero => intro k g hg Cg hg_bound simp only [Nat.add_zero, weightedValue] | succ m ih => intro k g hg Cg hg_bound obtain ⟨D, hD⟩ := weightedValue_bounded K append happend w hw Cw hw_bound g hg Cg hg_bound 1 have hgm := weightedValue_measurable K append happend w hw Cw hw_bound g hg Cg hg_bound 1 calc ∫ h, weight (k + (m + 1)) h * g h ∂μ (k + (m + 1)) = ∫ h, weight ((k + m) + 1) h * g h ∂μ ((k + m) + 1) := by rw [Nat.add_succ] _ = ∫ h, weight (k + m) h * weightedValue K append w 1 g h ∂μ (k + m) := integral_weighted_history_step K append happend w hw Cw hw_bound μ hμprob hμ weight hweight_meas hweight_bound hweight_step g hg Cg hg_bound (k + m) _ = ∫ h, weight k h * weightedValue K append w m (weightedValue K append w 1 g) h ∂μ k := ih k _ hgm D hD _ = ∫ h, weight k h * weightedValue K append w (m + 1) g h ∂μ k := by congr 1 funext h rw [weightedValue_succ_right] have hresult := hmain n 0 f hf Cf hf_bound simpa only [Nat.zero_add, hweight0, one_mul] using hresult

theorem weightedValue_eq_matrixValue {H B S : Type*} [MeasurableSpace H] [MeasurableSpace B] [MeasurableSpace S] [Fintype S] [MeasurableSingletonClass S] (K : Kernel H B) [IsMarkovKernel K] (append : H → B → H) (w : H → B → ℝ) (state : H → S) (P : Matrix S S ℝ) (hweighted : ∀ (v : S → ℝ), Measurable v → ∀ h, (∫ b, w h b * v (state (append h b)) ∂K h) = ∑ s, P (state h) s * v s) (reward : S → ℝ) (n : ℕ) (h : H) : weightedValue K append w n (reward ∘ state) h = matrixValue P n reward (state h) := by -- Induct on `n`, rewrite the recursive value using the induction hypothesis, -- then apply `hweighted` to `matrixValue P n reward`. have hm : ∀ m : ℕ, Measurable (matrixValue P m reward) := by intro m exact measurable_of_finite _ induction n generalizing h with | zero => rfl | succ n ih => simp only [weightedValue, matrixValue] have heq : (fun b => w h b * weightedValue K append w n (reward ∘ state) (append h b)) = (fun b => w h b * matrixValue P n reward (state (append h b))) := by funext b rw [ih (append h b)] rw [heq] exact hweighted (matrixValue P n reward) (hm n) h