MarkovMinorization.lean

1 import KomorebiLSM.MeasureTVCalculus
2 import Mathlib.Probability.Kernel.Composition.MeasureComp
3 
4 /-! Actual Markov-kernel minorization implies Dobrushin contraction. The
5 normalized pullback of each bounded test is derived from the measure inequality;
6 no contraction coefficient is supplied as a field. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.MarkovStability
9 open MeasureTheory ProbabilityTheory SequentialLowerCertificate MeasureTVCalculus
10 open scoped ENNReal
11 variable {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
12 
13 /-- Integrating a bounded test against an actual kernel-composed measure. -/
14 theorem integral_comp_measure (ν : Measure X) [IsProbabilityMeasure ν]
15     (K : Kernel X Y) [IsMarkovKernel K] (f : Y → ℝ) (hf : Measurable f)
16     (h0 : ∀ y,0≤f y) (h1 : ∀ y,f y≤1) :
17     (∫ y,f y∂K ∘ₘ ν)=∫ x,∫ y,f y∂K x∂ν := by
18   rw [← Measure.snd_compProd]
19   change (∫ y,f y∂(ν ⊗ₘ K).map Prod.snd)=_
20   rw [integral_map measurable_snd.aemeasurable hf.aestronglyMeasurable]
21   exact Measure.integral_compProd (bounded_test_integrable (ν ⊗ₘ K) _
22     (hf.comp measurable_snd) (fun p => h0 p.2) (fun p => h1 p.2))
23 
24 /-- A probability reference occurs with at least this real mass in every row. -/
25 def Minorized (P : Kernel X Y) (ρ : ℝ) (reference : Measure Y) : Prop :=
26   ∀ x,ENNReal.ofReal ρ • reference≤P x
27 
28 /-- Minorization bounds the oscillation of the actual pulled-back test. -/
29 theorem pullback_interval (P : Kernel X Y) [IsMarkovKernel P]
30     (reference : Measure Y) [IsProbabilityMeasure reference] (ρ : ℝ) (hρ : 0≤ρ)
31     (hmin : Minorized P ρ reference) (f : Y → ℝ) (hf : Measurable f)
32     (h0 : ∀ y,0≤f y) (h1 : ∀ y,f y≤1) (x : X) :
33     ρ*(∫ y,f y∂reference)≤∫ y,f y∂P x ∧
34       (∫ y,f y∂P x)≤ρ*(∫ y,f y∂reference)+(1-ρ) := by
35   have hl : ρ*(∫ y,f y∂reference)≤∫ y,f y∂P x := by
36     have h := integral_mono_measure (hmin x) (ae_of_all _ h0)
37       (bounded_test_integrable (P x) f hf h0 h1)
38     simpa only [integral_smul_measure,ENNReal.toReal_ofReal hρ,smul_eq_mul] using h
39   have hc : ρ*(∫ y,(1-f y)∂reference)≤∫ y,(1-f y)∂P x := by
40     have h := integral_mono_measure (hmin x) (ae_of_all _ (fun y => sub_nonneg.mpr (h1 y)))
41       ((integrable_const (1:ℝ)).sub (bounded_test_integrable (P x) f hf h0 h1))
42     simpa only [integral_smul_measure,ENNReal.toReal_ofReal hρ,smul_eq_mul] using h
43   rw [integral_sub (integrable_const _) (bounded_test_integrable reference f hf h0 h1),
44     integral_sub (integrable_const _) (bounded_test_integrable (P x) f hf h0 h1)] at hc
45   simp only [integral_const,measureReal_def,measure_univ,ENNReal.toReal_one,one_smul] at hc
46   exact ⟨hl,by linarith⟩
47 
48 /-- Dobrushin contraction is derived on actual output measures from the common
49 minorization, including the complete-refresh endpoint rho=1. -/
50 theorem minorization_contraction (P : Kernel X Y) [IsMarkovKernel P]
51     (reference : Measure Y) [IsProbabilityMeasure reference] (ρ : ℝ)
52     (hρ0 : 0≤ρ) (hρ1 : ρ≤1) (hmin : Minorized P ρ reference)
53     (ν η : Measure X) [IsProbabilityMeasure ν] [IsProbabilityMeasure η] :
54     lawTV (P ∘ₘ ν) (P ∘ₘ η)≤(1-ρ)*lawTV ν η := by
55   apply lawTV_le_of_bounded_tests
56   intro f hf h0 h1
57   rw [integral_comp_measure ν P f hf h0 h1,integral_comp_measure η P f hf h0 h1]
58   let F : X → ℝ := fun x => ∫ y,f y∂P x
59   let c : ℝ := ρ*(∫ y,f y∂reference)
60   have hm : Measurable F := hf.stronglyMeasurable.integral_kernel.measurable
61   have hb (x : X) : c≤F x ∧ F x≤c+(1-ρ) := pullback_interval P reference ρ hρ0 hmin f hf h0 h1 x
62   by_cases hz : ρ=1
63   · have he (x : X) : F x=c := by have h:=hb x; simp only [hz,sub_self,add_zero] at h; exact le_antisymm h.2 h.1
64     change |(∫ x,F x∂ν)-(∫ x,F x∂η)|≤(1-ρ)*lawTV ν η
65     simp only [he,integral_const,measureReal_def,measure_univ,ENNReal.toReal_one,one_smul,sub_self,abs_zero,hz,zero_mul,le_refl]
66   · have hp : 0<1-ρ := sub_pos.mpr (lt_of_le_of_ne hρ1 hz)
67     let g : X → ℝ := fun x => (F x-c)/(1-ρ)
68     have hgm : Measurable g := (hm.sub measurable_const).div_const _
69     have hg0 (x : X) : 0≤g x := div_nonneg (sub_nonneg.mpr (hb x).1) hp.le
70     have hg1 (x : X) : g x≤1 := (div_le_one hp).mpr (by linarith [(hb x).2])
71     have hge (x : X) : F x=c+(1-ρ)*g x := by dsimp [g]; field_simp; ring
72     have hi (ξ : Measure X) [IsProbabilityMeasure ξ] :
73         (∫ x,F x∂ξ)=c+(1-ρ)*(∫ x,g x∂ξ) := by
74       calc (∫ x,F x∂ξ)=∫ x,c+(1-ρ)*g x∂ξ := integral_congr_ae (ae_of_all _ hge)
75         _ = _ := by
76           rw [integral_add (integrable_const _) ((bounded_test_integrable ξ g hgm hg0 hg1).const_mul _),
77             integral_const_mul (1-ρ) g]
78           simp only [integral_const,measureReal_def,measure_univ,ENNReal.toReal_one,one_smul]
79     change |(∫ x,F x∂ν)-(∫ x,F x∂η)|≤(1-ρ)*lawTV ν η
80     rw [hi ν,hi η]
81     calc |c+(1-ρ)*(∫ x,g x∂ν)-(c+(1-ρ)*(∫ x,g x∂η))|=
82         (1-ρ)*|(∫ x,g x∂ν)-(∫ x,g x∂η)| := by
83           rw [show c+(1-ρ)*(∫ x,g x∂ν)-(c+(1-ρ)*(∫ x,g x∂η))=
84             (1-ρ)*((∫ x,g x∂ν)-(∫ x,g x∂η)) by ring,abs_mul,abs_of_pos hp]
85       _ ≤ (1-ρ)*lawTV ν η := mul_le_mul_of_nonneg_left
86         (bounded_test_integral_le_tv ν η g hgm hg0 hg1) hp.le
87 
88 /-- A uniform actual conditional-TV budget controls changing one kernel under
89 an actual common prefix. Conditional-TV measurability is not needed for this
90 constant budget on arbitrary measurable spaces. -/
91 theorem compProd_uniform_change (ν : Measure X) [IsProbabilityMeasure ν]
92     (K L : Kernel X Y) [IsMarkovKernel K] [IsMarkovKernel L] (Δ : ℝ)
93     (hΔ : ∀ x,lawTV (K x) (L x)≤Δ) : lawTV (ν ⊗ₘ K) (ν ⊗ₘ L)≤Δ := by
94   apply lawTV_le_of_bounded_tests
95   intro f hf h0 h1
96   have hfi (J : Kernel X Y) [IsMarkovKernel J] (x : X) : Integrable (fun y => f (x,y)) (J x) :=
97     bounded_test_integrable (J x) _ (hf.comp (measurable_const.prodMk measurable_id))
98       (fun y => h0 (x,y)) (fun y => h1 (x,y))
99   have hFm (J : Kernel X Y) [IsMarkovKernel J] : Measurable (fun x => ∫ y,f (x,y)∂J x) :=
100     hf.stronglyMeasurable.integral_kernel_prod_right'.measurable
101   have hF0 (J : Kernel X Y) [IsMarkovKernel J] (x : X) : 0≤∫ y,f (x,y)∂J x :=
102     integral_nonneg (fun y => h0 (x,y))
103   have hF1 (J : Kernel X Y) [IsMarkovKernel J] (x : X) : (∫ y,f (x,y)∂J x)≤1 := by
104     calc (∫ y,f (x,y)∂J x)≤∫ _ : Y,(1:ℝ)∂J x :=
105         integral_mono (hfi J x) (integrable_const _) (fun y => h1 (x,y))
106       _ = 1 := by simp
107   have hFk := bounded_test_integrable ν _ (hFm K) (hF0 K) (hF1 K)
108   have hFl := bounded_test_integrable ν _ (hFm L) (hF0 L) (hF1 L)
109   have hd : Integrable (fun x => (∫ y,f (x,y)∂K x)-(∫ y,f (x,y)∂L x)) ν :=
110     (hFk.sub hFl).congr (by filter_upwards with x; rfl)
111   rw [Measure.integral_compProd (bounded_test_integrable (ν ⊗ₘ K) f hf h0 h1),
112     Measure.integral_compProd (bounded_test_integrable (ν ⊗ₘ L) f hf h0 h1),← integral_sub hFk hFl]
113   calc |∫ x,(∫ y,f (x,y)∂K x)-(∫ y,f (x,y)∂L x)∂ν|≤
114       ∫ x,|(∫ y,f (x,y)∂K x)-(∫ y,f (x,y)∂L x)|∂ν := abs_integral_le_integral_abs
115     _ ≤ ∫ _ : X,Δ∂ν := by
116       apply integral_mono hd.abs (integrable_const _)
117       intro x
118       exact (bounded_test_integral_le_tv (K x) (L x) _
119         (hf.comp (measurable_const.prodMk measurable_id))
120         (fun y => h0 (x,y)) (fun y => h1 (x,y))).trans (hΔ x)
121     _ = Δ := by simp
122 
123 /-- The one-step output-marginal budget follows by actual projection of the
124 joint composition-product laws. -/
125 theorem comp_measure_uniform_change (ν : Measure X) [IsProbabilityMeasure ν]
126     (K L : Kernel X Y) [IsMarkovKernel K] [IsMarkovKernel L] (Δ : ℝ)
127     (hΔ : ∀ x,lawTV (K x) (L x)≤Δ) : lawTV (K ∘ₘ ν) (L ∘ₘ ν)≤Δ := by
128   have h := (lawTV_map (ν ⊗ₘ K) (ν ⊗ₘ L) Prod.snd measurable_snd).trans
129     (compProd_uniform_change ν K L Δ hΔ)
130   change lawTV (ν ⊗ₘ K).snd (ν ⊗ₘ L).snd≤Δ at h
131   simpa only [Measure.snd_compProd] using h
132 
133 end Komorebi.LSM.MarkovStability

Back to source controls