CurvedMomentInstrument.lean

1 import KomorebiLSM.CurvedMomentGeometry
2 import KomorebiLSM.ContinuousInstrument
3 import KomorebiLSM.ContinuousRecords
4 import Mathlib.MeasureTheory.Integral.IntegrableOn
5 import Mathlib.Tactic
6 
7 /-! The literal two-parameter rank-one density and general four-moment reference. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.CurvedMoment
10 open MeasureTheory ProbabilityTheory
11 open scoped BigOperators
12 noncomputable section
13 
14 def legendre (u : ℝ) : ℝ := (3*u^2-1)/2
15 
16 def likelihood (a b u : ℝ) (z : State) : ℝ := z 0+a*u*z 1+b*legendre u*z 2
17 
18 def row (a b u : ℝ) : State →L[ℝ] ℝ :=
19   (LinearMap.proj 0 : State →ₗ[ℝ] ℝ).toContinuousLinearMap +
20   (a*u) • (LinearMap.proj 1 : State →ₗ[ℝ] ℝ).toContinuousLinearMap +
21   (b*legendre u) • (LinearMap.proj 2 : State →ₗ[ℝ] ℝ).toContinuousLinearMap
22 
23 def branch (a b u : ℝ) : State →L[ℝ] State := (row a b u).smulRight (curve u)
24 
25 @[simp] theorem branch_apply (a b u : ℝ) (z : State) :
26     branch a b u z=likelihood a b u z • curve u := rfl
27 
28 @[simp] theorem branch_mass (a b u : ℝ) (z : State) :
29     mass (branch a b u z)=likelihood a b u z := by
30   rw [branch_apply,map_smul]
31   simp [mass,curve]
32 
33 theorem branch_continuous (a b : ℝ) : Continuous (branch a b) := by
34   unfold branch row legendre curve
35   fun_prop
36 
37 theorem legendre_abs (u : ℝ) (hu : u∈Set.Icc (-1:ℝ) 1) : |legendre u|≤1 := by
38   apply abs_le.mpr
39   dsimp [legendre]
40   constructor <;> nlinarith [sq_nonneg u,hu.1,hu.2]
41 
42 theorem likelihood_lower (a b ρ u : ℝ) (_hρ : 0≤ρ)
43     (hab : |a|+|b|≤1-ρ) (hu : u∈Set.Icc (-1:ℝ) 1)
44     {z : State} (hz : z∈normalized) : ρ≤likelihood a b u z := by
45   have hb := normalized_bounds hz
46   have hx : |u|≤1 := abs_le.mpr hu
47   have hax : |a*u*z 1|≤|a| := by
48     rw [abs_mul,abs_mul]
49     calc
50       |a| * |u| * |z 1|≤|a| * 1 * 1 := mul_le_mul (mul_le_mul_of_nonneg_left hx (abs_nonneg _)) hb.1 (abs_nonneg _) (by positivity)
51       _=|a| := by ring
52   have hby : |b*legendre u*z 2|≤|b| := by
53     rw [abs_mul,abs_mul,abs_of_nonneg hb.2.1]
54     calc
55       |b| * |legendre u| * z 2≤|b| * 1 * 1 := mul_le_mul (mul_le_mul_of_nonneg_left (legendre_abs u hu) (abs_nonneg _)) hb.2.2 hb.2.1 (by positivity)
56       _=|b| := by ring
57   dsimp [likelihood]
58   rw [hz.1]
59   linarith [neg_abs_le (a*u*z 1),neg_abs_le (b*legendre u*z 2)]
60 
61 theorem branch_positive (a b ρ u : ℝ) (hρ : 0≤ρ)
62     (hab : |a|+|b|≤1-ρ) (hu : u∈Set.Icc (-1:ℝ) 1)
63     {z : State} (hz : z∈cone) : branch a b u z∈cone := by
64   by_cases hm : z 0=0
65   · rw [cone_mass_zero hz hm,map_zero]
66     exact cone_zero
67   · have hp : 0<z 0 := probabilityCone.mass_pos hz (fun he => hm (by simp [he]))
68     have hs : (z 0)⁻¹•z∈probabilityCone.base := by
69       refine ⟨cone_smul (inv_nonneg.mpr hp.le) hz,?_⟩
70       change (z 0)⁻¹*z 0=1
71       exact inv_mul_cancel₀ hm
72     have hl := likelihood_lower a b ρ u hρ hab hu (by rw [←base_eq_normalized];exact hs)
73     have ho : branch a b u ((z 0)⁻¹•z)∈cone := by
74       rw [branch_apply]
75       exact cone_smul (hρ.trans hl) (curve_mem u hu)
76     have he : z=z 0•((z 0)⁻¹•z) := by rw [smul_smul,mul_inv_cancel₀ hm,one_smul]
77     rw [he,map_smul]
78     exact cone_smul hp.le ho
79 
80 theorem posterior_curve (a b u : ℝ) (z : State) (hp : 0<likelihood a b u z) :
81     (mass (branch a b u z))⁻¹ • branch a b u z=curve u := by
82   rw [branch_mass,branch_apply,smul_smul,inv_mul_cancel₀ hp.ne',one_smul]
83 
84 /-- The measure need not be Lebesgue or discrete; its support and four moments are explicit. -/
85 structure Reference (μ : Measure ℝ) where
86   probability : IsProbabilityMeasure μ
87   support : ∀ᵐ u∂μ,u∈Set.Icc (-1:ℝ) 1
88   first : (∫ u,u∂μ)=0
89   second : (∫ u,u^2∂μ)=1/3
90   third : (∫ u,u^3∂μ)=0
91   fourth : (∫ u,u^4∂μ)=1/5
92 
93 namespace Reference
94 variable {μ : Measure ℝ} (R : Reference μ)
95 include R
96 
97 theorem continuous_integrable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
98     {f : ℝ→F} (hf : Continuous f) : Integrable f μ := by
99   let := R.probability
100   have he : μ.restrict (Set.Icc (-1:ℝ) 1)=μ := Measure.restrict_eq_self_of_ae_mem R.support
101   have hi : IntegrableOn f (Set.Icc (-1:ℝ) 1) μ := hf.continuousOn.integrableOn_compact isCompact_Icc
102   simpa only [IntegrableOn,he] using hi
103 
104 theorem integral_legendre : (∫ u,legendre u∂μ)=0 := by
105   let := R.probability
106   have hi := R.continuous_integrable (f:=fun u : ℝ => u^2) (by fun_prop)
107   simp only [legendre,div_eq_mul_inv]
108   rw [integral_mul_const,integral_sub (hi.const_mul _) (integrable_const _),integral_const_mul,R.second]
109   norm_num
110 
111 theorem integral_likelihood (a b : ℝ) (z : State) :
112     (∫ u,likelihood a b u z∂μ)=mass z := by
113   let := R.probability
114   have h1 := R.continuous_integrable (f:=fun u : ℝ => u) continuous_id
115   have hL := R.continuous_integrable (f:=legendre) (by unfold legendre; fun_prop)
116   have hi1 : Integrable (fun u => z 0+a*u*z 1) μ := (integrable_const _).add ((h1.const_mul a).mul_const (z 1))
117   have hi2 : Integrable (fun u => b*legendre u*z 2) μ := (hL.const_mul b).mul_const (z 2)
118   simp only [likelihood]
119   rw [integral_add hi1 hi2,
120     integral_add (integrable_const _) ((h1.const_mul _).mul_const _),
121     integral_mul_const,integral_const_mul,R.first,integral_mul_const,integral_const_mul,R.integral_legendre]
122   simp
123 
124 /-- Genuine operator-valued instrument on the full proper moment cone. -/
125 def instrument (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) :
126     ContinuousInstrument.DensityInstrument (A:=Unit) probabilityCone μ where
127   op _ := branch a b
128   measurable_op _ := (branch_continuous a b).measurable
129   integrable_op _ := R.continuous_integrable (branch_continuous a b)
130   positive _ := R.support.mono (fun u hu z hz => branch_positive a b ρ u hρ hab hu hz)
131   mass_preserving _ z := by
132     change mass ((∫ u,branch a b u∂μ) z)=mass z
133     rw [ContinuousLinearMap.integral_apply (R.continuous_integrable (branch_continuous a b))]
134     change ContinuousInstrument.massCLM probabilityCone (∫ u,branch a b u z∂μ)=mass z
135     calc
136       ContinuousInstrument.massCLM probabilityCone (∫ u,branch a b u z∂μ) =
137           ∫ u,ContinuousInstrument.massCLM probabilityCone (branch a b u z)∂μ :=
138         ((ContinuousInstrument.massCLM probabilityCone).integral_comp_comm
139           ((ContinuousLinearMap.apply ℝ State z).integrable_comp
140             (R.continuous_integrable (branch_continuous a b)))).symm
141       _ = mass z := by
142         change (∫ u,mass (branch a b u z)∂μ)=mass z
143         simp_rw [branch_mass]
144         exact R.integral_likelihood a b z
145 
146 end Reference
147 end
148 end Komorebi.LSM.CurvedMoment

Back to source controls