CellDistance.lean

1 import KomorebiLSM.UniformIntervalMoments
2 import Mathlib.MeasureTheory.Integral.Bochner.Set
3 
4 /-! The exact average separation of two interval-uniform points. The factor
5 one third is derived from the two triangles, rather than supplied as data. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.CellDistance
8 open MeasureTheory intervalIntegral
9 open scoped ENNReal
10 
11 /-- Split the absolute difference at the observation point. -/
12 theorem integral_abs_sub (a b y : ℝ) (hay : a≤y) (hyb : y≤b) :
13     (∫ v in a..b, |y-v|)=((y-a)^2+(b-y)^2)/2 := by
14   have hl : (∫ v in a..y, |y-v|)=(y-a)^2/2 := by
15     calc
16       _ = ∫ v in a..y, y-v := by
17         apply integral_congr
18         intro v hv
19         rw [Set.uIcc_of_le hay] at hv
20         exact abs_of_nonneg (sub_nonneg.mpr hv.2)
21       _ = _ := by
22         rw [intervalIntegral.integral_sub (f := fun v : ℝ => y) (g := fun v : ℝ => v)
23           intervalIntegrable_const (continuous_id.intervalIntegrable a y),
24           intervalIntegral.integral_const,integral_id]
25         simp only [smul_eq_mul]
26         ring
27   have hr : (∫ v in y..b, |y-v|)=(b-y)^2/2 := by
28     calc
29       _ = ∫ v in y..b, v-y := by
30         apply integral_congr
31         intro v hv
32         rw [Set.uIcc_of_le hyb] at hv
33         change |y-v|=v-y
34         rw [abs_of_nonpos (sub_nonpos.mpr hv.1)]
35         ring
36       _ = _ := by
37         rw [intervalIntegral.integral_sub (f := fun v : ℝ => v) (g := fun v : ℝ => y)
38           (continuous_id.intervalIntegrable y b) intervalIntegrable_const,
39           integral_id,intervalIntegral.integral_const]
40         simp only [smul_eq_mul]
41         ring
42   rw [← integral_add_adjacent_intervals (f := fun v : ℝ => |y-v|)
43     ((continuous_const.sub continuous_id).abs.intervalIntegrable a y)
44     ((continuous_const.sub continuous_id).abs.intervalIntegrable y b),hl,hr]
45   ring
46 
47 /-- The unnormalized double-distance integral over the two triangles. -/
48 theorem double_integral_abs_sub (a b : ℝ) (hab : a≤b) :
49     (∫ y in a..b,∫ v in a..b,|y-v|)=(b-a)^3/3 := by
50   have he : (∫ y in a..b,∫ v in a..b,|y-v|)=
51       ∫ y in a..b,((y-a)^2+(b-y)^2)/2 := by
52     apply integral_congr
53     intro y hy
54     rw [Set.uIcc_of_le hab] at hy
55     exact integral_abs_sub a b y hy.1 hy.2
56   rw [he]
57   have hp : (fun y : ℝ => ((y-a)^2+(b-y)^2)/2)=
58       (fun y => y^2-(a+b)*y+(a^2+b^2)/2) := by funext y;ring
59   have hs : IntervalIntegrable (fun y : ℝ => y^2) volume a b :=
60     (continuous_id.pow 2).intervalIntegrable a b
61   have ht : IntervalIntegrable (fun y : ℝ => (a+b)*y) volume a b :=
62     (continuous_const.mul continuous_id).intervalIntegrable a b
63   rw [hp,intervalIntegral.integral_add (hs.sub ht) intervalIntegrable_const,
64     intervalIntegral.integral_sub hs ht,integral_pow,intervalIntegral.integral_const_mul,
65     integral_id,intervalIntegral.integral_const]
66   simp only [smul_eq_mul]
67   ring
68 
69 /-- Two independent uniform points have expected separation width/3. -/
70 theorem uniform_double_distance (a b : ℝ) (hab : a<b) :
71     (∫ y,∫ v,dist y v∂AveragedCongruence.uniformInterval a b
72       ∂AveragedCongruence.uniformInterval a b)=(b-a)/3 := by
73   simp_rw [Real.dist_eq,AveragedCongruence.integral_uniformInterval hab]
74   rw [intervalIntegral.integral_const_mul,double_integral_abs_sub a b hab.le]
75   field_simp [ne_of_gt (sub_pos.mpr hab)]
76 
77 /-- The original uniform reference restricted to an interior cell is exactly
78 half Lebesgue measure on that cell. -/
79 theorem uniform_restrict_cell (a b : ℝ) (ha : -1≤a) (hb : b≤1) :
80     UniformIntervalMoments.measure.restrict (Set.Ioc a b)=
81       (2:ℝ≥0∞)⁻¹ • volume.restrict (Set.Ioc a b) := by
82   have hsub : Set.Ioc a b⊆Set.Ioc (-1 : ℝ) 1 :=
83     fun _ h => ⟨lt_of_le_of_lt ha h.1,le_trans h.2 hb⟩
84   unfold UniformIntervalMoments.measure AveragedCongruence.uniformInterval ProbabilityTheory.cond
85   rw [Measure.restrict_smul,Measure.restrict_restrict_of_subset hsub,Real.volume_Ioc]
86   norm_num
87 
88 theorem uniform_cell_integral (a b : ℝ) (ha : -1≤a) (hb : b≤1) (hab : a≤b)
89     (f : ℝ → ℝ) :
90     (∫ y in Set.Ioc a b,f y∂UniformIntervalMoments.measure)=
91       (1/2:ℝ)*∫ y in a..b,f y := by
92   rw [uniform_restrict_cell a b ha hb,MeasureTheory.integral_smul_measure,
93     ← intervalIntegral.integral_of_le hab]
94   norm_num
95 
96 theorem uniform_cell_mass (a b : ℝ) (ha : -1≤a) (hb : b≤1) (hab : a≤b) :
97     UniformIntervalMoments.measure.real (Set.Ioc a b)=(b-a)/2 := by
98   have h := uniform_cell_integral a b ha hb hab (fun _ => 1)
99   simpa [intervalIntegral.integral_const,smul_eq_mul,div_eq_mul_inv,mul_comm] using h
100 
101 /-- The double cell integral under du/2 is width cubed over twelve. -/
102 theorem uniform_cell_double_distance (a b : ℝ) (ha : -1≤a) (hb : b≤1) (hab : a≤b) :
103     (∫ y in Set.Ioc a b,∫ v in Set.Ioc a b,dist y v∂UniformIntervalMoments.measure
104       ∂UniformIntervalMoments.measure)=(b-a)^3/12 := by
105   rw [uniform_cell_integral a b ha hb hab]
106   simp_rw [uniform_cell_integral a b ha hb hab,Real.dist_eq]
107   rw [intervalIntegral.integral_const_mul,double_integral_abs_sub a b hab]
108   ring
109 
110 end Komorebi.LSM.CellDistance

Back to source controls