UniformAbsoluteMoments.lean

1 import KomorebiLSM.UniformIntervalMoments
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.UniformAbsoluteMoments
5 open MeasureTheory
6 open UniformIntervalMoments
7 
8 /-- The actual normalized integral of the absolute observation coordinate. -/
9 theorem integral_abs : (∫ u,|u|∂measure)=(1/2 : ℝ) := by
10   rw [UniformIntervalMoments.integral_eq]
11   have hi (a b : ℝ) : IntervalIntegrable (fun u : ℝ => |u|) volume a b :=
12     continuous_abs.intervalIntegrable a b
13   have hneg : (∫ u in (-1 : ℝ)..0,|u|)=∫ u in (-1 : ℝ)..0,-u := by
14     apply intervalIntegral.integral_congr
15     intro u hu
16     rw [Set.uIcc_of_le (by norm_num : (-1 : ℝ)≤0)] at hu
17     exact abs_of_nonpos hu.2
18   have hpos : (∫ u in (0 : ℝ)..1,|u|)=∫ u in (0 : ℝ)..1,u := by
19     apply intervalIntegral.integral_congr
20     intro u hu
21     rw [Set.uIcc_of_le (by norm_num : (0 : ℝ)≤1)] at hu
22     exact abs_of_nonneg hu.1
23   rw [← intervalIntegral.integral_add_adjacent_intervals (hi (-1) 0) (hi 0 1),hneg,hpos]
24   rw [intervalIntegral.integral_neg]
25   norm_num [integral_id]
26 
27 theorem abs_power_integrable (k : ℕ) : Integrable (fun u : ℝ => |u|^k) measure :=
28   continuous_integrable (continuous_abs.pow k)
29 
30 /-- Exact moments used by the literal degree-two fixture, without signed cancellation. -/
31 theorem integral_abs_power (k : Fin 3) : (∫ u,|u|^(k : ℕ)∂measure)=1/((k : ℕ)+1 : ℝ) := by
32   fin_cases k
33   · norm_num
34   · convert integral_abs using 1 <;> norm_num
35   · have h : (∫ u,u^2∂measure)=(1/3 : ℝ) := by
36       change moment 2=1/3
37       norm_num [moment_formula]
38     simpa only [sq_abs] using h.trans (by norm_num : (1/3 : ℝ)=1/((2 : ℕ)+1 : ℝ))
39 
40 end Komorebi.LSM.UniformAbsoluteMoments

Back to source controls