From 4132319674b2345b2fcba9417b42baddccedfa39 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 14 Oct 2026 09:10:07 +0200 Subject: [PATCH 1/5] prove convergence of markov chain --- RandomDo.lean | 18 +- .../Integral/Lebesgue/Markov.lean | 57 ++ .../MeasurableSpace/Embedding.lean | 52 -- .../MeasureTheory/Measure/Basic.lean | 43 + .../Measure/Decomposition/Exhaustion.lean | 56 ++ .../MeasureTheory/Measure/Prod.lean | 93 +++ .../Measure/SeparableMeasure.lean | 99 +++ .../TotalVariation/DataProcessing.lean | 76 ++ .../Measure/TotalVariation/Defs.lean | 37 + .../NumberTheory/FrobeniusNumber.lean | 44 + .../Probability/Kernel/Aperiodic.lean | 216 +++++ .../Kernel/Composition/MeasureComp.lean | 102 +++ .../Probability/Kernel/ErgodicTheorem.lean | 768 ++++++++++++++++++ .../Probability/Kernel/HarrisRecurrent.lean | 87 ++ .../Probability/Kernel/Invariance.lean | 99 +++ .../Probability/Kernel/Irreducible.lean | 166 ++++ .../ForMathlib/Probability/Kernel/Pow.lean | 92 +++ .../Probability/Kernel/SmallSet/Basic.lean | 97 +++ .../Probability/Kernel/SmallSet/Exists.lean | 165 ++++ RandomDo/Measurable.lean | 4 +- 20 files changed, 2316 insertions(+), 55 deletions(-) create mode 100644 RandomDo/ForMathlib/MeasureTheory/Integral/Lebesgue/Markov.lean delete mode 100644 RandomDo/ForMathlib/MeasureTheory/MeasurableSpace/Embedding.lean create mode 100644 RandomDo/ForMathlib/MeasureTheory/Measure/Basic.lean create mode 100644 RandomDo/ForMathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean create mode 100644 RandomDo/ForMathlib/MeasureTheory/Measure/Prod.lean create mode 100644 RandomDo/ForMathlib/MeasureTheory/Measure/SeparableMeasure.lean create mode 100644 RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/DataProcessing.lean create mode 100644 RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean create mode 100644 RandomDo/ForMathlib/NumberTheory/FrobeniusNumber.lean create mode 100644 RandomDo/ForMathlib/Probability/Kernel/Aperiodic.lean create mode 100644 RandomDo/ForMathlib/Probability/Kernel/Composition/MeasureComp.lean create mode 100644 RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean create mode 100644 RandomDo/ForMathlib/Probability/Kernel/HarrisRecurrent.lean create mode 100644 RandomDo/ForMathlib/Probability/Kernel/Invariance.lean create mode 100644 RandomDo/ForMathlib/Probability/Kernel/Irreducible.lean create mode 100644 RandomDo/ForMathlib/Probability/Kernel/Pow.lean create mode 100644 RandomDo/ForMathlib/Probability/Kernel/SmallSet/Basic.lean create mode 100644 RandomDo/ForMathlib/Probability/Kernel/SmallSet/Exists.lean diff --git a/RandomDo.lean b/RandomDo.lean index b2d4043..4e802c6 100644 --- a/RandomDo.lean +++ b/RandomDo.lean @@ -1,6 +1,22 @@ module -- shake: keep-all --deprecated_module: ignore -public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Embedding +public import RandomDo.ForMathlib.MeasureTheory.Integral.Lebesgue.Markov +public import RandomDo.ForMathlib.MeasureTheory.Measure.Basic +public import RandomDo.ForMathlib.MeasureTheory.Measure.Decomposition.Exhaustion +public import RandomDo.ForMathlib.MeasureTheory.Measure.Prod +public import RandomDo.ForMathlib.MeasureTheory.Measure.SeparableMeasure +public import RandomDo.ForMathlib.MeasureTheory.Measure.TotalVariation.DataProcessing +public import RandomDo.ForMathlib.MeasureTheory.Measure.TotalVariation.Defs +public import RandomDo.ForMathlib.NumberTheory.FrobeniusNumber +public import RandomDo.ForMathlib.Probability.Kernel.Aperiodic +public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp +public import RandomDo.ForMathlib.Probability.Kernel.ErgodicTheorem +public import RandomDo.ForMathlib.Probability.Kernel.HarrisRecurrent +public import RandomDo.ForMathlib.Probability.Kernel.Invariance +public import RandomDo.ForMathlib.Probability.Kernel.Irreducible +public import RandomDo.ForMathlib.Probability.Kernel.Pow +public import RandomDo.ForMathlib.Probability.Kernel.SmallSet.Basic +public import RandomDo.ForMathlib.Probability.Kernel.SmallSet.Exists public import RandomDo.Measurable public import RandomDo.Monad.ForInInstances public import RandomDo.Monad.Instances diff --git a/RandomDo/ForMathlib/MeasureTheory/Integral/Lebesgue/Markov.lean b/RandomDo/ForMathlib/MeasureTheory/Integral/Lebesgue/Markov.lean new file mode 100644 index 0000000..aea128e --- /dev/null +++ b/RandomDo/ForMathlib/MeasureTheory/Integral/Lebesgue/Markov.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.MeasureTheory.Integral.Lebesgue.Markov + +/-! +# Superlevel sets and the Lebesgue integral + +## Main statements + +* `exists_pos_measure_lt_of_lintegral_pos`: if a function has positive integral, then one of its + strict superlevel sets has positive measure. +* `mul_measure_inter_lt_le_lintegral_mul`: Markov's inequality for a product of two functions. +-/ + +@[expose] public section + +open scoped ENNReal NNReal + +namespace MeasureTheory + +variable {α : Type*} {mα : MeasurableSpace α} {μ : Measure α} + +/-- If a function has positive integral, then one of its strict superlevel sets has positive +measure. -/ +lemma exists_pos_measure_lt_of_lintegral_pos {f : α → ℝ≥0∞} (hf : 0 < ∫⁻ a, f a ∂μ) : + ∃ ε : ℝ≥0, 0 < ε ∧ 0 < μ {a | (ε : ℝ≥0∞) < f a} := by + by_contra! h + refine hf.ne' (lintegral_eq_zero_of_ae_eq_zero ?_) + have h' : ∀ᵐ a ∂μ, ∀ n : ℕ, f a ≤ ((n : ℝ≥0∞) + 1)⁻¹ := by + rw [ae_all_iff] + intro n + have hn0 : ((n : ℝ≥0) + 1) ≠ 0 := by positivity + have hn := h ((n : ℝ≥0) + 1)⁻¹ (by positivity) + rw [nonpos_iff_eq_zero, measure_eq_zero_iff_ae_notMem] at hn + filter_upwards [hn] with a ha + simpa [ENNReal.coe_inv hn0] using ha + filter_upwards [h'] with a ha + by_contra h0 + obtain ⟨n, hn⟩ := ENNReal.exists_inv_nat_lt h0 + exact (ha n).not_gt ((ENNReal.inv_le_inv.mpr le_self_add).trans_lt hn) + +/-- Markov's inequality for a product of two functions. -/ +lemma mul_measure_inter_lt_le_lintegral_mul {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) + (hg : AEMeasurable g μ) (a b : ℝ≥0∞) : + a * b * μ ({x | a < f x} ∩ {x | b < g x}) ≤ ∫⁻ x, f x * g x ∂μ := + calc a * b * μ ({x | a < f x} ∩ {x | b < g x}) + _ ≤ a * b * μ {x | a * b ≤ f x * g x} := by + gcongr + exact fun x hx ↦ Set.mem_ofPred.mpr (mul_le_mul' hx.1.le hx.2.le) + _ ≤ ∫⁻ x, f x * g x ∂μ := mul_meas_ge_le_lintegral₀ (hf.mul hg) _ + +end MeasureTheory diff --git a/RandomDo/ForMathlib/MeasureTheory/MeasurableSpace/Embedding.lean b/RandomDo/ForMathlib/MeasureTheory/MeasurableSpace/Embedding.lean deleted file mode 100644 index e0eb517..0000000 --- a/RandomDo/ForMathlib/MeasureTheory/MeasurableSpace/Embedding.lean +++ /dev/null @@ -1,52 +0,0 @@ -/- -Copyright (c) 2026 Gaëtan Serré. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Gaëtan Serré --/ -module - -public import Mathlib.MeasureTheory.MeasurableSpace.Embedding - -/-! -# Lemmas about measurability of sigma types - -This file contains lemmas about measurability of sigma types, in particular the fact that the -canonical injection of a summand into a sigma type is a measurable embedding. - -## Main results - -* `measurableSet_sigma_iff`: a set of a sigma type is measurable exactly when its preimage under -every `Sigma.mk i` is. -* `measurable_sigmaMk`, `measurableEmbedding_sigmaMk`: the injection of a summand into a sigma type -is a measurable embedding. --/ - -@[expose] public section - -open MeasureTheory - -variable {ι : Type*} {β : ι → Type*} [∀ i, MeasurableSpace (β i)] - -theorem measurableSet_sigma_iff {s : Set (Σ i, β i)} : - MeasurableSet s ↔ ∀ i, MeasurableSet (Sigma.mk i ⁻¹' s) := - MeasurableSpace.measurableSet_iInf - -@[fun_prop] -theorem measurable_sigmaMk (i : ι) : Measurable (Sigma.mk i : β i → Σ j, β j) := - fun _ hs => measurableSet_sigma_iff.1 hs i - -theorem measurableEmbedding_sigmaMk (i : ι) : - MeasurableEmbedding (Sigma.mk i : β i → Σ j, β j) where - injective := sigma_mk_injective - measurable := measurable_sigmaMk i - measurableSet_image' {t} ht := measurableSet_sigma_iff.2 fun j => by - by_cases h : j = i - · subst h - simpa only [Set.preimage_image_eq _ sigma_mk_injective] using ht - · convert MeasurableSet.empty - ext x - simp only [Set.mem_preimage, Set.mem_image, Set.mem_empty_iff_false, iff_false] - rintro ⟨y, -, hy⟩ - exact h (congrArg Sigma.fst hy).symm - -end diff --git a/RandomDo/ForMathlib/MeasureTheory/Measure/Basic.lean b/RandomDo/ForMathlib/MeasureTheory/Measure/Basic.lean new file mode 100644 index 0000000..34d9bd9 --- /dev/null +++ b/RandomDo/ForMathlib/MeasureTheory/Measure/Basic.lean @@ -0,0 +1,43 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.MeasureTheory.Measure.Basic + +/-! +# Measure of an intersection and symmetric differences + +## Main statements + +* `measure_inter_le_measure_inter_add_symmDiff`: the measure of `s ∩ t` is at most the measure + of `s' ∩ t'` plus the measures of the symmetric differences of `s`, `s'` with a common set `u` + and of `t`, `t'` with a common set `v`. +-/ + +@[expose] public section + +open Set + +open scoped symmDiff + +namespace MeasureTheory + +variable {α : Type*} {mα : MeasurableSpace α} + +/-- If `s` is close to `s'` and `t` is close to `t'`, in the sense that they are close to common +sets `u` and `v` respectively, then the measure of `s ∩ t` is not much larger than the measure +of `s' ∩ t'`. -/ +lemma measure_inter_le_measure_inter_add_symmDiff (μ : Measure α) (s s' t t' u v : Set α) : + μ (s ∩ t) ≤ μ (s' ∩ t') + (μ (s ∆ u) + μ (s' ∆ u)) + (μ (t ∆ v) + μ (t' ∆ v)) := by + have hsub : s ∩ t ⊆ (s' ∩ t') ∪ (s ∆ u ∪ s' ∆ u) ∪ (t ∆ v ∪ t' ∆ v) := by + intro y hy + simp only [mem_union, mem_inter_iff, mem_symmDiff] at hy ⊢ + tauto + exact (measure_mono hsub).trans <| (measure_union_le _ _).trans <| add_le_add + ((measure_union_le _ _).trans (add_le_add le_rfl (measure_union_le _ _))) + (measure_union_le _ _) + +end MeasureTheory diff --git a/RandomDo/ForMathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean b/RandomDo/ForMathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean new file mode 100644 index 0000000..8c06be0 --- /dev/null +++ b/RandomDo/ForMathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean @@ -0,0 +1,56 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion + +/-! +# A Lebesgue-type decomposition with respect to an arbitrary measure + +## Main statements + +* `Measure.exists_null_restrict_compl_absolutelyContinuous`: for an s-finite measure `π` and an + arbitrary measure `φ`, there is a measurable `φ`-null set `N` such that `π.restrict Nᶜ ≪ φ`. +-/ + +@[expose] public section + +open scoped ENNReal + +namespace MeasureTheory.Measure + +variable {α : Type*} {mα : MeasurableSpace α} + +/-- For an s-finite measure `π` and an arbitrary measure `φ`, there is a measurable `φ`-null set +`N` such that the restriction of `π` to `Nᶜ` is absolutely continuous with respect to `φ`. No +finiteness assumption is made on `φ`. -/ +lemma exists_null_restrict_compl_absolutelyContinuous (φ π : Measure α) [SFinite π] : + ∃ N, MeasurableSet N ∧ φ N = 0 ∧ π.restrict Nᶜ ≪ φ := by + -- we apply the exhaustion method to the measure `∞ • φ`, which takes values in `{0, ∞}` + let N := ((∞ : ℝ≥0∞) • φ).sigmaFiniteSetWRT π + have hN : MeasurableSet N := measurableSet_sigmaFiniteSetWRT + refine ⟨N, hN, ?_, AbsolutelyContinuous.mk fun t ht hφt ↦ ?_⟩ + · have : SigmaFinite (((∞ : ℝ≥0∞) • φ).restrict N) := inferInstance + let S := spanningSets (((∞ : ℝ≥0∞) • φ).restrict N) + have hS : ∀ i, φ (S i ∩ N) = 0 := by + intro i + have h_lt := measure_spanningSets_lt_top (((∞ : ℝ≥0∞) • φ).restrict N) i + rw [restrict_apply (measurableSet_spanningSets _ i), smul_apply, smul_eq_mul] at h_lt + by_contra h0 + rw [ENNReal.top_mul h0] at h_lt + exact lt_irrefl _ h_lt + have h_eq : N = ⋃ i, S i ∩ N := by + rw [← Set.iUnion_inter, iUnion_spanningSets, Set.univ_inter] + rw [h_eq] + exact measure_iUnion_null hS + · rw [restrict_apply ht] + by_contra h0 + have h_top : ((∞ : ℝ≥0∞) • φ) (t ∩ Nᶜ) = ∞ := + measure_eq_top_of_subset_compl_sigmaFiniteSetWRT Set.inter_subset_right h0 + rw [measure_mono_null Set.inter_subset_left (by simp [hφt])] at h_top + exact ENNReal.zero_ne_top h_top + +end MeasureTheory.Measure diff --git a/RandomDo/ForMathlib/MeasureTheory/Measure/Prod.lean b/RandomDo/ForMathlib/MeasureTheory/Measure/Prod.lean new file mode 100644 index 0000000..eefe8d4 --- /dev/null +++ b/RandomDo/ForMathlib/MeasureTheory/Measure/Prod.lean @@ -0,0 +1,93 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.MeasureTheory.Measure.Prod + +/-! +# Measure of jointly measurable families of sets + +## Main statements + +* `measurable_measure_inter_of_measurableSet`: for jointly measurable families of sets `V x` and + `W z`, the measure of `V x ∩ W z` is a measurable function of `(x, z)`. +* `exists_lintegral_measure_inter_pos`: for countable collections of jointly measurable families + `V i x` and `W i' z` which cover almost all the space, there are `i, i'` such that the integral + over `x` and `z` of the measure of `V i x ∩ W i' z` is positive. +-/ + +@[expose] public section + +open Set + +open scoped ENNReal symmDiff + +namespace MeasureTheory + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ : Measure α} {φ : Measure β} {ν : Measure γ} + +/-- For a jointly measurable family of sets `V x`, the measure of the symmetric difference of +`V x` and a measurable set is a measurable function of `x`. -/ +lemma measurable_measure_symmDiff_of_measurableSet [SFinite φ] {V : α → Set β} + (hV : MeasurableSet {q : α × β | q.2 ∈ V q.1}) {S : Set β} (hS : MeasurableSet S) : + Measurable fun x ↦ φ (V x ∆ S) := + measurable_measure_prodMk_left (hV.symmDiff (measurable_snd hS)) + +/-- For two jointly measurable families of sets `V x` and `W z`, the measure of `V x ∩ W z` is a +measurable function of `(x, z)`. -/ +lemma measurable_measure_inter_of_measurableSet [SFinite φ] {V : α → Set β} {W : γ → Set β} + (hV : MeasurableSet {q : α × β | q.2 ∈ V q.1}) (hW : MeasurableSet {q : γ × β | q.2 ∈ W q.1}) : + Measurable fun q : α × γ ↦ φ (V q.1 ∩ W q.2) := + measurable_measure_prodMk_left + ((hV.preimage (measurable_fst.fst.prodMk measurable_snd : + Measurable fun t : (α × γ) × β ↦ (t.1.1, t.2))).inter + (hW.preimage (measurable_fst.snd.prodMk measurable_snd : + Measurable fun t : (α × γ) × β ↦ (t.1.2, t.2)))) + +/-- Consider two countable collections of jointly measurable families of sets `V i x` and +`W i' z` such that for almost all `x`, almost every `y` belongs to some `V i x`, and for almost +all `y`, for almost every `z`, `y` belongs to some `W i' z`. Then there are `i, i'` such that +the integral over `x` and `z` of the measure of `V i x ∩ W i' z` is positive. -/ +lemma exists_lintegral_measure_inter_pos {ι ι' : Type*} [Countable ι] [Countable ι'] + [SFinite φ] [SFinite ν] {V : ι → α → Set β} {W : ι' → γ → Set β} + (hV : ∀ i, MeasurableSet {q : α × β | q.2 ∈ V i q.1}) + (hW : ∀ i, MeasurableSet {q : γ × β | q.2 ∈ W i q.1}) + (hVae : ∀ᵐ x ∂μ, ∀ᵐ y ∂φ, ∃ i, y ∈ V i x) + (hWae : ∀ᵐ y ∂φ, ∀ᵐ z ∂ν, ∃ i, y ∈ W i z) + (hμ : μ ≠ 0) (hφ : φ ≠ 0) (hν : ν ≠ 0) : + ∃ i i', 0 < ∫⁻ x, ∫⁻ z, φ (V i x ∩ W i' z) ∂ν ∂μ := by + by_contra! h + have hm (i : ι) (i' : ι') : Measurable fun q : α × γ ↦ φ (V i q.1 ∩ W i' q.2) := + measurable_measure_inter_of_measurableSet (hV i) (hW i') + have : (ae μ).NeBot := ae_neBot.mpr hμ + have : (ae φ).NeBot := ae_neBot.mpr hφ + have : (ae ν).NeBot := ae_neBot.mpr hν + -- we can fix `x` such that for almost all `z`, the sets `V i x ∩ W i' z` have measure zero + have hx_ae : ∀ᵐ x ∂μ, ∀ᵐ z ∂ν, ∀ i i', φ (V i x ∩ W i' z) = 0 := by + simp_rw [ae_all_iff] + intro i i' + filter_upwards [(lintegral_eq_zero_iff (hm i i').lintegral_prod_right').mp + (nonpos_iff_eq_zero.mp (h i i'))] with x hx + exact (lintegral_eq_zero_iff ((hm i i').comp measurable_prodMk_left)).mp hx + obtain ⟨x, hx, hVx⟩ := (hx_ae.and hVae).exists + -- since the sets `V i x` cover almost all the space, the sets `W i' z` are almost empty + have h2 : ∀ᵐ z ∂ν, ∀ᵐ y ∂φ, ∀ i', y ∉ W i' z := by + filter_upwards [hx] with z hz + have h0 : φ (⋃ i, ⋃ i', V i x ∩ W i' z) = 0 := + measure_iUnion_null fun i ↦ measure_iUnion_null fun i' ↦ hz i i' + filter_upwards [hVx, measure_eq_zero_iff_ae_notMem.mp h0] with y ⟨i, hy⟩ hy' i' hi' + exact hy' (mem_iUnion₂.mpr ⟨i, i', hy, hi'⟩) + -- this contradicts the assumption on `W` after exchanging the two quantifiers + rw [Measure.ae_ae_comm] at h2 + swap + · simp only [ofPred_forall] + exact MeasurableSet.iInter fun i' ↦ (hW i').compl + obtain ⟨y, hy, hWy⟩ := (h2.and hWae).exists + obtain ⟨z, hz, i', hz'⟩ := (hy.and hWy).exists + exact hz i' hz' + +end MeasureTheory diff --git a/RandomDo/ForMathlib/MeasureTheory/Measure/SeparableMeasure.lean b/RandomDo/ForMathlib/MeasureTheory/Measure/SeparableMeasure.lean new file mode 100644 index 0000000..f45f772 --- /dev/null +++ b/RandomDo/ForMathlib/MeasureTheory/Measure/SeparableMeasure.lean @@ -0,0 +1,99 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.MeasureTheory.Measure.SeparableMeasure +public import RandomDo.ForMathlib.MeasureTheory.Integral.Lebesgue.Markov +public import RandomDo.ForMathlib.MeasureTheory.Measure.Basic +public import RandomDo.ForMathlib.MeasureTheory.Measure.Prod + +/-! +# Uniform lower bounds on the measure of intersections + +## Main statements + +* `exists_measurableSet_forall_le_measure_inter`: for jointly measurable families of sets `V x` + and `W z` and a separable finite measure `φ`, if the integral over + `x` and `z` of the measure of `V x ∩ W z` is positive, then there are sets `C` and `D` of + positive measure such that the measure of `V x ∩ W z` is bounded from below uniformly over + `x ∈ C` and `z ∈ D`. This replaces the use of a differentiation theorem for measures in the + classical proof of the existence of small sets for irreducible kernels. +-/ + +@[expose] public section + +open Set + +open scoped ENNReal NNReal symmDiff + +namespace MeasureTheory + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ : Measure α} {φ : Measure β} {ν : Measure γ} + +/-- Consider two jointly measurable families of sets `V x` and `W z` and a separable finite +measure `φ`, such that the integral over `x` and `z` of the measure of +`V x ∩ W z` is positive. Then there are sets `C` and `D` of positive measure such that the measure +of `V x ∩ W z` is bounded from below uniformly over `x ∈ C` and `z ∈ D`. -/ +lemma exists_measurableSet_forall_le_measure_inter [IsSeparable φ] [IsFiniteMeasure φ] + [SFinite ν] {V : α → Set β} {W : γ → Set β} + (hV : MeasurableSet {q : α × β | q.2 ∈ V q.1}) (hW : MeasurableSet {q : γ × β | q.2 ∈ W q.1}) + (h : 0 < ∫⁻ x, ∫⁻ z, φ (V x ∩ W z) ∂ν ∂μ) : + ∃ (C : Set α) (D : Set γ) (δ : ℝ≥0), MeasurableSet C ∧ MeasurableSet D ∧ 0 < μ C ∧ 0 < ν D ∧ + 0 < δ ∧ ∀ x ∈ C, ∀ z ∈ D, (δ : ℝ≥0∞) ≤ φ (V x ∩ W z) := by + have hm : Measurable fun q : α × γ ↦ φ (V q.1 ∩ W q.2) := + measurable_measure_inter_of_measurableSet hV hW + -- the set `G` of pairs `(x, z)` such that `5 * δ < φ (V x ∩ W z)` has positive measure + rw [← lintegral_prod (fun q : α × γ ↦ φ (V q.1 ∩ W q.2)) hm.aemeasurable] at h + obtain ⟨ε, hε, hG⟩ := exists_pos_measure_lt_of_lintegral_pos h + obtain ⟨δ, hδ, rfl⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ 5 * δ = ε := ⟨ε / 5, by positivity, by field_simp⟩ + set G : Set (α × γ) := {q | ((5 * δ : ℝ≥0) : ℝ≥0∞) < φ (V q.1 ∩ W q.2)} + -- `P S` and `Q S` are the sets of points `x`, `z` such that `V x`, `W z` are `δ`-close to `S` + obtain ⟨𝒜, h𝒜c, h𝒜⟩ := exists_countable_measureDense (μ := φ) + let P : Set β → Set α := fun S ↦ {x | φ (V x ∆ S) < δ} + let Q : Set β → Set γ := fun S ↦ {z | φ (W z ∆ S) < δ} + have hP (S : Set β) (hS : S ∈ 𝒜) : MeasurableSet (P S) := + measurableSet_lt (measurable_measure_symmDiff_of_measurableSet hV (h𝒜.measurable S hS)) + measurable_const + have hQ (S : Set β) (hS : S ∈ 𝒜) : MeasurableSet (Q S) := + measurableSet_lt (measurable_measure_symmDiff_of_measurableSet hW (h𝒜.measurable S hS)) + measurable_const + have hPcov (x : α) : ∃ S ∈ 𝒜, x ∈ P S := by + obtain ⟨S, hS, hxS⟩ := h𝒜.approx (V x) (measurable_prodMk_left hV) (measure_ne_top _ _) δ hδ + exact ⟨S, hS, (by simpa using hxS : φ (V x ∆ S) < δ)⟩ + have hQcov (z : γ) : ∃ S ∈ 𝒜, z ∈ Q S := by + obtain ⟨S, hS, hzS⟩ := h𝒜.approx (W z) (measurable_prodMk_left hW) (measure_ne_top _ _) δ hδ + exact ⟨S, hS, (by simpa using hzS : φ (W z ∆ S) < δ)⟩ + -- the countably many rectangles `P S ×ˢ Q S'` cover `G`, hence one of them meets `G` on a set + -- of positive measure + obtain ⟨⟨S, S'⟩, ⟨hS, hS'⟩, hpos⟩ : ∃ T ∈ 𝒜 ×ˢ 𝒜, 0 < (μ.prod ν) (G ∩ P T.1 ×ˢ Q T.2) := by + by_contra! hcon + refine hG.ne' (measure_mono_null (t := ⋃ T ∈ 𝒜 ×ˢ 𝒜, G ∩ P T.1 ×ˢ Q T.2) (fun q hq ↦ ?_) ?_) + · obtain ⟨S, hS, hxS⟩ := hPcov q.1 + obtain ⟨S', hS', hzS'⟩ := hQcov q.2 + exact mem_iUnion₂.mpr ⟨(S, S'), ⟨hS, hS'⟩, hq, hxS, hzS'⟩ + · exact (measure_biUnion_null_iff (h𝒜c.prod h𝒜c)).mpr + fun T hT ↦ nonpos_iff_eq_zero.mp (hcon T hT) + have hrect : 0 < μ (P S) * ν (Q S') := by + rw [← Measure.prod_prod] + exact hpos.trans_le (measure_mono inter_subset_right) + obtain ⟨⟨x₀, z₀⟩, hq₀, hx₀, hz₀⟩ := nonempty_of_measure_ne_zero hpos.ne' + refine ⟨P S, Q S', δ, hP S hS, hQ S' hS', pos_of_mul_pos_left hrect zero_le, + pos_of_mul_pos_right hrect zero_le, hδ, fun x hx z hz ↦ ?_⟩ + -- for `x ∈ P S` and `z ∈ Q S'`, the set `V x ∩ W z` is `4 * δ`-close to `V x₀ ∩ W z₀` + by_contra! hlt + refine lt_asymm (a := ((5 * δ : ℝ≥0) : ℝ≥0∞)) hq₀ ?_ + calc φ (V x₀ ∩ W z₀) + _ ≤ φ (V x ∩ W z) + (φ (V x₀ ∆ S) + φ (V x ∆ S)) + (φ (W z₀ ∆ S') + φ (W z ∆ S')) := + measure_inter_le_measure_inter_add_symmDiff .. + _ < δ + (δ + δ) + (δ + δ) := + ENNReal.add_lt_add (ENNReal.add_lt_add hlt (ENNReal.add_lt_add hx₀ hx)) + (ENNReal.add_lt_add hz₀ hz) + _ = ((5 * δ : ℝ≥0) : ℝ≥0∞) := by + push_cast + ring + +end MeasureTheory diff --git a/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/DataProcessing.lean b/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/DataProcessing.lean new file mode 100644 index 0000000..ec9cc07 --- /dev/null +++ b/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/DataProcessing.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.MeasureTheory.Measure.TotalVariation.Basic +public import Mathlib.Probability.Kernel.Composition.MeasureComp +public import RandomDo.ForMathlib.MeasureTheory.Measure.TotalVariation.Defs + +/-! +# Data-processing inequality for the total variation distance + +## Main statements + +* `etvDist_comp_le`, `tvDist_comp_le`: **data-processing inequality** for the total variation + distance, `etvDist (κ ∘ₘ μ) (κ ∘ₘ ν) ≤ etvDist μ ν` for a Markov kernel `κ`. +-/ + +@[expose] public section + +open ProbabilityTheory + +open scoped ENNReal + +namespace MeasureTheory + +variable {𝓧 𝓨 : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} + +/-- **Data-processing inequality** for the total variation distance: composition with a Markov +kernel does not increase the distance. -/ +lemma etvDist_comp_le (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] (μ ν : Measure 𝓧) : + etvDist (κ ∘ₘ μ) (κ ∘ₘ ν) ≤ etvDist μ ν := by + by_cases h : IsFiniteMeasure μ ∧ IsFiniteMeasure ν + swap; · simp [etvDist_of_not_isFiniteMeasure h] + obtain ⟨_, _⟩ := h + obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν + have hμ : μ = μ.restrict s + ν.restrict sᶜ + (μ.restrict sᶜ - ν.restrict sᶜ) := by + rw [add_assoc, add_comm (ν.restrict sᶜ), Measure.sub_add_cancel_of_le hs.ge_on_compl, + Measure.restrict_add_restrict_compl hs.measurableSet] + have hν : ν = μ.restrict s + ν.restrict sᶜ + (ν.restrict s - μ.restrict s) := by + rw [add_comm (μ.restrict s), add_assoc, add_comm (μ.restrict s), + Measure.sub_add_cancel_of_le hs.le_on, add_comm, + Measure.restrict_add_restrict_compl hs.measurableSet] + calc etvDist (κ ∘ₘ μ) (κ ∘ₘ ν) + _ = etvDist (κ ∘ₘ (μ.restrict s + ν.restrict sᶜ) + κ ∘ₘ (μ.restrict sᶜ - ν.restrict sᶜ)) + (κ ∘ₘ (μ.restrict s + ν.restrict sᶜ) + κ ∘ₘ (ν.restrict s - μ.restrict s)) := by + rw [← Measure.comp_add, ← Measure.comp_add, ← hμ, ← hν] + _ ≤ (κ ∘ₘ (μ.restrict sᶜ - ν.restrict sᶜ)) Set.univ + + (κ ∘ₘ (ν.restrict s - μ.restrict s)) Set.univ := etvDist_add_left_le _ _ _ + _ = ν s - μ s + (μ sᶜ - ν sᶜ) := by + rw [Measure.comp_apply_univ, Measure.comp_apply_univ, + Measure.sub_apply .univ hs.ge_on_compl, Measure.sub_apply .univ hs.le_on, add_comm] + simp + _ = etvDist μ ν := hs.etvDist_eq.symm + +/-- **Data-processing inequality** for the total variation distance: composition with a Markov +kernel does not increase the distance. -/ +lemma tvDist_comp_le (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] (μ ν : Measure 𝓧) : + tvDist (κ ∘ₘ μ) (κ ∘ₘ ν) ≤ tvDist μ ν := by + by_cases h : IsFiniteMeasure μ ∧ IsFiniteMeasure ν + · obtain ⟨_, _⟩ := h + exact ENNReal.toReal_mono (etvDist_ne_top μ ν) (etvDist_comp_le κ μ ν) + -- if `μ` or `ν` is not finite, neither is its image, and both distances are `(∞).toReal = 0` + · have h' : ¬ (IsFiniteMeasure (κ ∘ₘ μ) ∧ IsFiniteMeasure (κ ∘ₘ ν)) := by + rintro ⟨hμ, hν⟩ + refine h ⟨⟨?_⟩, ⟨?_⟩⟩ + · rw [← Measure.comp_apply_univ (κ := κ)] + exact measure_lt_top _ _ + · rw [← Measure.comp_apply_univ (κ := κ)] + exact measure_lt_top _ _ + rw [tvDist, etvDist_of_not_isFiniteMeasure h', ENNReal.toReal_top] + exact tvDist_nonneg + +end MeasureTheory diff --git a/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean b/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean new file mode 100644 index 0000000..f38836f --- /dev/null +++ b/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean @@ -0,0 +1,37 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs + +/-! +# Total variation distance of measures with a common part + +## Main statements + +* `etvDist_add_left_le`: `etvDist (ξ + μ) (ξ + ν) ≤ μ univ + ν univ`. +-/ + +@[expose] public section + +open scoped ENNReal + +namespace MeasureTheory + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} + +/-- If two measures have a common part `ξ`, their total variation distance is at most the sum of +the masses of the remaining parts. -/ +lemma etvDist_add_left_le (ξ μ ν : Measure 𝓧) [IsFiniteMeasure ξ] : + etvDist (ξ + μ) (ξ + ν) ≤ μ Set.univ + ν Set.univ := by + calc etvDist (ξ + μ) (ξ + ν) + _ ≤ etvDist (ξ + μ) ξ + etvDist ξ (ξ + ν) := etvDist_triangle _ _ _ + _ = μ Set.univ + ν Set.univ := by + rw [etvDist_of_ge (Measure.le_add_right le_rfl), etvDist_of_le (Measure.le_add_right le_rfl), + Measure.add_apply, Measure.add_apply, ENNReal.add_sub_cancel_left (measure_ne_top _ _), + ENNReal.add_sub_cancel_left (measure_ne_top _ _)] + +end MeasureTheory diff --git a/RandomDo/ForMathlib/NumberTheory/FrobeniusNumber.lean b/RandomDo/ForMathlib/NumberTheory/FrobeniusNumber.lean new file mode 100644 index 0000000..a3f22a6 --- /dev/null +++ b/RandomDo/ForMathlib/NumberTheory/FrobeniusNumber.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.NumberTheory.FrobeniusNumber + +/-! +# Sets of natural numbers closed under addition + +## Main statements + +* `Nat.exists_forall_ge_mem_of_setGcd_eq_one`: a set of natural numbers which is closed under + addition and whose greatest common divisor is 1 contains all large enough natural numbers. +-/ + +@[expose] public section + +namespace Nat + +/-- A set of natural numbers which is closed under addition and whose greatest common divisor +is 1 contains all large enough natural numbers. -/ +lemma exists_forall_ge_mem_of_setGcd_eq_one {s : Set ℕ} + (hadd : ∀ a ∈ s, ∀ b ∈ s, a + b ∈ s) (hs : Nat.setGcd s = 1) : ∃ N, ∀ n ≥ N, n ∈ s := by + obtain ⟨N, hN⟩ := Nat.exists_mem_closure_of_ge s + have hsub : ∀ m ∈ AddSubmonoid.closure s, m = 0 ∨ m ∈ s := by + intro m hm + induction hm using AddSubmonoid.closure_induction with + | mem m hm => exact .inr hm + | zero => exact .inl rfl + | add a b _ _ ha hb => + rcases ha with rfl | ha + · simpa using hb + · rcases hb with rfl | hb + · simpa using Or.inr ha + · exact .inr (hadd a ha b hb) + refine ⟨max N 1, fun n hn ↦ ?_⟩ + rcases hsub n (hN n (le_of_max_le_left hn) (by simp [hs])) with rfl | h + · simp at hn + · exact h + +end Nat diff --git a/RandomDo/ForMathlib/Probability/Kernel/Aperiodic.lean b/RandomDo/ForMathlib/Probability/Kernel/Aperiodic.lean new file mode 100644 index 0000000..59d4f51 --- /dev/null +++ b/RandomDo/ForMathlib/Probability/Kernel/Aperiodic.lean @@ -0,0 +1,216 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import RandomDo.ForMathlib.NumberTheory.FrobeniusNumber +public import RandomDo.ForMathlib.Probability.Kernel.Irreducible +public import RandomDo.ForMathlib.Probability.Kernel.SmallSet.Basic + +/-! +# Aperiodic kernels + +A kernel `κ : Kernel α α` is *periodic* with respect to a measure `π` if the space contains a +cycle of `d ≥ 2` disjoint measurable sets `D 0, ..., D (d - 1)`, the first of which has positive +`π`-measure, such that `κ` sends every point of `D i` to `D (i + 1)` almost surely. It is +*aperiodic* if it is not periodic. + +## Main definitions + +* `ProbabilityTheory.Kernel.IsAperiodic κ π`: the kernel `κ` has no cyclic decomposition of + period at least 2 charged by `π`. + +## Main statements + +* `ProbabilityTheory.Kernel.IsAperiodic.exists_forall_pow_comp_apply_pos`: if `κ` is an + irreducible aperiodic Markov kernel and `C` is a `(k, ν)`-small set, then `C` is reached from + `ν` with positive probability in `n` steps for all `n` large enough. +* `ProbabilityTheory.Kernel.IsAperiodic.exists_forall_pow_apply_pos`: if `κ` is an irreducible + aperiodic Markov kernel and `C` is a small set, then every point reaches `C` with positive + probability in `n` steps for all `n` large enough. + +## References + +* [G. O. Roberts, J. S. Rosenthal, *General state space Markov chains and MCMC algorithms*, + Probability Surveys, 2004][robertsrosenthal2004] +-/ + +@[expose] public section + +open MeasureTheory Function + +open scoped ENNReal ProbabilityTheory + +namespace ProbabilityTheory.Kernel + +variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {φ π ν : Measure α} + +/-- A kernel `κ : Kernel α α` is aperiodic with respect to a measure `π` if there is no cycle of +`d ≥ 2` pairwise disjoint measurable sets `D 0, ..., D (d - 1)` with `π (D 0) > 0`, such that +`κ` sends every point of `D i` to `D (i + 1)` almost surely (indices are taken modulo `d`). +Ref. *Roberts-Rosenthal*, Section 3.2. -/ +def IsAperiodic (κ : Kernel α α) (π : Measure α) : Prop := + ∀ (d : ℕ) (D : Fin (d + 2) → Set α), (∀ i, MeasurableSet (D i)) → Pairwise (Disjoint on D) → + (∀ i, ∀ x ∈ D i, κ x (D (i + 1)) = 1) → π (D 0) = 0 + +/-- For an aperiodic kernel, all the sets of a cyclic decomposition have measure zero, not only +the first one. -/ +lemma IsAperiodic.measure_eq_zero (hκ : κ.IsAperiodic π) {d : ℕ} {D : Fin (d + 2) → Set α} + (hD : ∀ i, MeasurableSet (D i)) (hdisj : Pairwise (Disjoint on D)) + (h : ∀ i, ∀ x ∈ D i, κ x (D (i + 1)) = 1) (i : Fin (d + 2)) : + π (D i) = 0 := by + have h0 := hκ d (fun j ↦ D (i + j)) (fun j ↦ hD _) + (hdisj.comp_of_injective (add_right_injective i)) + (fun j x hx ↦ by rw [← add_assoc]; exact h _ x hx) + simpa using h0 + +/-- If a measurable set `S` is a null set for all the measures `(κ ^ m) ∘ₘ ν`, then it is +contained in a measurable `ν`-null set `B` whose complement is absorbing for `κ`: `κ y B = 0` for +all `y ∉ B`. -/ +lemma exists_measurableSet_superset_forall_notMem_apply_eq_zero {S : Set α} + (hS : MeasurableSet S) (h : ∀ m : ℕ, ((κ ^ m) ∘ₘ ν) S = 0) : + ∃ B, MeasurableSet B ∧ S ⊆ B ∧ ν B = 0 ∧ ∀ y ∉ B, κ y B = 0 := by + refine ⟨⋃ m : ℕ, {y | 0 < (κ ^ m) y S}, .iUnion fun m ↦ measurableSet_apply_pos _ hS, + fun y hy ↦ Set.mem_iUnion.mpr ⟨0, ?_⟩, ?_, fun y hy ↦ ?_⟩ + · rw [Set.mem_ofPred_eq, pow_zero_apply, Measure.dirac_apply_of_mem hy] + exact zero_lt_one + · rw [measure_iUnion_null_iff] + exact fun m ↦ (Measure.comp_apply_eq_zero_iff hS).mp (h m) + · rw [measure_iUnion_null_iff] + intro m + rw [← Measure.comp_apply_eq_zero_iff hS, ← pow_succ_apply] + simp only [Set.mem_iUnion, Set.mem_ofPred_eq, not_exists, not_lt, nonpos_iff_eq_zero] at hy + exact hy (m + 1) + +open Fin.NatCast in +/-- Let `E : ℕ → Set α` be a family of measurable sets covering the space such that every point +which is sent to `E n` by `κ` with positive probability belongs to `E (n + 1)`. Let `B` be a +measurable set whose complement is absorbing for `κ` and which contains all the intersections +`E n₁ ∩ E n₂` for `n₁` and `n₂` not congruent modulo `d + 2`. If `κ` is aperiodic with respect to +`π`, then the complement of `B` is a `π`-null set. + +Indeed, the sets `{y ∉ B | ∃ n, y ∈ E n ∧ d + 2 ∣ n + i}` for `i : Fin (d + 2)` form a cyclic +decomposition of the complement of `B`. -/ +lemma IsAperiodic.measure_compl_eq_zero_of_inter_subset [IsMarkovKernel κ] + (hκ : κ.IsAperiodic π) {d : ℕ} {E : ℕ → Set α} (hE : ∀ n, MeasurableSet (E n)) + (hcov : ∀ y, ∃ n, y ∈ E n) (hstep : ∀ y n, 0 < κ y (E n) → y ∈ E (n + 1)) + {B : Set α} (hB : MeasurableSet B) (hBabs : ∀ y ∉ B, κ y B = 0) + (hEB : ∀ n₁ n₂, ¬ n₁ ≡ n₂ [MOD d + 2] → E n₁ ∩ E n₂ ⊆ B) : + π Bᶜ = 0 := by + have hcast {n₁ n₂ : ℕ} (h : (n₁ : Fin (d + 2)) ≠ n₂) : E n₁ ∩ E n₂ ⊆ B := + hEB n₁ n₂ fun h' ↦ h (Fin.ext (by simpa [Nat.ModEq] using h')) + let D : Fin (d + 2) → Set α := fun i ↦ (⋃ n : ℕ, ⋃ (_ : (n : Fin (d + 2)) + i = 0), E n) \ B + have hD_mem (i : Fin (d + 2)) (y : α) : + y ∈ D i ↔ y ∉ B ∧ ∃ n : ℕ, (n : Fin (d + 2)) + i = 0 ∧ y ∈ E n := by + simp [D, and_comm] + have hD (i : Fin (d + 2)) : MeasurableSet (D i) := + (MeasurableSet.iUnion fun n ↦ .iUnion fun _ ↦ hE n).diff hB + have hdisj : Pairwise (Disjoint on D) := by + intro i j hij + rw [Function.onFun, Set.disjoint_left] + intro y hyi hyj + obtain ⟨hyB, n, hn, hyn⟩ := (hD_mem i y).mp hyi + obtain ⟨-, n', hn', hyn'⟩ := (hD_mem j y).mp hyj + refine hyB (hcast (fun h ↦ hij ?_) ⟨hyn, hyn'⟩) + rw [h] at hn + exact add_left_cancel (hn.trans hn'.symm) + have hD_step (i : Fin (d + 2)) (y : α) (hy : y ∈ D i) : κ y (D (i + 1)) = 1 := by + obtain ⟨hyB, n₀, hn₀, hyn₀⟩ := (hD_mem i y).mp hy + rw [← prob_compl_eq_zero_iff (hD _)] + have hsub : (D (i + 1))ᶜ ⊆ B ∪ ⋃ n : ℕ, ⋃ (_ : (n : Fin (d + 2)) + (i + 1) ≠ 0), E n := by + intro z hz + by_cases hzB : z ∈ B + · exact .inl hzB + obtain ⟨n, hn⟩ := hcov z + exact .inr (Set.mem_iUnion₂.mpr ⟨n, fun h ↦ hz ((hD_mem _ z).mpr ⟨hzB, n, h, hn⟩), hn⟩) + refine measure_mono_null hsub (measure_union_null (hBabs y hyB) ?_) + simp only [measure_iUnion_null_iff] + intro n hn + by_contra hpos + refine hyB (hcast (fun h ↦ hn ?_) ⟨hstep y n (pos_iff_ne_zero.mpr hpos), hyn₀⟩) + rw [← hn₀, ← h, Nat.cast_succ, add_assoc, add_comm 1 i] + refine measure_mono_null (fun y hy ↦ ?_) + (measure_iUnion_null (hκ.measure_eq_zero hD hdisj hD_step)) + obtain ⟨n, hn⟩ := hcov y + exact Set.mem_iUnion.mpr ⟨-(n : Fin (d + 2)), (hD_mem _ y).mpr ⟨hy, n, add_neg_cancel _, hn⟩⟩ + +/-- Let `E : ℕ → Set α` be a family of measurable sets covering the space such that every point +which is sent to `E n` by `κ` with positive probability belongs to `E (n + 1)`. If `κ` is +aperiodic with respect to `π` and `ν ≪ π` is a nonzero measure then for every `d`, there are +`n₁` and `n₂` not congruent modulo `d + 2` such that `E n₁ ∩ E n₂` has positive measure for one of +the measures `(κ ^ m) ∘ₘ ν`. -/ +lemma IsAperiodic.exists_pow_comp_inter_pos [IsMarkovKernel κ] (hκ : κ.IsAperiodic π) + (hν : ν ≠ 0) (hνπ : ν ≪ π) {E : ℕ → Set α} (hE : ∀ n, MeasurableSet (E n)) + (hcov : ∀ y, ∃ n, y ∈ E n) (hstep : ∀ y n, 0 < κ y (E n) → y ∈ E (n + 1)) (d : ℕ) : + ∃ m n₁ n₂ : ℕ, ¬ n₁ ≡ n₂ [MOD d + 2] ∧ 0 < ((κ ^ m) ∘ₘ ν) (E n₁ ∩ E n₂) := by + by_contra! h + simp only [nonpos_iff_eq_zero] at h + obtain ⟨B, hB, hSB, hνB, hBabs⟩ := exists_measurableSet_superset_forall_notMem_apply_eq_zero + (κ := κ) (ν := ν) (S := ⋃ n₁, ⋃ n₂, ⋃ (_ : ¬ n₁ ≡ n₂ [MOD d + 2]), E n₁ ∩ E n₂) + (.iUnion fun n₁ ↦ .iUnion fun n₂ ↦ .iUnion fun _ ↦ (hE n₁).inter (hE n₂)) + (fun m ↦ by simpa only [measure_iUnion_null_iff] using h m) + have hπB : π Bᶜ = 0 := + hκ.measure_compl_eq_zero_of_inter_subset (d := d) hE hcov hstep hB hBabs fun n₁ n₂ hn y hy ↦ + hSB (Set.mem_iUnion₂.mpr ⟨n₁, n₂, Set.mem_iUnion.mpr ⟨hn, hy⟩⟩) + refine hν (Measure.measure_univ_eq_zero.mp ?_) + rw [← Set.union_compl_self B] + exact measure_union_null hνB (hνπ hπB) + +/-- If `κ` is a `φ`-irreducible Markov kernel which is aperiodic with respect to `π`, and `C` is a +`(k, ν)`-small set with `ν ≪ π` and `φ C > 0`, then starting from `ν`, the set `C` is reached +with positive probability in `n` steps for all `n` large enough. -/ +lemma IsAperiodic.exists_forall_pow_comp_apply_pos [IsMarkovKernel κ] [IsIrreducible φ κ] + (hκ : κ.IsAperiodic π) {C : Set α} (hC : MeasurableSet C) (hφC : 0 < φ C) {k : ℕ} + (hk : 0 < k) (hν : ν ≠ 0) (hνπ : ν ≪ π) (hsmall : IsSmallSet κ C k ν) : + ∃ N : ℕ, ∀ n ≥ N, 0 < ((κ ^ n) ∘ₘ ν) C := by + -- the set of times at which `C` is reached from `ν`, shifted by `k`, is closed under addition + let T : Set ℕ := (· + k) '' {n : ℕ | 0 < ((κ ^ n) ∘ₘ ν) C} + have hT_add : ∀ a ∈ T, ∀ b ∈ T, a + b ∈ T := by + rintro _ ⟨m, hm, rfl⟩ _ ⟨n, hn, rfl⟩ + exact ⟨m + k + n, hsmall.pow_comp_apply_pos_of_pow_comp_apply_pos hC hn hm, by ring⟩ + -- it suffices to prove that its gcd is 1 + suffices hgcd : Nat.setGcd T = 1 by + obtain ⟨N, hN⟩ := Nat.exists_forall_ge_mem_of_setGcd_eq_one hT_add hgcd + refine ⟨N, fun n hn ↦ ?_⟩ + obtain ⟨m, hm, hmn⟩ := hN (n + k) (by omega) + obtain rfl : m = n := by simpa using hmn + exact hm + by_contra hgcd + obtain ⟨n₀, hn₀⟩ := IsIrreducible.exists_pow_comp_apply_pos (φ := φ) (κ := κ) hC hφC hν + have h0 : Nat.setGcd T ≠ 0 := by + rw [Ne, Nat.setGcd_eq_zero_iff] + intro h + have : n₀ + k = 0 := h ⟨n₀, hn₀, rfl⟩ + omega + obtain ⟨d, hd⟩ : ∃ d, Nat.setGcd T = d + 2 := ⟨Nat.setGcd T - 2, by omega⟩ + have hdvd (n : ℕ) (hn : 0 < ((κ ^ n) ∘ₘ ν) C) : d + 2 ∣ n + k := + hd ▸ Nat.setGcd_dvd_of_mem ⟨n, hn, rfl⟩ + -- otherwise, we get two times with different phases reachable from the same points + obtain ⟨m, n₁, n₂, hne, hpos⟩ := hκ.exists_pow_comp_inter_pos hν hνπ + (E := fun n ↦ {y | 0 < (κ ^ n) y C}) (fun n ↦ measurableSet_apply_pos _ hC) + (IsIrreducible.irreducible (φ := φ) hC hφC) (fun y n h ↦ (pow_succ_apply_pos_iff hC).mpr h) d + have h₁ : d + 2 ∣ n₁ + m + k := hdvd _ ((pow_add_comp_apply_pos_iff hC).mpr + (hpos.trans_le (measure_mono Set.inter_subset_left))) + have h₂ : d + 2 ∣ n₂ + m + k := hdvd _ ((pow_add_comp_apply_pos_iff hC).mpr + (hpos.trans_le (measure_mono Set.inter_subset_right))) + have h₁₂ : n₁ + m + k ≡ n₂ + m + k [MOD d + 2] := + ((Nat.modEq_zero_iff_dvd).mpr h₁).trans ((Nat.modEq_zero_iff_dvd).mpr h₂).symm + exact hne (Nat.ModEq.add_right_cancel' _ (Nat.ModEq.add_right_cancel' _ h₁₂)) + +/-- If `κ` is a `φ`-irreducible Markov kernel which is aperiodic with respect to `π`, and `C` is a +`(k, ν)`-small set with `ν ≪ π` and `φ C > 0`, then from every point `x`, the set `C` is reached +with positive probability in `n` steps for all `n` large enough. +Ref. *Roberts-Rosenthal*, proof of Theorem 4. -/ +theorem IsAperiodic.exists_forall_pow_apply_pos [IsMarkovKernel κ] [IsIrreducible φ κ] + (hκ : κ.IsAperiodic π) {C : Set α} (hC : MeasurableSet C) (hφC : 0 < φ C) {k : ℕ} + (hk : 0 < k) (hν : ν ≠ 0) (hνπ : ν ≪ π) (hsmall : IsSmallSet κ C k ν) (x : α) : + ∃ N, ∀ n ≥ N, 0 < (κ ^ n) x C := by + obtain ⟨N, hN⟩ := hκ.exists_forall_pow_comp_apply_pos hC hφC hk hν hνπ hsmall + obtain ⟨n₁, hn₁⟩ := IsIrreducible.irreducible (φ := φ) (κ := κ) hC hφC x + refine ⟨N + k + n₁, fun n hn ↦ ?_⟩ + obtain ⟨m, rfl⟩ : ∃ m, n = m + k + n₁ := ⟨n - (k + n₁), by omega⟩ + exact hsmall.pow_apply_pos_of_pow_comp_apply_pos hn₁ (hN m (by omega)) + +end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/Composition/MeasureComp.lean b/RandomDo/ForMathlib/Probability/Kernel/Composition/MeasureComp.lean new file mode 100644 index 0000000..642ef83 --- /dev/null +++ b/RandomDo/ForMathlib/Probability/Kernel/Composition/MeasureComp.lean @@ -0,0 +1,102 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.Probability.Kernel.Composition.MeasureComp + +/-! +# Lemmas about the composition of a measure and a kernel + +## Main statements + +* `Measure.comp_le_comp_right`, `Measure.comp_le_comp_left`: monotonicity of `κ ∘ₘ μ` in the + measure and in the kernel. +* `Measure.restrict_comp`: `(κ.restrict hs) ∘ₘ μ = (κ ∘ₘ μ).restrict s`. +* `Measure.comp_apply_pos_iff`: `0 < (η ∘ₘ μ) s ↔ 0 < μ {a | 0 < η a s}`. +* `Measure.withDensity_lintegral_mul_le_comp`: Chapman-Kolmogorov inequality for densities. +-/ + +@[expose] public section + +open ProbabilityTheory + +open scoped ENNReal + +namespace ProbabilityTheory.Kernel + +variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} + +/-- The set of points `a` such that `η a s` is positive is measurable. -/ +lemma measurableSet_apply_pos (η : Kernel α β) (hs : MeasurableSet s) : + MeasurableSet {a | 0 < η a s} := + measurableSet_lt measurable_const (η.measurable_coe hs) + +end ProbabilityTheory.Kernel + +namespace MeasureTheory.Measure + +variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {μ ν : Measure α} {κ η : Kernel α β} {s : Set β} + +@[gcongr] +lemma comp_le_comp_right (h : μ ≤ ν) (κ : Kernel α β) : κ ∘ₘ μ ≤ κ ∘ₘ ν := by + refine Measure.le_iff.mpr fun s hs ↦ ?_ + rw [Measure.bind_apply hs κ.aemeasurable, Measure.bind_apply hs κ.aemeasurable] + exact lintegral_mono' h le_rfl + +lemma comp_le_comp_left (μ : Measure α) (h : κ ≤ η) : κ ∘ₘ μ ≤ η ∘ₘ μ := by + refine Measure.le_iff.mpr fun s hs ↦ ?_ + rw [Measure.bind_apply hs κ.aemeasurable, Measure.bind_apply hs η.aemeasurable] + exact lintegral_mono fun a ↦ h a s + +lemma comp_le_comp (hμν : μ ≤ ν) (h : κ ≤ η) : κ ∘ₘ μ ≤ η ∘ₘ ν := + (comp_le_comp_left μ h).trans (comp_le_comp_right hμν η) + +lemma restrict_comp (hs : MeasurableSet s) : (κ.restrict hs) ∘ₘ μ = (κ ∘ₘ μ).restrict s := by + rw [comp_eq_comp_const_apply, Kernel.comp_restrict, Kernel.restrict_apply, + ← comp_eq_comp_const_apply] + +/-- The measure `η ∘ₘ μ` gives positive mass to a measurable set `s` iff the set of points `a` +such that `η a s` is positive has positive `μ`-measure. -/ +lemma comp_apply_pos_iff (hs : MeasurableSet s) : + 0 < (η ∘ₘ μ) s ↔ 0 < μ {a | 0 < η a s} := by + rw [Measure.bind_apply hs η.aemeasurable, lintegral_pos_iff_support (η.measurable_coe hs)] + congr! 2 + ext a + simp [pos_iff_ne_zero] + +/-- The measure `η ∘ₘ μ` gives zero mass to a measurable set `s` iff the set of points `a` +such that `η a s` is positive has `μ`-measure zero. -/ +lemma comp_apply_eq_zero_iff (hs : MeasurableSet s) : + (η ∘ₘ μ) s = 0 ↔ μ {a | 0 < η a s} = 0 := by + rw [← not_iff_not, ← Ne, ← Ne, ← pos_iff_ne_zero, ← pos_iff_ne_zero, comp_apply_pos_iff hs] + +/-- Chapman-Kolmogorov inequality for densities: if a measure `μ` dominates the measure with +density `p` with respect to `φ` and a kernel `η` dominates the kernel with density `q` with respect +to `ψ`, then `η ∘ₘ μ` dominates the measure with density `z ↦ ∫⁻ y, p y * q y z ∂φ` with respect +to `ψ`. -/ +lemma withDensity_lintegral_mul_le_comp {μ φ : Measure α} {ψ : Measure β} [SFinite φ] [SFinite ψ] + {η : ProbabilityTheory.Kernel α β} {p : α → ℝ≥0∞} {q : α → β → ℝ≥0∞} + (hp : Measurable p) (hq : Measurable (Function.uncurry q)) + (hpμ : φ.withDensity p ≤ μ) (hqη : ∀ y, ψ.withDensity (q y) ≤ η y) : + ψ.withDensity (fun z ↦ ∫⁻ y, p y * q y z ∂φ) ≤ η ∘ₘ μ := by + refine Measure.le_iff.mpr fun B hB ↦ ?_ + rw [withDensity_apply _ hB, Measure.bind_apply hB η.aemeasurable] + calc ∫⁻ z in B, ∫⁻ y, p y * q y z ∂φ ∂ψ + _ = ∫⁻ y, ∫⁻ z in B, p y * q y z ∂ψ ∂φ := + lintegral_lintegral_swap + ((hp.comp measurable_snd).mul (hq.comp measurable_swap)).aemeasurable + _ = ∫⁻ y, p y * ψ.withDensity (q y) B ∂φ := by + congr with y + rw [lintegral_const_mul _ hq.of_uncurry_left, withDensity_apply _ hB] + _ ≤ ∫⁻ y, p y * η y B ∂φ := by + gcongr with y + exact hqη y + _ = ∫⁻ y, η y B ∂(φ.withDensity p) := + (lintegral_withDensity_eq_lintegral_mul _ hp (η.measurable_coe hB)).symm + _ ≤ ∫⁻ y, η y B ∂μ := lintegral_mono' hpμ le_rfl + +end MeasureTheory.Measure diff --git a/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean b/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean new file mode 100644 index 0000000..1c39bf0 --- /dev/null +++ b/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean @@ -0,0 +1,768 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import LeanMachineLearning.ForMathlib.Probability.Kernel.KernelSub +public import RandomDo.ForMathlib.MeasureTheory.Measure.TotalVariation.DataProcessing +public import RandomDo.ForMathlib.Probability.Kernel.Aperiodic +public import RandomDo.ForMathlib.Probability.Kernel.HarrisRecurrent +public import RandomDo.ForMathlib.Probability.Kernel.Invariance +public import RandomDo.ForMathlib.Probability.Kernel.SmallSet.Exists + +/-! +# Convergence in total variation of irreducible aperiodic Markov kernels + +Let `κ : Kernel α α` be a Markov kernel on a countably generated measurable space, with an +invariant probability measure `π`. If `κ` is irreducible and aperiodic, then for `π`-almost every +`x`, the law `(κ ^ n) x` at time `n` of the Markov chain with kernel `κ` started at `x` converges +to `π` in total variation. If `κ` is Harris recurrent, this holds for every `x`. A Harris recurrent +Markov kernel is irreducible (`Kernel.IsHarrisRecurrent.isIrreducible`), hence the statements for +Harris recurrent kernels do not assume irreducibility. + +Note that the total variation distance `tvDist` takes values in `[0, 2]` for probability measures: +it is twice the supremum over measurable sets of the difference of the measures. + +## Main statements + +* `Kernel.ae_tendsto_tvDist_pow_apply`: `tvDist ((κ ^ n) x) π` tends to zero for `π`-almost + every `x`. +* `Kernel.tendsto_tvDist_pow_comp`: `tvDist ((κ ^ n) ∘ₘ μ) π` tends to zero for every probability + measure `μ ≪ π`. +* `Kernel.IsHarrisRecurrent.tendsto_tvDist_pow_apply`: if `κ` is Harris recurrent, then + `tvDist ((κ ^ n) x) π` tends to zero for every `x`. +* `Kernel.IsHarrisRecurrent.tendsto_tvDist_pow_comp`: if `κ` is Harris recurrent, then + `tvDist ((κ ^ n) ∘ₘ μ) π` tends to zero for every probability measure `μ`. + +Each of these statements has a version for the extended distance `etvDist`. + +Intermediate results which do not mention irreducibility or aperiodicity: + +* `Kernel.exists_isSmallSet_measure_compl_le`: if a small set is reached from every point at all + large times, then there are small sets of `π`-measure arbitrarily close to full. +* `Kernel.tendsto_etvDist_pow_comp_of_le`: under the same assumption, `(κ ^ n) ∘ₘ a` tends to + `a univ • π` in total variation for every measure `a` dominated by a multiple of `π`. + +## Proof + +The proof does not use the law of the trajectories of the Markov chain: it only manipulates +measures and kernels. + +1. There is a small set `C` (`Kernel.exists_isSmallSet`), and by aperiodicity every point + reaches `C` with positive probability in `n` steps for all `n` large enough + (`Kernel.IsAperiodic.exists_forall_pow_apply_pos`). It follows that for every `θ > 0` there is a + small set `B` with `π Bᶜ ≤ θ` (`Kernel.exists_isSmallSet_measure_compl_le`). +2. Let `a ≤ K • π` be an initial measure. We write `(κ ^ (j * i)) ∘ₘ a` and `a univ • π` as sums of + a common part and of remainders with equal mass, which are still dominated by `K • π`. The + remainders give mass at most `K * θ` to `Bᶜ`, and their restrictions to the small set `B` have a + common part after `j` more steps. Hence the mass of the remainders decreases geometrically + with `i`, up to a term of order `K * θ` (`Kernel.etvDist_pow_comp_le`). Since `θ` is arbitrary, + `(κ ^ n) ∘ₘ a` tends to `a univ • π` (`Kernel.tendsto_etvDist_pow_comp_of_le`). +3. For a general starting point `x`, let `r i x` be the mass of `(κ ^ i) x - i • π`, the part of + `(κ ^ i) x` which is not dominated by `i • π`. It is nonincreasing in `i`, and its limit `ρ x` is + a subharmonic function of `x`: `ρ x ≤ ∫⁻ y, ρ y ∂κ x`. The existence of a small set gives + `ρ x < 1` for all `x`, and a subharmonic function of an irreducible kernel with an invariant + probability measure is almost everywhere less than any level which it does not exceed on a set of + positive measure (`Kernel.Invariant.ae_le_of_le_lintegral`). Hence `ρ ≤ t` almost everywhere for + some `t < 1`. Together with the inequality `ρ x ≤ ∫⁻ y, ρ y ∂((κ ^ i) x - i • π)`, this gives + `ρ x ≤ t * ρ x` and then `ρ x = 0` for almost every `x`. +4. If `ρ x = 0`, then `(κ ^ i) x` is the sum of a measure dominated by `i • π`, to which step 2 + applies, and of a measure with arbitrarily small mass. +5. If `κ` is Harris recurrent, then `ρ x = 0` for every `x`: by subharmonicity and since `ρ` + vanishes on a set `G` of positive measure, `ρ x` is at most the probability that the chain + started at `x` does not visit `G` during its first `n` steps, which tends to zero. + +## References + +* [Meyn, S.P. and Tweedie, R.L., *Markov Chains and Stochastic Stability*][meyntweedie1993] +* [G. O. Roberts, J. S. Rosenthal, *General state space Markov chains and MCMC algorithms*, + Probability Surveys, 2004][robertsrosenthal2004] +* [L. Tierney, *Markov chains for exploring posterior distributions*, Annals of Statistics, + 1994][tierney1994] +-/ + +@[expose] public section + +open MeasureTheory Filter Topology + +open scoped ENNReal NNReal ProbabilityTheory + +namespace ProbabilityTheory.Kernel + +variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {π ν : Measure α} + +/-! ### Small sets of large measure -/ + +/-- If every point reaches a small set `C` with positive probability in `n` steps for all `n` +large enough, then there are small sets of measure arbitrarily close to full, for any finite +measure `π`. -/ +lemma exists_isSmallSet_measure_compl_le [IsFiniteMeasure π] {C : Set α} + (hC : MeasurableSet C) {k : ℕ} (hsmall : IsSmallSet κ C k ν) + (hreach : ∀ x, ∃ N, ∀ n ≥ N, 0 < (κ ^ n) x C) {θ : ℝ≥0∞} (hθ : θ ≠ 0) : + ∃ (B : Set α) (j : ℕ) (δ : ℝ≥0∞), MeasurableSet B ∧ π Bᶜ ≤ θ ∧ δ ≠ 0 ∧ δ ≠ ∞ ∧ + IsSmallSet κ B j (δ • ν) := by + rcases eq_or_ne (π Set.univ) 0 with h0 | h0 + · exact ⟨∅, 0, 1, .empty, by simp [Measure.measure_univ_eq_zero.mp h0], one_ne_zero, + ENNReal.one_ne_top, fun x hx ↦ absurd hx (Set.notMem_empty x)⟩ + have hlt : π Set.univ - θ < π Set.univ := ENNReal.sub_lt_self (measure_ne_top _ _) h0 hθ + -- first, the points which reach `C` in `n` steps for all `n ≥ N` + let W : ℕ → Set α := fun N ↦ ⋂ n, ⋂ (_ : N ≤ n), {x | 0 < (κ ^ n) x C} + have hW_mono : Monotone W := fun N M hNM x hx ↦ by + simp only [W, Set.mem_iInter] at hx ⊢ + exact fun n hn ↦ hx n (hNM.trans hn) + have hW_univ : ⋃ N, W N = Set.univ := by + ext x + simpa [W] using hreach x + obtain ⟨N, hN⟩ : ∃ N, π Set.univ - θ < π (W N) := by + have h_tendsto := tendsto_measure_iUnion_atTop (μ := π) hW_mono + rw [hW_univ] at h_tendsto + exact (h_tendsto.eventually_const_lt hlt).exists + -- then the points which reach `C` in `N` steps with probability at least `1 / (i + 1)` + let V : ℕ → Set α := fun i ↦ {x | ((i : ℝ≥0∞) + 1)⁻¹ ≤ (κ ^ N) x C} + have hV_meas : ∀ i, MeasurableSet (V i) := + fun i ↦ measurableSet_le measurable_const ((κ ^ N).measurable_coe hC) + have hV_mono : Monotone V := fun i j hij x hx ↦ + (ENNReal.inv_le_inv.mpr (by gcongr : (i : ℝ≥0∞) + 1 ≤ j + 1)).trans hx + have hWV : W N ⊆ ⋃ i, V i := by + intro x hx + have hx_pos : 0 < (κ ^ N) x C := by + simp only [W, Set.mem_iInter] at hx + exact hx N le_rfl + obtain ⟨i, hi⟩ := ENNReal.exists_inv_nat_lt hx_pos.ne' + exact Set.mem_iUnion.mpr ⟨i, (ENNReal.inv_le_inv.mpr le_self_add).trans hi.le⟩ + obtain ⟨i, hi⟩ : ∃ i, π Set.univ - θ < π (V i) := + ((tendsto_measure_iUnion_atTop (μ := π) hV_mono).eventually_const_lt + (hN.trans_le (measure_mono hWV))).exists + refine ⟨V i, k + N, ((i : ℝ≥0∞) + 1)⁻¹, hV_meas i, ?_, by simp, by simp, fun x hx ↦ ?_⟩ + · rw [measure_compl (hV_meas i) (measure_ne_top _ _), tsub_le_iff_left] + exact tsub_le_iff_right.mp hi.le + · refine le_trans ?_ (hsmall.smul_le_pow_add_apply N x) + refine Measure.le_iff.mpr fun s _ ↦ ?_ + simp only [Measure.smul_apply, smul_eq_mul] + gcongr + exact hx + +/-! ### Convergence for initial measures dominated by the invariant measure -/ + +/-- Auxiliary lemma for `etvDist_pow_comp_le`. The measures `(κ ^ (j * i)) ∘ₘ a` and +`a univ • π` are the sums of a common part `g` and of remainders `a'` and `b'` whose mass +decreases geometrically with `i`, up to a small term. -/ +private lemma exists_split_pow_comp [IsMarkovKernel κ] [IsProbabilityMeasure π] + (hπ : κ.Invariant π) {B : Set α} (hB : MeasurableSet B) {j : ℕ} + (hsmall : IsSmallSet κ B j ν) {K : ℝ≥0∞} (hK : K ≠ ∞) {a : Measure α} (ha : a ≤ K • π) + (i : ℕ) : + ∃ g a' b' : Measure α, IsFiniteMeasure g ∧ (κ ^ (j * i)) ∘ₘ a = g + a' + ∧ a Set.univ • π = g + b' ∧ a' ≤ K • π ∧ b' ≤ K • π ∧ a' Set.univ = b' Set.univ + ∧ a' Set.univ ≤ K * π Bᶜ + (1 - ν Set.univ) ^ i * a Set.univ := by + have ha_univ : a Set.univ ≤ K := by simpa using ha Set.univ + have hKπ : IsFiniteMeasure (K • π) := ⟨by simp [hK.lt_top]⟩ + induction i with + | zero => + refine ⟨0, a, a Set.univ • π, inferInstance, ?_, ?_, ha, ?_, ?_, ?_⟩ + · rw [Nat.mul_zero, pow_zero_comp, zero_add] + · simp + · refine Measure.le_iff.mpr fun s _ ↦ ?_ + simp only [Measure.smul_apply, smul_eq_mul] + gcongr + · simp + · simp + | succ i ih => + obtain ⟨g, a', b', hg, hag, hbg, ha', hb', hab, h_le⟩ := ih + have ha'_fin : IsFiniteMeasure a' := isFiniteMeasure_of_le _ ha' + have hb'_fin : IsFiniteMeasure b' := isFiniteMeasure_of_le _ hb' + set c := a' Set.univ - K * π Bᶜ with hc + have key : ∀ d : Measure α, d ≤ K • π → d Set.univ = a' Set.univ → c • ν ≤ (κ ^ j) ∘ₘ d := by + intro d hd hd_univ + have hdB : c ≤ d B := by + rw [hc, tsub_le_iff_right, ← hd_univ, ← measure_add_measure_compl hB] + gcongr + simpa using hd Bᶜ + refine le_trans ?_ (hsmall.smul_le_comp d) + refine Measure.le_iff.mpr fun s _ ↦ ?_ + simp only [Measure.smul_apply, smul_eq_mul] + gcongr + have hca := key a' ha' rfl + have hcb := key b' hb' hab.symm + -- `c • ν` is finite since it is dominated by the finite measure `(κ ^ j) ∘ₘ a'` + have hcν : IsFiniteMeasure (c • ν) := isFiniteMeasure_of_le _ hca + refine ⟨(κ ^ j) ∘ₘ g + c • ν, (κ ^ j) ∘ₘ a' - c • ν, (κ ^ j) ∘ₘ b' - c • ν, inferInstance, + ?_, ?_, ?_, ?_, ?_, ?_⟩ + · rw [Nat.mul_succ, add_comm, pow_add_comp, hag, Measure.comp_add, add_assoc, + add_comm (c • ν), Measure.sub_add_cancel_of_le hca] + · calc a Set.univ • π = (κ ^ j) ∘ₘ (a Set.univ • π) := (hπ.pow_comp_smul j _).symm + _ = (κ ^ j) ∘ₘ g + c • ν + ((κ ^ j) ∘ₘ b' - c • ν) := by + rw [hbg, Measure.comp_add, add_assoc, add_comm (c • ν), + Measure.sub_add_cancel_of_le hcb] + · exact Measure.sub_le.trans + ((Measure.comp_le_comp_right ha' _).trans_eq (hπ.pow_comp_smul j K)) + · exact Measure.sub_le.trans + ((Measure.comp_le_comp_right hb' _).trans_eq (hπ.pow_comp_smul j K)) + · rw [Measure.sub_apply .univ hca, Measure.sub_apply .univ hcb, Measure.comp_apply_univ, + Measure.comp_apply_univ, hab] + · rw [Measure.sub_apply .univ hca, Measure.comp_apply_univ, Measure.smul_apply, smul_eq_mul, + tsub_le_iff_right] + have h1 : c ≤ c * ν Set.univ + c * (1 - ν Set.univ) := by + rw [← mul_add] + exact le_mul_of_one_le_right' le_add_tsub + have h2 : c ≤ (1 - ν Set.univ) ^ i * a Set.univ := by + rw [hc, tsub_le_iff_left] + exact h_le + calc a' Set.univ ≤ K * π Bᶜ + c := le_add_tsub + _ ≤ K * π Bᶜ + (c * ν Set.univ + c * (1 - ν Set.univ)) := by gcongr + _ ≤ K * π Bᶜ + + (c * ν Set.univ + (1 - ν Set.univ) ^ i * a Set.univ * (1 - ν Set.univ)) := by gcongr + _ = K * π Bᶜ + (1 - ν Set.univ) ^ (i + 1) * a Set.univ + c * ν Set.univ := by + rw [pow_succ] + ring + +/-- If `B` is a `(j, ν)`-small set and `a ≤ K • π` for an invariant probability measure `π`, then +the total variation distance between `(κ ^ (j * i)) ∘ₘ a` and `a univ • π` decreases geometrically +with `i`, up to a term proportional to `π Bᶜ`. -/ +lemma etvDist_pow_comp_le [IsMarkovKernel κ] [IsProbabilityMeasure π] (hπ : κ.Invariant π) + {B : Set α} (hB : MeasurableSet B) {j : ℕ} (hsmall : IsSmallSet κ B j ν) + {K : ℝ≥0∞} (hK : K ≠ ∞) {a : Measure α} (ha : a ≤ K • π) (i : ℕ) : + etvDist ((κ ^ (j * i)) ∘ₘ a) (a Set.univ • π) + ≤ 2 * (K * π Bᶜ + (1 - ν Set.univ) ^ i * a Set.univ) := by + obtain ⟨g, a', b', hg, hag, hbg, ha', hb', hab, h_le⟩ := + exists_split_pow_comp hπ hB hsmall hK ha i + rw [hag, hbg] + calc etvDist (g + a') (g + b') ≤ a' Set.univ + b' Set.univ := etvDist_add_left_le g a' b' + _ = 2 * a' Set.univ := by rw [← hab, two_mul] + _ ≤ 2 * (K * π Bᶜ + (1 - ν Set.univ) ^ i * a Set.univ) := by gcongr + +/-- The total variation distance to a multiple of an invariant measure is nonincreasing along +the iterates of a Markov kernel. -/ +lemma antitone_etvDist_pow_comp [IsMarkovKernel κ] (hπ : κ.Invariant π) (a : Measure α) + (c : ℝ≥0∞) : + Antitone fun n : ℕ ↦ etvDist ((κ ^ n) ∘ₘ a) (c • π) := by + refine antitone_nat_of_succ_le fun n ↦ ?_ + calc etvDist ((κ ^ (n + 1)) ∘ₘ a) (c • π) + _ = etvDist (κ ∘ₘ ((κ ^ n) ∘ₘ a)) (κ ∘ₘ (c • π)) := by + rw [pow_succ_comp', Measure.comp_smul, hπ.def] + _ ≤ etvDist ((κ ^ n) ∘ₘ a) (c • π) := etvDist_comp_le κ _ _ + +/-- If a measure `a` is dominated by a multiple of the invariant probability measure `π` of a +Markov kernel `κ`, and every point reaches a small set `C` with positive probability in `n` steps +for all `n` large enough, then `(κ ^ n) ∘ₘ a` tends to `a univ • π` in total variation. -/ +theorem tendsto_etvDist_pow_comp_of_le [IsMarkovKernel κ] [IsProbabilityMeasure π] + (hπ : κ.Invariant π) {C : Set α} (hC : MeasurableSet C) {k : ℕ} + (hν : ν ≠ 0) (hsmall : IsSmallSet κ C k ν) (hreach : ∀ x, ∃ N, ∀ n ≥ N, 0 < (κ ^ n) x C) + {K : ℝ≥0∞} (hK : K ≠ ∞) {a : Measure α} (ha : a ≤ K • π) : + Tendsto (fun n : ℕ ↦ etvDist ((κ ^ n) ∘ₘ a) (a Set.univ • π)) atTop (𝓝 0) := by + have ha_univ : a Set.univ ≤ K := by simpa using ha Set.univ + have h_event : ∀ θ : ℝ≥0∞, θ ≠ 0 → + ∀ᶠ n : ℕ in atTop, etvDist ((κ ^ n) ∘ₘ a) (a Set.univ • π) ≤ 2 * (K * θ + θ) := by + intro θ hθ + obtain ⟨B, j, δ, hB, hBθ, hδ0, hδ_top, hB_small⟩ := + exists_isSmallSet_measure_compl_le (π := π) hC hsmall hreach hθ + have hδν : (δ • ν) Set.univ ≠ 0 := by simp [hδ0, hν] + have hq : 1 - (δ • ν) Set.univ < 1 := ENNReal.sub_lt_self ENNReal.one_ne_top one_ne_zero hδν + have h_tendsto : Tendsto (fun i : ℕ ↦ (1 - (δ • ν) Set.univ) ^ i * a Set.univ) atTop (𝓝 0) := by + have h := ENNReal.Tendsto.mul_const (b := a Set.univ) + (ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hq) (Or.inr (ne_top_of_le_ne_top hK ha_univ)) + simpa using h + obtain ⟨i, hi⟩ := (h_tendsto.eventually_lt_const (pos_iff_ne_zero.mpr hθ)).exists + refine eventually_atTop.mpr ⟨j * i, fun n hn ↦ ?_⟩ + calc etvDist ((κ ^ n) ∘ₘ a) (a Set.univ • π) + _ ≤ etvDist ((κ ^ (j * i)) ∘ₘ a) (a Set.univ • π) := antitone_etvDist_pow_comp hπ a _ hn + _ ≤ 2 * (K * π Bᶜ + (1 - (δ • ν) Set.univ) ^ i * a Set.univ) := + etvDist_pow_comp_le hπ hB hB_small hK ha i + _ ≤ 2 * (K * θ + θ) := by gcongr + rw [ENNReal.tendsto_nhds_zero] + intro ε hε + rcases eq_or_ne ε ∞ with rfl | hε_top + · simp + have h2K : 2 * (K + 1) ≠ 0 := by simp + have h2K' : 2 * (K + 1) ≠ ∞ := ENNReal.mul_ne_top (by simp) (by simp [hK]) + refine (h_event (ε / (2 * (K + 1))) (ENNReal.div_pos hε.ne' h2K').ne').mono + fun n hn ↦ hn.trans_eq ?_ + rw [← add_one_mul, ← mul_assoc, ENNReal.mul_div_cancel h2K h2K'] + +/-- If a probability measure `μ` is the sum of a measure `ζ` dominated by a multiple of the +invariant probability measure `π` and of a measure `ξ`, then the total variation distance between +`(κ ^ n) ∘ₘ μ` and `π` is eventually at most `2 * ξ univ + ε`. -/ +lemma eventually_etvDist_pow_comp_le [IsMarkovKernel κ] [IsProbabilityMeasure π] + (hπ : κ.Invariant π) {C : Set α} (hC : MeasurableSet C) {k : ℕ} + (hν : ν ≠ 0) (hsmall : IsSmallSet κ C k ν) (hreach : ∀ x, ∃ N, ∀ n ≥ N, 0 < (κ ^ n) x C) + {μ ζ ξ : Measure α} [IsProbabilityMeasure μ] (hμ : μ = ζ + ξ) {K : ℝ≥0∞} (hK : K ≠ ∞) + (hζ : ζ ≤ K • π) {ε : ℝ≥0∞} (hε : ε ≠ 0) : + ∀ᶠ n : ℕ in atTop, etvDist ((κ ^ n) ∘ₘ μ) π ≤ 2 * ξ Set.univ + ε := by + have hζμ : ζ ≤ μ := hμ ▸ Measure.le_add_right le_rfl + have hζ_fin : IsFiniteMeasure ζ := isFiniteMeasure_of_le μ hζμ + have h_univ : ζ Set.univ + ξ Set.univ = 1 := by rw [← Measure.add_apply, ← hμ, measure_univ] + have hζ_smul : ζ Set.univ • π ≤ π := by + refine Measure.le_iff.mpr fun s _ ↦ ?_ + simp only [Measure.smul_apply, smul_eq_mul] + exact mul_le_of_le_one_left' (h_univ ▸ le_self_add) + have hζ_smul_fin : IsFiniteMeasure (ζ Set.univ • π) := isFiniteMeasure_of_le π hζ_smul + have h_tendsto := tendsto_etvDist_pow_comp_of_le hπ hC hν hsmall hreach hK hζ + filter_upwards [ENNReal.tendsto_nhds_zero.mp h_tendsto ε (pos_iff_ne_zero.mpr hε)] with n hn + set η : Kernel α α := κ ^ n + have h1 : etvDist (η ∘ₘ μ) (η ∘ₘ ζ) = ξ Set.univ := by + rw [hμ, Measure.comp_add, etvDist_of_ge (Measure.le_add_right le_rfl), Measure.add_apply, + Measure.comp_apply_univ, Measure.comp_apply_univ, + ENNReal.add_sub_cancel_left (measure_ne_top _ _)] + have h2 : etvDist (ζ Set.univ • π) π ≤ ξ Set.univ := by + rw [etvDist_of_le hζ_smul, Measure.smul_apply, measure_univ, smul_eq_mul, mul_one, + tsub_le_iff_left, h_univ] + calc etvDist (η ∘ₘ μ) π + _ ≤ etvDist (η ∘ₘ μ) (η ∘ₘ ζ) + etvDist (η ∘ₘ ζ) π := etvDist_triangle _ _ _ + _ ≤ etvDist (η ∘ₘ μ) (η ∘ₘ ζ) + + (etvDist (η ∘ₘ ζ) (ζ Set.univ • π) + etvDist (ζ Set.univ • π) π) := by + gcongr + exact etvDist_triangle _ _ _ + _ ≤ ξ Set.univ + (ε + ξ Set.univ) := by + rw [h1] + gcongr + _ = 2 * ξ Set.univ + ε := by ring + +/-! ### The part of `κ ^ i` which is not dominated by the invariant measure -/ + +section Excess + +variable [MeasurableSpace.CountablyGenerated α] + +open Classical in +/-- `excess κ π i x` is the part of the measure `(κ ^ i) x` which exceeds `i • π`. -/ +private noncomputable def excess (κ : Kernel α α) (π : Measure α) (i : ℕ) : Kernel α α := + κ ^ i - Kernel.const α ((i : ℝ≥0) • π) + +/-- The infimum over `i` of the mass of the part of `(κ ^ i) x` which exceeds `i • π`. -/ +private noncomputable def excessMass (κ : Kernel α α) (π : Measure α) (x : α) : ℝ≥0∞ := + ⨅ i, excess κ π i x Set.univ + +variable [IsMarkovKernel κ] [IsFiniteMeasure π] + +private lemma excess_apply (i : ℕ) (x : α) : + excess κ π i x = (κ ^ i) x - (i : ℝ≥0) • π := by + classical + rw [excess, Kernel.sub_apply, const_apply] + +private lemma excess_apply_le (i : ℕ) (x : α) : excess κ π i x ≤ (κ ^ i) x := by + rw [excess_apply] + exact Measure.sub_le + +private lemma pow_apply_le_excess_add (i : ℕ) (x : α) : + (κ ^ i) x ≤ excess κ π i x + (i : ℝ≥0) • π := by + rw [excess_apply] + exact Measure.sub_le_iff_le_add.mp le_rfl + +private lemma excess_apply_univ_le_of_le {i : ℕ} {x : α} {d : Measure α} + (h : (κ ^ i) x ≤ d + (i : ℝ≥0) • π) : + excess κ π i x Set.univ ≤ d Set.univ := by + rw [excess_apply] + exact Measure.sub_le_of_le_add h Set.univ + +private lemma excess_apply_univ_le_one (i : ℕ) (x : α) : excess κ π i x Set.univ ≤ 1 := + (excess_apply_le i x Set.univ).trans prob_le_one + +private lemma pow_comp_le_excess_comp_add (i : ℕ) (μ : Measure α) : + (κ ^ i) ∘ₘ μ ≤ (excess κ π i) ∘ₘ μ + μ Set.univ • ((i : ℝ≥0) • π) := by + calc (κ ^ i) ∘ₘ μ + _ ≤ (excess κ π i + Kernel.const α ((i : ℝ≥0) • π)) ∘ₘ μ := + Measure.comp_le_comp_left μ fun x ↦ by + rw [FunLike.coe_add, Pi.add_apply, const_apply] + exact pow_apply_le_excess_add i x + _ = (excess κ π i) ∘ₘ μ + μ Set.univ • ((i : ℝ≥0) • π) := by + rw [Measure.add_comp, Measure.const_comp] + +private lemma excess_add_apply_univ_le (hπ : κ.Invariant π) (m i : ℕ) (x : α) : + excess κ π (m + i) x Set.univ ≤ ∫⁻ y, excess κ π m y Set.univ ∂(excess κ π i x) := by + rw [← Measure.bind_apply .univ (excess κ π m).aemeasurable] + refine excess_apply_univ_le_of_le ?_ + set η : Kernel α α := κ ^ m + have h_inv : η ∘ₘ ((i : ℝ≥0) • π) = (i : ℝ≥0) • π := hπ.pow_comp_smul m (i : ℝ≥0) + have h_le_one : excess κ π i x Set.univ • ((m : ℝ≥0) • π) ≤ (m : ℝ≥0) • π := by + refine Measure.le_iff.mpr fun s _ ↦ ?_ + rw [Measure.smul_apply, smul_eq_mul] + exact mul_le_of_le_one_left' (excess_apply_univ_le_one i x) + calc (κ ^ (m + i)) x = η ∘ₘ (κ ^ i) x := pow_add_apply κ m i x + _ ≤ η ∘ₘ (excess κ π i x + (i : ℝ≥0) • π) := + Measure.comp_le_comp_right (pow_apply_le_excess_add i x) _ + _ = η ∘ₘ (excess κ π i x) + (i : ℝ≥0) • π := by rw [Measure.comp_add, h_inv] + _ ≤ (excess κ π m) ∘ₘ (excess κ π i x) + excess κ π i x Set.univ • ((m : ℝ≥0) • π) + + (i : ℝ≥0) • π := by + gcongr + exact pow_comp_le_excess_comp_add m _ + _ ≤ (excess κ π m) ∘ₘ (excess κ π i x) + (m : ℝ≥0) • π + (i : ℝ≥0) • π := by gcongr + _ = (excess κ π m) ∘ₘ (excess κ π i x) + ((m + i : ℕ) : ℝ≥0) • π := by + rw [add_assoc, ← add_smul, Nat.cast_add] + +private lemma antitone_excess_apply_univ (hπ : κ.Invariant π) (x : α) : + Antitone fun i ↦ excess κ π i x Set.univ := by + refine antitone_nat_of_succ_le fun i ↦ ?_ + calc excess κ π (i + 1) x Set.univ = excess κ π (1 + i) x Set.univ := by rw [add_comm] + _ ≤ ∫⁻ y, excess κ π 1 y Set.univ ∂(excess κ π i x) := excess_add_apply_univ_le hπ 1 i x + _ ≤ ∫⁻ _, 1 ∂(excess κ π i x) := lintegral_mono fun y ↦ excess_apply_univ_le_one 1 y + _ = excess κ π i x Set.univ := by simp + +private lemma excess_succ_apply_univ_le (hπ : κ.Invariant π) (i : ℕ) (x : α) : + excess κ π (i + 1) x Set.univ ≤ ∫⁻ y, excess κ π i y Set.univ ∂κ x := by + calc excess κ π (i + 1) x Set.univ + _ ≤ ∫⁻ y, excess κ π i y Set.univ ∂(excess κ π 1 x) := excess_add_apply_univ_le hπ i 1 x + _ ≤ ∫⁻ y, excess κ π i y Set.univ ∂κ x := + lintegral_mono' (by simpa using excess_apply_le (κ := κ) (π := π) 1 x) le_rfl + +omit [IsMarkovKernel κ] [IsFiniteMeasure π] in +private lemma measurable_excessMass : Measurable (excessMass κ π) := + Measurable.iInf fun i ↦ (excess κ π i).measurable_coe .univ + +private lemma excessMass_le_one (x : α) : excessMass κ π x ≤ 1 := + (iInf_le _ 0).trans (excess_apply_univ_le_one 0 x) + +private lemma lintegral_excessMass (hπ : κ.Invariant π) (μ : Measure α) [IsFiniteMeasure μ] : + ∫⁻ y, excessMass κ π y ∂μ = ⨅ i, ∫⁻ y, excess κ π i y Set.univ ∂μ := by + refine lintegral_iInf (fun i ↦ (excess κ π i).measurable_coe .univ) + (fun i j hij y ↦ antitone_excess_apply_univ hπ y hij) ?_ + refine ((lintegral_mono fun y ↦ excess_apply_univ_le_one 0 y).trans_lt ?_).ne + simp + +private lemma excessMass_le_lintegral (hπ : κ.Invariant π) (x : α) : + excessMass κ π x ≤ ∫⁻ y, excessMass κ π y ∂κ x := by + rw [lintegral_excessMass hπ] + exact le_iInf fun i ↦ (iInf_le _ (i + 1)).trans (excess_succ_apply_univ_le hπ i x) + +private lemma excessMass_lt_one (hπ : κ.Invariant π) {c : ℝ≥0} (hνc : ν ≤ c • π) (hν : ν ≠ 0) + {w : ℝ≥0∞} (hw : w ≠ 0) (hw1 : w ≤ 1) {n : ℕ} {x : α} (h : w • ν ≤ (κ ^ n) x) : + excessMass κ π x < 1 := by + have hwν_fin : IsFiniteMeasure (w • ν) := isFiniteMeasure_of_le _ h + have hwν : w • ν ≤ ν := by + refine Measure.le_iff.mpr fun s _ ↦ ?_ + rw [Measure.smul_apply, smul_eq_mul] + exact mul_le_of_le_one_left' hw1 + set p := ⌈c⌉₊ + set η : Kernel α α := κ ^ p + have hcp : c • π ≤ ((p + n : ℕ) : ℝ≥0) • π := by + refine Measure.le_iff.mpr fun s _ ↦ ?_ + rw [Measure.coe_nnreal_smul_apply, Measure.coe_nnreal_smul_apply] + gcongr + exact (Nat.le_ceil c).trans (by exact_mod_cast Nat.le_add_right ⌈c⌉₊ n) + have h_inv : η ∘ₘ (c • π) = c • π := hπ.pow_comp_smul p c + have h_le : (κ ^ (p + n)) x ≤ η ∘ₘ ((κ ^ n) x - w • ν) + ((p + n : ℕ) : ℝ≥0) • π := by + calc (κ ^ (p + n)) x = η ∘ₘ (κ ^ n) x := pow_add_apply κ p n x + _ = η ∘ₘ ((κ ^ n) x - w • ν) + η ∘ₘ (w • ν) := by + rw [← Measure.comp_add, Measure.sub_add_cancel_of_le h] + _ ≤ η ∘ₘ ((κ ^ n) x - w • ν) + η ∘ₘ (c • π) := by + gcongr + exact hwν.trans hνc + _ = η ∘ₘ ((κ ^ n) x - w • ν) + c • π := by rw [h_inv] + _ ≤ η ∘ₘ ((κ ^ n) x - w • ν) + ((p + n : ℕ) : ℝ≥0) • π := by gcongr + calc excessMass κ π x ≤ excess κ π (p + n) x Set.univ := iInf_le _ _ + _ ≤ (η ∘ₘ ((κ ^ n) x - w • ν)) Set.univ := excess_apply_univ_le_of_le h_le + _ = 1 - w * ν Set.univ := by + rw [Measure.comp_apply_univ, Measure.sub_apply .univ h, measure_univ, Measure.smul_apply, + smul_eq_mul] + _ < 1 := ENNReal.sub_lt_self ENNReal.one_ne_top one_ne_zero (mul_ne_zero hw (by simpa using hν)) + +private lemma ae_excessMass_eq_zero [IsProbabilityMeasure π] {φ : Measure α} [IsIrreducible φ κ] + (hφ : φ ≠ 0) (hπ : κ.Invariant π) (h_lt : ∀ x, excessMass κ π x < 1) : + ∀ᵐ x ∂π, excessMass κ π x = 0 := by + -- there is a level `t < 1` such that the set `{x | excessMass κ π x ≤ t}` is not null + obtain ⟨t, ht1, ht⟩ : ∃ t : ℝ≥0∞, t < 1 ∧ π {x | excessMass κ π x ≤ t} ≠ 0 := by + by_contra! h + have h_univ : (Set.univ : Set α) = ⋃ q : {q : ℚ // ((q : ℝ).toNNReal : ℝ≥0∞) < 1}, + {x | excessMass κ π x ≤ ((q : ℝ).toNNReal : ℝ≥0∞)} := by + ext x + simp only [Set.mem_univ, Set.mem_iUnion, Set.mem_ofPred_eq, true_iff] + obtain ⟨q, -, hq1, hq2⟩ := ENNReal.lt_iff_exists_rat_btwn.mp (h_lt x) + exact ⟨⟨q, hq2⟩, hq1.le⟩ + have h_zero : π Set.univ = 0 := by + rw [h_univ] + exact measure_iUnion_null fun q ↦ h _ q.2 + simp at h_zero + -- hence the excess mass is at most `t` almost everywhere, since it is subharmonic + have h_ae : ∀ᵐ x ∂π, excessMass κ π x ≤ t := by + refine hπ.ae_le_of_le_lintegral hφ measurable_excessMass ?_ + (ae_of_all _ (excessMass_le_lintegral hπ)) ht + refine ((lintegral_mono fun y ↦ excessMass_le_one y).trans_lt ?_).ne + simp + filter_upwards [hπ.ae_ae_pow h_ae] with x hx + have h1 : ∀ i, excessMass κ π x ≤ t * excess κ π i x Set.univ := by + intro i + have h_fin : IsFiniteMeasure (excess κ π i x) := isFiniteMeasure_of_le _ (excess_apply_le i x) + calc excessMass κ π x + _ ≤ ⨅ m, ∫⁻ y, excess κ π m y Set.univ ∂(excess κ π i x) := + le_iInf fun m ↦ (iInf_le _ (m + i)).trans (excess_add_apply_univ_le hπ m i x) + _ = ∫⁻ y, excessMass κ π y ∂(excess κ π i x) := (lintegral_excessMass hπ _).symm + _ ≤ ∫⁻ _, t ∂(excess κ π i x) := + lintegral_mono_ae ((hx i).filter_mono (ae_mono (excess_apply_le i x))) + _ = t * excess κ π i x Set.univ := MeasureTheory.lintegral_const _ + have h2 : excessMass κ π x ≤ t * excessMass κ π x := by + rcases eq_or_ne t 0 with rfl | ht0 + · simpa using h1 0 + · have h_eq : t * excessMass κ π x = ⨅ i, t * excess κ π i x Set.univ := + ENNReal.mul_iInf_of_ne ht0 (ht1.trans_le le_top).ne + rw [h_eq] + exact le_iInf h1 + by_contra h0 + have h_fin : excessMass κ π x ≠ ∞ := ((excessMass_le_one x).trans_lt ENNReal.one_lt_top).ne + have h3 : t * excessMass κ π x < 1 * excessMass κ π x := ENNReal.mul_lt_mul_left h0 h_fin ht1 + rw [one_mul] at h3 + exact not_le.mpr h3 h2 + +private lemma tendsto_etvDist_pow_comp_of_lintegral_excessMass_eq_zero [IsProbabilityMeasure π] + (hπ : κ.Invariant π) {C : Set α} (hC : MeasurableSet C) {k : ℕ} + (hν : ν ≠ 0) (hsmall : IsSmallSet κ C k ν) (hreach : ∀ x, ∃ N, ∀ n ≥ N, 0 < (κ ^ n) x C) + {μ : Measure α} [IsProbabilityMeasure μ] (hμ : ∫⁻ x, excessMass κ π x ∂μ = 0) : + Tendsto (fun n : ℕ ↦ etvDist ((κ ^ n) ∘ₘ μ) π) atTop (𝓝 0) := by + rw [ENNReal.tendsto_nhds_zero] + intro ε hε + have hε2 : ε / 2 ≠ 0 := (ENNReal.half_pos hε.ne').ne' + have hε4 : 0 < ε / 2 / 2 := ENNReal.half_pos hε2 + obtain ⟨i, hi⟩ : ∃ i, ∫⁻ x, excess κ π i x Set.univ ∂μ < ε / 2 / 2 := by + by_contra! h + have h_le : ε / 2 / 2 ≤ ∫⁻ x, excessMass κ π x ∂μ := by + rw [lintegral_excessMass hπ] + exact le_iInf h + rw [hμ] at h_le + exact (hε4.trans_le h_le).false + -- we split `(κ ^ i) ∘ₘ μ` into a part `ξ` of small mass and a part dominated by `i • π` + set θ : Kernel α α := κ ^ i with hθ + set ξ := (excess κ π i) ∘ₘ μ + have hξ_univ : ξ Set.univ = ∫⁻ x, excess κ π i x Set.univ ∂μ := + Measure.bind_apply .univ (excess κ π i).aemeasurable + have hξ_le : ξ ≤ θ ∘ₘ μ := Measure.comp_le_comp_left μ (excess_apply_le i) + have hξ_fin : IsFiniteMeasure ξ := isFiniteMeasure_of_le _ hξ_le + have hμ' : θ ∘ₘ μ = (θ ∘ₘ μ - ξ) + ξ := (Measure.sub_add_cancel_of_le hξ_le).symm + have hζ : θ ∘ₘ μ - ξ ≤ ((i : ℝ≥0) : ℝ≥0∞) • π := by + refine Measure.sub_le_of_le_add ?_ + have h := pow_comp_le_excess_comp_add (κ := κ) (π := π) i μ + rwa [measure_univ, one_smul, add_comm] at h + have h_event := + eventually_etvDist_pow_comp_le hπ hC hν hsmall hreach hμ' ENNReal.coe_ne_top hζ hε2 + obtain ⟨N, hN⟩ := eventually_atTop.mp h_event + refine eventually_atTop.mpr ⟨N + i, fun n hn ↦ ?_⟩ + obtain ⟨n', rfl⟩ : ∃ n', n = n' + i := ⟨n - i, (Nat.sub_add_cancel (by omega)).symm⟩ + have hN' := hN n' (by omega) + rw [hθ, ← pow_add_comp] at hN' + calc etvDist ((κ ^ (n' + i)) ∘ₘ μ) π ≤ 2 * ξ Set.univ + ε / 2 := hN' + _ ≤ 2 * (ε / 2 / 2) + ε / 2 := by + rw [hξ_univ] + gcongr + _ = ε := by rw [two_mul, ENNReal.add_halves, ENNReal.add_halves] + +private lemma excessMass_eq_zero_of_isHarrisRecurrent {φ : Measure α} (hφ : φ ≠ 0) (hφπ : φ ≪ π) + (hπ : κ.Invariant π) (hH : κ.IsHarrisRecurrent φ) (h_ae : ∀ᵐ x ∂π, excessMass κ π x = 0) + (x : α) : + excessMass κ π x = 0 := by + -- `G` is the set on which the excess mass vanishes. It has positive `φ`-measure. + have hG : MeasurableSet {x | excessMass κ π x = 0} := + measurable_excessMass (measurableSet_singleton 0) + set G : Set α := {x | excessMass κ π x = 0} + have hφG : 0 < φ G := by + rw [pos_iff_ne_zero] + intro h0 + refine hφ ?_ + rw [← Measure.measure_univ_eq_zero, ← Set.union_compl_self G] + refine measure_union_null h0 (hφπ (measure_eq_zero_iff_ae_notMem.mpr ?_)) + filter_upwards [h_ae] with y hy using fun h ↦ h hy + -- the excess mass at `y` is at most its integral against one step of the chain killed in `G` + have h_step : ∀ y, excessMass κ π y ≤ ∫⁻ z, excessMass κ π z ∂(κ.restrict hG.compl y) := by + intro y + calc excessMass κ π y ≤ ∫⁻ z, excessMass κ π z ∂κ y := excessMass_le_lintegral hπ y + _ = ∫⁻ z in G, excessMass κ π z ∂κ y + ∫⁻ z in Gᶜ, excessMass κ π z ∂κ y := + (lintegral_add_compl _ hG).symm + _ = ∫⁻ z, excessMass κ π z ∂(κ.restrict hG.compl y) := by + rw [setLIntegral_congr_fun hG (fun z hz ↦ hz), lintegral_zero, zero_add, restrict_apply] + -- hence it is at most the probability that the chain avoids `G` for `n` steps + have h_pow : ∀ n : ℕ, ∀ y, + excessMass κ π y ≤ ∫⁻ z, excessMass κ π z ∂((κ.restrict hG.compl) ^ n) y := by + intro n + induction n with + | zero => + intro y + rw [pow_zero_apply, lintegral_dirac' _ measurable_excessMass] + | succ n ih => + intro y + calc excessMass κ π y ≤ ∫⁻ z, excessMass κ π z ∂((κ.restrict hG.compl) ^ n) y := ih y + _ ≤ ∫⁻ z, ∫⁻ z', excessMass κ π z' ∂(κ.restrict hG.compl z) + ∂((κ.restrict hG.compl) ^ n) y := lintegral_mono h_step + _ = ∫⁻ z, excessMass κ π z ∂((κ.restrict hG.compl) ^ (n + 1)) y := by + rw [pow_succ_apply', Measure.lintegral_bind (Kernel.aemeasurable _) + measurable_excessMass.aemeasurable] + refine le_antisymm (ge_of_tendsto' (hH hG hφG x) fun n ↦ ?_) bot_le + calc excessMass κ π x ≤ ∫⁻ z, excessMass κ π z ∂((κ.restrict hG.compl) ^ n) x := h_pow n x + _ ≤ ∫⁻ _, 1 ∂((κ.restrict hG.compl) ^ n) x := lintegral_mono fun z ↦ excessMass_le_one z + _ = ((κ.restrict hG.compl) ^ n) x Set.univ := by simp + +end Excess + +/-! ### Main results -/ + +private lemma tendsto_tvDist_of_tendsto_etvDist {ι : Type*} {l : Filter ι} + {μ ν : ι → Measure α} (h : Tendsto (fun i ↦ etvDist (μ i) (ν i)) l (𝓝 0)) : + Tendsto (fun i ↦ tvDist (μ i) (ν i)) l (𝓝 0) := by + have h' := (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp h + rw [ENNReal.toReal_zero] at h' + exact h' + +section SmallSet + +variable [MeasurableSpace.CountablyGenerated α] [IsMarkovKernel κ] [IsFiniteMeasure π] [NeZero π] + {φ : Measure α} [hφ : NeZero φ] [hκφ : IsIrreducible φ κ] + +include hφ hκφ + +/-- An irreducible aperiodic Markov kernel `κ` on a countably generated measurable space, with a +nonzero finite invariant measure `π`, has a small set `C` which is reached with positive +probability from every point in `n` steps, for all `n` large enough. The measure `ν` of the small +set can be chosen to be dominated by a multiple of `π`. -/ +lemma exists_isSmallSet_forall_pow_apply_pos (hπ : κ.Invariant π) (hκ : κ.IsAperiodic π) : + ∃ (C : Set α) (k : ℕ) (ν : Measure α) (c : ℝ≥0), MeasurableSet C ∧ ν ≠ 0 ∧ ν ≤ c • π ∧ + IsSmallSet κ C k ν ∧ ∀ x, ∃ N, ∀ n ≥ N, 0 < (κ ^ n) x C := by + -- we can assume that the irreducibility measure is finite and dominated by `π` + obtain ⟨φ', hφ'π, hφ'0, hφ'⟩ := IsIrreducible.exists_measure_le (κ := κ) (NeZero.ne φ) + (IsIrreducible.absolutelyContinuous hπ (NeZero.ne π)) + have hφ'_fin : IsFiniteMeasure φ' := isFiniteMeasure_of_le π hφ'π + -- there is a small set `C` + obtain ⟨C, D, k, c, hC, hD, -, hφC, hφD, hk, hc, hsmall⟩ := exists_isSmallSet (κ := κ) (φ := φ') + MeasurableSet.univ (by simpa [pos_iff_ne_zero] using hφ'0) + have hν0 : c • φ'.restrict D ≠ 0 := by + rw [← Measure.measure_univ_ne_zero, Measure.coe_nnreal_smul_apply, + Measure.restrict_apply_univ] + exact mul_ne_zero (by simpa using hc.ne') hφD.ne' + have hνπ : c • φ'.restrict D ≤ c • π := by + refine Measure.le_iff.mpr fun s _ ↦ ?_ + rw [Measure.coe_nnreal_smul_apply, Measure.coe_nnreal_smul_apply] + gcongr + exact Measure.restrict_le_self.trans hφ'π + -- by aperiodicity, every point reaches `C` at all large times + exact ⟨C, k, c • φ'.restrict D, c, hC, hν0, hνπ, hsmall, fun x ↦ + hκ.exists_forall_pow_apply_pos (φ := φ') hC hφC hk hν0 + (Measure.absolutelyContinuous_of_le_smul hνπ) hsmall x⟩ + +end SmallSet + +section Main + +variable [MeasurableSpace.CountablyGenerated α] [IsMarkovKernel κ] [IsProbabilityMeasure π] + {φ : Measure α} [hφ : NeZero φ] [hκφ : IsIrreducible φ κ] {μ : Measure α} + +include hφ hκφ + +private lemma ae_excessMass_eq_zero_of_isAperiodic (hπ : κ.Invariant π) (hκ : κ.IsAperiodic π) : + ∀ᵐ x ∂π, excessMass κ π x = 0 := by + obtain ⟨C, k, ν, c, -, hν0, hνπ, hsmall, hreach⟩ := + exists_isSmallSet_forall_pow_apply_pos (φ := φ) hπ hκ + refine ae_excessMass_eq_zero (NeZero.ne φ) hπ fun x ↦ ?_ + obtain ⟨N, hN⟩ := hreach x + exact excessMass_lt_one hπ hνπ hν0 (hN N le_rfl).ne' prob_le_one + (hsmall.smul_le_pow_add_apply N x) + +private lemma tendsto_etvDist_pow_comp_of_isAperiodic (hπ : κ.Invariant π) + (hκ : κ.IsAperiodic π) [IsProbabilityMeasure μ] (hμ : ∫⁻ x, excessMass κ π x ∂μ = 0) : + Tendsto (fun n : ℕ ↦ etvDist ((κ ^ n) ∘ₘ μ) π) atTop (𝓝 0) := by + obtain ⟨C, k, ν, c, hC, hν0, hνπ, hsmall, hreach⟩ := + exists_isSmallSet_forall_pow_apply_pos (φ := φ) hπ hκ + exact tendsto_etvDist_pow_comp_of_lintegral_excessMass_eq_zero hπ hC hν0 hsmall hreach hμ + +private lemma tendsto_etvDist_pow_apply_of_isAperiodic (hπ : κ.Invariant π) + (hκ : κ.IsAperiodic π) {x : α} (hx : excessMass κ π x = 0) : + Tendsto (fun n : ℕ ↦ etvDist ((κ ^ n) x) π) atTop (𝓝 0) := by + have h := tendsto_etvDist_pow_comp_of_isAperiodic (φ := φ) (μ := Measure.dirac x) hπ hκ + (by rw [lintegral_dirac' _ measurable_excessMass, hx]) + simpa only [Measure.dirac_bind (Kernel.measurable _)] using h + +/-- **Ergodic theorem for Markov kernels**. Let `κ` be a Markov kernel on a countably generated +measurable space, with an invariant probability measure `π`. If `κ` is irreducible with respect +to a nonzero measure `φ` and aperiodic, then for `π`-almost every `x`, the measures `(κ ^ n) x` +converge to `π` in total variation. +Ref. *Roberts-Rosenthal* Theorem 4, *Tierney* Theorem 1. -/ +theorem ae_tendsto_etvDist_pow_apply (hπ : κ.Invariant π) (hκ : κ.IsAperiodic π) : + ∀ᵐ x ∂π, Tendsto (fun n : ℕ ↦ etvDist ((κ ^ n) x) π) atTop (𝓝 0) := by + filter_upwards [ae_excessMass_eq_zero_of_isAperiodic (φ := φ) hπ hκ] with x hx + exact tendsto_etvDist_pow_apply_of_isAperiodic (φ := φ) hπ hκ hx + +/-- **Ergodic theorem for Markov kernels**. Let `κ` be a Markov kernel on a countably generated +measurable space, with an invariant probability measure `π`. If `κ` is irreducible with respect +to a nonzero measure `φ` and aperiodic, then for `π`-almost every `x`, the measures `(κ ^ n) x` +converge to `π` in total variation. +Ref. *Roberts-Rosenthal* Theorem 4, *Tierney* Theorem 1. -/ +theorem ae_tendsto_tvDist_pow_apply (hπ : κ.Invariant π) (hκ : κ.IsAperiodic π) : + ∀ᵐ x ∂π, Tendsto (fun n : ℕ ↦ tvDist ((κ ^ n) x) π) atTop (𝓝 0) := by + filter_upwards [ae_tendsto_etvDist_pow_apply (φ := φ) hπ hκ] with x hx + exact tendsto_tvDist_of_tendsto_etvDist hx + +/-- Let `κ` be an irreducible aperiodic Markov kernel on a countably generated measurable space, +with an invariant probability measure `π`. For every initial probability measure `μ` which is +absolutely continuous with respect to `π`, the measures `(κ ^ n) ∘ₘ μ` converge to `π` in total +variation. -/ +theorem tendsto_etvDist_pow_comp (hπ : κ.Invariant π) (hκ : κ.IsAperiodic π) + [IsProbabilityMeasure μ] (hμ : μ ≪ π) : + Tendsto (fun n : ℕ ↦ etvDist ((κ ^ n) ∘ₘ μ) π) atTop (𝓝 0) := by + refine tendsto_etvDist_pow_comp_of_isAperiodic (φ := φ) hπ hκ ?_ + rw [lintegral_eq_zero_iff measurable_excessMass] + exact hμ.ae_le (ae_excessMass_eq_zero_of_isAperiodic (φ := φ) hπ hκ) + +/-- Let `κ` be an irreducible aperiodic Markov kernel on a countably generated measurable space, +with an invariant probability measure `π`. For every initial probability measure `μ` which is +absolutely continuous with respect to `π`, the measures `(κ ^ n) ∘ₘ μ` converge to `π` in total +variation. -/ +theorem tendsto_tvDist_pow_comp (hπ : κ.Invariant π) (hκ : κ.IsAperiodic π) + [IsProbabilityMeasure μ] (hμ : μ ≪ π) : + Tendsto (fun n : ℕ ↦ tvDist ((κ ^ n) ∘ₘ μ) π) atTop (𝓝 0) := + tendsto_tvDist_of_tendsto_etvDist (tendsto_etvDist_pow_comp (φ := φ) hπ hκ hμ) + +end Main + +section Harris + +variable [MeasurableSpace.CountablyGenerated α] [IsMarkovKernel κ] [IsProbabilityMeasure π] + {φ : Measure α} [hφ : NeZero φ] + +include hφ + +/-- **Ergodic theorem for Harris recurrent Markov kernels**. Let `κ` be a Markov kernel on a +countably generated measurable space, with an invariant probability measure `π`. If `κ` is Harris +recurrent with respect to a nonzero measure `φ` and aperiodic, then for +every initial probability measure `μ`, the measures `(κ ^ n) ∘ₘ μ` converge to `π` in total +variation. +Ref. *Meyn-Tweedie* Theorem 13.0.1, *Tierney* Theorem 1. -/ +theorem IsHarrisRecurrent.tendsto_etvDist_pow_comp (hH : κ.IsHarrisRecurrent φ) + (hπ : κ.Invariant π) (hκ : κ.IsAperiodic π) (μ : Measure α) [IsProbabilityMeasure μ] : + Tendsto (fun n : ℕ ↦ etvDist ((κ ^ n) ∘ₘ μ) π) atTop (𝓝 0) := by + have hκφ : IsIrreducible φ κ := hH.isIrreducible + refine tendsto_etvDist_pow_comp_of_isAperiodic (φ := φ) hπ hκ ?_ + have h_zero : ∀ x, excessMass κ π x = 0 := + excessMass_eq_zero_of_isHarrisRecurrent (NeZero.ne φ) + (IsIrreducible.absolutelyContinuous hπ (NeZero.ne π)) hπ hH + (ae_excessMass_eq_zero_of_isAperiodic (φ := φ) hπ hκ) + simp [h_zero] + +/-- **Ergodic theorem for Harris recurrent Markov kernels**. Let `κ` be a Markov kernel on a +countably generated measurable space, with an invariant probability measure `π`. If `κ` is Harris +recurrent with respect to a nonzero measure `φ` and aperiodic, then for +every initial probability measure `μ`, the measures `(κ ^ n) ∘ₘ μ` converge to `π` in total +variation. +Ref. *Meyn-Tweedie* Theorem 13.0.1, *Tierney* Theorem 1. -/ +theorem IsHarrisRecurrent.tendsto_tvDist_pow_comp (hH : κ.IsHarrisRecurrent φ) + (hπ : κ.Invariant π) (hκ : κ.IsAperiodic π) (μ : Measure α) [IsProbabilityMeasure μ] : + Tendsto (fun n : ℕ ↦ tvDist ((κ ^ n) ∘ₘ μ) π) atTop (𝓝 0) := + tendsto_tvDist_of_tendsto_etvDist (hH.tendsto_etvDist_pow_comp hπ hκ μ) + +/-- **Ergodic theorem for Harris recurrent Markov kernels**. Let `κ` be a Markov kernel on a +countably generated measurable space, with an invariant probability measure `π`. If `κ` is Harris +recurrent with respect to a nonzero measure `φ` and aperiodic, then for +every `x`, the measures `(κ ^ n) x` converge to `π` in total variation. +Ref. *Meyn-Tweedie* Theorem 13.0.1, *Tierney* Theorem 1. -/ +theorem IsHarrisRecurrent.tendsto_etvDist_pow_apply (hH : κ.IsHarrisRecurrent φ) + (hπ : κ.Invariant π) (hκ : κ.IsAperiodic π) (x : α) : + Tendsto (fun n : ℕ ↦ etvDist ((κ ^ n) x) π) atTop (𝓝 0) := by + have h := hH.tendsto_etvDist_pow_comp hπ hκ (Measure.dirac x) + simpa only [Measure.dirac_bind (Kernel.measurable _)] using h + +/-- **Ergodic theorem for Harris recurrent Markov kernels**. Let `κ` be a Markov kernel on a +countably generated measurable space, with an invariant probability measure `π`. If `κ` is Harris +recurrent with respect to a nonzero measure `φ` and aperiodic, then for +every `x`, the measures `(κ ^ n) x` converge to `π` in total variation. +Ref. *Meyn-Tweedie* Theorem 13.0.1, *Tierney* Theorem 1. -/ +theorem IsHarrisRecurrent.tendsto_tvDist_pow_apply (hH : κ.IsHarrisRecurrent φ) + (hπ : κ.Invariant π) (hκ : κ.IsAperiodic π) (x : α) : + Tendsto (fun n : ℕ ↦ tvDist ((κ ^ n) x) π) atTop (𝓝 0) := + tendsto_tvDist_of_tendsto_etvDist (hH.tendsto_etvDist_pow_apply hπ hκ x) + +end Harris + +end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/HarrisRecurrent.lean b/RandomDo/ForMathlib/Probability/Kernel/HarrisRecurrent.lean new file mode 100644 index 0000000..5a5dc9e --- /dev/null +++ b/RandomDo/ForMathlib/Probability/Kernel/HarrisRecurrent.lean @@ -0,0 +1,87 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.Probability.Kernel.Irreducible +public import RandomDo.ForMathlib.Probability.Kernel.Pow + +/-! +# Harris recurrent kernels + +A Markov chain with transition kernel `κ : Kernel α α` is Harris recurrent with respect to a +measure `φ` if from every starting point, it reaches every set of positive `φ`-measure almost +surely. + +We state this property without reference to the law of the trajectories of the chain. For a +measurable set `A`, the kernel `κ.restrict hA.compl` describes one step of the chain killed when +it enters `A`. Hence `((κ.restrict hA.compl) ^ n) x Set.univ` is the probability that the chain +started at `x` does not visit `A` during its first `n` steps, and the chain reaches `A` almost +surely if and only if that quantity tends to zero as `n` tends to infinity. + +## Main definitions + +* `ProbabilityTheory.Kernel.IsHarrisRecurrent κ φ`: from every point, the chain with kernel `κ` + reaches every set of positive `φ`-measure almost surely. + +## Main statements + +* `ProbabilityTheory.Kernel.IsHarrisRecurrent.isIrreducible`: a Markov kernel which is Harris + recurrent with respect to `φ` is `φ`-irreducible. + +## References + +* [Meyn, S.P. and Tweedie, R.L., *Markov Chains and Stochastic Stability*][meyntweedie1993] +-/ + +@[expose] public section + +open MeasureTheory Filter Topology + +open scoped ENNReal ProbabilityTheory + +namespace ProbabilityTheory.Kernel + +variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {φ : Measure α} + +/-- A kernel `κ : Kernel α α` is Harris recurrent with respect to a measure `φ` if for every +measurable set `A` with `φ A > 0` and every `x`, the probability +`((κ.restrict hA.compl) ^ n) x Set.univ` that the Markov chain with kernel `κ` started at `x` +does not visit `A` during its first `n` steps tends to zero as `n` tends to infinity. In other +words, every set of positive `φ`-measure is reached almost surely from every point. +Ref. *Meyn-Tweedie*, Section 9.1. -/ +def IsHarrisRecurrent (κ : Kernel α α) (φ : Measure α) : Prop := + ∀ ⦃A : Set α⦄ (hA : MeasurableSet A), 0 < φ A → ∀ x, + Tendsto (fun n : ℕ ↦ ((κ.restrict hA.compl) ^ n) x Set.univ) atTop (𝓝 0) + +/-- If a kernel is Harris recurrent with respect to a measure `φ₂`, then it is Harris recurrent +with respect to every measure `φ₁ ≪ φ₂`. -/ +lemma IsHarrisRecurrent.mono_ac {φ₁ φ₂ : Measure α} (h : κ.IsHarrisRecurrent φ₂) + (hφ : φ₁ ≪ φ₂) : + κ.IsHarrisRecurrent φ₁ := + fun _ hA hφA x ↦ h hA (pos_iff_ne_zero.mpr fun h0 ↦ hφA.ne' (hφ h0)) x + +/-- A Markov kernel which is Harris recurrent with respect to a measure `φ` is `φ`-irreducible: +if a point never reaches a set, then the chain killed when it enters that set is never killed. -/ +lemma IsHarrisRecurrent.isIrreducible [IsMarkovKernel κ] (h : κ.IsHarrisRecurrent φ) : + IsIrreducible φ κ := by + refine ⟨fun A hA hφA a ↦ ?_⟩ + by_contra! hcon + -- if `a` never reaches `A`, then the powers of `κ` and of its restriction to `Aᶜ` agree at `a` + have h_eq : ∀ n : ℕ, ((κ.restrict hA.compl) ^ n) a = (κ ^ n) a := by + intro n + induction n with + | zero => rw [pow_zero_apply, pow_zero_apply] + | succ n ih => + have h0 : (κ ∘ₘ (κ ^ n) a) A = 0 := by + rw [← pow_succ_apply'] + exact nonpos_iff_eq_zero.mp (hcon (n + 1)) + rw [pow_succ_apply', ih, pow_succ_apply', Measure.restrict_comp] + exact Measure.restrict_eq_self_of_ae_mem (measure_eq_zero_iff_ae_notMem.mp h0) + have h_tendsto := h hA hφA a + simp_rw [h_eq, measure_univ] at h_tendsto + exact one_ne_zero (tendsto_nhds_unique tendsto_const_nhds h_tendsto) + +end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean b/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean new file mode 100644 index 0000000..c2558ff --- /dev/null +++ b/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean @@ -0,0 +1,99 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.Probability.Kernel.Invariance +public import RandomDo.ForMathlib.Probability.Kernel.Pow + +/-! +# Invariant measures and powers of a kernel + +## Main statements + +* `Kernel.Invariant.pow`: a measure invariant for `κ` is invariant for `κ ^ n`. +* `Kernel.Invariant.ae_ae_pow`: if a property holds `μ`-almost everywhere for a measure `μ` + invariant for `κ`, then for `μ`-almost every `a` it holds `(κ ^ n) a`-almost everywhere for + all `n`. +* `Kernel.Invariant.ae_apply_eq_zero_of_ae_absorbing`: if a measurable set of finite measure is + absorbing almost everywhere with respect to an invariant measure of a Markov kernel, then so is + its complement. +-/ + +@[expose] public section + +open MeasureTheory + +open scoped ENNReal ProbabilityTheory + +namespace ProbabilityTheory.Kernel + +variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ π : Measure α} {G : Set α} + +lemma Invariant.pow (h : κ.Invariant μ) (n : ℕ) : (κ ^ n).Invariant μ := by + induction n with + | zero => exact pow_zero_comp κ μ + | succ n ih => rw [Invariant, pow_succ_comp, h.def, ih.def] + +lemma Invariant.pow_comp_eq (h : κ.Invariant μ) (n : ℕ) : (κ ^ n) ∘ₘ μ = μ := h.pow n + +lemma Invariant.pow_comp_smul (h : κ.Invariant μ) (n : ℕ) (c : ℝ≥0∞) : + (κ ^ n) ∘ₘ (c • μ) = c • μ := by + rw [Measure.comp_smul, h.pow_comp_eq] + +/-- If `μ` is invariant for `κ` and a property holds `μ`-almost everywhere, then for `μ`-almost +every `a` it holds `(κ ^ n) a`-almost everywhere for all `n`. -/ +lemma Invariant.ae_ae_pow (h : κ.Invariant μ) {p : α → Prop} (hp : ∀ᵐ a ∂μ, p a) : + ∀ᵐ a ∂μ, ∀ n, ∀ᵐ b ∂(κ ^ n) a, p b := by + rw [ae_all_iff] + intro n + rw [← h.pow_comp_eq n] at hp + exact Measure.ae_ae_of_ae_comp hp + +/-! ### Absorbing sets -/ + +/-- If a measurable set `G` is absorbing almost everywhere with respect to an invariant measure +`π`, then for `π`-almost every point of `G`, no power of `κ` charges `Gᶜ`. -/ +lemma Invariant.ae_pow_apply_compl_eq_zero (hπ : κ.Invariant π) (hG : MeasurableSet G) + (h : ∀ᵐ x ∂π, x ∈ G → κ x Gᶜ = 0) : + ∀ᵐ x ∂π, x ∈ G → ∀ n, (κ ^ n) x Gᶜ = 0 := by + suffices ∀ n, ∀ᵐ x ∂π, x ∈ G → (κ ^ n) x Gᶜ = 0 by + filter_upwards [ae_all_iff.mpr this] with x hx hxG n using hx n hxG + intro n + induction n with + | zero => + refine ae_of_all _ fun x hx ↦ ?_ + rw [pow_zero_apply, Measure.dirac_apply' _ hG.compl] + simp [hx] + | succ n ih => + have h1 : ∀ᵐ x ∂π, ∀ᵐ y ∂κ x, y ∈ G → (κ ^ n) y Gᶜ = 0 := by + rw [← hπ.def] at ih + exact Measure.ae_ae_of_ae_comp ih + filter_upwards [h, h1] with x hx hx1 hxG + rw [pow_succ_apply, Measure.bind_apply hG.compl (κ ^ n).aemeasurable, + lintegral_eq_zero_iff ((κ ^ n).measurable_coe hG.compl)] + have hxG' : ∀ᵐ y ∂κ x, y ∈ G := by + have := measure_eq_zero_iff_ae_notMem.mp (hx hxG) + filter_upwards [this] with y hy using by simpa using hy + filter_upwards [hx1, hxG'] with y hy hyG using hy hyG + +/-- If a measurable set `G` of finite measure is absorbing almost everywhere with respect to an +invariant measure of a Markov kernel, then so is its complement. -/ +lemma Invariant.ae_apply_eq_zero_of_ae_absorbing [IsMarkovKernel κ] (hπ : κ.Invariant π) + (hG : MeasurableSet G) (hπG : π G ≠ ∞) (h : ∀ᵐ x ∂π, x ∈ G → κ x Gᶜ = 0) : + ∀ᵐ x ∂π, x ∈ Gᶜ → κ x G = 0 := by + have h1 : ∫⁻ x, κ x G ∂π = π G := by + rw [← Measure.bind_apply hG κ.aemeasurable, hπ.def] + have h2 : ∫⁻ x in G, κ x G ∂π = π G := by + rw [← setLIntegral_one] + refine setLIntegral_congr_fun_ae hG ?_ + filter_upwards [h] with x hx hxG using (prob_compl_eq_zero_iff hG).mp (hx hxG) + have h3 : ∫⁻ x in Gᶜ, κ x G ∂π = 0 := by + have h_add := lintegral_add_compl (μ := π) (fun x ↦ κ x G) hG + rw [h1, h2] at h_add + exact (ENNReal.add_right_inj hπG).mp (by rw [h_add, add_zero]) + rwa [setLIntegral_eq_zero_iff hG.compl (κ.measurable_coe hG)] at h3 + +end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/Irreducible.lean b/RandomDo/ForMathlib/Probability/Kernel/Irreducible.lean new file mode 100644 index 0000000..5b7b9e6 --- /dev/null +++ b/RandomDo/ForMathlib/Probability/Kernel/Irreducible.lean @@ -0,0 +1,166 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.Probability.Kernel.Irreducible +public import RandomDo.ForMathlib.MeasureTheory.Measure.Decomposition.Exhaustion +public import RandomDo.ForMathlib.Probability.Kernel.Invariance + +/-! +# Irreducible kernels + +Lemmas about irreducible kernels, in particular in the presence of an invariant measure. + +## Main statements + +* `Kernel.IsIrreducible.exists_pow_succ_pos`: for a `φ`-irreducible kernel, every set of positive + `φ`-measure is reached with positive probability in a positive number of steps from every + point `x` with `κ x ≠ 0`. +* `Kernel.IsIrreducible.exists_pow_comp_apply_pos`: for a `φ`-irreducible kernel, every set of + positive `φ`-measure is reached with positive probability from any nonzero initial measure. +* `Kernel.IsIrreducible.absolutelyContinuous`: `φ ≪ π` for every nonzero invariant measure `π` + of a `φ`-irreducible kernel. +* `Kernel.IsIrreducible.exists_measure_le`: a kernel which is irreducible with respect to `φ ≪ π` + is irreducible with respect to a nonzero measure `φ' ≤ π`. This allows to replace an arbitrary + irreducibility measure by a finite one. +* `Kernel.Invariant.measure_eq_zero_or_measure_compl_eq_zero`: a measurable set of finite + measure which is absorbing `π`-almost everywhere has `π`-measure zero or `π`-null complement. +* `Kernel.Invariant.ae_le_of_le_lintegral`: a function `f` with `f x ≤ ∫⁻ y, f y ∂κ x` for + `π`-almost every `x` (a subharmonic function) is `π`-a.e. less than `t` as soon as + `{x | f x ≤ t}` is not `π`-null. +-/ + +@[expose] public section + +open MeasureTheory + +open scoped ENNReal ProbabilityTheory + +namespace ProbabilityTheory.Kernel + +variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {φ π : Measure α} {G : Set α} + +/-- For a `φ`-irreducible kernel, the sets of points which reach a set `A` of positive +`φ`-measure with positive probability in `n` steps cover the space. -/ +lemma IsIrreducible.iUnion_setOf_pow_apply_pos_eq_univ [IsIrreducible φ κ] {A : Set α} + (hA : MeasurableSet A) (hφA : 0 < φ A) : + ⋃ n, {y | 0 < (κ ^ n) y A} = Set.univ := by + ext y + simpa using IsIrreducible.irreducible (φ := φ) hA hφA y + +/-- For a `φ`-irreducible kernel, every set of positive `φ`-measure is reached with positive +probability in a positive number of steps from every point `x` with `κ x ≠ 0`, hence from every +point if `κ` is a Markov kernel. -/ +lemma IsIrreducible.exists_pow_succ_pos [IsIrreducible φ κ] {A : Set α} (hA : MeasurableSet A) + (hφA : 0 < φ A) {x : α} (hx : κ x ≠ 0) : + ∃ n, 0 < (κ ^ (n + 1)) x A := by + have hpos : κ x (⋃ n, {y | 0 < (κ ^ n) y A}) ≠ 0 := by + rw [IsIrreducible.iUnion_setOf_pow_apply_pos_eq_univ (φ := φ) hA hφA] + exact Measure.measure_univ_ne_zero.mpr hx + obtain ⟨n, hn⟩ := exists_measure_pos_of_not_measure_iUnion_null hpos + exact ⟨n, (pow_succ_apply_pos_iff hA).mpr hn⟩ + +/-- For a `φ`-irreducible kernel, every set of positive `φ`-measure is reached with positive +probability from any nonzero initial measure. -/ +lemma IsIrreducible.exists_pow_comp_apply_pos [IsIrreducible φ κ] {C : Set α} + (hC : MeasurableSet C) (hφC : 0 < φ C) {μ : Measure α} (hμ : μ ≠ 0) : + ∃ n : ℕ, 0 < ((κ ^ n) ∘ₘ μ) C := by + have hpos : μ (⋃ n : ℕ, {y | 0 < (κ ^ n) y C}) ≠ 0 := by + simp [IsIrreducible.iUnion_setOf_pow_apply_pos_eq_univ (φ := φ) hC hφC, hμ] + obtain ⟨n, hn⟩ := exists_measure_pos_of_not_measure_iUnion_null hpos + exact ⟨n, (Measure.comp_apply_pos_iff hC).mpr hn⟩ + +/-! ### Irreducible kernels with an invariant measure -/ + +/-- An irreducibility measure of a kernel is absolutely continuous with respect to every nonzero +invariant measure. -/ +lemma IsIrreducible.absolutelyContinuous [IsIrreducible φ κ] (hπ : κ.Invariant π) (hπ0 : π ≠ 0) : + φ ≪ π := by + refine Measure.AbsolutelyContinuous.mk fun A hA hπA ↦ ?_ + by_contra hφA + have : NeZero π := ⟨hπ0⟩ + obtain ⟨x, hx⟩ := (hπ.ae_ae_pow (measure_eq_zero_iff_ae_notMem.mp hπA)).exists + obtain ⟨n, hn⟩ := IsIrreducible.irreducible (φ := φ) (κ := κ) hA (pos_iff_ne_zero.mpr hφA) x + exact hn.ne' (measure_eq_zero_iff_ae_notMem.mpr (hx n)) + +/-- If `κ` is `φ`-irreducible for a nonzero measure `φ ≪ π` with `π` s-finite, then `κ` is +irreducible with respect to a nonzero measure which is less than `π`. No finiteness assumption is +needed on `φ`. -/ +lemma IsIrreducible.exists_measure_le [SFinite π] [IsIrreducible φ κ] (hφ : φ ≠ 0) (hφπ : φ ≪ π) : + ∃ φ' : Measure α, φ' ≤ π ∧ φ' ≠ 0 ∧ IsIrreducible φ' κ := by + obtain ⟨N, hN, hφN, hac⟩ := Measure.exists_null_restrict_compl_absolutelyContinuous φ π + refine ⟨π.restrict Nᶜ, Measure.restrict_le_self, fun h0 ↦ hφ ?_, ⟨fun A hA hA_pos a ↦ ?_⟩⟩ + · rw [Measure.restrict_eq_zero] at h0 + rw [← Measure.measure_univ_eq_zero, ← Set.union_compl_self N] + exact measure_union_null hφN (hφπ h0) + · exact IsIrreducible.irreducible (φ := φ) hA (pos_iff_ne_zero.mpr fun h ↦ hA_pos.ne' (hac h)) a + +/-- If `κ` is `φ`-irreducible with invariant measure `π` and `G` is absorbing `π`-almost +everywhere, with `π G ≠ 0`, then the complement of `G` is `φ`-null. -/ +lemma Invariant.measure_compl_eq_zero_of_ae_absorbing [IsIrreducible φ κ] (hπ : κ.Invariant π) + (hG : MeasurableSet G) (h : ∀ᵐ x ∂π, x ∈ G → κ x Gᶜ = 0) (hπG : π G ≠ 0) : + φ Gᶜ = 0 := by + by_contra hφ + have hfreq : ∃ᵐ x ∂π, x ∈ G := frequently_ae_mem_iff.mpr hπG + obtain ⟨x, hxG, hx⟩ := (hfreq.and_eventually (hπ.ae_pow_apply_compl_eq_zero hG h)).exists + obtain ⟨n, hn⟩ := IsIrreducible.irreducible (φ := φ) (κ := κ) hG.compl (pos_iff_ne_zero.mpr hφ) x + exact hn.ne' (hx hxG n) + +/-- **Ergodicity** of an irreducible Markov kernel with respect to an invariant measure `π`: a +measurable set of finite measure which is absorbing `π`-almost everywhere has measure zero or its +complement has measure zero. -/ +lemma Invariant.measure_eq_zero_or_measure_compl_eq_zero [IsMarkovKernel κ] [IsIrreducible φ κ] + (hφ : φ ≠ 0) (hπ : κ.Invariant π) (hG : MeasurableSet G) (hπG : π G ≠ ∞) + (h : ∀ᵐ x ∂π, x ∈ G → κ x Gᶜ = 0) : + π G = 0 ∨ π Gᶜ = 0 := by + by_contra! hcon + have h1 : φ Gᶜ = 0 := hπ.measure_compl_eq_zero_of_ae_absorbing hG h hcon.1 + have h2 : φ Gᶜᶜ = 0 := by + refine hπ.measure_compl_eq_zero_of_ae_absorbing hG.compl ?_ hcon.2 + simpa using hπ.ae_apply_eq_zero_of_ae_absorbing hG hπG h + rw [compl_compl] at h2 + refine hφ ?_ + rw [← Measure.measure_univ_eq_zero, ← Set.union_compl_self G] + exact measure_union_null h2 h1 + +/-- Let `κ` be an irreducible Markov kernel with finite invariant measure `π` and let `f` be a +`π`-integrable function which is subharmonic `π`-almost everywhere: `f x ≤ ∫⁻ y, f y ∂κ x` for +`π`-almost every `x`. If the set `{x | f x ≤ t}` is not `π`-null, then `f ≤ t` almost +everywhere. -/ +lemma Invariant.ae_le_of_le_lintegral [IsMarkovKernel κ] [IsFiniteMeasure π] [IsIrreducible φ κ] + (hφ : φ ≠ 0) (hπ : κ.Invariant π) {f : α → ℝ≥0∞} (hf : Measurable f) + (hf_int : ∫⁻ x, f x ∂π ≠ ∞) (hsub : ∀ᵐ x ∂π, f x ≤ ∫⁻ y, f y ∂κ x) {t : ℝ≥0∞} + (ht : π {x | f x ≤ t} ≠ 0) : + ∀ᵐ x ∂π, f x ≤ t := by + have hG : MeasurableSet {x | f x ≤ t} := measurableSet_le hf measurable_const + -- the function `g = f - t` is subharmonic + have hg : Measurable fun x ↦ f x - t := hf.sub_const t + have hg_sub : ∀ᵐ x ∂π, f x - t ≤ ∫⁻ y, f y - t ∂κ x := by + filter_upwards [hsub] with x hx + rw [tsub_le_iff_right] + calc f x ≤ ∫⁻ y, f y ∂κ x := hx + _ ≤ ∫⁻ y, (f y - t) + t ∂κ x := lintegral_mono fun y ↦ le_tsub_add + _ = ∫⁻ y, f y - t ∂κ x + t := by + rw [lintegral_add_right _ measurable_const, MeasureTheory.lintegral_const, measure_univ, + mul_one] + -- hence `g` is harmonic almost everywhere + have hg_ae : (fun x ↦ f x - t) =ᵐ[π] fun x ↦ ∫⁻ y, f y - t ∂κ x := by + refine ae_eq_of_ae_le_of_lintegral_le hg_sub ?_ hg.lintegral_kernel.aemeasurable (le_of_eq ?_) + · exact ((lintegral_mono fun x ↦ tsub_le_self).trans_lt hf_int.lt_top).ne + · rw [← Measure.lintegral_bind κ.aemeasurable hg.aemeasurable, hπ.def] + -- so the sublevel set is absorbing almost everywhere + have h_abs : ∀ᵐ x ∂π, x ∈ {x | f x ≤ t} → κ x {x | f x ≤ t}ᶜ = 0 := by + filter_upwards [hg_ae] with x hx hxG + have h0 : ∫⁻ y, f y - t ∂κ x = 0 := by rw [← hx]; exact tsub_eq_zero_of_le hxG + rw [lintegral_eq_zero_iff hg] at h0 + rw [measure_eq_zero_iff_ae_notMem] + filter_upwards [h0] with y hy + simpa [tsub_eq_zero_iff_le] using hy + rcases hπ.measure_eq_zero_or_measure_compl_eq_zero hφ hG (measure_ne_top π _) h_abs with h | h + · exact absurd h ht + · filter_upwards [measure_eq_zero_iff_ae_notMem.mp h] with x hx using by simpa using hx + +end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/Pow.lean b/RandomDo/ForMathlib/Probability/Kernel/Pow.lean new file mode 100644 index 0000000..880d0b8 --- /dev/null +++ b/RandomDo/ForMathlib/Probability/Kernel/Pow.lean @@ -0,0 +1,92 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp + +/-! +# Powers of kernels + +Lemmas about the powers `κ ^ n` of a kernel `κ : Kernel α α` for the monoid structure given by +composition. + +## Main statements + +* `Kernel.pow_add_apply`: `(κ ^ (m + n)) a = (κ ^ m) ∘ₘ (κ ^ n) a`. +* `Kernel.pow_add_comp`: `(κ ^ (m + n)) ∘ₘ μ = (κ ^ m) ∘ₘ ((κ ^ n) ∘ₘ μ)`. +* `Kernel.pow_succ_apply_pos_iff`: a point reaches a set with positive probability in `n + 1` + steps iff its first step goes with positive probability to the set of points which reach it + with positive probability in `n` steps. +-/ + +@[expose] public section + +open MeasureTheory + +open scoped ENNReal ProbabilityTheory + +namespace ProbabilityTheory.Kernel + +variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ : Measure α} + +instance [IsMarkovKernel κ] (n : ℕ) : IsMarkovKernel (κ ^ n) := by + induction n with + | zero => rw [pow_zero]; exact inferInstanceAs (IsMarkovKernel Kernel.id) + | succ n ih => rw [pow_succ]; exact inferInstanceAs (IsMarkovKernel ((κ ^ n) ∘ₖ κ)) + +instance [IsFiniteKernel κ] (n : ℕ) : IsFiniteKernel (κ ^ n) := by + induction n with + | zero => rw [pow_zero]; exact inferInstanceAs (IsFiniteKernel Kernel.id) + | succ n ih => rw [pow_succ]; exact inferInstanceAs (IsFiniteKernel ((κ ^ n) ∘ₖ κ)) + +instance [IsSFiniteKernel κ] (n : ℕ) : IsSFiniteKernel (κ ^ n) := by + induction n with + | zero => rw [pow_zero]; exact inferInstanceAs (IsSFiniteKernel Kernel.id) + | succ n ih => rw [pow_succ]; exact inferInstanceAs (IsSFiniteKernel ((κ ^ n) ∘ₖ κ)) + +lemma pow_zero_apply (κ : Kernel α α) (a : α) : (κ ^ 0) a = Measure.dirac a := by + rw [pow_zero]; exact Kernel.id_apply a + +lemma pow_add_apply (κ : Kernel α α) (m n : ℕ) (a : α) : + (κ ^ (m + n)) a = (κ ^ m) ∘ₘ (κ ^ n) a := by + rw [pow_add, comp_apply] + +lemma pow_succ_apply (κ : Kernel α α) (n : ℕ) (a : α) : (κ ^ (n + 1)) a = (κ ^ n) ∘ₘ κ a := by + rw [pow_add_apply, pow_one] + +lemma pow_succ_apply' (κ : Kernel α α) (n : ℕ) (a : α) : (κ ^ (n + 1)) a = κ ∘ₘ (κ ^ n) a := by + rw [add_comm, pow_add_apply, pow_one] + +lemma pow_add_comp (κ : Kernel α α) (m n : ℕ) (μ : Measure α) : + (κ ^ (m + n)) ∘ₘ μ = (κ ^ m) ∘ₘ ((κ ^ n) ∘ₘ μ) := by + rw [pow_add, Measure.comp_assoc] + +lemma pow_succ_comp (κ : Kernel α α) (n : ℕ) (μ : Measure α) : + (κ ^ (n + 1)) ∘ₘ μ = (κ ^ n) ∘ₘ (κ ∘ₘ μ) := by + rw [pow_add_comp, pow_one] + +lemma pow_succ_comp' (κ : Kernel α α) (n : ℕ) (μ : Measure α) : + (κ ^ (n + 1)) ∘ₘ μ = κ ∘ₘ ((κ ^ n) ∘ₘ μ) := by + rw [add_comm, pow_add_comp, pow_one] + +lemma pow_zero_comp (κ : Kernel α α) (μ : Measure α) : (κ ^ 0 : Kernel α α) ∘ₘ μ = μ := by + rw [pow_zero]; exact Measure.id_comp + +/-- A point `y` reaches the measurable set `C` with positive probability in `n + 1` steps iff +its first step goes with positive probability to the set of points which reach `C` with positive +probability in `n` steps. -/ +lemma pow_succ_apply_pos_iff {C : Set α} (hC : MeasurableSet C) {n : ℕ} {y : α} : + 0 < (κ ^ (n + 1)) y C ↔ 0 < κ y {z | 0 < (κ ^ n) z C} := by + rw [pow_succ_apply, Measure.comp_apply_pos_iff hC] + +/-- The measurable set `C` is reached from the measure `μ` with positive probability in `n + m` +steps iff after `m` steps, the set of points which reach `C` with positive probability in `n` +steps has positive measure. -/ +lemma pow_add_comp_apply_pos_iff {C : Set α} (hC : MeasurableSet C) {m n : ℕ} : + 0 < ((κ ^ (n + m)) ∘ₘ μ) C ↔ 0 < ((κ ^ m) ∘ₘ μ) {y | 0 < (κ ^ n) y C} := by + rw [pow_add_comp, Measure.comp_apply_pos_iff hC] + +end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Basic.lean b/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Basic.lean new file mode 100644 index 0000000..e10d4cc --- /dev/null +++ b/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Basic.lean @@ -0,0 +1,97 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import RandomDo.ForMathlib.Probability.Kernel.Pow + +/-! +# Small sets of a kernel + +A set `C` is *small* for a kernel `κ : Kernel α α` if the measures `(κ ^ n) x` for `x ∈ C` have a +common component: there is an `n : ℕ` and a measure `ν` such that `ν ≤ (κ ^ n) x` for all `x ∈ C`. +When `κ` is the transition kernel of a Markov chain, this means that the chain forgets where it +started in `C` with positive probability after `n` steps. + +## Main definitions + +* `ProbabilityTheory.Kernel.IsSmallSet κ C n ν`: `ν ≤ (κ ^ n) x` for all `x ∈ C`. + +## References + +* [Meyn, S.P. and Tweedie, R.L., *Markov Chains and Stochastic Stability*][meyntweedie1993] +-/ + +@[expose] public section + +open MeasureTheory + +open scoped ENNReal ProbabilityTheory + +namespace ProbabilityTheory.Kernel + +variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {C C' : Set α} {n : ℕ} + {ν ν' : Measure α} + +/-- A set `C` is `(n, ν)`-small for the kernel `κ : Kernel α α` if `ν ≤ (κ ^ n) x` for all +`x ∈ C`. +Ref. *Meyn-Tweedie*, Section 5.2. -/ +def IsSmallSet (κ : Kernel α α) (C : Set α) (n : ℕ) (ν : Measure α) : Prop := + ∀ x ∈ C, ν ≤ (κ ^ n) x + +namespace IsSmallSet + +lemma mono (h : IsSmallSet κ C n ν) (hC : C' ⊆ C) : IsSmallSet κ C' n ν := + fun x hx ↦ h x (hC hx) + +lemma mono_measure (h : IsSmallSet κ C n ν) (hν : ν' ≤ ν) : IsSmallSet κ C n ν' := + fun x hx ↦ hν.trans (h x hx) + +lemma isFiniteMeasure [IsFiniteKernel κ] (h : IsSmallSet κ C n ν) (hC : C.Nonempty) : + IsFiniteMeasure ν := + isFiniteMeasure_of_le _ (h hC.some hC.some_mem) + +/-- If `C` is `(n, ν)`-small, then a measure `μ` is sent by `κ ^ n` to a measure which is at +least `μ C • ν`. -/ +lemma smul_le_comp (h : IsSmallSet κ C n ν) (μ : Measure α) : μ C • ν ≤ (κ ^ n) ∘ₘ μ := by + refine Measure.le_iff.mpr fun s hs ↦ ?_ + rw [Measure.bind_apply hs (κ ^ n).aemeasurable, Measure.smul_apply, smul_eq_mul] + calc μ C * ν s = ∫⁻ _ in C, ν s ∂μ := by rw [MeasureTheory.setLIntegral_const, mul_comm] + _ ≤ ∫⁻ x in C, (κ ^ n) x s ∂μ := + setLIntegral_mono ((κ ^ n).measurable_coe hs) fun x hx ↦ h x hx s + _ ≤ ∫⁻ x, (κ ^ n) x s ∂μ := setLIntegral_le_lintegral _ _ + +/-- If `C` is `(n, ν)`-small, then `(κ ^ (n + m)) x` is at least `(κ ^ m) x C • ν`. -/ +lemma smul_le_pow_add_apply (h : IsSmallSet κ C n ν) (m : ℕ) (x : α) : + (κ ^ m) x C • ν ≤ (κ ^ (n + m)) x := by + rw [pow_add_apply] + exact h.smul_le_comp _ + +end IsSmallSet + +/-- If `C` is `(k, ν)`-small, the point `y` reaches `C` with positive probability in `n` steps +and `C` is reached from `ν` with positive probability in `m` steps, then `y` reaches `C` with +positive probability in `m + k + n` steps. -/ +lemma IsSmallSet.pow_apply_pos_of_pow_comp_apply_pos {C : Set α} {k m n : ℕ} {y : α} + (h : IsSmallSet κ C k ν) (hy : 0 < (κ ^ n) y C) (hm : 0 < ((κ ^ m) ∘ₘ ν) C) : + 0 < (κ ^ (m + k + n)) y C := by + have hle : (κ ^ n) y C • ((κ ^ m) ∘ₘ ν) ≤ (κ ^ (m + k + n)) y := by + rw [add_assoc, pow_add_apply, ← Measure.comp_smul] + exact Measure.comp_le_comp_right (h.smul_le_pow_add_apply n y) _ + refine lt_of_lt_of_le ?_ (hle C) + rw [Measure.smul_apply, smul_eq_mul] + exact ENNReal.mul_pos hy.ne' hm.ne' + +/-- If `C` is `(k, ν)`-small and is reached with positive probability from `μ` in `n` steps and +from `ν` in `m` steps, then it is reached with positive probability from `μ` in `m + k + n` +steps. -/ +lemma IsSmallSet.pow_comp_apply_pos_of_pow_comp_apply_pos {C : Set α} {k m n : ℕ} + {μ : Measure α} (h : IsSmallSet κ C k ν) (hC : MeasurableSet C) + (hμ : 0 < ((κ ^ n) ∘ₘ μ) C) (hm : 0 < ((κ ^ m) ∘ₘ ν) C) : + 0 < ((κ ^ (m + k + n)) ∘ₘ μ) C := by + rw [Measure.comp_apply_pos_iff hC] at hμ ⊢ + exact hμ.trans_le (measure_mono fun y hy ↦ h.pow_apply_pos_of_pow_comp_apply_pos hy hm) + +end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Exists.lean b/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Exists.lean new file mode 100644 index 0000000..c59bb22 --- /dev/null +++ b/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Exists.lean @@ -0,0 +1,165 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.Probability.Kernel.RadonNikodym +public import RandomDo.ForMathlib.MeasureTheory.Measure.SeparableMeasure +public import RandomDo.ForMathlib.Probability.Kernel.Irreducible +public import RandomDo.ForMathlib.Probability.Kernel.SmallSet.Basic + +/-! +# Existence of small sets + +For a `φ`-irreducible Markov kernel on a countably generated measurable space, every set of +positive `φ`-measure contains a small set of positive `φ`-measure. + +## Main statements + +* `ProbabilityTheory.Kernel.exists_isSmallSet`: existence of small sets. + +## Proof sketch + +Let `p n x` be the density of the absolutely continuous part of `(κ ^ (n + 1)) x` with respect to +`φ`, which is jointly measurable in `(x, y)` since the space is countably generated. + +* By irreducibility, for all `x`, for `φ`-almost every `y` there is `n` with `0 < p n x y` + (`IsIrreducible.ae_exists_rnDeriv_pow_succ_pos`). +* For `V x = {y | ε < p m x y}` and `W z = {y | ε' < p n y z}`, the previous point implies that we + can choose `m`, `n`, `ε`, `ε'` such that `∫⁻ x in A, ∫⁻ z, φ (V x ∩ W z) ∂φ ∂φ` is positive + (`exists_lintegral_measure_inter_pos`). +* Since `φ` is a finite measure on a countably generated space, there is a countable family of + sets which approximates every measurable set up to an arbitrarily small `φ`-measure. Sorting + the points `x` and `z` according to the sets of the family which approximate `V x` and `W z`, we + get sets `C ⊆ A` and `D` of positive measure and `δ > 0` such that `δ ≤ φ (V x ∩ W z)` for all + `x ∈ C` and `z ∈ D` (`exists_measurableSet_forall_le_measure_inter`). This replaces the use of a + differentiation theorem for measures in the classical proof. +* By the Chapman-Kolmogorov equation, `(κ ^ ((n + 1) + (m + 1))) x` dominates the measure with + density `z ↦ ∫⁻ y, p m x y * p n y z ∂φ` with respect to `φ` + (`Measure.withDensity_lintegral_mul_le_comp`), and that density is at least `ε * ε' * δ` for + `x ∈ C` and `z ∈ D` (`isSmallSet_of_le_lintegral_mul`). + +## References + +* [Meyn, S.P. and Tweedie, R.L., *Markov Chains and Stochastic Stability*][meyntweedie1993] +-/ + +@[expose] public section + +open MeasureTheory Set + +open scoped ENNReal NNReal ProbabilityTheory + +namespace ProbabilityTheory.Kernel + +variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {φ : Measure α} + +/-- If the measures `(κ ^ m) x` and `(κ ^ n) y` dominate the measures with densities `p x` and +`q y` with respect to `φ`, and if `∫⁻ y, p x y * q y z ∂φ` is bounded from below by `c` for +`x ∈ C` and `z ∈ D`, then `C` is a small set for `κ`. -/ +lemma isSmallSet_of_le_lintegral_mul [SFinite φ] {p q : α → α → ℝ≥0∞} {m n : ℕ} {C D : Set α} + {c : ℝ≥0} (hp : Measurable (Function.uncurry p)) (hq : Measurable (Function.uncurry q)) + (hpκ : ∀ x, φ.withDensity (p x) ≤ (κ ^ m) x) (hqκ : ∀ y, φ.withDensity (q y) ≤ (κ ^ n) y) + (hD : MeasurableSet D) (h : ∀ x ∈ C, ∀ z ∈ D, (c : ℝ≥0∞) ≤ ∫⁻ y, p x y * q y z ∂φ) : + IsSmallSet κ C (n + m) (c • φ.restrict D) := by + intro x hx + rw [pow_add_apply] + refine le_trans (Measure.le_iff.mpr fun B hB ↦ ?_) + (Measure.withDensity_lintegral_mul_le_comp hp.of_uncurry_left hq (hpκ x) hqκ) + rw [withDensity_apply _ hB, Measure.smul_apply, Measure.restrict_apply hB, + Measure.nnreal_smul_coe_apply] + calc c * φ (B ∩ D) + _ = ∫⁻ _ in B ∩ D, c ∂φ := by rw [MeasureTheory.setLIntegral_const] + _ ≤ ∫⁻ z in B ∩ D, ∫⁻ y, p x y * q y z ∂φ ∂φ := + setLIntegral_mono' (hB.inter hD) fun z hz ↦ h x hx z hz.2 + _ ≤ ∫⁻ z in B, ∫⁻ y, p x y * q y z ∂φ ∂φ := lintegral_mono_set inter_subset_left + +/-- For a `φ`-irreducible Markov kernel `κ` and all `x`, for `φ`-almost every `y`, one of the +densities of the measures `(κ ^ (n + 1)) x` with respect to `φ` is positive at `y`. -/ +lemma IsIrreducible.ae_exists_rnDeriv_pow_succ_pos [MeasurableSpace.CountablyGenerated α] + [IsMarkovKernel κ] [IsFiniteMeasure φ] [IsIrreducible φ κ] (x : α) : + ∀ᵐ y ∂φ, ∃ n, 0 < rnDeriv (κ ^ (n + 1)) (const α φ) x y := by + -- `N n` is a `φ`-null set outside of which `(κ ^ (n + 1)) x` has no singular part + let N : ℕ → Set α := fun n ↦ mutuallySingularSetSlice (κ ^ (n + 1)) (const α φ) x + have hN : MeasurableSet (⋃ n, N n) := + MeasurableSet.iUnion fun n ↦ measurableSet_mutuallySingularSetSlice _ _ _ + have hφN : φ (⋃ n, N n) = 0 := measure_iUnion_null fun n ↦ by + simpa using measure_mutuallySingularSetSlice (κ ^ (n + 1)) (const α φ) x + let B : Set α := {y | ∀ n, rnDeriv (κ ^ (n + 1)) (const α φ) x y = 0} + have hB : MeasurableSet B := by + simp only [B, ofPred_forall] + exact MeasurableSet.iInter fun n ↦ + measurableSet_eq_fun (measurable_rnDeriv_right _ _ _) measurable_const + suffices φ B = 0 by + filter_upwards [measure_eq_zero_iff_ae_notMem.mp this] with y hy + simpa [B, pos_iff_ne_zero] using hy + -- otherwise, by irreducibility `B \ ⋃ n, N n` would be charged by some `(κ ^ (n + 1)) x` + by_contra hB0 + have hB' : 0 < φ (B \ ⋃ n, N n) := by + rw [measure_sdiff_null hφN] + exact pos_iff_ne_zero.mpr hB0 + obtain ⟨n, hn⟩ := IsIrreducible.exists_pow_succ_pos (κ := κ) (hB.diff hN) hB' + (IsProbabilityMeasure.ne_zero (κ x)) + refine hn.ne' ?_ + rw [← withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice (η := const α φ) + (hB.diff hN) fun y hy hyN ↦ hy.2 (mem_iUnion.2 ⟨n, hyN⟩), + Kernel.withDensity_apply' _ (measurable_rnDeriv _ _), + setLIntegral_congr_fun (hB.diff hN) fun y hy ↦ hy.1 n, lintegral_zero] + +/-- **Existence of small sets**. For a `φ`-irreducible Markov kernel `κ` on a countably generated +measurable space, every set `A` of positive `φ`-measure contains a set `C` of positive +`φ`-measure which is small: there are `n > 0`, `c > 0` and a set `D` of positive `φ`-measure +such that `c • φ.restrict D ≤ (κ ^ n) x` for all `x ∈ C`. +Ref. *Meyn-Tweedie* Theorem 5.2.2. -/ +theorem exists_isSmallSet [MeasurableSpace.CountablyGenerated α] [IsMarkovKernel κ] + [IsFiniteMeasure φ] [IsIrreducible φ κ] {A : Set α} (hA : MeasurableSet A) (hφA : 0 < φ A) : + ∃ (C D : Set α) (n : ℕ) (c : ℝ≥0), MeasurableSet C ∧ MeasurableSet D ∧ C ⊆ A ∧ + 0 < φ C ∧ 0 < φ D ∧ 0 < n ∧ 0 < c ∧ IsSmallSet κ C n (c • φ.restrict D) := by + -- `p n x` is the density of the absolutely continuous part of `(κ ^ (n + 1)) x` w.r.t. `φ` + let p : ℕ → α → α → ℝ≥0∞ := fun n ↦ rnDeriv (κ ^ (n + 1)) (const α φ) + have hp (n : ℕ) : Measurable (Function.uncurry (p n)) := measurable_rnDeriv _ _ + have hpκ (n : ℕ) (x : α) : φ.withDensity (p n x) ≤ (κ ^ (n + 1)) x := by + have h := withDensity_rnDeriv_le (κ ^ (n + 1)) (const α φ) x + rwa [Kernel.withDensity_apply _ (hp n), const_apply] at h + -- `V (m, j) x` and `W (n, j) z` are the sets of `y` where `p m x y` and `p n y z` exceed `ε j` + let ε : ℕ → ℝ≥0 := fun j ↦ ((j : ℝ≥0) + 1)⁻¹ + have hε (j : ℕ) : 0 < ε j := by positivity + have hε_le (j : ℕ) : (ε j : ℝ≥0∞) ≤ (j : ℝ≥0∞)⁻¹ := by + have hj : ((j : ℝ≥0) + 1) ≠ 0 := by positivity + simp only [ε, ENNReal.coe_inv hj, ENNReal.coe_add, ENNReal.coe_natCast, ENNReal.coe_one] + exact ENNReal.inv_le_inv.mpr le_self_add + let V : ℕ × ℕ → α → Set α := fun i x ↦ {y | (ε i.2 : ℝ≥0∞) < p i.1 x y} + let W : ℕ × ℕ → α → Set α := fun i z ↦ {y | (ε i.2 : ℝ≥0∞) < p i.1 y z} + have hV (i : ℕ × ℕ) : MeasurableSet {q : α × α | q.2 ∈ V i q.1} := + measurableSet_lt measurable_const (hp i.1) + have hW (i : ℕ × ℕ) : MeasurableSet {q : α × α | q.2 ∈ W i q.1} := + measurableSet_lt measurable_const ((hp i.1).comp measurable_swap) + have hp_pos (x : α) : ∀ᵐ y ∂φ, ∃ i : ℕ × ℕ, (ε i.2 : ℝ≥0∞) < p i.1 x y := by + filter_upwards [IsIrreducible.ae_exists_rnDeriv_pow_succ_pos (κ := κ) x] with y ⟨n, hn⟩ + obtain ⟨j, hj⟩ := ENNReal.exists_inv_nat_lt hn.ne' + exact ⟨(n, j), (hε_le j).trans_lt hj⟩ + -- we find `C ⊆ A` and `D` such that `φ (V i x ∩ W i' z)` is bounded from below on `C ×ˢ D` + have hφ : φ ≠ 0 := fun h ↦ hφA.ne' (by simp [h]) + have hφA' : φ.restrict A ≠ 0 := Measure.restrict_eq_zero.not.mpr hφA.ne' + obtain ⟨i, i', hi⟩ := exists_lintegral_measure_inter_pos (μ := φ.restrict A) hV hW + (ae_of_all _ hp_pos) (ae_of_all _ hp_pos) hφA' hφ hφ + obtain ⟨C, D, δ, hC, hD, hφC, hφD, hδ, hCD⟩ := + exists_measurableSet_forall_le_measure_inter (hV i) (hW i') hi + rw [Measure.restrict_apply hC] at hφC + -- the set `C ∩ A` is small + refine ⟨C ∩ A, D, (i'.1 + 1) + (i.1 + 1), ε i.2 * ε i'.2 * δ, hC.inter hA, hD, inter_subset_right, + hφC, hφD, by lia, mul_pos (mul_pos (hε _) (hε _)) hδ, ?_⟩ + refine isSmallSet_of_le_lintegral_mul (hp i.1) (hp i'.1) (hpκ i.1) (hpκ i'.1) hD + fun x hx z hz ↦ ?_ + calc ((ε i.2 * ε i'.2 * δ : ℝ≥0) : ℝ≥0∞) + _ = ε i.2 * ε i'.2 * δ := by simp only [ENNReal.coe_mul] + _ ≤ ε i.2 * ε i'.2 * φ (V i x ∩ W i' z) := by + gcongr + exact hCD x hx.1 z hz + _ ≤ ∫⁻ y, p i.1 x y * p i'.1 y z ∂φ := + mul_measure_inter_lt_le_lintegral_mul (hp i.1).of_uncurry_left.aemeasurable + (hp i'.1).of_uncurry_right.aemeasurable _ _ + +end ProbabilityTheory.Kernel diff --git a/RandomDo/Measurable.lean b/RandomDo/Measurable.lean index 2aab168..3dbc146 100644 --- a/RandomDo/Measurable.lean +++ b/RandomDo/Measurable.lean @@ -6,7 +6,7 @@ Authors: Gaëtan Serré module public import RandomDo.Monad.ForInInstances -public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Embedding +public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma public import Mathlib.MeasureTheory.MeasurableSpace.Prod public import Mathlib.Data.List.OfFn @@ -44,7 +44,7 @@ def List.measurableEquivSigmaTuple : List α ≃ᵐ Σ n, Fin n → α where lemma measurableEmbedding_ofFn (n : ℕ) : MeasurableEmbedding (List.ofFn : (Fin n → α) → List α) := - List.measurableEquivSigmaTuple.symm.measurableEmbedding.comp (measurableEmbedding_sigmaMk n) + List.measurableEquivSigmaTuple.symm.measurableEmbedding.comp (measurableEmbedding_sigma_mk n) @[fun_prop] lemma measurable_ofFn (n : ℕ) : Measurable (List.ofFn : (Fin n → α) → List α) := From c61ce2b22ea5d2553d3153c6895085521fcffe5b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 14 Oct 2026 09:15:53 +0200 Subject: [PATCH 2/5] simplify lemma --- .../TotalVariation/DataProcessing.lean | 3 +- .../Measure/TotalVariation/Defs.lean | 35 ++++++++++++------- .../Probability/Kernel/ErgodicTheorem.lean | 3 +- 3 files changed, 27 insertions(+), 14 deletions(-) diff --git a/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/DataProcessing.lean b/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/DataProcessing.lean index ec9cc07..f227c66 100644 --- a/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/DataProcessing.lean +++ b/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/DataProcessing.lean @@ -48,7 +48,8 @@ lemma etvDist_comp_le (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] (μ ν : Measu (κ ∘ₘ (μ.restrict s + ν.restrict sᶜ) + κ ∘ₘ (ν.restrict s - μ.restrict s)) := by rw [← Measure.comp_add, ← Measure.comp_add, ← hμ, ← hν] _ ≤ (κ ∘ₘ (μ.restrict sᶜ - ν.restrict sᶜ)) Set.univ - + (κ ∘ₘ (ν.restrict s - μ.restrict s)) Set.univ := etvDist_add_left_le _ _ _ + + (κ ∘ₘ (ν.restrict s - μ.restrict s)) Set.univ := + (etvDist_add_left _ _ _).trans_le etvDist_le_add _ = ν s - μ s + (μ sᶜ - ν sᶜ) := by rw [Measure.comp_apply_univ, Measure.comp_apply_univ, Measure.sub_apply .univ hs.ge_on_compl, Measure.sub_apply .univ hs.le_on, add_comm] diff --git a/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean b/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean index f38836f..122199d 100644 --- a/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean +++ b/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean @@ -8,11 +8,12 @@ module public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs /-! -# Total variation distance of measures with a common part +# Translation invariance of the total variation distance ## Main statements -* `etvDist_add_left_le`: `etvDist (ξ + μ) (ξ + ν) ≤ μ univ + ν univ`. +* `etvDist_add_left`, `etvDist_add_right`: `etvDist (ξ + μ) (ξ + ν) = etvDist μ ν` for a finite + measure `ξ`. -/ @[expose] public section @@ -23,15 +24,25 @@ namespace MeasureTheory variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} -/-- If two measures have a common part `ξ`, their total variation distance is at most the sum of -the masses of the remaining parts. -/ -lemma etvDist_add_left_le (ξ μ ν : Measure 𝓧) [IsFiniteMeasure ξ] : - etvDist (ξ + μ) (ξ + ν) ≤ μ Set.univ + ν Set.univ := by - calc etvDist (ξ + μ) (ξ + ν) - _ ≤ etvDist (ξ + μ) ξ + etvDist ξ (ξ + ν) := etvDist_triangle _ _ _ - _ = μ Set.univ + ν Set.univ := by - rw [etvDist_of_ge (Measure.le_add_right le_rfl), etvDist_of_le (Measure.le_add_right le_rfl), - Measure.add_apply, Measure.add_apply, ENNReal.add_sub_cancel_left (measure_ne_top _ _), - ENNReal.add_sub_cancel_left (measure_ne_top _ _)] +/-- The total variation distance is invariant by translation: adding a common finite part `ξ` +to two measures does not change their distance. -/ +lemma etvDist_add_left (ξ μ ν : Measure 𝓧) [IsFiniteMeasure ξ] : + etvDist (ξ + μ) (ξ + ν) = etvDist μ ν := by + by_cases h : IsFiniteMeasure μ ∧ IsFiniteMeasure ν + · obtain ⟨_, _⟩ := h + rw [etvDist_eq_etvDist_toSignedMeasure, etvDist_eq_etvDist_toSignedMeasure, + Measure.toSignedMeasure_add, Measure.toSignedMeasure_add, VectorMeasure.etvDist, + VectorMeasure.etvDist, add_sub_add_left_eq_sub] + · have h' : ¬ (IsFiniteMeasure (ξ + μ) ∧ IsFiniteMeasure (ξ + ν)) := by + rintro ⟨hμ, hν⟩ + exact h ⟨isFiniteMeasure_of_le (ξ + μ) (Measure.le_add_left le_rfl), + isFiniteMeasure_of_le (ξ + ν) (Measure.le_add_left le_rfl)⟩ + rw [etvDist_of_not_isFiniteMeasure h', etvDist_of_not_isFiniteMeasure h] + +/-- The total variation distance is invariant by translation: adding a common finite part `ξ` +to two measures does not change their distance. -/ +lemma etvDist_add_right (μ ν ξ : Measure 𝓧) [IsFiniteMeasure ξ] : + etvDist (μ + ξ) (ν + ξ) = etvDist μ ν := by + rw [add_comm μ, add_comm ν, etvDist_add_left] end MeasureTheory diff --git a/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean b/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean index 1c39bf0..7677754 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean @@ -228,7 +228,8 @@ lemma etvDist_pow_comp_le [IsMarkovKernel κ] [IsProbabilityMeasure π] (hπ : obtain ⟨g, a', b', hg, hag, hbg, ha', hb', hab, h_le⟩ := exists_split_pow_comp hπ hB hsmall hK ha i rw [hag, hbg] - calc etvDist (g + a') (g + b') ≤ a' Set.univ + b' Set.univ := etvDist_add_left_le g a' b' + calc etvDist (g + a') (g + b') ≤ a' Set.univ + b' Set.univ := + (etvDist_add_left g a' b').trans_le etvDist_le_add _ = 2 * a' Set.univ := by rw [← hab, two_mul] _ ≤ 2 * (K * π Bᶜ + (1 - ν Set.univ) ^ i * a Set.univ) := by gcongr From 3535525f58aa59a1dbbd51b5c3c28c8bb8605965 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 14 Oct 2026 09:19:44 +0200 Subject: [PATCH 3/5] generalize a lemma to vector measures --- RandomDo.lean | 1 + .../Measure/TotalVariation/Defs.lean | 4 +-- .../VectorMeasure/TotalVariation.lean | 35 +++++++++++++++++++ 3 files changed, 38 insertions(+), 2 deletions(-) create mode 100644 RandomDo/ForMathlib/MeasureTheory/VectorMeasure/TotalVariation.lean diff --git a/RandomDo.lean b/RandomDo.lean index 4e802c6..c1043b2 100644 --- a/RandomDo.lean +++ b/RandomDo.lean @@ -7,6 +7,7 @@ public import RandomDo.ForMathlib.MeasureTheory.Measure.Prod public import RandomDo.ForMathlib.MeasureTheory.Measure.SeparableMeasure public import RandomDo.ForMathlib.MeasureTheory.Measure.TotalVariation.DataProcessing public import RandomDo.ForMathlib.MeasureTheory.Measure.TotalVariation.Defs +public import RandomDo.ForMathlib.MeasureTheory.VectorMeasure.TotalVariation public import RandomDo.ForMathlib.NumberTheory.FrobeniusNumber public import RandomDo.ForMathlib.Probability.Kernel.Aperiodic public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp diff --git a/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean b/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean index 122199d..09808e5 100644 --- a/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean +++ b/RandomDo/ForMathlib/MeasureTheory/Measure/TotalVariation/Defs.lean @@ -6,6 +6,7 @@ Authors: Rémy Degenne module public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs +public import RandomDo.ForMathlib.MeasureTheory.VectorMeasure.TotalVariation /-! # Translation invariance of the total variation distance @@ -31,8 +32,7 @@ lemma etvDist_add_left (ξ μ ν : Measure 𝓧) [IsFiniteMeasure ξ] : by_cases h : IsFiniteMeasure μ ∧ IsFiniteMeasure ν · obtain ⟨_, _⟩ := h rw [etvDist_eq_etvDist_toSignedMeasure, etvDist_eq_etvDist_toSignedMeasure, - Measure.toSignedMeasure_add, Measure.toSignedMeasure_add, VectorMeasure.etvDist, - VectorMeasure.etvDist, add_sub_add_left_eq_sub] + Measure.toSignedMeasure_add, Measure.toSignedMeasure_add, VectorMeasure.etvDist_add_left] · have h' : ¬ (IsFiniteMeasure (ξ + μ) ∧ IsFiniteMeasure (ξ + ν)) := by rintro ⟨hμ, hν⟩ exact h ⟨isFiniteMeasure_of_le (ξ + μ) (Measure.le_add_left le_rfl), diff --git a/RandomDo/ForMathlib/MeasureTheory/VectorMeasure/TotalVariation.lean b/RandomDo/ForMathlib/MeasureTheory/VectorMeasure/TotalVariation.lean new file mode 100644 index 0000000..d387392 --- /dev/null +++ b/RandomDo/ForMathlib/MeasureTheory/VectorMeasure/TotalVariation.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.MeasureTheory.VectorMeasure.TotalVariation + +/-! +# Translation invariance of the total variation distance of vector measures + +## Main statements + +* `VectorMeasure.etvDist_add_left`, `VectorMeasure.etvDist_add_right`: + `etvDist (ξ + μ) (ξ + ν) = etvDist μ ν`. +-/ + +@[expose] public section + +open scoped ENNReal + +namespace MeasureTheory.VectorMeasure + +variable {𝓧 M : Type*} {m𝓧 : MeasurableSpace 𝓧} [NormedAddCommGroup M] + +/-- The total variation distance is invariant by translation. -/ +lemma etvDist_add_left (ξ μ ν : VectorMeasure 𝓧 M) : etvDist (ξ + μ) (ξ + ν) = etvDist μ ν := by + rw [etvDist, etvDist, add_sub_add_left_eq_sub] + +/-- The total variation distance is invariant by translation. -/ +lemma etvDist_add_right (μ ν ξ : VectorMeasure 𝓧 M) : etvDist (μ + ξ) (ν + ξ) = etvDist μ ν := by + rw [etvDist, etvDist, add_sub_add_right_eq_sub] + +end MeasureTheory.VectorMeasure From e72b6608c825a39d33b8776a220faeecaf3bdd14 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 14 Oct 2026 10:45:46 +0200 Subject: [PATCH 4/5] review --- .../Probability/Kernel/ErgodicTheorem.lean | 10 +++---- .../Probability/Kernel/Invariance.lean | 12 ++++---- .../ForMathlib/Probability/Kernel/Pow.lean | 29 ++++++++++++++----- 3 files changed, 31 insertions(+), 20 deletions(-) diff --git a/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean b/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean index 7677754..aa6a101 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean @@ -191,14 +191,14 @@ private lemma exists_split_pow_comp [IsMarkovKernel κ] [IsProbabilityMeasure π ?_, ?_, ?_, ?_, ?_, ?_⟩ · rw [Nat.mul_succ, add_comm, pow_add_comp, hag, Measure.comp_add, add_assoc, add_comm (c • ν), Measure.sub_add_cancel_of_le hca] - · calc a Set.univ • π = (κ ^ j) ∘ₘ (a Set.univ • π) := (hπ.pow_comp_smul j _).symm + · calc a Set.univ • π = (κ ^ j) ∘ₘ (a Set.univ • π) := ((hπ.smul _).pow j).def.symm _ = (κ ^ j) ∘ₘ g + c • ν + ((κ ^ j) ∘ₘ b' - c • ν) := by rw [hbg, Measure.comp_add, add_assoc, add_comm (c • ν), Measure.sub_add_cancel_of_le hcb] · exact Measure.sub_le.trans - ((Measure.comp_le_comp_right ha' _).trans_eq (hπ.pow_comp_smul j K)) + ((Measure.comp_le_comp_right ha' _).trans_eq ((hπ.smul K).pow j).def) · exact Measure.sub_le.trans - ((Measure.comp_le_comp_right hb' _).trans_eq (hπ.pow_comp_smul j K)) + ((Measure.comp_le_comp_right hb' _).trans_eq ((hπ.smul K).pow j).def) · rw [Measure.sub_apply .univ hca, Measure.sub_apply .univ hcb, Measure.comp_apply_univ, Measure.comp_apply_univ, hab] · rw [Measure.sub_apply .univ hca, Measure.comp_apply_univ, Measure.smul_apply, smul_eq_mul, @@ -374,7 +374,7 @@ private lemma excess_add_apply_univ_le (hπ : κ.Invariant π) (m i : ℕ) (x : rw [← Measure.bind_apply .univ (excess κ π m).aemeasurable] refine excess_apply_univ_le_of_le ?_ set η : Kernel α α := κ ^ m - have h_inv : η ∘ₘ ((i : ℝ≥0) • π) = (i : ℝ≥0) • π := hπ.pow_comp_smul m (i : ℝ≥0) + have h_inv : η ∘ₘ ((i : ℝ≥0) • π) = (i : ℝ≥0) • π := ((hπ.smul (i : ℝ≥0)).pow m).def have h_le_one : excess κ π i x Set.univ • ((m : ℝ≥0) • π) ≤ (m : ℝ≥0) • π := by refine Measure.le_iff.mpr fun s _ ↦ ?_ rw [Measure.smul_apply, smul_eq_mul] @@ -440,7 +440,7 @@ private lemma excessMass_lt_one (hπ : κ.Invariant π) {c : ℝ≥0} (hνc : ν rw [Measure.coe_nnreal_smul_apply, Measure.coe_nnreal_smul_apply] gcongr exact (Nat.le_ceil c).trans (by exact_mod_cast Nat.le_add_right ⌈c⌉₊ n) - have h_inv : η ∘ₘ (c • π) = c • π := hπ.pow_comp_smul p c + have h_inv : η ∘ₘ (c • π) = c • π := ((hπ.smul c).pow p).def have h_le : (κ ^ (p + n)) x ≤ η ∘ₘ ((κ ^ n) x - w • ν) + ((p + n : ℕ) : ℝ≥0) • π := by calc (κ ^ (p + n)) x = η ∘ₘ (κ ^ n) x := pow_add_apply κ p n x _ = η ∘ₘ ((κ ^ n) x - w • ν) + η ∘ₘ (w • ν) := by diff --git a/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean b/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean index c2558ff..7b5138f 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean @@ -14,6 +14,7 @@ public import RandomDo.ForMathlib.Probability.Kernel.Pow ## Main statements * `Kernel.Invariant.pow`: a measure invariant for `κ` is invariant for `κ ^ n`. +* `Kernel.Invariant.smul`: a multiple of an invariant measure is invariant. * `Kernel.Invariant.ae_ae_pow`: if a property holds `μ`-almost everywhere for a measure `μ` invariant for `κ`, then for `μ`-almost every `a` it holds `(κ ^ n) a`-almost everywhere for all `n`. @@ -35,13 +36,10 @@ variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ π : Me lemma Invariant.pow (h : κ.Invariant μ) (n : ℕ) : (κ ^ n).Invariant μ := by induction n with | zero => exact pow_zero_comp κ μ - | succ n ih => rw [Invariant, pow_succ_comp, h.def, ih.def] + | succ n ih => rw [pow_succ, mul_eq_comp]; exact ih.comp h -lemma Invariant.pow_comp_eq (h : κ.Invariant μ) (n : ℕ) : (κ ^ n) ∘ₘ μ = μ := h.pow n - -lemma Invariant.pow_comp_smul (h : κ.Invariant μ) (n : ℕ) (c : ℝ≥0∞) : - (κ ^ n) ∘ₘ (c • μ) = c • μ := by - rw [Measure.comp_smul, h.pow_comp_eq] +lemma Invariant.smul (h : κ.Invariant μ) (c : ℝ≥0∞) : κ.Invariant (c • μ) := by + rw [Invariant, Measure.comp_smul, h.def] /-- If `μ` is invariant for `κ` and a property holds `μ`-almost everywhere, then for `μ`-almost every `a` it holds `(κ ^ n) a`-almost everywhere for all `n`. -/ @@ -49,7 +47,7 @@ lemma Invariant.ae_ae_pow (h : κ.Invariant μ) {p : α → Prop} (hp : ∀ᵐ a ∀ᵐ a ∂μ, ∀ n, ∀ᵐ b ∂(κ ^ n) a, p b := by rw [ae_all_iff] intro n - rw [← h.pow_comp_eq n] at hp + rw [← (h.pow n).def] at hp exact Measure.ae_ae_of_ae_comp hp /-! ### Absorbing sets -/ diff --git a/RandomDo/ForMathlib/Probability/Kernel/Pow.lean b/RandomDo/ForMathlib/Probability/Kernel/Pow.lean index 880d0b8..cccacf7 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/Pow.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/Pow.lean @@ -15,6 +15,10 @@ composition. ## Main statements +* `Kernel.one_eq_id`, `Kernel.mul_eq_comp`: the unit of the monoid is `Kernel.id` and its + multiplication is the composition `∘ₖ`. +* Instances: `κ ^ n` is a Markov kernel (resp. a zero or Markov kernel, a finite kernel, + an s-finite kernel) if `κ` is. * `Kernel.pow_add_apply`: `(κ ^ (m + n)) a = (κ ^ m) ∘ₘ (κ ^ n) a`. * `Kernel.pow_add_comp`: `(κ ^ (m + n)) ∘ₘ μ = (κ ^ m) ∘ₘ ((κ ^ n) ∘ₘ μ)`. * `Kernel.pow_succ_apply_pos_iff`: a point reaches a set with positive probability in `n + 1` @@ -32,23 +36,32 @@ namespace ProbabilityTheory.Kernel variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ : Measure α} +@[simp] lemma one_eq_id : (1 : Kernel α α) = Kernel.id := rfl + +@[simp] lemma mul_eq_comp (η κ : Kernel α α) : η * κ = η ∘ₖ κ := rfl + instance [IsMarkovKernel κ] (n : ℕ) : IsMarkovKernel (κ ^ n) := by induction n with - | zero => rw [pow_zero]; exact inferInstanceAs (IsMarkovKernel Kernel.id) - | succ n ih => rw [pow_succ]; exact inferInstanceAs (IsMarkovKernel ((κ ^ n) ∘ₖ κ)) + | zero => rw [pow_zero, one_eq_id]; infer_instance + | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance + +instance [IsZeroOrMarkovKernel κ] (n : ℕ) : IsZeroOrMarkovKernel (κ ^ n) := by + induction n with + | zero => rw [pow_zero, one_eq_id]; infer_instance + | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance instance [IsFiniteKernel κ] (n : ℕ) : IsFiniteKernel (κ ^ n) := by induction n with - | zero => rw [pow_zero]; exact inferInstanceAs (IsFiniteKernel Kernel.id) - | succ n ih => rw [pow_succ]; exact inferInstanceAs (IsFiniteKernel ((κ ^ n) ∘ₖ κ)) + | zero => rw [pow_zero, one_eq_id]; infer_instance + | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance instance [IsSFiniteKernel κ] (n : ℕ) : IsSFiniteKernel (κ ^ n) := by induction n with - | zero => rw [pow_zero]; exact inferInstanceAs (IsSFiniteKernel Kernel.id) - | succ n ih => rw [pow_succ]; exact inferInstanceAs (IsSFiniteKernel ((κ ^ n) ∘ₖ κ)) + | zero => rw [pow_zero, one_eq_id]; infer_instance + | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance lemma pow_zero_apply (κ : Kernel α α) (a : α) : (κ ^ 0) a = Measure.dirac a := by - rw [pow_zero]; exact Kernel.id_apply a + rw [pow_zero, one_eq_id, id_apply] lemma pow_add_apply (κ : Kernel α α) (m n : ℕ) (a : α) : (κ ^ (m + n)) a = (κ ^ m) ∘ₘ (κ ^ n) a := by @@ -73,7 +86,7 @@ lemma pow_succ_comp' (κ : Kernel α α) (n : ℕ) (μ : Measure α) : rw [add_comm, pow_add_comp, pow_one] lemma pow_zero_comp (κ : Kernel α α) (μ : Measure α) : (κ ^ 0 : Kernel α α) ∘ₘ μ = μ := by - rw [pow_zero]; exact Measure.id_comp + simp /-- A point `y` reaches the measurable set `C` with positive probability in `n + 1` steps iff its first step goes with positive probability to the set of points which reach `C` with positive From d343758c4ef38ffae8c01a656f862fa04162e636 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 16 Oct 2026 13:10:46 +0200 Subject: [PATCH 5/5] update --- RandomDo.lean | 2 +- .../Probability/Kernel/Aperiodic.lean | 6 +- .../Probability/Kernel/Composition/Comp.lean | 67 +++++++++++ .../Kernel/Composition/MeasureComp.lean | 31 +++++- .../Probability/Kernel/ErgodicTheorem.lean | 16 +-- .../Probability/Kernel/HarrisRecurrent.lean | 8 +- .../Probability/Kernel/Invariance.lean | 37 +++--- .../Probability/Kernel/Irreducible.lean | 4 +- .../ForMathlib/Probability/Kernel/Pow.lean | 105 ------------------ .../Probability/Kernel/SmallSet/Basic.lean | 6 +- .../Probability/Kernel/SmallSet/Exists.lean | 2 +- 11 files changed, 137 insertions(+), 147 deletions(-) create mode 100644 RandomDo/ForMathlib/Probability/Kernel/Composition/Comp.lean delete mode 100644 RandomDo/ForMathlib/Probability/Kernel/Pow.lean diff --git a/RandomDo.lean b/RandomDo.lean index c1043b2..5d7ef44 100644 --- a/RandomDo.lean +++ b/RandomDo.lean @@ -10,12 +10,12 @@ public import RandomDo.ForMathlib.MeasureTheory.Measure.TotalVariation.Defs public import RandomDo.ForMathlib.MeasureTheory.VectorMeasure.TotalVariation public import RandomDo.ForMathlib.NumberTheory.FrobeniusNumber public import RandomDo.ForMathlib.Probability.Kernel.Aperiodic +public import RandomDo.ForMathlib.Probability.Kernel.Composition.Comp public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp public import RandomDo.ForMathlib.Probability.Kernel.ErgodicTheorem public import RandomDo.ForMathlib.Probability.Kernel.HarrisRecurrent public import RandomDo.ForMathlib.Probability.Kernel.Invariance public import RandomDo.ForMathlib.Probability.Kernel.Irreducible -public import RandomDo.ForMathlib.Probability.Kernel.Pow public import RandomDo.ForMathlib.Probability.Kernel.SmallSet.Basic public import RandomDo.ForMathlib.Probability.Kernel.SmallSet.Exists public import RandomDo.Measurable diff --git a/RandomDo/ForMathlib/Probability/Kernel/Aperiodic.lean b/RandomDo/ForMathlib/Probability/Kernel/Aperiodic.lean index 59d4f51..f00e5aa 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/Aperiodic.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/Aperiodic.lean @@ -74,13 +74,13 @@ lemma exists_measurableSet_superset_forall_notMem_apply_eq_zero {S : Set α} ∃ B, MeasurableSet B ∧ S ⊆ B ∧ ν B = 0 ∧ ∀ y ∉ B, κ y B = 0 := by refine ⟨⋃ m : ℕ, {y | 0 < (κ ^ m) y S}, .iUnion fun m ↦ measurableSet_apply_pos _ hS, fun y hy ↦ Set.mem_iUnion.mpr ⟨0, ?_⟩, ?_, fun y hy ↦ ?_⟩ - · rw [Set.mem_ofPred_eq, pow_zero_apply, Measure.dirac_apply_of_mem hy] + · rw [Set.mem_ofPred_eq, pow_zero, one_eq_id, Kernel.id_apply, Measure.dirac_apply_of_mem hy] exact zero_lt_one · rw [measure_iUnion_null_iff] exact fun m ↦ (Measure.comp_apply_eq_zero_iff hS).mp (h m) · rw [measure_iUnion_null_iff] intro m - rw [← Measure.comp_apply_eq_zero_iff hS, ← pow_succ_apply] + rw [← Measure.comp_apply_eq_zero_iff hS, ← comp_apply, ← pow_add_one] simp only [Set.mem_iUnion, Set.mem_ofPred_eq, not_exists, not_lt, nonpos_iff_eq_zero] at hy exact hy (m + 1) @@ -190,7 +190,7 @@ lemma IsAperiodic.exists_forall_pow_comp_apply_pos [IsMarkovKernel κ] [IsIrredu -- otherwise, we get two times with different phases reachable from the same points obtain ⟨m, n₁, n₂, hne, hpos⟩ := hκ.exists_pow_comp_inter_pos hν hνπ (E := fun n ↦ {y | 0 < (κ ^ n) y C}) (fun n ↦ measurableSet_apply_pos _ hC) - (IsIrreducible.irreducible (φ := φ) hC hφC) (fun y n h ↦ (pow_succ_apply_pos_iff hC).mpr h) d + (IsIrreducible.irreducible (φ := φ) hC hφC) (fun y n h ↦ (pow_add_one_apply_pos_iff hC).mpr h) d have h₁ : d + 2 ∣ n₁ + m + k := hdvd _ ((pow_add_comp_apply_pos_iff hC).mpr (hpos.trans_le (measure_mono Set.inter_subset_left))) have h₂ : d + 2 ∣ n₂ + m + k := hdvd _ ((pow_add_comp_apply_pos_iff hC).mpr diff --git a/RandomDo/ForMathlib/Probability/Kernel/Composition/Comp.lean b/RandomDo/ForMathlib/Probability/Kernel/Composition/Comp.lean new file mode 100644 index 0000000..f6d4a29 --- /dev/null +++ b/RandomDo/ForMathlib/Probability/Kernel/Composition/Comp.lean @@ -0,0 +1,67 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import Mathlib.Probability.Kernel.Composition.Comp + +/-! +# The monoid of kernels + +Lemmas about the monoid structure on `Kernel α α` given by composition, and about the powers +`κ ^ n` of a kernel `κ : Kernel α α`. + +## Main statements + +* `Kernel.one_eq_id`, `Kernel.mul_eq_comp`: the unit of the monoid is `Kernel.id` and its + multiplication is the composition `∘ₖ`. +* Instances: `κ ^ n` is a Markov kernel (resp. a zero or Markov kernel, a finite kernel, + an s-finite kernel) if `κ` is. +* `Kernel.pow_add_one`, `Kernel.pow_add_one'`: `κ ^ (n + 1) = κ ^ n ∘ₖ κ = κ ∘ₖ κ ^ n`. +-/ + +@[expose] public section + +open MeasureTheory + +namespace ProbabilityTheory.Kernel + +variable {α : Type*} {mα : MeasurableSpace α} + +@[simp] lemma one_eq_id : (1 : Kernel α α) = Kernel.id := rfl + +@[simp] lemma mul_eq_comp (η κ : Kernel α α) : η * κ = η ∘ₖ κ := rfl + +instance IsMarkovKernel.pow (κ : Kernel α α) [IsMarkovKernel κ] (n : ℕ) : + IsMarkovKernel (κ ^ n) := by + induction n with + | zero => rw [pow_zero, one_eq_id]; infer_instance + | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance + +instance IsZeroOrMarkovKernel.pow (κ : Kernel α α) [IsZeroOrMarkovKernel κ] (n : ℕ) : + IsZeroOrMarkovKernel (κ ^ n) := by + induction n with + | zero => rw [pow_zero, one_eq_id]; infer_instance + | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance + +instance IsFiniteKernel.pow (κ : Kernel α α) [IsFiniteKernel κ] (n : ℕ) : + IsFiniteKernel (κ ^ n) := by + induction n with + | zero => rw [pow_zero, one_eq_id]; infer_instance + | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance + +instance IsSFiniteKernel.pow (κ : Kernel α α) [IsSFiniteKernel κ] (n : ℕ) : + IsSFiniteKernel (κ ^ n) := by + induction n with + | zero => rw [pow_zero, one_eq_id]; infer_instance + | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance + +lemma pow_add_one (κ : Kernel α α) (n : ℕ) : κ ^ (n + 1) = (κ ^ n) ∘ₖ κ := by + rw [pow_add, pow_one] + +lemma pow_add_one' (κ : Kernel α α) (n : ℕ) : κ ^ (n + 1) = κ ∘ₖ (κ ^ n) := by + rw [add_comm, pow_add, pow_one] + +end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/Composition/MeasureComp.lean b/RandomDo/ForMathlib/Probability/Kernel/Composition/MeasureComp.lean index 642ef83..b4358eb 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/Composition/MeasureComp.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/Composition/MeasureComp.lean @@ -6,6 +6,7 @@ Authors: Rémy Degenne module public import Mathlib.Probability.Kernel.Composition.MeasureComp +public import RandomDo.ForMathlib.Probability.Kernel.Composition.Comp /-! # Lemmas about the composition of a measure and a kernel @@ -17,6 +18,8 @@ public import Mathlib.Probability.Kernel.Composition.MeasureComp * `Measure.restrict_comp`: `(κ.restrict hs) ∘ₘ μ = (κ ∘ₘ μ).restrict s`. * `Measure.comp_apply_pos_iff`: `0 < (η ∘ₘ μ) s ↔ 0 < μ {a | 0 < η a s}`. * `Measure.withDensity_lintegral_mul_le_comp`: Chapman-Kolmogorov inequality for densities. +* `Kernel.pow_add_one_apply_pos_iff`, `Kernel.pow_add_comp_apply_pos_iff`: positivity of the + measure of a set after `n + 1` (resp. `n + m`) steps of a kernel. -/ @[expose] public section @@ -61,7 +64,7 @@ lemma restrict_comp (hs : MeasurableSet s) : (κ.restrict hs) ∘ₘ μ = (κ /-- The measure `η ∘ₘ μ` gives positive mass to a measurable set `s` iff the set of points `a` such that `η a s` is positive has positive `μ`-measure. -/ -lemma comp_apply_pos_iff (hs : MeasurableSet s) : +lemma comp_apply_pos_iff {s : Set β} (hs : MeasurableSet s) : 0 < (η ∘ₘ μ) s ↔ 0 < μ {a | 0 < η a s} := by rw [Measure.bind_apply hs η.aemeasurable, lintegral_pos_iff_support (η.measurable_coe hs)] congr! 2 @@ -70,7 +73,7 @@ lemma comp_apply_pos_iff (hs : MeasurableSet s) : /-- The measure `η ∘ₘ μ` gives zero mass to a measurable set `s` iff the set of points `a` such that `η a s` is positive has `μ`-measure zero. -/ -lemma comp_apply_eq_zero_iff (hs : MeasurableSet s) : +lemma comp_apply_eq_zero_iff {s : Set β} (hs : MeasurableSet s) : (η ∘ₘ μ) s = 0 ↔ μ {a | 0 < η a s} = 0 := by rw [← not_iff_not, ← Ne, ← Ne, ← pos_iff_ne_zero, ← pos_iff_ne_zero, comp_apply_pos_iff hs] @@ -100,3 +103,27 @@ lemma withDensity_lintegral_mul_le_comp {μ φ : Measure α} {ψ : Measure β} [ _ ≤ ∫⁻ y, η y B ∂μ := lintegral_mono' hpμ le_rfl end MeasureTheory.Measure + +namespace ProbabilityTheory.Kernel + +/-! ### Powers of a kernel -/ + +open MeasureTheory + +variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ : Measure α} + +/-- A point `y` reaches the measurable set `C` with positive probability in `n + 1` steps iff +its first step goes with positive probability to the set of points which reach `C` with positive +probability in `n` steps. -/ +lemma pow_add_one_apply_pos_iff {C : Set α} (hC : MeasurableSet C) {n : ℕ} {y : α} : + 0 < (κ ^ (n + 1)) y C ↔ 0 < κ y {z | 0 < (κ ^ n) z C} := by + rw [pow_add_one, comp_apply, Measure.comp_apply_pos_iff hC] + +/-- The measurable set `C` is reached from the measure `μ` with positive probability in `n + m` +steps iff after `m` steps, the set of points which reach `C` with positive probability in `n` +steps has positive measure. -/ +lemma pow_add_comp_apply_pos_iff {C : Set α} (hC : MeasurableSet C) {m n : ℕ} : + 0 < ((κ ^ (n + m)) ∘ₘ μ) C ↔ 0 < ((κ ^ m) ∘ₘ μ) {y | 0 < (κ ^ n) y C} := by + rw [pow_add, ← Measure.comp_assoc, Measure.comp_apply_pos_iff hC] + +end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean b/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean index aa6a101..4b4acea 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean @@ -161,7 +161,7 @@ private lemma exists_split_pow_comp [IsMarkovKernel κ] [IsProbabilityMeasure π induction i with | zero => refine ⟨0, a, a Set.univ • π, inferInstance, ?_, ?_, ha, ?_, ?_, ?_⟩ - · rw [Nat.mul_zero, pow_zero_comp, zero_add] + · rw [Nat.mul_zero, pow_zero, one_eq_id, Measure.id_comp, zero_add] · simp · refine Measure.le_iff.mpr fun s _ ↦ ?_ simp only [Measure.smul_apply, smul_eq_mul] @@ -189,7 +189,7 @@ private lemma exists_split_pow_comp [IsMarkovKernel κ] [IsProbabilityMeasure π have hcν : IsFiniteMeasure (c • ν) := isFiniteMeasure_of_le _ hca refine ⟨(κ ^ j) ∘ₘ g + c • ν, (κ ^ j) ∘ₘ a' - c • ν, (κ ^ j) ∘ₘ b' - c • ν, inferInstance, ?_, ?_, ?_, ?_, ?_, ?_⟩ - · rw [Nat.mul_succ, add_comm, pow_add_comp, hag, Measure.comp_add, add_assoc, + · rw [Nat.mul_succ, add_comm, pow_add, ← Measure.comp_assoc, hag, Measure.comp_add, add_assoc, add_comm (c • ν), Measure.sub_add_cancel_of_le hca] · calc a Set.univ • π = (κ ^ j) ∘ₘ (a Set.univ • π) := ((hπ.smul _).pow j).def.symm _ = (κ ^ j) ∘ₘ g + c • ν + ((κ ^ j) ∘ₘ b' - c • ν) := by @@ -241,7 +241,7 @@ lemma antitone_etvDist_pow_comp [IsMarkovKernel κ] (hπ : κ.Invariant π) (a : refine antitone_nat_of_succ_le fun n ↦ ?_ calc etvDist ((κ ^ (n + 1)) ∘ₘ a) (c • π) _ = etvDist (κ ∘ₘ ((κ ^ n) ∘ₘ a)) (κ ∘ₘ (c • π)) := by - rw [pow_succ_comp', Measure.comp_smul, hπ.def] + rw [pow_add_one', ← Measure.comp_assoc, Measure.comp_smul, hπ.def] _ ≤ etvDist ((κ ^ n) ∘ₘ a) (c • π) := etvDist_comp_le κ _ _ /-- If a measure `a` is dominated by a multiple of the invariant probability measure `π` of a @@ -379,7 +379,7 @@ private lemma excess_add_apply_univ_le (hπ : κ.Invariant π) (m i : ℕ) (x : refine Measure.le_iff.mpr fun s _ ↦ ?_ rw [Measure.smul_apply, smul_eq_mul] exact mul_le_of_le_one_left' (excess_apply_univ_le_one i x) - calc (κ ^ (m + i)) x = η ∘ₘ (κ ^ i) x := pow_add_apply κ m i x + calc (κ ^ (m + i)) x = η ∘ₘ (κ ^ i) x := by rw [pow_add]; rfl _ ≤ η ∘ₘ (excess κ π i x + (i : ℝ≥0) • π) := Measure.comp_le_comp_right (pow_apply_le_excess_add i x) _ _ = η ∘ₘ (excess κ π i x) + (i : ℝ≥0) • π := by rw [Measure.comp_add, h_inv] @@ -442,7 +442,7 @@ private lemma excessMass_lt_one (hπ : κ.Invariant π) {c : ℝ≥0} (hνc : ν exact (Nat.le_ceil c).trans (by exact_mod_cast Nat.le_add_right ⌈c⌉₊ n) have h_inv : η ∘ₘ (c • π) = c • π := ((hπ.smul c).pow p).def have h_le : (κ ^ (p + n)) x ≤ η ∘ₘ ((κ ^ n) x - w • ν) + ((p + n : ℕ) : ℝ≥0) • π := by - calc (κ ^ (p + n)) x = η ∘ₘ (κ ^ n) x := pow_add_apply κ p n x + calc (κ ^ (p + n)) x = η ∘ₘ (κ ^ n) x := by rw [pow_add]; rfl _ = η ∘ₘ ((κ ^ n) x - w • ν) + η ∘ₘ (w • ν) := by rw [← Measure.comp_add, Measure.sub_add_cancel_of_le h] _ ≤ η ∘ₘ ((κ ^ n) x - w • ν) + η ∘ₘ (c • π) := by @@ -537,7 +537,7 @@ private lemma tendsto_etvDist_pow_comp_of_lintegral_excessMass_eq_zero [IsProbab refine eventually_atTop.mpr ⟨N + i, fun n hn ↦ ?_⟩ obtain ⟨n', rfl⟩ : ∃ n', n = n' + i := ⟨n - i, (Nat.sub_add_cancel (by omega)).symm⟩ have hN' := hN n' (by omega) - rw [hθ, ← pow_add_comp] at hN' + rw [hθ, Measure.comp_assoc, ← pow_add] at hN' calc etvDist ((κ ^ (n' + i)) ∘ₘ μ) π ≤ 2 * ξ Set.univ + ε / 2 := hN' _ ≤ 2 * (ε / 2 / 2) + ε / 2 := by rw [hξ_univ] @@ -574,14 +574,14 @@ private lemma excessMass_eq_zero_of_isHarrisRecurrent {φ : Measure α} (hφ : induction n with | zero => intro y - rw [pow_zero_apply, lintegral_dirac' _ measurable_excessMass] + rw [pow_zero, one_eq_id, Kernel.id_apply, lintegral_dirac' _ measurable_excessMass] | succ n ih => intro y calc excessMass κ π y ≤ ∫⁻ z, excessMass κ π z ∂((κ.restrict hG.compl) ^ n) y := ih y _ ≤ ∫⁻ z, ∫⁻ z', excessMass κ π z' ∂(κ.restrict hG.compl z) ∂((κ.restrict hG.compl) ^ n) y := lintegral_mono h_step _ = ∫⁻ z, excessMass κ π z ∂((κ.restrict hG.compl) ^ (n + 1)) y := by - rw [pow_succ_apply', Measure.lintegral_bind (Kernel.aemeasurable _) + rw [pow_add_one', comp_apply, Measure.lintegral_bind (Kernel.aemeasurable _) measurable_excessMass.aemeasurable] refine le_antisymm (ge_of_tendsto' (hH hG hφG x) fun n ↦ ?_) bot_le calc excessMass κ π x ≤ ∫⁻ z, excessMass κ π z ∂((κ.restrict hG.compl) ^ n) x := h_pow n x diff --git a/RandomDo/ForMathlib/Probability/Kernel/HarrisRecurrent.lean b/RandomDo/ForMathlib/Probability/Kernel/HarrisRecurrent.lean index 5a5dc9e..f77aa44 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/HarrisRecurrent.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/HarrisRecurrent.lean @@ -6,7 +6,7 @@ Authors: Rémy Degenne module public import Mathlib.Probability.Kernel.Irreducible -public import RandomDo.ForMathlib.Probability.Kernel.Pow +public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp /-! # Harris recurrent kernels @@ -73,12 +73,12 @@ lemma IsHarrisRecurrent.isIrreducible [IsMarkovKernel κ] (h : κ.IsHarrisRecurr have h_eq : ∀ n : ℕ, ((κ.restrict hA.compl) ^ n) a = (κ ^ n) a := by intro n induction n with - | zero => rw [pow_zero_apply, pow_zero_apply] + | zero => simp | succ n ih => have h0 : (κ ∘ₘ (κ ^ n) a) A = 0 := by - rw [← pow_succ_apply'] + rw [← comp_apply, ← pow_add_one'] exact nonpos_iff_eq_zero.mp (hcon (n + 1)) - rw [pow_succ_apply', ih, pow_succ_apply', Measure.restrict_comp] + rw [pow_add_one', comp_apply, ih, pow_add_one', comp_apply, Measure.restrict_comp] exact Measure.restrict_eq_self_of_ae_mem (measure_eq_zero_iff_ae_notMem.mp h0) have h_tendsto := h hA hφA a simp_rw [h_eq, measure_univ] at h_tendsto diff --git a/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean b/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean index 7b5138f..b1c77bc 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/Invariance.lean @@ -6,7 +6,7 @@ Authors: Rémy Degenne module public import Mathlib.Probability.Kernel.Invariance -public import RandomDo.ForMathlib.Probability.Kernel.Pow +public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp /-! # Invariant measures and powers of a kernel @@ -18,7 +18,7 @@ public import RandomDo.ForMathlib.Probability.Kernel.Pow * `Kernel.Invariant.ae_ae_pow`: if a property holds `μ`-almost everywhere for a measure `μ` invariant for `κ`, then for `μ`-almost every `a` it holds `(κ ^ n) a`-almost everywhere for all `n`. -* `Kernel.Invariant.ae_apply_eq_zero_of_ae_absorbing`: if a measurable set of finite measure is +* `Kernel.Invariant.ae_apply_eq_zero_of_compl`: if a measurable set of finite measure is absorbing almost everywhere with respect to an invariant measure of a Markov kernel, then so is its complement. -/ @@ -31,55 +31,54 @@ open scoped ENNReal ProbabilityTheory namespace ProbabilityTheory.Kernel -variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ π : Measure α} {G : Set α} +variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ : Measure α} -lemma Invariant.pow (h : κ.Invariant μ) (n : ℕ) : (κ ^ n).Invariant μ := by +theorem Invariant.pow (h : Invariant κ μ) (n : ℕ) : Invariant (κ ^ n) μ := by induction n with - | zero => exact pow_zero_comp κ μ + | zero => simp [Invariant] | succ n ih => rw [pow_succ, mul_eq_comp]; exact ih.comp h -lemma Invariant.smul (h : κ.Invariant μ) (c : ℝ≥0∞) : κ.Invariant (c • μ) := by +theorem Invariant.smul (h : Invariant κ μ) (c : ℝ≥0∞) : Invariant κ (c • μ) := by rw [Invariant, Measure.comp_smul, h.def] /-- If `μ` is invariant for `κ` and a property holds `μ`-almost everywhere, then for `μ`-almost every `a` it holds `(κ ^ n) a`-almost everywhere for all `n`. -/ -lemma Invariant.ae_ae_pow (h : κ.Invariant μ) {p : α → Prop} (hp : ∀ᵐ a ∂μ, p a) : +theorem Invariant.ae_ae_pow (h : Invariant κ μ) {p : α → Prop} (hp : ∀ᵐ a ∂μ, p a) : ∀ᵐ a ∂μ, ∀ n, ∀ᵐ b ∂(κ ^ n) a, p b := by rw [ae_all_iff] intro n rw [← (h.pow n).def] at hp exact Measure.ae_ae_of_ae_comp hp -/-! ### Absorbing sets -/ +section Absorbing + +variable {π : Measure α} {G : Set α} /-- If a measurable set `G` is absorbing almost everywhere with respect to an invariant measure `π`, then for `π`-almost every point of `G`, no power of `κ` charges `Gᶜ`. -/ -lemma Invariant.ae_pow_apply_compl_eq_zero (hπ : κ.Invariant π) (hG : MeasurableSet G) +theorem Invariant.ae_pow_apply_compl_eq_zero (hπ : Invariant κ π) (hG : MeasurableSet G) (h : ∀ᵐ x ∂π, x ∈ G → κ x Gᶜ = 0) : ∀ᵐ x ∂π, x ∈ G → ∀ n, (κ ^ n) x Gᶜ = 0 := by suffices ∀ n, ∀ᵐ x ∂π, x ∈ G → (κ ^ n) x Gᶜ = 0 by filter_upwards [ae_all_iff.mpr this] with x hx hxG n using hx n hxG intro n induction n with - | zero => - refine ae_of_all _ fun x hx ↦ ?_ - rw [pow_zero_apply, Measure.dirac_apply' _ hG.compl] - simp [hx] + | zero => simp [Kernel.id_apply, Measure.dirac_apply' _ hG.compl] | succ n ih => have h1 : ∀ᵐ x ∂π, ∀ᵐ y ∂κ x, y ∈ G → (κ ^ n) y Gᶜ = 0 := by rw [← hπ.def] at ih exact Measure.ae_ae_of_ae_comp ih filter_upwards [h, h1] with x hx hx1 hxG - rw [pow_succ_apply, Measure.bind_apply hG.compl (κ ^ n).aemeasurable, - lintegral_eq_zero_iff ((κ ^ n).measurable_coe hG.compl)] + suffices (fun a ↦ (κ ^ n) a Gᶜ) =ᵐ[κ x] 0 by + rwa [pow_add_one, comp_apply, Measure.bind_apply hG.compl (κ ^ n).aemeasurable, + lintegral_eq_zero_iff ((κ ^ n).measurable_coe hG.compl)] have hxG' : ∀ᵐ y ∂κ x, y ∈ G := by - have := measure_eq_zero_iff_ae_notMem.mp (hx hxG) - filter_upwards [this] with y hy using by simpa using hy + simpa using measure_eq_zero_iff_ae_notMem.mp (hx hxG) filter_upwards [hx1, hxG'] with y hy hyG using hy hyG /-- If a measurable set `G` of finite measure is absorbing almost everywhere with respect to an invariant measure of a Markov kernel, then so is its complement. -/ -lemma Invariant.ae_apply_eq_zero_of_ae_absorbing [IsMarkovKernel κ] (hπ : κ.Invariant π) +theorem Invariant.ae_apply_eq_zero_of_compl [IsMarkovKernel κ] (hπ : Invariant κ π) (hG : MeasurableSet G) (hπG : π G ≠ ∞) (h : ∀ᵐ x ∂π, x ∈ G → κ x Gᶜ = 0) : ∀ᵐ x ∂π, x ∈ Gᶜ → κ x G = 0 := by have h1 : ∫⁻ x, κ x G ∂π = π G := by @@ -94,4 +93,6 @@ lemma Invariant.ae_apply_eq_zero_of_ae_absorbing [IsMarkovKernel κ] (hπ : κ.I exact (ENNReal.add_right_inj hπG).mp (by rw [h_add, add_zero]) rwa [setLIntegral_eq_zero_iff hG.compl (κ.measurable_coe hG)] at h3 +end Absorbing + end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/Irreducible.lean b/RandomDo/ForMathlib/Probability/Kernel/Irreducible.lean index 5b7b9e6..5261ea2 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/Irreducible.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/Irreducible.lean @@ -61,7 +61,7 @@ lemma IsIrreducible.exists_pow_succ_pos [IsIrreducible φ κ] {A : Set α} (hA : rw [IsIrreducible.iUnion_setOf_pow_apply_pos_eq_univ (φ := φ) hA hφA] exact Measure.measure_univ_ne_zero.mpr hx obtain ⟨n, hn⟩ := exists_measure_pos_of_not_measure_iUnion_null hpos - exact ⟨n, (pow_succ_apply_pos_iff hA).mpr hn⟩ + exact ⟨n, (pow_add_one_apply_pos_iff hA).mpr hn⟩ /-- For a `φ`-irreducible kernel, every set of positive `φ`-measure is reached with positive probability from any nonzero initial measure. -/ @@ -120,7 +120,7 @@ lemma Invariant.measure_eq_zero_or_measure_compl_eq_zero [IsMarkovKernel κ] [Is have h1 : φ Gᶜ = 0 := hπ.measure_compl_eq_zero_of_ae_absorbing hG h hcon.1 have h2 : φ Gᶜᶜ = 0 := by refine hπ.measure_compl_eq_zero_of_ae_absorbing hG.compl ?_ hcon.2 - simpa using hπ.ae_apply_eq_zero_of_ae_absorbing hG hπG h + simpa using hπ.ae_apply_eq_zero_of_compl hG hπG h rw [compl_compl] at h2 refine hφ ?_ rw [← Measure.measure_univ_eq_zero, ← Set.union_compl_self G] diff --git a/RandomDo/ForMathlib/Probability/Kernel/Pow.lean b/RandomDo/ForMathlib/Probability/Kernel/Pow.lean deleted file mode 100644 index cccacf7..0000000 --- a/RandomDo/ForMathlib/Probability/Kernel/Pow.lean +++ /dev/null @@ -1,105 +0,0 @@ -/- -Copyright (c) 2026 Rémy Degenne. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rémy Degenne --/ -module - -public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp - -/-! -# Powers of kernels - -Lemmas about the powers `κ ^ n` of a kernel `κ : Kernel α α` for the monoid structure given by -composition. - -## Main statements - -* `Kernel.one_eq_id`, `Kernel.mul_eq_comp`: the unit of the monoid is `Kernel.id` and its - multiplication is the composition `∘ₖ`. -* Instances: `κ ^ n` is a Markov kernel (resp. a zero or Markov kernel, a finite kernel, - an s-finite kernel) if `κ` is. -* `Kernel.pow_add_apply`: `(κ ^ (m + n)) a = (κ ^ m) ∘ₘ (κ ^ n) a`. -* `Kernel.pow_add_comp`: `(κ ^ (m + n)) ∘ₘ μ = (κ ^ m) ∘ₘ ((κ ^ n) ∘ₘ μ)`. -* `Kernel.pow_succ_apply_pos_iff`: a point reaches a set with positive probability in `n + 1` - steps iff its first step goes with positive probability to the set of points which reach it - with positive probability in `n` steps. --/ - -@[expose] public section - -open MeasureTheory - -open scoped ENNReal ProbabilityTheory - -namespace ProbabilityTheory.Kernel - -variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ : Measure α} - -@[simp] lemma one_eq_id : (1 : Kernel α α) = Kernel.id := rfl - -@[simp] lemma mul_eq_comp (η κ : Kernel α α) : η * κ = η ∘ₖ κ := rfl - -instance [IsMarkovKernel κ] (n : ℕ) : IsMarkovKernel (κ ^ n) := by - induction n with - | zero => rw [pow_zero, one_eq_id]; infer_instance - | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance - -instance [IsZeroOrMarkovKernel κ] (n : ℕ) : IsZeroOrMarkovKernel (κ ^ n) := by - induction n with - | zero => rw [pow_zero, one_eq_id]; infer_instance - | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance - -instance [IsFiniteKernel κ] (n : ℕ) : IsFiniteKernel (κ ^ n) := by - induction n with - | zero => rw [pow_zero, one_eq_id]; infer_instance - | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance - -instance [IsSFiniteKernel κ] (n : ℕ) : IsSFiniteKernel (κ ^ n) := by - induction n with - | zero => rw [pow_zero, one_eq_id]; infer_instance - | succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance - -lemma pow_zero_apply (κ : Kernel α α) (a : α) : (κ ^ 0) a = Measure.dirac a := by - rw [pow_zero, one_eq_id, id_apply] - -lemma pow_add_apply (κ : Kernel α α) (m n : ℕ) (a : α) : - (κ ^ (m + n)) a = (κ ^ m) ∘ₘ (κ ^ n) a := by - rw [pow_add, comp_apply] - -lemma pow_succ_apply (κ : Kernel α α) (n : ℕ) (a : α) : (κ ^ (n + 1)) a = (κ ^ n) ∘ₘ κ a := by - rw [pow_add_apply, pow_one] - -lemma pow_succ_apply' (κ : Kernel α α) (n : ℕ) (a : α) : (κ ^ (n + 1)) a = κ ∘ₘ (κ ^ n) a := by - rw [add_comm, pow_add_apply, pow_one] - -lemma pow_add_comp (κ : Kernel α α) (m n : ℕ) (μ : Measure α) : - (κ ^ (m + n)) ∘ₘ μ = (κ ^ m) ∘ₘ ((κ ^ n) ∘ₘ μ) := by - rw [pow_add, Measure.comp_assoc] - -lemma pow_succ_comp (κ : Kernel α α) (n : ℕ) (μ : Measure α) : - (κ ^ (n + 1)) ∘ₘ μ = (κ ^ n) ∘ₘ (κ ∘ₘ μ) := by - rw [pow_add_comp, pow_one] - -lemma pow_succ_comp' (κ : Kernel α α) (n : ℕ) (μ : Measure α) : - (κ ^ (n + 1)) ∘ₘ μ = κ ∘ₘ ((κ ^ n) ∘ₘ μ) := by - rw [add_comm, pow_add_comp, pow_one] - -lemma pow_zero_comp (κ : Kernel α α) (μ : Measure α) : (κ ^ 0 : Kernel α α) ∘ₘ μ = μ := by - simp - -/-- A point `y` reaches the measurable set `C` with positive probability in `n + 1` steps iff -its first step goes with positive probability to the set of points which reach `C` with positive -probability in `n` steps. -/ -lemma pow_succ_apply_pos_iff {C : Set α} (hC : MeasurableSet C) {n : ℕ} {y : α} : - 0 < (κ ^ (n + 1)) y C ↔ 0 < κ y {z | 0 < (κ ^ n) z C} := by - rw [pow_succ_apply, Measure.comp_apply_pos_iff hC] - -/-- The measurable set `C` is reached from the measure `μ` with positive probability in `n + m` -steps iff after `m` steps, the set of points which reach `C` with positive probability in `n` -steps has positive measure. -/ -lemma pow_add_comp_apply_pos_iff {C : Set α} (hC : MeasurableSet C) {m n : ℕ} : - 0 < ((κ ^ (n + m)) ∘ₘ μ) C ↔ 0 < ((κ ^ m) ∘ₘ μ) {y | 0 < (κ ^ n) y C} := by - rw [pow_add_comp, Measure.comp_apply_pos_iff hC] - -end ProbabilityTheory.Kernel diff --git a/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Basic.lean b/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Basic.lean index e10d4cc..6b69b92 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Basic.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Basic.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne -/ module -public import RandomDo.ForMathlib.Probability.Kernel.Pow +public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp /-! # Small sets of a kernel @@ -66,7 +66,7 @@ lemma smul_le_comp (h : IsSmallSet κ C n ν) (μ : Measure α) : μ C • ν /-- If `C` is `(n, ν)`-small, then `(κ ^ (n + m)) x` is at least `(κ ^ m) x C • ν`. -/ lemma smul_le_pow_add_apply (h : IsSmallSet κ C n ν) (m : ℕ) (x : α) : (κ ^ m) x C • ν ≤ (κ ^ (n + m)) x := by - rw [pow_add_apply] + rw [pow_add, comp_apply] exact h.smul_le_comp _ end IsSmallSet @@ -78,7 +78,7 @@ lemma IsSmallSet.pow_apply_pos_of_pow_comp_apply_pos {C : Set α} {k m n : ℕ} (h : IsSmallSet κ C k ν) (hy : 0 < (κ ^ n) y C) (hm : 0 < ((κ ^ m) ∘ₘ ν) C) : 0 < (κ ^ (m + k + n)) y C := by have hle : (κ ^ n) y C • ((κ ^ m) ∘ₘ ν) ≤ (κ ^ (m + k + n)) y := by - rw [add_assoc, pow_add_apply, ← Measure.comp_smul] + rw [add_assoc, pow_add, comp_apply, ← Measure.comp_smul] exact Measure.comp_le_comp_right (h.smul_le_pow_add_apply n y) _ refine lt_of_lt_of_le ?_ (hle C) rw [Measure.smul_apply, smul_eq_mul] diff --git a/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Exists.lean b/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Exists.lean index c59bb22..47509c0 100644 --- a/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Exists.lean +++ b/RandomDo/ForMathlib/Probability/Kernel/SmallSet/Exists.lean @@ -65,7 +65,7 @@ lemma isSmallSet_of_le_lintegral_mul [SFinite φ] {p q : α → α → ℝ≥0 (hD : MeasurableSet D) (h : ∀ x ∈ C, ∀ z ∈ D, (c : ℝ≥0∞) ≤ ∫⁻ y, p x y * q y z ∂φ) : IsSmallSet κ C (n + m) (c • φ.restrict D) := by intro x hx - rw [pow_add_apply] + rw [pow_add, comp_apply] refine le_trans (Measure.le_iff.mpr fun B hB ↦ ?_) (Measure.withDensity_lintegral_mul_le_comp hp.of_uncurry_left hq (hpκ x) hqκ) rw [withDensity_apply _ hB, Measure.smul_apply, Measure.restrict_apply hB,