ContinuousTVDensity.lean

1 import KomorebiLSM.SequentialLowerCertificate
2 import Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
3 
4 /-! Exact probability-convention total variation for actual measures with a
5 common reference density. The half-integral identity is derived through the
6 variation of the genuine signed-measure difference. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.ContinuousTVDensity
9 open MeasureTheory
10 open scoped ENNReal
11 
12 variable {Ω : Type*} [MeasurableSpace Ω]
13 
14 /-- An actual nonnegative integrable density has its expected signed measure. -/
15 theorem toSignedMeasure_withDensity_real (ν : Measure Ω) (f : Ω → ℝ)
16     [IsFiniteMeasure (ν.withDensity (fun x => ENNReal.ofReal (f x)))]
17     (hf : Integrable f ν) (hf0 : 0 ≤ᵐ[ν] f) :
18     (ν.withDensity (fun x => ENNReal.ofReal (f x))).toSignedMeasure=ν.withDensityᵥ f := by
19   have hfin : (∫⁻ x, ENNReal.ofReal (f x) ∂ν) ≠ ⊤ :=
20     ((hasFiniteIntegral_iff_ofReal hf0).mp hf.hasFiniteIntegral).ne
21   have hreal := withDensityᵥ_toReal hf.aestronglyMeasurable.aemeasurable.ennreal_ofReal hfin
22   refine hreal.symm.trans (WithDensityᵥEq.congr_ae ?_)
23   filter_upwards [hf0] with x hx
24   exact ENNReal.toReal_ofReal hx
25 
26 /-- The exact half absolute-integral formula for actual real density laws. -/
27 theorem lawTV_withDensity_real (ν : Measure Ω) (f g : Ω → ℝ)
28     [IsProbabilityMeasure (ν.withDensity (fun x => ENNReal.ofReal (f x)))]
29     [IsProbabilityMeasure (ν.withDensity (fun x => ENNReal.ofReal (g x)))]
30     (hf : Integrable f ν) (hg : Integrable g ν)
31     (hf0 : 0 ≤ᵐ[ν] f) (hg0 : 0 ≤ᵐ[ν] g) :
32     SequentialLowerCertificate.lawTV
33       (ν.withDensity (fun x => ENNReal.ofReal (f x)))
34       (ν.withDensity (fun x => ENNReal.ofReal (g x)))=
35       (1/2:ℝ) * ∫ x, |f x-g x| ∂ν := by
36   have hdiff : Integrable (fun x => f x-g x) ν := (hf.sub hg).congr (by filter_upwards with x; rfl)
37   rw [SequentialLowerCertificate.lawTV,toSignedMeasure_withDensity_real ν f hf hf0,
38     toSignedMeasure_withDensity_real ν g hg hg0,← withDensityᵥ_sub' hf hg,
39     SignedMeasure.totalVariation_eq_variation,Measure.variation_withDensityᵥ hdiff,
40     Measure.real,withDensity_apply _ MeasurableSet.univ,Measure.restrict_univ,
41     ← integral_norm_eq_lintegral_enorm hdiff.aestronglyMeasurable]
42   simp only [Real.norm_eq_abs]
43 
44 /-- A probability density has finite reference integral, even when the common
45 reference measure itself is infinite. -/
46 theorem density_lintegral_finite (ν : Measure Ω) (f : Ω → ℝ≥0∞)
47     [IsProbabilityMeasure (ν.withDensity f)] : (∫⁻ x, f x ∂ν) ≠ ⊤ := by
48   have he : (∫⁻ x, f x ∂ν)=1 := by
49     rw [← Measure.restrict_univ (μ := ν),← withDensity_apply _ MeasurableSet.univ]
50     exact measure_univ
51   rw [he]
52   exact ENNReal.one_ne_top
53 
54 /-- No real-density integrability premise is needed: finite probability laws
55 derive it from the measurable ENNReal densities. -/
56 theorem lawTV_withDensity_lintegral (ν : Measure Ω) (f g : Ω → ℝ≥0∞)
57     [IsProbabilityMeasure (ν.withDensity f)] [IsProbabilityMeasure (ν.withDensity g)]
58     (hf : AEMeasurable f ν) (hg : AEMeasurable g ν) :
59     SequentialLowerCertificate.lawTV (ν.withDensity f) (ν.withDensity g)=
60       (1/2:ℝ) * (∫⁻ x, ENNReal.ofReal |(f x).toReal-(g x).toReal| ∂ν).toReal := by
61   have hfi := density_lintegral_finite ν f
62   have hgi := density_lintegral_finite ν g
63   have hfr := integrable_toReal_of_lintegral_ne_top hf hfi
64   have hgr := integrable_toReal_of_lintegral_ne_top hg hgi
65   have hdiff : Integrable (fun x => (f x).toReal-(g x).toReal) ν := (hfr.sub hgr).congr (by filter_upwards with x; rfl)
66   rw [SequentialLowerCertificate.lawTV,← withDensityᵥ_toReal hf hfi,
67     ← withDensityᵥ_toReal hg hgi,← withDensityᵥ_sub' hfr hgr,
68     SignedMeasure.totalVariation_eq_variation,Measure.variation_withDensityᵥ hdiff,
69     Measure.real,withDensity_apply _ MeasurableSet.univ,Measure.restrict_univ]
70   simp only [Real.enorm_eq_ofReal_abs]
71 
72 /-- The ENNReal half-integral identity can be compared directly with a
73 nonnegative reference-integral error budget. -/
74 theorem ofReal_lawTV_withDensity_lintegral (ν : Measure Ω) (f g : Ω → ℝ≥0∞)
75     [IsProbabilityMeasure (ν.withDensity f)] [IsProbabilityMeasure (ν.withDensity g)]
76     (hf : AEMeasurable f ν) (hg : AEMeasurable g ν) :
77     ENNReal.ofReal (SequentialLowerCertificate.lawTV (ν.withDensity f) (ν.withDensity g))=
78       (1/2:ℝ≥0∞) * ∫⁻ x, ENNReal.ofReal |(f x).toReal-(g x).toReal| ∂ν := by
79   have hfr := integrable_toReal_of_lintegral_ne_top hf (density_lintegral_finite ν f)
80   have hgr := integrable_toReal_of_lintegral_ne_top hg (density_lintegral_finite ν g)
81   have hdiff : Integrable (fun x => (f x).toReal-(g x).toReal) ν := (hfr.sub hgr).congr (by filter_upwards with x; rfl)
82   have hfin : (∫⁻ x, ENNReal.ofReal |(f x).toReal-(g x).toReal| ∂ν) ≠ ⊤ := by
83     simpa only [← Real.enorm_eq_ofReal_abs] using hdiff.hasFiniteIntegral.ne
84   rw [lawTV_withDensity_lintegral ν f g hf hg,ENNReal.ofReal_mul (by norm_num : (0:ℝ)≤1/2),
85     ENNReal.ofReal_toReal hfin,ENNReal.ofReal_div_of_pos (by norm_num : (0:ℝ)<2)]
86   norm_num
87 
88 end Komorebi.LSM.ContinuousTVDensity

Back to source controls