MarkovMarginals.lean

1 import KomorebiLSM.MarkovMinorization
2 
3 /-! P86: actual Markov marginal iterates satisfy the geometric stability bound
4 because minorization contracts the common-kernel part of each comparison. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.MarkovStability
7 open MeasureTheory ProbabilityTheory SequentialLowerCertificate MeasureTVCalculus
8 open scoped ENNReal
9 variable {X : Type*} [MeasurableSpace X]
10 
11 /-- The literal recursively composed one-time laws. -/
12 noncomputable def marginal (P : Kernel X X) (ν0 : Measure X) : ℕ → Measure X
13   | 0 => ν0
14   | n+1 => P ∘ₘ marginal P ν0 n
15 
16 instance marginal_probability (P : Kernel X X) [IsMarkovKernel P]
17     (ν0 : Measure X) [IsProbabilityMeasure ν0] (n : ℕ) : IsProbabilityMeasure (marginal P ν0 n) := by
18   induction n with
19   | zero => exact inferInstanceAs (IsProbabilityMeasure ν0)
20   | succ n ih =>
21     have := ih
22     exact inferInstanceAs (IsProbabilityMeasure (P ∘ₘ marginal P ν0 n))
23 
24 /-- The actual one-step recurrence, derived by adding a common-P continuation
25 and then changing the conditional kernel under the second current law. -/
26 theorem marginal_step (P Q : Kernel X X) [IsMarkovKernel P] [IsMarkovKernel Q]
27     (reference : Measure X) [IsProbabilityMeasure reference] (ρ Δ : ℝ)
28     (hρ0 : 0≤ρ) (hρ1 : ρ≤1) (hmin : Minorized P ρ reference)
29     (hΔ : ∀ x,lawTV (P x) (Q x)≤Δ)
30     (ν0 η0 : Measure X) [IsProbabilityMeasure ν0] [IsProbabilityMeasure η0] (n : ℕ) :
31     lawTV (marginal P ν0 (n+1)) (marginal Q η0 (n+1))≤
32       (1-ρ)*lawTV (marginal P ν0 n) (marginal Q η0 n)+Δ :=
33   (lawTV_triangle (P ∘ₘ marginal P ν0 n) (P ∘ₘ marginal Q η0 n) (Q ∘ₘ marginal Q η0 n)).trans
34     (add_le_add (minorization_contraction P reference ρ hρ0 hρ1 hmin (marginal P ν0 n) (marginal Q η0 n))
35       (comp_measure_uniform_change (marginal Q η0 n) P Q Δ hΔ))
36 
37 /-- The source's closed geometric error budget, including n=0 and rho=1. -/
38 noncomputable def marginalBudget (ρ Δ e0 : ℝ) (n : ℕ) : ℝ :=
39   (1-ρ)^n*e0+Δ*(1-(1-ρ)^n)/ρ
40 
41 omit [MeasurableSpace X] in
42 theorem marginalBudget_succ (ρ Δ e0 : ℝ) (hρ : ρ≠0) (n : ℕ) :
43     (1-ρ)*marginalBudget ρ Δ e0 n+Δ=marginalBudget ρ Δ e0 (n+1) := by
44   unfold marginalBudget
45   rw [pow_succ]
46   field_simp
47   ring
48 
49 /-- Full geometric bound for the actual one-time marginal measures. -/
50 theorem marginal_bound (P Q : Kernel X X) [IsMarkovKernel P] [IsMarkovKernel Q]
51     (reference : Measure X) [IsProbabilityMeasure reference] (ρ Δ : ℝ)
52     (hρ0 : 0<ρ) (hρ1 : ρ≤1) (hmin : Minorized P ρ reference)
53     (hΔ : ∀ x,lawTV (P x) (Q x)≤Δ)
54     (ν0 η0 : Measure X) [IsProbabilityMeasure ν0] [IsProbabilityMeasure η0] (n : ℕ) :
55     lawTV (marginal P ν0 n) (marginal Q η0 n)≤
56       min 1 ((1-ρ)^n*lawTV ν0 η0+Δ*(1-(1-ρ)^n)/ρ) := by
57   apply le_min (lawTV_le_one _ _)
58   change lawTV (marginal P ν0 n) (marginal Q η0 n)≤marginalBudget ρ Δ (lawTV ν0 η0) n
59   induction n with
60   | zero => simp [marginal,marginalBudget]
61   | succ n ih =>
62     calc lawTV (marginal P ν0 (n+1)) (marginal Q η0 (n+1))≤
63         (1-ρ)*lawTV (marginal P ν0 n) (marginal Q η0 n)+Δ :=
64           marginal_step P Q reference ρ Δ hρ0.le hρ1 hmin hΔ ν0 η0 n
65       _ ≤ (1-ρ)*marginalBudget ρ Δ (lawTV ν0 η0) n+Δ :=
66         add_le_add (mul_le_mul_of_nonneg_left ih (sub_nonneg.mpr hρ1)) le_rfl
67       _ = marginalBudget ρ Δ (lawTV ν0 η0) (n+1) :=
68         marginalBudget_succ ρ Δ (lawTV ν0 η0) (ne_of_gt hρ0) n
69 
70 /-- Complete refresh rho=1 removes every initial discrepancy after one step. -/
71 theorem marginal_bound_refresh (P Q : Kernel X X) [IsMarkovKernel P] [IsMarkovKernel Q]
72     (reference : Measure X) [IsProbabilityMeasure reference] (Δ : ℝ)
73     (hmin : Minorized P 1 reference) (hΔ : ∀ x,lawTV (P x) (Q x)≤Δ)
74     (ν0 η0 : Measure X) [IsProbabilityMeasure ν0] [IsProbabilityMeasure η0] (n : ℕ) :
75     lawTV (marginal P ν0 (n+1)) (marginal Q η0 (n+1))≤min 1 Δ := by
76   apply le_min (lawTV_le_one _ _)
77   simpa only [sub_self,zero_mul,zero_add] using
78     marginal_step P Q reference 1 Δ (by norm_num) le_rfl hmin hΔ ν0 η0 n
79 
80 /-- A common initial law has a uniform all-time one-marginal budget. -/
81 theorem marginal_same_initial_uniform (P Q : Kernel X X) [IsMarkovKernel P] [IsMarkovKernel Q]
82     (reference : Measure X) [IsProbabilityMeasure reference] (ρ Δ : ℝ)
83     (hρ0 : 0<ρ) (hρ1 : ρ≤1) (hΔ0 : 0≤Δ) (hmin : Minorized P ρ reference)
84     (hΔ : ∀ x,lawTV (P x) (Q x)≤Δ)
85     (ν0 : Measure X) [IsProbabilityMeasure ν0] (n : ℕ) :
86     lawTV (marginal P ν0 n) (marginal Q ν0 n)≤min 1 (Δ/ρ) := by
87   apply (marginal_bound P Q reference ρ Δ hρ0 hρ1 hmin hΔ ν0 ν0 n).trans
88   apply min_le_min le_rfl
89   simp only [lawTV_self,mul_zero,zero_add]
90   apply (div_le_div_iff_of_pos_right hρ0).2
91   have hn : 0≤(1-ρ)^n := pow_nonneg (sub_nonneg.mpr hρ1) n
92   nlinarith
93 
94 end Komorebi.LSM.MarkovStability

Back to source controls