Convergence in total variation of irreducible aperiodic Markov kernels

RandomDo.lean

@@ -1,6 +1,23 @@
 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.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.SmallSet.Basic
+public import RandomDo.ForMathlib.Probability.Kernel.SmallSet.Exists
 public import RandomDo.Measurable
 public import RandomDo.Monad.ForInInstances
 public import RandomDo.Monad.Instances

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

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

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

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