CurvedMomentTV.lean

1 import KomorebiLSM.CurvedMomentMarkov
2 import KomorebiLSM.ContinuousTVDensity
3 import KomorebiLSM.KernelTVMeasurable
4 import Mathlib.Tactic
5 
6 /-! Exact parameter-to-law bounds for the literal curved-moment instrument. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.CurvedMoment
9 open MeasureTheory ProbabilityTheory
10 noncomputable section
11 
12 namespace Reference
13 variable {μ : Measure ℝ} (R : Reference μ)
14 
15 def absoluteFirst (_R : Reference μ) : ℝ := ∫ u, |u| ∂μ
16 
17 def absoluteLegendre (_R : Reference μ) : ℝ := ∫ u, |legendre u| ∂μ
18 
19 def parameterBudget (da db : ℝ) : ℝ :=
20   (R.absoluteFirst * da + R.absoluteLegendre * db) / 2
21 
22 theorem absoluteFirst_nonneg : 0 ≤ R.absoluteFirst := integral_nonneg (fun _ => abs_nonneg _)
23 
24 theorem absoluteLegendre_nonneg : 0 ≤ R.absoluteLegendre := integral_nonneg (fun _ => abs_nonneg _)
25 
26 theorem parameterBudget_nonneg {da db : ℝ} (ha : 0 ≤ da) (hb : 0 ≤ db) :
27     0 ≤ R.parameterBudget da db := by
28   exact div_nonneg (add_nonneg (mul_nonneg R.absoluteFirst_nonneg ha)
29     (mul_nonneg R.absoluteLegendre_nonneg hb)) (by norm_num)
30 
31 theorem likelihood_difference_le (a b a' b' da db u : ℝ)
32     (ha : |a-a'| ≤ da) (hb : |b-b'| ≤ db) {z : State} (hz : z ∈ normalized) :
33     |likelihood a b u z-likelihood a' b' u z| ≤ da*|u|+db*|legendre u| := by
34   have hbounds := normalized_bounds hz
35   have he : likelihood a b u z-likelihood a' b' u z =
36       (a-a')*u*z 1+(b-b')*legendre u*z 2 := by unfold likelihood;ring
37   rw [he]
38   calc
39     |(a-a')*u*z 1+(b-b')*legendre u*z 2| ≤
40         |(a-a')*u*z 1|+|(b-b')*legendre u*z 2| := abs_add_le _ _
41     _ ≤ da*|u|+db*|legendre u| := by
42       simp only [abs_mul]
43       apply add_le_add
44       · calc
45           |a-a'| * |u| * |z 1| ≤ da*|u| * 1 :=
46             mul_le_mul (mul_le_mul_of_nonneg_right ha (abs_nonneg _)) hbounds.1
47               (abs_nonneg _) (mul_nonneg (le_trans (abs_nonneg _) ha) (abs_nonneg _))
48           _ = da*|u| := by ring
49       · calc
50           |b-b'| * |legendre u| * |z 2| ≤ db*|legendre u| * 1 :=
51             mul_le_mul (mul_le_mul_of_nonneg_right hb (abs_nonneg _))
52               (by simpa [abs_of_nonneg hbounds.2.1] using hbounds.2.2)
53               (abs_nonneg _) (mul_nonneg (le_trans (abs_nonneg _) hb) (abs_nonneg _))
54           _ = db*|legendre u| := by ring
55 
56 /-- The half-L1 identity is for the actual normalized kernel measures. -/
57 theorem observation_lawTV_le [IsProbabilityMeasure μ] (a b ρ a' b' ρ' da db : ℝ)
58     (hρ : 0 ≤ ρ) (hab : |a|+|b| ≤ 1-ρ)
59     (hρ' : 0 ≤ ρ') (hab' : |a'|+|b'| ≤ 1-ρ')
60     (ha : |a-a'| ≤ da) (hb : |b-b'| ≤ db)
61     (z : ContinuousInstrument.DensityInstrument.State probabilityCone) :
62     SequentialLowerCertificate.lawTV
63       ((R.instrument a b ρ hρ hab).kernel () z)
64       ((R.instrument a' b' ρ' hρ' hab').kernel () z) ≤ R.parameterBudget da db := by
65   let := R.probability
66   let D := R.instrument a b ρ hρ hab
67   let D' := R.instrument a' b' ρ' hρ' hab'
68   have hz : z.1 ∈ normalized := by rw [← base_eq_normalized];exact z.2
69   have hf : Integrable (fun u => likelihood a b u z.1) μ := R.continuous_integrable (by unfold likelihood legendre;fun_prop)
70   have hg : Integrable (fun u => likelihood a' b' u z.1) μ := R.continuous_integrable (by unfold likelihood legendre;fun_prop)
71   have hfm : D.kernel () z=μ.withDensity (fun u => ENNReal.ofReal (likelihood a b u z.1)) := by
72     rw [D.kernel_apply]
73     congr 1
74     funext u
75     congr 1
76     exact R.instrument_density a b ρ u hρ hab z.1
77   have hgm : D'.kernel () z=μ.withDensity (fun u => ENNReal.ofReal (likelihood a' b' u z.1)) := by
78     rw [D'.kernel_apply]
79     congr 1
80     funext u
81     congr 1
82     exact R.instrument_density a' b' ρ' u hρ' hab' z.1
83   have : IsProbabilityMeasure (μ.withDensity (fun u => ENNReal.ofReal (likelihood a b u z.1))) := by rw [← hfm];infer_instance
84   have : IsProbabilityMeasure (μ.withDensity (fun u => ENNReal.ofReal (likelihood a' b' u z.1))) := by rw [← hgm];infer_instance
85   change SequentialLowerCertificate.lawTV (D.kernel () z) (D'.kernel () z) ≤ _
86   have htv := ContinuousTVDensity.lawTV_withDensity_real μ _ _ hf hg
87     (R.support.mono (fun u hu => hρ.trans (likelihood_lower a b ρ u hρ hab hu hz)))
88     (R.support.mono (fun u hu => hρ'.trans (likelihood_lower a' b' ρ' u hρ' hab' hu hz)))
89   simp only [←hfm,←hgm] at htv
90   rw [htv]
91   have hiu : Integrable (fun u : ℝ => |u|) μ := R.continuous_integrable continuous_abs
92   have hiL : Integrable (fun u => |legendre u|) μ := R.continuous_integrable (by unfold legendre;fun_prop)
93   have hle : (∫ u, |likelihood a b u z.1-likelihood a' b' u z.1| ∂μ) ≤
94       ∫ u, da*|u|+db*|legendre u| ∂μ :=
95     integral_mono_ae (hf.sub hg).abs ((hiu.const_mul da).add (hiL.const_mul db))
96       (Filter.Eventually.of_forall (fun u => likelihood_difference_le a b a' b' da db u ha hb hz))
97   rw [integral_add (hiu.const_mul da) (hiL.const_mul db),integral_const_mul,integral_const_mul] at hle
98   unfold parameterBudget absoluteFirst absoluteLegendre
99   nlinarith
100 
101 theorem signalKernel_lawTV_le (a b ρ a' b' ρ' da db : ℝ)
102     (hρ : 0 ≤ ρ) (hab : |a|+|b| ≤ 1-ρ)
103     (hρ' : 0 ≤ ρ') (hab' : |a'|+|b'| ≤ 1-ρ')
104     (ha : |a-a'| ≤ da) (hb : |b-b'| ≤ db) (s : Signal) :
105     SequentialLowerCertificate.lawTV (R.signalKernel a b ρ hρ hab s)
106       (R.signalKernel a' b' ρ' hρ' hab' s) ≤ R.parameterBudget da db := by
107   let := R.probability
108   exact R.observation_lawTV_le a b ρ a' b' ρ' da db hρ hab hρ' hab' ha hb (curveState s)
109 
110 end Reference
111 end
112 end Komorebi.LSM.CurvedMoment

Back to source controls