KernelTVMeasurable.lean

1 import KomorebiLSM.ContinuousTVDensity
2 import Mathlib.Probability.Kernel.RadonNikodym
3 import Mathlib.Probability.Kernel.MeasurableLIntegral
4 
5 /-! Measurability of actual probability-kernel total variation follows from
6 joint Radon--Nikodym densities against the sum kernel. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.KernelTVMeasurable
9 open MeasureTheory ProbabilityTheory
10 open scoped ENNReal
11 variable {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
12 variable [MeasurableSpace.CountableOrCountablyGenerated X Y]
13 variable (κ η : Kernel X Y) [IsMarkovKernel κ] [IsMarkovKernel η]
14 
15 noncomputable def distance (x : X) : ℝ := SequentialLowerCertificate.lawTV (κ x) (η x)
16 
17 noncomputable def leftDensity (x : X) (y : Y) : ℝ≥0∞ :=
18   ENNReal.ofReal (Kernel.rnDerivAux κ (κ+η) x y)
19 
20 noncomputable def rightDensity (x : X) (y : Y) : ℝ≥0∞ :=
21   ENNReal.ofReal (1-Kernel.rnDerivAux κ (κ+η) x y)
22 
23 omit [IsMarkovKernel κ] [IsMarkovKernel η] in
24 theorem leftDensity_measurable : Measurable (Function.uncurry (leftDensity κ η)) :=
25   (Kernel.measurable_rnDerivAux κ (κ+η)).ennreal_ofReal
26 
27 omit [IsMarkovKernel κ] [IsMarkovKernel η] in
28 theorem rightDensity_measurable : Measurable (Function.uncurry (rightDensity κ η)) :=
29   (measurable_const.sub (Kernel.measurable_rnDerivAux κ (κ+η))).ennreal_ofReal
30 
31 theorem leftDensity_kernel : (κ+η).withDensity (leftDensity κ η)=κ := by
32   change (κ+η).withDensity (fun x y => ENNReal.ofReal (Kernel.rnDerivAux κ (κ+η) x y))=κ
33   simpa only [ENNReal.ofNNReal_toNNReal] using Kernel.withDensity_rnDerivAux κ η
34 
35 theorem rightDensity_kernel : (κ+η).withDensity (rightDensity κ η)=η := by
36   change (κ+η).withDensity (fun x y => ENNReal.ofReal (1-Kernel.rnDerivAux κ (κ+η) x y))=η
37   simpa only [ENNReal.ofNNReal_toNNReal] using Kernel.withDensity_one_sub_rnDerivAux κ η
38 
39 theorem leftDensity_measure (x : X) :
40     ((κ+η) x).withDensity (leftDensity κ η x)=κ x := by
41   rw [← Kernel.withDensity_apply _ (leftDensity_measurable κ η),leftDensity_kernel κ η]
42 
43 theorem rightDensity_measure (x : X) :
44     ((κ+η) x).withDensity (rightDensity κ η x)=η x := by
45   rw [← Kernel.withDensity_apply _ (rightDensity_measurable κ η),rightDensity_kernel κ η]
46 
47 /-- The actual total variation has a jointly measurable reference-integral formula. -/
48 theorem distance_eq_lintegral (x : X) :
49     distance κ η x=(1/2:ℝ)*(∫⁻ y,ENNReal.ofReal
50       |(leftDensity κ η x y).toReal-(rightDensity κ η x y).toReal|∂(κ+η) x).toReal := by
51   have : IsProbabilityMeasure (((κ+η) x).withDensity (leftDensity κ η x)) := by
52     rw [leftDensity_measure κ η x]
53     infer_instance
54   have : IsProbabilityMeasure (((κ+η) x).withDensity (rightDensity κ η x)) := by
55     rw [rightDensity_measure κ η x]
56     infer_instance
57   have h := ContinuousTVDensity.lawTV_withDensity_lintegral ((κ+η) x)
58     (leftDensity κ η x) (rightDensity κ η x)
59     (leftDensity_measurable κ η).of_uncurry_left.aemeasurable
60     (rightDensity_measurable κ η).of_uncurry_left.aemeasurable
61   simpa only [leftDensity_measure κ η x,rightDensity_measure κ η x,distance] using h
62 
63 theorem distance_measurable : Measurable (distance κ η) := by
64   have hd : Measurable (fun p : X × Y =>
65       (leftDensity κ η p.1 p.2).toReal-(rightDensity κ η p.1 p.2).toReal) :=
66     (leftDensity_measurable κ η).ennreal_toReal.sub (rightDensity_measurable κ η).ennreal_toReal
67   have hm : Measurable (fun p : X × Y => ENNReal.ofReal
68       |(leftDensity κ η p.1 p.2).toReal-(rightDensity κ η p.1 p.2).toReal|) := by
69     simpa only [Function.comp_apply,Real.norm_eq_abs] using (measurable_norm.comp hd).ennreal_ofReal
70   have he : distance κ η=(fun x => (1/2:ℝ)*(∫⁻ y,ENNReal.ofReal
71       |(leftDensity κ η x y).toReal-(rightDensity κ η x y).toReal|∂(κ+η) x).toReal) :=
72     funext (distance_eq_lintegral κ η)
73   rw [he]
74   exact measurable_const.mul (hm.lintegral_kernel_prod_right' (κ := κ+η)).ennreal_toReal
75 
76 omit [MeasurableSpace.CountableOrCountablyGenerated X Y] in
77 theorem distance_nonneg (x : X) : 0≤distance κ η x :=
78   SequentialLowerCertificate.lawTV_nonneg _ _
79 
80 omit [MeasurableSpace.CountableOrCountablyGenerated X Y] in
81 theorem distance_le_one (x : X) : distance κ η x≤1 :=
82   SequentialLowerCertificate.lawTV_le_one _ _
83 
84 theorem distance_integrable (ρ : Measure X) [IsFiniteMeasure ρ] :
85     Integrable (distance κ η) ρ := by
86   apply Integrable.of_bound (distance_measurable κ η).aestronglyMeasurable 1
87   filter_upwards [] with x
88   simpa only [Real.norm_eq_abs,abs_of_nonneg (distance_nonneg κ η x)] using distance_le_one κ η x
89 
90 end Komorebi.LSM.KernelTVMeasurable

Back to source controls