Skip to content

Commit d343758

Browse files
RemyDegenneRemyDegenne
committed
update
1 parent e72b660 commit d343758

11 files changed

Lines changed: 137 additions & 147 deletions

File tree

‎RandomDo.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,12 +10,12 @@ public import RandomDo.ForMathlib.MeasureTheory.Measure.TotalVariation.Defs
1010
public import RandomDo.ForMathlib.MeasureTheory.VectorMeasure.TotalVariation
1111
public import RandomDo.ForMathlib.NumberTheory.FrobeniusNumber
1212
public import RandomDo.ForMathlib.Probability.Kernel.Aperiodic
13+
public import RandomDo.ForMathlib.Probability.Kernel.Composition.Comp
1314
public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp
1415
public import RandomDo.ForMathlib.Probability.Kernel.ErgodicTheorem
1516
public import RandomDo.ForMathlib.Probability.Kernel.HarrisRecurrent
1617
public import RandomDo.ForMathlib.Probability.Kernel.Invariance
1718
public import RandomDo.ForMathlib.Probability.Kernel.Irreducible
18-
public import RandomDo.ForMathlib.Probability.Kernel.Pow
1919
public import RandomDo.ForMathlib.Probability.Kernel.SmallSet.Basic
2020
public import RandomDo.ForMathlib.Probability.Kernel.SmallSet.Exists
2121
public import RandomDo.Measurable

‎RandomDo/ForMathlib/Probability/Kernel/Aperiodic.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -74,13 +74,13 @@ lemma exists_measurableSet_superset_forall_notMem_apply_eq_zero {S : Set α}
7474
∃ B, MeasurableSet B ∧ S ⊆ B ∧ ν B = 0 ∧ ∀ y ∉ B, κ y B = 0 := by
7575
refine ⟨⋃ m : ℕ, {y | 0 < (κ ^ m) y S}, .iUnion fun m ↦ measurableSet_apply_pos _ hS,
7676
fun y hy ↦ Set.mem_iUnion.mpr ⟨0, ?_⟩, ?_, fun y hy ↦ ?_⟩
77-
· rw [Set.mem_ofPred_eq, pow_zero_apply, Measure.dirac_apply_of_mem hy]
77+
· rw [Set.mem_ofPred_eq, pow_zero, one_eq_id, Kernel.id_apply, Measure.dirac_apply_of_mem hy]
7878
exact zero_lt_one
7979
· rw [measure_iUnion_null_iff]
8080
exact fun m ↦ (Measure.comp_apply_eq_zero_iff hS).mp (h m)
8181
· rw [measure_iUnion_null_iff]
8282
intro m
83-
rw [← Measure.comp_apply_eq_zero_iff hS, ← pow_succ_apply]
83+
rw [← Measure.comp_apply_eq_zero_iff hS, ← comp_apply, ← pow_add_one]
8484
simp only [Set.mem_iUnion, Set.mem_ofPred_eq, not_exists, not_lt, nonpos_iff_eq_zero] at hy
8585
exact hy (m + 1)
8686

@@ -190,7 +190,7 @@ lemma IsAperiodic.exists_forall_pow_comp_apply_pos [IsMarkovKernel κ] [IsIrredu
190190
-- otherwise, we get two times with different phases reachable from the same points
191191
obtain ⟨m, n₁, n₂, hne, hpos⟩ := hκ.exists_pow_comp_inter_pos hν hνπ
192192
(E := fun n ↦ {y | 0 < (κ ^ n) y C}) (fun n ↦ measurableSet_apply_pos _ hC)
193-
(IsIrreducible.irreducible (φ := φ) hC hφC) (fun y n h ↦ (pow_succ_apply_pos_iff hC).mpr h) d
193+
(IsIrreducible.irreducible (φ := φ) hC hφC) (fun y n h ↦ (pow_add_one_apply_pos_iff hC).mpr h) d
194194
have h₁ : d + 2 ∣ n₁ + m + k := hdvd _ ((pow_add_comp_apply_pos_iff hC).mpr
195195
(hpos.trans_le (measure_mono Set.inter_subset_left)))
196196
have h₂ : d + 2 ∣ n₂ + m + k := hdvd _ ((pow_add_comp_apply_pos_iff hC).mpr

‎RandomDo/ForMathlib/Probability/Kernel/Composition/Comp.lean‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
/-
2+
Copyright (c) 2026 Rémy Degenne. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Rémy Degenne
5+
-/
6+
module
7+
8+
public import Mathlib.Probability.Kernel.Composition.Comp
9+
10+
/-!
11+
# The monoid of kernels
12+
13+
Lemmas about the monoid structure on `Kernel α α` given by composition, and about the powers
14+
`κ ^ n` of a kernel `κ : Kernel α α`.
15+
16+
## Main statements
17+
18+
* `Kernel.one_eq_id`, `Kernel.mul_eq_comp`: the unit of the monoid is `Kernel.id` and its
19+
multiplication is the composition `∘ₖ`.
20+
* Instances: `κ ^ n` is a Markov kernel (resp. a zero or Markov kernel, a finite kernel,
21+
an s-finite kernel) if `κ` is.
22+
* `Kernel.pow_add_one`, `Kernel.pow_add_one'`: `κ ^ (n + 1) = κ ^ n ∘ₖ κ = κ ∘ₖ κ ^ n`.
23+
-/
24+
25+
@[expose] public section
26+
27+
open MeasureTheory
28+
29+
namespace ProbabilityTheory.Kernel
30+
31+
variable {α : Type*} {mα : MeasurableSpace α}
32+
33+
@[simp] lemma one_eq_id : (1 : Kernel α α) = Kernel.id := rfl
34+
35+
@[simp] lemma mul_eq_comp (η κ : Kernel α α) : η * κ = η ∘ₖ κ := rfl
36+
37+
instance IsMarkovKernel.pow (κ : Kernel α α) [IsMarkovKernel κ] (n : ℕ) :
38+
IsMarkovKernel (κ ^ n) := by
39+
induction n with
40+
| zero => rw [pow_zero, one_eq_id]; infer_instance
41+
| succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance
42+
43+
instance IsZeroOrMarkovKernel.pow (κ : Kernel α α) [IsZeroOrMarkovKernel κ] (n : ℕ) :
44+
IsZeroOrMarkovKernel (κ ^ n) := by
45+
induction n with
46+
| zero => rw [pow_zero, one_eq_id]; infer_instance
47+
| succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance
48+
49+
instance IsFiniteKernel.pow (κ : Kernel α α) [IsFiniteKernel κ] (n : ℕ) :
50+
IsFiniteKernel (κ ^ n) := by
51+
induction n with
52+
| zero => rw [pow_zero, one_eq_id]; infer_instance
53+
| succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance
54+
55+
instance IsSFiniteKernel.pow (κ : Kernel α α) [IsSFiniteKernel κ] (n : ℕ) :
56+
IsSFiniteKernel (κ ^ n) := by
57+
induction n with
58+
| zero => rw [pow_zero, one_eq_id]; infer_instance
59+
| succ n ih => rw [pow_succ, mul_eq_comp]; infer_instance
60+
61+
lemma pow_add_one (κ : Kernel α α) (n : ℕ) : κ ^ (n + 1) = (κ ^ n) ∘ₖ κ := by
62+
rw [pow_add, pow_one]
63+
64+
lemma pow_add_one' (κ : Kernel α α) (n : ℕ) : κ ^ (n + 1) = κ ∘ₖ (κ ^ n) := by
65+
rw [add_comm, pow_add, pow_one]
66+
67+
end ProbabilityTheory.Kernel

‎RandomDo/ForMathlib/Probability/Kernel/Composition/MeasureComp.lean‎

Lines changed: 29 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Rémy Degenne
66
module
77

88
public import Mathlib.Probability.Kernel.Composition.MeasureComp
9+
public import RandomDo.ForMathlib.Probability.Kernel.Composition.Comp
910

1011
/-!
1112
# Lemmas about the composition of a measure and a kernel
@@ -17,6 +18,8 @@ public import Mathlib.Probability.Kernel.Composition.MeasureComp
1718
* `Measure.restrict_comp`: `(κ.restrict hs) ∘ₘ μ = (κ ∘ₘ μ).restrict s`.
1819
* `Measure.comp_apply_pos_iff`: `0 < (η ∘ₘ μ) s ↔ 0 < μ {a | 0 < η a s}`.
1920
* `Measure.withDensity_lintegral_mul_le_comp`: Chapman-Kolmogorov inequality for densities.
21+
* `Kernel.pow_add_one_apply_pos_iff`, `Kernel.pow_add_comp_apply_pos_iff`: positivity of the
22+
measure of a set after `n + 1` (resp. `n + m`) steps of a kernel.
2023
-/
2124

2225
@[expose] public section
@@ -61,7 +64,7 @@ lemma restrict_comp (hs : MeasurableSet s) : (κ.restrict hs) ∘ₘ μ = (κ
6164

6265
/-- The measure `η ∘ₘ μ` gives positive mass to a measurable set `s` iff the set of points `a`
6366
such that `η a s` is positive has positive `μ`-measure. -/
64-
lemma comp_apply_pos_iff (hs : MeasurableSet s) :
67+
lemma comp_apply_pos_iff {s : Set β} (hs : MeasurableSet s) :
6568
0 < (η ∘ₘ μ) s ↔ 0 < μ {a | 0 < η a s} := by
6669
rw [Measure.bind_apply hs η.aemeasurable, lintegral_pos_iff_support (η.measurable_coe hs)]
6770
congr! 2
@@ -70,7 +73,7 @@ lemma comp_apply_pos_iff (hs : MeasurableSet s) :
7073

7174
/-- The measure `η ∘ₘ μ` gives zero mass to a measurable set `s` iff the set of points `a`
7275
such that `η a s` is positive has `μ`-measure zero. -/
73-
lemma comp_apply_eq_zero_iff (hs : MeasurableSet s) :
76+
lemma comp_apply_eq_zero_iff {s : Set β} (hs : MeasurableSet s) :
7477
(η ∘ₘ μ) s = 0 ↔ μ {a | 0 < η a s} = 0 := by
7578
rw [← not_iff_not, ← Ne, ← Ne, ← pos_iff_ne_zero, ← pos_iff_ne_zero, comp_apply_pos_iff hs]
7679

@@ -100,3 +103,27 @@ lemma withDensity_lintegral_mul_le_comp {μ φ : Measure α} {ψ : Measure β} [
100103
_ ≤ ∫⁻ y, η y B ∂μ := lintegral_mono' hpμ le_rfl
101104

102105
end MeasureTheory.Measure
106+
107+
namespace ProbabilityTheory.Kernel
108+
109+
/-! ### Powers of a kernel -/
110+
111+
open MeasureTheory
112+
113+
variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ : Measure α}
114+
115+
/-- A point `y` reaches the measurable set `C` with positive probability in `n + 1` steps iff
116+
its first step goes with positive probability to the set of points which reach `C` with positive
117+
probability in `n` steps. -/
118+
lemma pow_add_one_apply_pos_iff {C : Set α} (hC : MeasurableSet C) {n : ℕ} {y : α} :
119+
0 < (κ ^ (n + 1)) y C ↔ 0 < κ y {z | 0 < (κ ^ n) z C} := by
120+
rw [pow_add_one, comp_apply, Measure.comp_apply_pos_iff hC]
121+
122+
/-- The measurable set `C` is reached from the measure `μ` with positive probability in `n + m`
123+
steps iff after `m` steps, the set of points which reach `C` with positive probability in `n`
124+
steps has positive measure. -/
125+
lemma pow_add_comp_apply_pos_iff {C : Set α} (hC : MeasurableSet C) {m n : ℕ} :
126+
0 < ((κ ^ (n + m)) ∘ₘ μ) C ↔ 0 < ((κ ^ m) ∘ₘ μ) {y | 0 < (κ ^ n) y C} := by
127+
rw [pow_add, ← Measure.comp_assoc, Measure.comp_apply_pos_iff hC]
128+
129+
end ProbabilityTheory.Kernel

‎RandomDo/ForMathlib/Probability/Kernel/ErgodicTheorem.lean‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@ private lemma exists_split_pow_comp [IsMarkovKernel κ] [IsProbabilityMeasure π
161161
induction i with
162162
| zero =>
163163
refine ⟨0, a, a Set.univ • π, inferInstance, ?_, ?_, ha, ?_, ?_, ?_⟩
164-
· rw [Nat.mul_zero, pow_zero_comp, zero_add]
164+
· rw [Nat.mul_zero, pow_zero, one_eq_id, Measure.id_comp, zero_add]
165165
· simp
166166
· refine Measure.le_iff.mpr fun s _ ↦ ?_
167167
simp only [Measure.smul_apply, smul_eq_mul]
@@ -189,7 +189,7 @@ private lemma exists_split_pow_comp [IsMarkovKernel κ] [IsProbabilityMeasure π
189189
have hcν : IsFiniteMeasure (c • ν) := isFiniteMeasure_of_le _ hca
190190
refine ⟨(κ ^ j) ∘ₘ g + c • ν, (κ ^ j) ∘ₘ a' - c • ν, (κ ^ j) ∘ₘ b' - c • ν, inferInstance,
191191
?_, ?_, ?_, ?_, ?_, ?_⟩
192-
· rw [Nat.mul_succ, add_comm, pow_add_comp, hag, Measure.comp_add, add_assoc,
192+
· rw [Nat.mul_succ, add_comm, pow_add, ← Measure.comp_assoc, hag, Measure.comp_add, add_assoc,
193193
add_comm (c • ν), Measure.sub_add_cancel_of_le hca]
194194
· calc a Set.univ • π = (κ ^ j) ∘ₘ (a Set.univ • π) := ((hπ.smul _).pow j).def.symm
195195
_ = (κ ^ j) ∘ₘ g + c • ν + ((κ ^ j) ∘ₘ b' - c • ν) := by
@@ -241,7 +241,7 @@ lemma antitone_etvDist_pow_comp [IsMarkovKernel κ] (hπ : κ.Invariant π) (a :
241241
refine antitone_nat_of_succ_le fun n ↦ ?_
242242
calc etvDist ((κ ^ (n + 1)) ∘ₘ a) (c • π)
243243
_ = etvDist (κ ∘ₘ ((κ ^ n) ∘ₘ a)) (κ ∘ₘ (c • π)) := by
244-
rw [pow_succ_comp', Measure.comp_smul, hπ.def]
244+
rw [pow_add_one', ← Measure.comp_assoc, Measure.comp_smul, hπ.def]
245245
_ ≤ etvDist ((κ ^ n) ∘ₘ a) (c • π) := etvDist_comp_le κ _ _
246246

247247
/-- 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 :
379379
refine Measure.le_iff.mpr fun s _ ↦ ?_
380380
rw [Measure.smul_apply, smul_eq_mul]
381381
exact mul_le_of_le_one_left' (excess_apply_univ_le_one i x)
382-
calc (κ ^ (m + i)) x = η ∘ₘ (κ ^ i) x := pow_add_apply κ m i x
382+
calc (κ ^ (m + i)) x = η ∘ₘ (κ ^ i) x := by rw [pow_add]; rfl
383383
_ ≤ η ∘ₘ (excess κ π i x + (i : ℝ≥0) • π) :=
384384
Measure.comp_le_comp_right (pow_apply_le_excess_add i x) _
385385
_ = η ∘ₘ (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 : ν
442442
exact (Nat.le_ceil c).trans (by exact_mod_cast Nat.le_add_right ⌈c⌉₊ n)
443443
have h_inv : η ∘ₘ (c • π) = c • π := ((hπ.smul c).pow p).def
444444
have h_le : (κ ^ (p + n)) x ≤ η ∘ₘ ((κ ^ n) x - w • ν) + ((p + n : ℕ) : ℝ≥0) • π := by
445-
calc (κ ^ (p + n)) x = η ∘ₘ (κ ^ n) x := pow_add_apply κ p n x
445+
calc (κ ^ (p + n)) x = η ∘ₘ (κ ^ n) x := by rw [pow_add]; rfl
446446
_ = η ∘ₘ ((κ ^ n) x - w • ν) + η ∘ₘ (w • ν) := by
447447
rw [← Measure.comp_add, Measure.sub_add_cancel_of_le h]
448448
_ ≤ η ∘ₘ ((κ ^ n) x - w • ν) + η ∘ₘ (c • π) := by
@@ -537,7 +537,7 @@ private lemma tendsto_etvDist_pow_comp_of_lintegral_excessMass_eq_zero [IsProbab
537537
refine eventually_atTop.mpr ⟨N + i, fun n hn ↦ ?_⟩
538538
obtain ⟨n', rfl⟩ : ∃ n', n = n' + i := ⟨n - i, (Nat.sub_add_cancel (by omega)).symm⟩
539539
have hN' := hN n' (by omega)
540-
rw [hθ, ← pow_add_comp] at hN'
540+
rw [hθ, Measure.comp_assoc, ← pow_add] at hN'
541541
calc etvDist ((κ ^ (n' + i)) ∘ₘ μ) π ≤ 2 * ξ Set.univ + ε / 2 := hN'
542542
_ ≤ 2 * (ε / 2 / 2) + ε / 2 := by
543543
rw [hξ_univ]
@@ -574,14 +574,14 @@ private lemma excessMass_eq_zero_of_isHarrisRecurrent {φ : Measure α} (hφ :
574574
induction n with
575575
| zero =>
576576
intro y
577-
rw [pow_zero_apply, lintegral_dirac' _ measurable_excessMass]
577+
rw [pow_zero, one_eq_id, Kernel.id_apply, lintegral_dirac' _ measurable_excessMass]
578578
| succ n ih =>
579579
intro y
580580
calc excessMass κ π y ≤ ∫⁻ z, excessMass κ π z ∂((κ.restrict hG.compl) ^ n) y := ih y
581581
_ ≤ ∫⁻ z, ∫⁻ z', excessMass κ π z' ∂(κ.restrict hG.compl z)
582582
∂((κ.restrict hG.compl) ^ n) y := lintegral_mono h_step
583583
_ = ∫⁻ z, excessMass κ π z ∂((κ.restrict hG.compl) ^ (n + 1)) y := by
584-
rw [pow_succ_apply', Measure.lintegral_bind (Kernel.aemeasurable _)
584+
rw [pow_add_one', comp_apply, Measure.lintegral_bind (Kernel.aemeasurable _)
585585
measurable_excessMass.aemeasurable]
586586
refine le_antisymm (ge_of_tendsto' (hH hG hφG x) fun n ↦ ?_) bot_le
587587
calc excessMass κ π x ≤ ∫⁻ z, excessMass κ π z ∂((κ.restrict hG.compl) ^ n) x := h_pow n x

‎RandomDo/ForMathlib/Probability/Kernel/HarrisRecurrent.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Rémy Degenne
66
module
77

88
public import Mathlib.Probability.Kernel.Irreducible
9-
public import RandomDo.ForMathlib.Probability.Kernel.Pow
9+
public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp
1010

1111
/-!
1212
# Harris recurrent kernels
@@ -73,12 +73,12 @@ lemma IsHarrisRecurrent.isIrreducible [IsMarkovKernel κ] (h : κ.IsHarrisRecurr
7373
have h_eq : ∀ n : ℕ, ((κ.restrict hA.compl) ^ n) a = (κ ^ n) a := by
7474
intro n
7575
induction n with
76-
| zero => rw [pow_zero_apply, pow_zero_apply]
76+
| zero => simp
7777
| succ n ih =>
7878
have h0 : (κ ∘ₘ (κ ^ n) a) A = 0 := by
79-
rw [← pow_succ_apply']
79+
rw [← comp_apply, ← pow_add_one']
8080
exact nonpos_iff_eq_zero.mp (hcon (n + 1))
81-
rw [pow_succ_apply', ih, pow_succ_apply', Measure.restrict_comp]
81+
rw [pow_add_one', comp_apply, ih, pow_add_one', comp_apply, Measure.restrict_comp]
8282
exact Measure.restrict_eq_self_of_ae_mem (measure_eq_zero_iff_ae_notMem.mp h0)
8383
have h_tendsto := h hA hφA a
8484
simp_rw [h_eq, measure_univ] at h_tendsto

‎RandomDo/ForMathlib/Probability/Kernel/Invariance.lean‎

Lines changed: 19 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Rémy Degenne
66
module
77

88
public import Mathlib.Probability.Kernel.Invariance
9-
public import RandomDo.ForMathlib.Probability.Kernel.Pow
9+
public import RandomDo.ForMathlib.Probability.Kernel.Composition.MeasureComp
1010

1111
/-!
1212
# Invariant measures and powers of a kernel
@@ -18,7 +18,7 @@ public import RandomDo.ForMathlib.Probability.Kernel.Pow
1818
* `Kernel.Invariant.ae_ae_pow`: if a property holds `μ`-almost everywhere for a measure `μ`
1919
invariant for `κ`, then for `μ`-almost every `a` it holds `(κ ^ n) a`-almost everywhere for
2020
all `n`.
21-
* `Kernel.Invariant.ae_apply_eq_zero_of_ae_absorbing`: if a measurable set of finite measure is
21+
* `Kernel.Invariant.ae_apply_eq_zero_of_compl`: if a measurable set of finite measure is
2222
absorbing almost everywhere with respect to an invariant measure of a Markov kernel, then so is
2323
its complement.
2424
-/
@@ -31,55 +31,54 @@ open scoped ENNReal ProbabilityTheory
3131

3232
namespace ProbabilityTheory.Kernel
3333

34-
variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ π : Measure α} {G : Set α}
34+
variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α α} {μ : Measure α}
3535

36-
lemma Invariant.pow (h : κ.Invariant μ) (n : ℕ) : (κ ^ n).Invariant μ := by
36+
theorem Invariant.pow (h : Invariant κ μ) (n : ℕ) : Invariant (κ ^ n) μ := by
3737
induction n with
38-
| zero => exact pow_zero_comp κ μ
38+
| zero => simp [Invariant]
3939
| succ n ih => rw [pow_succ, mul_eq_comp]; exact ih.comp h
4040

41-
lemma Invariant.smul (h : κ.Invariant μ) (c : ℝ≥0∞) : κ.Invariant (c • μ) := by
41+
theorem Invariant.smul (h : Invariant κ μ) (c : ℝ≥0∞) : Invariant κ (c • μ) := by
4242
rw [Invariant, Measure.comp_smul, h.def]
4343

4444
/-- If `μ` is invariant for `κ` and a property holds `μ`-almost everywhere, then for `μ`-almost
4545
every `a` it holds `(κ ^ n) a`-almost everywhere for all `n`. -/
46-
lemma Invariant.ae_ae_pow (h : κ.Invariant μ) {p : α → Prop} (hp : ∀ᵐ a ∂μ, p a) :
46+
theorem Invariant.ae_ae_pow (h : Invariant κ μ) {p : α → Prop} (hp : ∀ᵐ a ∂μ, p a) :
4747
∀ᵐ a ∂μ, ∀ n, ∀ᵐ b ∂(κ ^ n) a, p b := by
4848
rw [ae_all_iff]
4949
intro n
5050
rw [← (h.pow n).def] at hp
5151
exact Measure.ae_ae_of_ae_comp hp
5252

53-
/-! ### Absorbing sets -/
53+
section Absorbing
54+
55+
variable {π : Measure α} {G : Set α}
5456

5557
/-- If a measurable set `G` is absorbing almost everywhere with respect to an invariant measure
5658
`π`, then for `π`-almost every point of `G`, no power of `κ` charges `Gᶜ`. -/
57-
lemma Invariant.ae_pow_apply_compl_eq_zero (hπ : κ.Invariant π) (hG : MeasurableSet G)
59+
theorem Invariant.ae_pow_apply_compl_eq_zero (hπ : Invariant κ π) (hG : MeasurableSet G)
5860
(h : ∀ᵐ x ∂π, x ∈ G → κ x Gᶜ = 0) :
5961
∀ᵐ x ∂π, x ∈ G → ∀ n, (κ ^ n) x Gᶜ = 0 := by
6062
suffices ∀ n, ∀ᵐ x ∂π, x ∈ G → (κ ^ n) x Gᶜ = 0 by
6163
filter_upwards [ae_all_iff.mpr this] with x hx hxG n using hx n hxG
6264
intro n
6365
induction n with
64-
| zero =>
65-
refine ae_of_all _ fun x hx ↦ ?_
66-
rw [pow_zero_apply, Measure.dirac_apply' _ hG.compl]
67-
simp [hx]
66+
| zero => simp [Kernel.id_apply, Measure.dirac_apply' _ hG.compl]
6867
| succ n ih =>
6968
have h1 : ∀ᵐ x ∂π, ∀ᵐ y ∂κ x, y ∈ G → (κ ^ n) y Gᶜ = 0 := by
7069
rw [← hπ.def] at ih
7170
exact Measure.ae_ae_of_ae_comp ih
7271
filter_upwards [h, h1] with x hx hx1 hxG
73-
rw [pow_succ_apply, Measure.bind_apply hG.compl (κ ^ n).aemeasurable,
74-
lintegral_eq_zero_iff ((κ ^ n).measurable_coe hG.compl)]
72+
suffices (fun a ↦ (κ ^ n) a Gᶜ) =ᵐ[κ x] 0 by
73+
rwa [pow_add_one, comp_apply, Measure.bind_apply hG.compl (κ ^ n).aemeasurable,
74+
lintegral_eq_zero_iff ((κ ^ n).measurable_coe hG.compl)]
7575
have hxG' : ∀ᵐ y ∂κ x, y ∈ G := by
76-
have := measure_eq_zero_iff_ae_notMem.mp (hx hxG)
77-
filter_upwards [this] with y hy using by simpa using hy
76+
simpa using measure_eq_zero_iff_ae_notMem.mp (hx hxG)
7877
filter_upwards [hx1, hxG'] with y hy hyG using hy hyG
7978

8079
/-- If a measurable set `G` of finite measure is absorbing almost everywhere with respect to an
8180
invariant measure of a Markov kernel, then so is its complement. -/
82-
lemma Invariant.ae_apply_eq_zero_of_ae_absorbing [IsMarkovKernel κ] (hπ : κ.Invariant π)
81+
theorem Invariant.ae_apply_eq_zero_of_compl [IsMarkovKernel κ] (hπ : Invariant κ π)
8382
(hG : MeasurableSet G) (hπG : π G ≠ ∞) (h : ∀ᵐ x ∂π, x ∈ G → κ x Gᶜ = 0) :
8483
∀ᵐ x ∂π, x ∈ Gᶜ → κ x G = 0 := by
8584
have h1 : ∫⁻ x, κ x G ∂π = π G := by
@@ -94,4 +93,6 @@ lemma Invariant.ae_apply_eq_zero_of_ae_absorbing [IsMarkovKernel κ] (hπ : κ.I
9493
exact (ENNReal.add_right_inj hπG).mp (by rw [h_add, add_zero])
9594
rwa [setLIntegral_eq_zero_iff hG.compl (κ.measurable_coe hG)] at h3
9695

96+
end Absorbing
97+
9798
end ProbabilityTheory.Kernel

‎RandomDo/ForMathlib/Probability/Kernel/Irreducible.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ lemma IsIrreducible.exists_pow_succ_pos [IsIrreducible φ κ] {A : Set α} (hA :
6161
rw [IsIrreducible.iUnion_setOf_pow_apply_pos_eq_univ (φ := φ) hA hφA]
6262
exact Measure.measure_univ_ne_zero.mpr hx
6363
obtain ⟨n, hn⟩ := exists_measure_pos_of_not_measure_iUnion_null hpos
64-
exact ⟨n, (pow_succ_apply_pos_iff hA).mpr hn⟩
64+
exact ⟨n, (pow_add_one_apply_pos_iff hA).mpr hn⟩
6565

6666
/-- For a `φ`-irreducible kernel, every set of positive `φ`-measure is reached with positive
6767
probability from any nonzero initial measure. -/
@@ -120,7 +120,7 @@ lemma Invariant.measure_eq_zero_or_measure_compl_eq_zero [IsMarkovKernel κ] [Is
120120
have h1 : φ Gᶜ = 0 := hπ.measure_compl_eq_zero_of_ae_absorbing hG h hcon.1
121121
have h2 : φ Gᶜᶜ = 0 := by
122122
refine hπ.measure_compl_eq_zero_of_ae_absorbing hG.compl ?_ hcon.2
123-
simpa using hπ.ae_apply_eq_zero_of_ae_absorbing hG hπG h
123+
simpa using hπ.ae_apply_eq_zero_of_compl hG hπG h
124124
rw [compl_compl] at h2
125125
refine hφ ?_
126126
rw [← Measure.measure_univ_eq_zero, ← Set.union_compl_self G]

0 commit comments

Comments
 (0)