CurvedMomentReferences.lean

1 import KomorebiLSM.CurvedMomentTV
2 import KomorebiLSM.PolynomialGram
3 import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
4 import Mathlib.Tactic
5 
6 /-! Actual five-node and normalized Lebesgue references, with exact absolute
7 moments. The finite experiment and continuous experiment remain distinct. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.CurvedMoment
10 open MeasureTheory
11 open scoped BigOperators ENNReal
12 noncomputable section
13 
14 namespace FiveNode
15 
16 def node : Fin 5 → ℝ := ![-1,-1/2,0,1/2,1]
17 def weight : Fin 5 → ℝ≥0∞ := ![7/90,16/45,2/15,16/45,7/90]
18 def measure : Measure ℝ := ∑ i : Fin 5, weight i • Measure.dirac (node i)
19 
20 theorem weight_ne_top (i : Fin 5) : weight i≠∞ := by
21   fin_cases i <;> dsimp [weight] <;>
22     exact ENNReal.div_ne_top (by norm_num) (by norm_num)
23 
24 instance measure_probability : IsProbabilityMeasure measure := by
25   constructor
26   apply (ENNReal.toReal_eq_one_iff _).mp
27   have he : measure Set.univ=∑ i : Fin 5,weight i := by
28     simp [measure]
29   rw [he,ENNReal.toReal_sum (fun i _ => weight_ne_top i)]
30   norm_num [Fin.sum_univ_succ,weight]
31 
32 theorem integral_eq (f : ℝ → ℝ) :
33     (∫ u,f u∂measure)=∑ i : Fin 5,(weight i).toReal*f (node i) := by
34   rw [measure,integral_finsetSum_measure]
35   · simp only [integral_smul_measure,integral_dirac,smul_eq_mul]
36   · intro i _
37     exact (integrable_dirac (f:=f) (by simp)).smul_measure (weight_ne_top i)
38 
39 theorem support : ∀ᵐ u∂measure,u∈Set.Icc (-1:ℝ) 1 := by
40   rw [measure,ae_finsetSum_measure_iff]
41   intro i _
42   apply Measure.ae_smul_measure
43   apply (ae_dirac_iff (p := fun x : ℝ => x∈Set.Icc (-1:ℝ) 1) measurableSet_Icc).mpr
44   fin_cases i <;> norm_num [node]
45 
46 theorem reference : Reference measure := by
47   refine ⟨measure_probability,support,?_,?_,?_,?_⟩ <;>
48     norm_num [integral_eq,weight,node,Fin.sum_univ_succ]
49 
50 theorem absoluteFirst_eq : reference.absoluteFirst=23/45 := by
51   norm_num [Reference.absoluteFirst,integral_eq,weight,node,Fin.sum_univ_succ]
52 
53 theorem absoluteLegendre_eq : reference.absoluteLegendre=14/45 := by
54   norm_num [Reference.absoluteLegendre,integral_eq,weight,node,Fin.sum_univ_succ,legendre]
55 
56 theorem parameterBudget_eq (da db : ℝ) :
57     reference.parameterBudget da db=(23*da+14*db)/90 := by
58   rw [Reference.parameterBudget,absoluteFirst_eq,absoluteLegendre_eq]
59   ring
60 
61 theorem final_rectangle_budget : reference.parameterBudget (53/1000) (87/1000)=2437/90000 := by
62   rw [parameterBudget_eq]
63   norm_num
64 
65 end FiveNode
66 
67 namespace Uniform
68 
69 theorem reference : Reference UniformIntervalMoments.measure where
70   probability := UniformIntervalMoments.measure_isProbability
71   support := PolynomialGram.uniform_ae_interval
72   first := by simpa [UniformIntervalMoments.moment] using UniformIntervalMoments.moment_one
73   second := UniformIntervalMoments.moment_two
74   third := by
75     change UniformIntervalMoments.moment 3=0
76     norm_num [UniformIntervalMoments.moment_formula]
77   fourth := by
78     change UniformIntervalMoments.moment 4=1/5
79     norm_num [UniformIntervalMoments.moment_formula]
80 
81 theorem absoluteFirst_eq : reference.absoluteFirst=1/2 := by
82   rw [Reference.absoluteFirst,UniformIntervalMoments.integral_eq]
83   have hsplit := intervalIntegral.integral_add_adjacent_intervals (μ:=volume)
84     (continuous_abs.intervalIntegrable (-1) 0) (continuous_abs.intervalIntegrable 0 1)
85   have hn : (∫ u : ℝ in (-1)..0,|u|)=∫ u : ℝ in (-1)..0,-u := by
86     apply intervalIntegral.integral_congr
87     intro u hu
88     rw [Set.uIcc_of_le (by norm_num : (-1:ℝ)≤0)] at hu
89     exact abs_of_nonpos hu.2
90   have hp : (∫ u : ℝ in 0..1,|u|)=∫ u : ℝ in 0..1,u := by
91     apply intervalIntegral.integral_congr
92     intro u hu
93     rw [Set.uIcc_of_le (by norm_num : (0:ℝ)≤1)] at hu
94     exact abs_of_nonneg hu.1
95   rw [← hsplit,hn,hp,intervalIntegral.integral_neg]
96   norm_num
97 
98 private theorem integral_legendre (a b : ℝ) :
99     (∫ u in a..b,legendre u)=((b^3-b)-(a^3-a))/2 := by
100   have hp : IntervalIntegrable (fun u : ℝ => 3*u^2) volume a b :=
101     (show Continuous (fun u : ℝ => 3*u^2) by fun_prop).intervalIntegrable a b
102   have hc : IntervalIntegrable (fun _ : ℝ => (1:ℝ)) volume a b :=
103     continuous_const.intervalIntegrable a b
104   simp only [legendre]
105   rw [intervalIntegral.integral_div,intervalIntegral.integral_sub hp hc,
106     intervalIntegral.integral_const_mul]
107   norm_num
108   ring
109 
110 theorem absoluteLegendre_eq : reference.absoluteLegendre=2/(3*Real.sqrt 3) := by
111   let q : ℝ := 1/Real.sqrt 3
112   have hs : 0<Real.sqrt 3 := Real.sqrt_pos.2 (by norm_num)
113   have hs2 : (Real.sqrt 3)^2=3 := Real.sq_sqrt (by norm_num)
114   have hq : 0<q := by dsimp [q];positivity
115   have hq2 : q^2=1/3 := by dsimp [q];rw [div_pow,hs2];norm_num
116   have hq1 : q≤1 := by nlinarith
117   have hq3 : q^3=q/3 := by rw [pow_succ,hq2];ring
118   have hneg : (∫ u in (-1:ℝ)..(-q),|legendre u|)=∫ u in (-1:ℝ)..(-q),legendre u := by
119     apply intervalIntegral.integral_congr
120     intro u hu
121     rw [Set.uIcc_of_le (by linarith : (-1:ℝ)≤-q)] at hu
122     apply abs_of_nonneg
123     dsimp [legendre]
124     have : q^2≤u^2 := by nlinarith [sq_nonneg (u+q),hu.2]
125     nlinarith
126   have hmid : (∫ u in (-q)..q,|legendre u|)=∫ u in (-q)..q,-legendre u := by
127     apply intervalIntegral.integral_congr
128     intro u hu
129     rw [Set.uIcc_of_le (by linarith : -q≤q)] at hu
130     apply abs_of_nonpos
131     dsimp [legendre]
132     have : u^2≤q^2 := by nlinarith [mul_nonneg (by linarith [hu.2] : 0≤q-u) (by linarith [hu.1] : 0≤q+u)]
133     nlinarith
134   have hpos : (∫ u in q..(1:ℝ),|legendre u|)=∫ u in q..(1:ℝ),legendre u := by
135     apply intervalIntegral.integral_congr
136     intro u hu
137     rw [Set.uIcc_of_le hq1] at hu
138     apply abs_of_nonneg
139     dsimp [legendre]
140     have : q^2≤u^2 := by nlinarith [sq_nonneg (u-q),hu.1]
141     nlinarith
142   have hc : Continuous (fun u => |legendre u|) := by unfold legendre;fun_prop
143   have hleft := intervalIntegral.integral_add_adjacent_intervals (μ:=volume)
144     (hc.intervalIntegrable (-1) (-q)) (hc.intervalIntegrable (-q) q)
145   have hright := intervalIntegral.integral_add_adjacent_intervals (μ:=volume)
146     (hc.intervalIntegrable (-1) q) (hc.intervalIntegrable q 1)
147   rw [Reference.absoluteLegendre,UniformIntervalMoments.integral_eq,← hright,← hleft,
148     hneg,hmid,hpos,intervalIntegral.integral_neg,integral_legendre,integral_legendre,integral_legendre]
149   rw [show (-q)^3= -(q^3) by ring]
150   norm_num
151   rw [hq3]
152   dsimp [q]
153   field_simp
154   ring
155 
156 end Uniform
157 
158 end
159 end Komorebi.LSM.CurvedMoment

Back to source controls