SequentialLowerCertificate.lean

1 import Mathlib.MeasureTheory.VectorMeasure.Integral
2 import Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure
3 import Mathlib.MeasureTheory.Integral.IntegrableOn
4 import Mathlib.Tactic
5 
6 set_option autoImplicit false
7 
8 /-!
9 # Sequential lower discrepancy certificate
10 
11 The law distance is the probability convention for total variation: one half
12 the total mass of the variation of the actual signed measure `P - Q`.
13 The observation space is an arbitrary measurable space. The certificate is
14 conditional on the simultaneous residual event of Proposition 66; no new
15 concentration statement is assumed or asserted here.
16 -/
17 namespace Komorebi.LSM.SequentialLowerCertificate
18 
19 noncomputable section
20 
21 open MeasureTheory Set
22 open scoped ENNReal BigOperators
23 
24 variable {Ω : Type*} [MeasurableSpace Ω]
25 
26 /-- Standard total variation distance between finite probability laws. -/
27 def lawTV (P Q : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] : ℝ :=
28   (1 / 2 : ℝ) * (P.toSignedMeasure - Q.toSignedMeasure).totalVariation.real univ
29 
30 /-- The probability convention gives a nonnegative law discrepancy. -/
31 theorem lawTV_nonneg (P Q : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] :
32     0 ≤ lawTV P Q := by
33   exact mul_nonneg (by norm_num) ENNReal.toReal_nonneg
34 
35 /-- Identical laws have zero discrepancy. -/
36 theorem lawTV_self (P : Measure Ω) [IsProbabilityMeasure P] : lawTV P P = 0 := by
37   simp [lawTV, SignedMeasure.totalVariation_zero]
38 
39 /-- Two probability laws have total variation at most one. -/
40 theorem lawTV_le_one (P Q : Measure Ω)
41     [IsProbabilityMeasure P] [IsProbabilityMeasure Q] : lawTV P Q ≤ 1 := by
42   have hle := VectorMeasure.variation_sub_le (μ := P.toSignedMeasure) (ν := Q.toSignedMeasure)
43   have hset : (P.toSignedMeasure - Q.toSignedMeasure).totalVariation univ ≤ (2 : ℝ≥0∞) := by
44     rw [SignedMeasure.totalVariation_eq_variation]
45     convert hle univ using 1
46     norm_num [Measure.variation_toSignedMeasure]
47   have hr := ENNReal.toReal_mono (by norm_num : (2 : ℝ≥0∞) ≠ ⊤) hset
48   norm_num only [ENNReal.toReal_ofNat] at hr
49   dsimp [lawTV, Measure.real]
50   linarith
51 
52 /-- A measurable test bounded in `[0,1]` is integrable under a probability law. -/
53 theorem bounded_test_integrable (P : Measure Ω) [IsProbabilityMeasure P]
54     (φ : Ω → ℝ) (hφ : Measurable φ) (h0 : ∀ x, 0 ≤ φ x) (h1 : ∀ x, φ x ≤ 1) :
55     Integrable φ P := by
56   apply Integrable.of_bound hφ.aestronglyMeasurable 1
57   exact ae_of_all P (fun x => by rw [Real.norm_eq_abs, abs_of_nonneg (h0 x)]; exact h1 x)
58 
59 /-- Actual bounded-test integral discrepancy is controlled by actual total variation. -/
60 theorem bounded_test_integral_le_tv (P Q : Measure Ω)
61     [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
62     (φ : Ω → ℝ) (hφ : Measurable φ) (h0 : ∀ x, 0 ≤ φ x) (h1 : ∀ x, φ x ≤ 1) :
63     |(∫ x, φ x ∂P) - (∫ x, φ x ∂Q)| ≤ lawTV P Q := by
64   let s : SignedMeasure Ω := P.toSignedMeasure - Q.toSignedMeasure
65   have : IsFiniteMeasure s.variation := by
66     rw [← s.totalVariation_eq_variation]
67     infer_instance
68   have hp := bounded_test_integrable P φ hφ h0 h1
69   have hq := bounded_test_integrable Q φ hφ h0 h1
70   have hpc : P.toSignedMeasure.Integrable (fun x => φ x - (1 / 2 : ℝ)) := by
71     simpa only [VectorMeasure.Integrable, Measure.variation_toSignedMeasure] using
72       hp.sub' (integrable_const (1 / 2 : ℝ))
73   have hqc : Q.toSignedMeasure.Integrable (fun x => φ x - (1 / 2 : ℝ)) := by
74     simpa only [VectorMeasure.Integrable, Measure.variation_toSignedMeasure] using
75       hq.sub' (integrable_const (1 / 2 : ℝ))
76   have hid : (∫ᵛ x, (φ x - (1 / 2 : ℝ)) ∂<•s) =
77       (∫ x, φ x ∂P) - (∫ x, φ x ∂Q) := by
78     change (∫ᵛ x, (φ x - (1 / 2 : ℝ)) ∂<•(P.toSignedMeasure - Q.toSignedMeasure)) = _
79     rw [VectorMeasure.integral_sub_vectorMeasure hpc hqc]
80     simp only [VectorMeasure.integral_toSignedMeasure,
81       integral_sub hp (integrable_const (1 / 2 : ℝ)),
82       integral_sub hq (integrable_const (1 / 2 : ℝ)), integral_const,
83       Measure.real, measure_univ, ENNReal.toReal_one, smul_eq_mul, one_mul]
84     ring
85   have hbound : ∀ᵐ x ∂s.variation, ‖φ x - (1 / 2 : ℝ)‖ ≤ (1 / 2 : ℝ) := by
86     exact ae_of_all _ (fun x => by
87       rw [Real.norm_eq_abs]
88       exact abs_le.mpr ⟨by linarith [h0 x], by linarith [h1 x]⟩)
89   have hn := VectorMeasure.norm_integral_le_of_norm_le_const
90     (B := (ContinuousLinearMap.lsmul ℝ ℝ).flip) hbound
91   rw [hid, Real.norm_eq_abs] at hn
92   change |(∫ x, φ x ∂P) - (∫ x, φ x ∂Q)| ≤ (1 / 2 : ℝ) * s.totalVariation.real univ
93   rw [s.totalVariation_eq_variation]
94   simpa only [ContinuousLinearMap.opNorm_flip, ContinuousLinearMap.opNorm_lsmul, mul_one] using hn
95 
96 /-- Distinct point masses are separated by unit total variation. -/
97 theorem lawTV_dirac_eq_one [MeasurableSingletonClass Ω] (x y : Ω) (hxy : x ≠ y) :
98     lawTV (Measure.dirac x) (Measure.dirac y) = 1 := by
99   let φ : Ω → ℝ := ({x} : Set Ω).indicator (fun _ => 1)
100   have hφ : Measurable φ := measurable_const.indicator (measurableSet_singleton x)
101   have h0 : ∀ z, 0 ≤ φ z := by
102     intro z
103     by_cases hz : z ∈ ({x} : Set Ω) <;> simp [φ, hz]
104   have h1 : ∀ z, φ z ≤ 1 := by
105     intro z
106     by_cases hz : z ∈ ({x} : Set Ω) <;> simp [φ, hz]
107   have hbound := bounded_test_integral_le_tv (Measure.dirac x) (Measure.dirac y) φ hφ h0 h1
108   have hlower : 1 ≤ lawTV (Measure.dirac x) (Measure.dirac y) := by
109     simpa [φ, integral_dirac, hxy, Ne.symm hxy] using hbound
110   exact le_antisymm (lawTV_le_one _ _) hlower
111 
112 /-- The accumulated observed residual, storing the first time at index zero. -/
113 def residual (t : ℕ) (observed modelMean : ℕ → ℝ) : ℝ :=
114   ∑ s ∈ Finset.range t, (observed s - modelMean s)
115 
116 /-- Accumulated conditional predictive drift on those same histories and actions. -/
117 def drift (t : ℕ) (trueMean modelMean : ℕ → ℝ) : ℝ :=
118   ∑ s ∈ Finset.range t, (trueMean s - modelMean s)
119 
120 /-- On the simultaneous event, positive residual excess is bounded by accumulated drift. -/
121 theorem residual_excess_le_abs_drift (R D boundary : ℝ)
122     (hevent : |R - D| ≤ boundary) : max (|R| - boundary) 0 ≤ |D| := by
123   have htriangle : |R| ≤ |R - D| + |D| := by
124     simpa only [sub_add_cancel] using abs_add_le (R - D) D
125   exact max_le (by linarith) (abs_nonneg D)
126 
127 /-- Actual conditional test drift is controlled by the sum of actual law discrepancies. -/
128 theorem abs_drift_le_tv_sum (t : ℕ) (P Q : ℕ → Measure Ω)
129     [∀ s, IsProbabilityMeasure (P s)] [∀ s, IsProbabilityMeasure (Q s)]
130     (φ : ℕ → Ω → ℝ) (hφ : ∀ s, Measurable (φ s))
131     (h0 : ∀ s x, 0 ≤ φ s x) (h1 : ∀ s x, φ s x ≤ 1) :
132     |drift t (fun s => ∫ x, φ s x ∂P s) (fun s => ∫ x, φ s x ∂Q s)| ≤
133       ∑ s ∈ Finset.range t, lawTV (P s) (Q s) := by
134   unfold drift
135   apply (Finset.abs_sum_le_sum_abs _ _).trans
136   exact Finset.sum_le_sum (fun s _ =>
137     bounded_test_integral_le_tv (P s) (Q s) (φ s) (hφ s) (h0 s) (h1 s))
138 
139 /-- Proposition 68, conditional on the actual simultaneous residual event of Proposition 66. -/
140 theorem sequential_lower_certificate (t : ℕ) (ht : 0 < t)
141     (P Q : ℕ → Measure Ω)
142     [∀ s, IsProbabilityMeasure (P s)] [∀ s, IsProbabilityMeasure (Q s)]
143     (φ : ℕ → Ω → ℝ) (observed : ℕ → ℝ) (boundary : ℝ)
144     (hφ : ∀ s, Measurable (φ s))
145     (h0 : ∀ s x, 0 ≤ φ s x) (h1 : ∀ s x, φ s x ≤ 1)
146     (hevent : |residual t observed (fun s => ∫ x, φ s x ∂Q s) -
147       drift t (fun s => ∫ x, φ s x ∂P s) (fun s => ∫ x, φ s x ∂Q s)| ≤ boundary) :
148     max (|residual t observed (fun s => ∫ x, φ s x ∂Q s)| - boundary) 0 / (t : ℝ) ≤
149       (∑ s ∈ Finset.range t, lawTV (P s) (Q s)) / (t : ℝ) := by
150   have hle := (residual_excess_le_abs_drift _ _ _ hevent).trans
151     (abs_drift_le_tv_sum t P Q φ hφ h0 h1)
152   exact (div_le_div_iff_of_pos_right (Nat.cast_pos.mpr ht)).mpr hle
153 
154 /-- The conditional certificate holds at all times and all registered rules on one event. -/
155 theorem simultaneous_sequential_lower_certificate {J : Type*}
156     (P Q : ℕ → J → Measure Ω)
157     [∀ s j, IsProbabilityMeasure (P s j)] [∀ s j, IsProbabilityMeasure (Q s j)]
158     (φ : ℕ → J → Ω → ℝ) (observed : ℕ → J → ℝ) (boundary : ℕ → J → ℝ)
159     (hφ : ∀ s j, Measurable (φ s j))
160     (h0 : ∀ s j x, 0 ≤ φ s j x) (h1 : ∀ s j x, φ s j x ≤ 1)
161     (hevent : ∀ t, 0 < t → ∀ j,
162       |residual t (fun s => observed s j) (fun s => ∫ x, φ s j x ∂Q s j) -
163       drift t (fun s => ∫ x, φ s j x ∂P s j) (fun s => ∫ x, φ s j x ∂Q s j)| ≤
164         boundary t j) :
165     ∀ t, 0 < t → ∀ j,
166       max (|residual t (fun s => observed s j) (fun s => ∫ x, φ s j x ∂Q s j)| -
167         boundary t j) 0 / (t : ℝ) ≤
168       (∑ s ∈ Finset.range t, lawTV (P s j) (Q s j)) / (t : ℝ) := by
169   intro t ht j
170   exact sequential_lower_certificate t ht (fun s => P s j) (fun s => Q s j)
171     (fun s => φ s j) (fun s => observed s j) (boundary t j)
172     (fun s => hφ s j) (fun s => h0 s j) (fun s => h1 s j) (hevent t ht j)
173 
174 /-- A constant-zero test never crosses, even for laws at maximum TV distance. -/
175 theorem zero_test_misses_disjoint_laws :
176     residual 1 (fun _ => 0)
177       (fun _ => ∫ _x : ℝ, (0 : ℝ) ∂Measure.dirac (1 : ℝ)) = 0 ∧
178       lawTV (Measure.dirac (0 : ℝ)) (Measure.dirac (1 : ℝ)) = 1 := by
179   constructor
180   · simp [residual]
181   · exact lawTV_dirac_eq_one 0 1 (by norm_num)
182 
183 end
184 end Komorebi.LSM.SequentialLowerCertificate

Back to source controls