MeasureTVCalculus.lean

1 import KomorebiLSM.SequentialLowerCertificate
2 import Mathlib.Probability.Kernel.Composition.IntegralCompProd
3 import Mathlib.Probability.Kernel.MeasurableIntegral
4 
5 /-! Actual probability-law total variation: event attainment, test duality,
6 triangle inequality, and contraction under measurable reporting or continuation.
7 -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.MeasureTVCalculus
10 noncomputable section
11 open MeasureTheory Set ProbabilityTheory
12 open scoped ENNReal
13 open SequentialLowerCertificate
14 
15 variable {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
16 
17 /-- A measurable event attains the probability convention of total variation. -/
18 theorem lawTV_event_attained (P Q : Measure X)
19     [IsProbabilityMeasure P] [IsProbabilityMeasure Q] :
20     ∃ s : Set X, MeasurableSet s ∧ P.real s-Q.real s=lawTV P Q := by
21   let v : SignedMeasure X := P.toSignedMeasure-Q.toSignedMeasure
22   let j := v.toJordanDecomposition
23   obtain ⟨s, hs, hp, hn⟩ := j.mutuallySingular
24   have hpu : j.posPart.real sᶜ = j.posPart.real univ := by
25     have h : j.posPart sᶜ = j.posPart univ := by
26       simpa only [hp, zero_add] using (measure_add_measure_compl hs (μ := j.posPart))
27     exact congrArg ENNReal.toReal h
28   have hv0 : v univ=0 := by simp [v]
29   have hj0 : j.posPart.real univ=j.negPart.real univ := by
30     have h := v.apply_eq_posPart_real_sub_negPart_real MeasurableSet.univ
31     change v univ=j.posPart.real univ-j.negPart.real univ at h
32     linarith
33   have hvs : v sᶜ=j.posPart.real univ := by
34     rw [v.apply_eq_posPart_real_sub_negPart_real hs.compl]
35     change j.posPart.real sᶜ-j.negPart.real sᶜ= _
36     rw [hpu]
37     simp only [Measure.real, hn, ENNReal.toReal_zero, sub_zero]
38   refine ⟨sᶜ, hs.compl, ?_⟩
39   have hid : v sᶜ=P.real sᶜ-Q.real sᶜ := by
40     simp [v, hs.compl]
41   have htv : lawTV P Q=j.posPart.real univ := by
42     change (1/2:ℝ)*v.totalVariation.real univ= _
43     rw [SignedMeasure.totalVariation, measureReal_add_apply]
44     change (1/2:ℝ)*(j.posPart.real univ+j.negPart.real univ)= _
45     rw [← hj0]
46     ring
47   linarith
48 
49 /-- Bounds on every actual measurable [0,1] test imply a total variation bound. -/
50 theorem lawTV_le_of_bounded_tests (P Q : Measure X)
51     [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (e : ℝ)
52     (h : ∀ (f : X → ℝ), Measurable f → (∀ x, 0 ≤ f x) → (∀ x, f x ≤ 1) →
53       |(∫ x, f x ∂P)-(∫ x, f x ∂Q)| ≤ e) : lawTV P Q ≤ e := by
54   obtain ⟨s, hs, he⟩ := lawTV_event_attained P Q
55   let f : X → ℝ := s.indicator (fun _ => 1)
56   have hf : Measurable f := measurable_const.indicator hs
57   have hf0 : ∀ x, 0 ≤ f x := fun x => by by_cases hx : x∈s <;> simp [f,hx]
58   have hf1 : ∀ x, f x ≤ 1 := fun x => by by_cases hx : x∈s <;> simp [f,hx]
59   have hb := h f hf hf0 hf1
60   have hi (μ : Measure X) : (∫ x, f x ∂μ)=μ.real s := by
61     simp [f, integral_indicator hs]
62   rw [hi P,hi Q,he,abs_of_nonneg (lawTV_nonneg P Q)] at hb
63   exact hb
64 
65 theorem lawTV_symm (P Q : Measure X)
66     [IsProbabilityMeasure P] [IsProbabilityMeasure Q] : lawTV P Q=lawTV Q P := by
67   unfold lawTV
68   rw [← SignedMeasure.totalVariation_neg, neg_sub]
69 
70 theorem lawTV_triangle (P Q R : Measure X)
71     [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [IsProbabilityMeasure R] :
72     lawTV P R ≤ lawTV P Q+lawTV Q R := by
73   apply lawTV_le_of_bounded_tests
74   intro f hf h0 h1
75   have hp := bounded_test_integral_le_tv P Q f hf h0 h1
76   have hq := bounded_test_integral_le_tv Q R f hf h0 h1
77   exact (abs_sub_le (∫ x, f x ∂P) (∫ x, f x ∂Q) (∫ x, f x ∂R)).trans (add_le_add hp hq)
78 
79 /-- Common measurable reporting cannot increase actual total variation. -/
80 theorem lawTV_map (P Q : Measure X)
81     [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
82     (f : X → Y) (hf : Measurable f) :
83     lawTV (P.map f) (Q.map f) ≤ lawTV P Q := by
84   apply lawTV_le_of_bounded_tests
85   intro g hg h0 h1
86   rw [integral_map hf.aemeasurable hg.aestronglyMeasurable,
87     integral_map hf.aemeasurable hg.aestronglyMeasurable]
88   exact bounded_test_integral_le_tv P Q (fun x => g (f x)) (hg.comp hf)
89     (fun x => h0 (f x)) (fun x => h1 (f x))
90 
91 /-- A common Markov continuation, retaining the starting history, is contractive. -/
92 theorem lawTV_compProd (P Q : Measure X)
93     [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
94     (κ : Kernel X Y) [IsMarkovKernel κ] :
95     lawTV (P ⊗ₘ κ) (Q ⊗ₘ κ) ≤ lawTV P Q := by
96   apply lawTV_le_of_bounded_tests
97   intro f hf h0 h1
98   have hfi (x : X) : Integrable (fun y => f (x,y)) (κ x) :=
99     bounded_test_integrable (κ x) (fun y => f (x,y))
100       (hf.comp (measurable_const.prodMk measurable_id))
101       (fun y => h0 (x,y)) (fun y => h1 (x,y))
102   have hF : Measurable (fun x => ∫ y, f (x,y) ∂κ x) :=
103     hf.stronglyMeasurable.integral_kernel_prod_right'.measurable
104   have hF0 (x : X) : 0 ≤ ∫ y, f (x,y) ∂κ x :=
105     integral_nonneg fun y => h0 (x,y)
106   have hF1 (x : X) : (∫ y, f (x,y) ∂κ x) ≤ 1 := by
107     calc
108       _ ≤ ∫ _ : Y, (1:ℝ) ∂κ x := integral_mono (hfi x) (integrable_const _) (fun y => h1 (x,y))
109       _ = 1 := by simp
110   rw [Measure.integral_compProd (bounded_test_integrable (P ⊗ₘ κ) f hf h0 h1),
111     Measure.integral_compProd (bounded_test_integrable (Q ⊗ₘ κ) f hf h0 h1)]
112   exact bounded_test_integral_le_tv P Q _ hF hF0 hF1
113 
114 end
115 end Komorebi.LSM.MeasureTVCalculus

Back to source controls