MarkovRecords.lean

1 import KomorebiLSM.MarkovMarginals
2 import Mathlib.Probability.Kernel.Composition.CompMap
3 import Mathlib.Probability.Kernel.Composition.Lemmas
4 
5 /-! Actual chronological Markov records and rolling-window laws. A record with
6 L transitions contains L+1 consecutive states, including its entry state. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.MarkovStability
9 open MeasureTheory ProbabilityTheory SequentialLowerCertificate MeasureTVCalculus
10 open scoped ENNReal
11 universe u
12 
13 def Record (X : Type u) : ℕ → Type u
14   | 0 => X
15   | n+1 => Record X n × X
16 
17 instance recordMeasurable {X : Type*} [MeasurableSpace X] :
18     (n : ℕ) → MeasurableSpace (Record X n)
19   | 0 => inferInstanceAs (MeasurableSpace X)
20   | n+1 => by
21     letI := recordMeasurable (X := X) n
22     exact inferInstanceAs (MeasurableSpace (Record X n × X))
23 attribute [reducible] Record
24 
25 def recordLast {X : Type*} : (n : ℕ) → Record X n → X
26   | 0,x => x
27   | _+1,x => x.2
28 
29 theorem recordLast_measurable {X : Type*} [MeasurableSpace X] :
30     (n : ℕ) → Measurable (recordLast (X := X) n)
31   | 0 => measurable_id
32   | _+1 => measurable_snd
33 
34 variable {X : Type*} [MeasurableSpace X]
35 
36 /-- Literal chronological extension by the row at the most recent state. -/
37 noncomputable def recordLaw (P : Kernel X X) (ν0 : Measure X) :
38     (n : ℕ) → Measure (Record X n)
39   | 0 => ν0
40   | n+1 => recordLaw P ν0 n ⊗ₘ P.comap (recordLast n) (recordLast_measurable n)
41 
42 theorem recordLaw_probability_aux (P : Kernel X X) [IsMarkovKernel P]
43     (ν0 : Measure X) [IsProbabilityMeasure ν0] :
44     (n : ℕ) → IsProbabilityMeasure (recordLaw P ν0 n)
45   | 0 => inferInstanceAs (IsProbabilityMeasure ν0)
46   | n+1 => by
47     have := recordLaw_probability_aux P ν0 n
48     exact inferInstanceAs (IsProbabilityMeasure
49       (recordLaw P ν0 n ⊗ₘ P.comap (recordLast n) (recordLast_measurable n)))
50 
51 instance recordLaw_probability (P : Kernel X X) [IsMarkovKernel P]
52     (ν0 : Measure X) [IsProbabilityMeasure ν0] (n : ℕ) :
53     IsProbabilityMeasure (recordLaw P ν0 n) := recordLaw_probability_aux P ν0 n
54 instance recordLaw_zero_probability (P : Kernel X X) [IsMarkovKernel P]
55     (ν0 : Measure X) [IsProbabilityMeasure ν0] :
56     IsProbabilityMeasure (recordLaw P ν0 0) := recordLaw_probability_aux P ν0 0
57 instance recordLaw_succ_probability (P : Kernel X X) [IsMarkovKernel P]
58     (ν0 : Measure X) [IsProbabilityMeasure ν0] (n : ℕ) :
59     IsProbabilityMeasure (recordLaw P ν0 (n+1)) := recordLaw_probability_aux P ν0 (n+1)
60 
61 /-- The constructed joint laws have the actual prefix consistency property. -/
62 theorem recordLaw_consistent (P : Kernel X X) [IsMarkovKernel P]
63     (ν0 : Measure X) [IsProbabilityMeasure ν0] (n : ℕ) :
64     (recordLaw P ν0 (n+1)).fst=recordLaw P ν0 n := Measure.fst_compProd _ _
65 
66 /-- The last coordinate of the actual record is the iterated Markov marginal. -/
67 theorem recordLaw_last (P : Kernel X X) [IsMarkovKernel P]
68     (ν0 : Measure X) [IsProbabilityMeasure ν0] :
69     ∀ n,(recordLaw P ν0 n).map (recordLast n)=marginal P ν0 n
70   | 0 => by change ν0.map id=ν0; exact Measure.map_id
71   | n+1 => by
72     change (recordLaw P ν0 n ⊗ₘ P.comap (recordLast n) (recordLast_measurable n)).snd=
73       P ∘ₘ marginal P ν0 n
74     rw [Measure.snd_compProd,← Kernel.comp_deterministic_eq_comap,
75       ← Measure.comp_assoc,Measure.deterministic_comp_eq_map,recordLaw_last P ν0 n]
76 
77 /-- Full records accumulate one uniform conditional error per transition. -/
78 theorem recordLaw_step (P Q : Kernel X X) [IsMarkovKernel P] [IsMarkovKernel Q]
79     (Δ : ℝ) (hΔ : ∀ x,lawTV (P x) (Q x)≤Δ)
80     (ν0 η0 : Measure X) [IsProbabilityMeasure ν0] [IsProbabilityMeasure η0] (n : ℕ) :
81     lawTV (recordLaw P ν0 (n+1)) (recordLaw Q η0 (n+1))≤
82       lawTV (recordLaw P ν0 n) (recordLaw Q η0 n)+Δ := by
83   let KP := P.comap (recordLast n) (recordLast_measurable n)
84   let KQ := Q.comap (recordLast n) (recordLast_measurable n)
85   have hcost := compProd_uniform_change (recordLaw P ν0 n) KP KQ Δ (fun r => hΔ (recordLast n r))
86   have hcont := lawTV_compProd (recordLaw P ν0 n) (recordLaw Q η0 n) KQ
87   have htri := lawTV_triangle (recordLaw P ν0 n ⊗ₘ KP)
88     (recordLaw P ν0 n ⊗ₘ KQ) (recordLaw Q η0 n ⊗ₘ KQ)
89   exact (htri.trans (add_le_add hcost hcont)).trans_eq (add_comm _ _)
90 
91 /-- The finite-window telescoping bound is for literal joint record measures. -/
92 theorem recordLaw_bound (P Q : Kernel X X) [IsMarkovKernel P] [IsMarkovKernel Q]
93     (Δ : ℝ) (hΔ : ∀ x,lawTV (P x) (Q x)≤Δ)
94     (ν0 η0 : Measure X) [IsProbabilityMeasure ν0] [IsProbabilityMeasure η0] (n : ℕ) :
95     lawTV (recordLaw P ν0 n) (recordLaw Q η0 n)≤min 1 (lawTV ν0 η0+(n:ℝ)*Δ) := by
96   apply le_min (lawTV_le_one _ _)
97   induction n with
98   | zero =>
99     simp only [recordLaw,Nat.cast_zero,zero_mul,add_zero]
100     exact le_rfl
101   | succ n ih =>
102     calc lawTV (recordLaw P ν0 (n+1)) (recordLaw Q η0 (n+1))≤
103         lawTV (recordLaw P ν0 n) (recordLaw Q η0 n)+Δ := recordLaw_step P Q Δ hΔ ν0 η0 n
104       _ ≤ (lawTV ν0 η0+(n:ℝ)*Δ)+Δ := add_le_add ih le_rfl
105       _ = lawTV ν0 η0+((n+1:ℕ):ℝ)*Δ := by push_cast; ring
106 
107 end Komorebi.LSM.MarkovStability

Back to source controls