Physics

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 import KomorebiPhysics.Relativistic3DGeneratorBridge
2 import KomorebiPhysics.Relativistic3DCenteredConvergence
3 import KomorebiPhysics.Relativistic3DModalPerturbation
4 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
5 
6 /-!
7 # Global quadratic spacing estimates for the centered Dirac family
8 
9 The moment in this module is a spatial third-order Fourier moment on the
10 unchanged infinite coefficient space. No finite sampled lattice is substituted.
11 Copyright (c) 2026 Komorebi P. Released under the MIT license.
12 -/
13 
14 noncomputable section
15 set_option autoImplicit false
16 set_option maxHeartbeats 1000000
17 
18 open Filter
19 open scoped ENNReal BigOperators Topology lp LinearPMap
20 
21 namespace KomorebiPhysics
22 namespace Relativistic3DCenteredRates
23 
24 open Relativistic3DFourierGenerator
25 open Relativistic3DFourierHilbertStability
26 open Relativistic3DFullFourierEvolution
27 open Relativistic3DUnboundedDirac
28 open Relativistic3DWeightedDomain
29 open Relativistic3DTorusFourierEvolution
30 open Relativistic3DCenteredConvergence
31 open Relativistic3DModalPerturbation
32 
33 abbrev CoeffL2 := Relativistic3DFullFourierEvolution.CoeffL2
34 abbrev Mode := Relativistic3DFullFourierEvolution.Mode
35 abbrev HilbertSpinor := Relativistic3DFourierHilbertStability.HilbertSpinor
36 
37 /-- The global scalar bound includes the removable zero-spacing value. -/
38 theorem sinQuot_cubic_bound (k h : ℝ) :
39     |sinQuot k h - k| ≤ h ^ 2 / 6 * |k| ^ 3 := by
40   by_cases hh : h = 0
41   · subst h
42     simp
43   have habs : |h| ≠ 0 := abs_ne_zero.mpr hh
44   have he : sinQuot k h - k = (Real.sin (k * h) - k * h) / h := by
45     simp only [sinQuot, Relativistic1DContinuumLimit.sinQuot, hh, ↓reduceIte]
46     field_simp
47   rw [he, abs_div]
48   calc
49     _ ≤ (|k * h| ^ 3 / 6) / |h| := by
50       apply div_le_div_of_nonneg_right _ (abs_nonneg h)
51       simpa only [abs_sub_comm] using Real.abs_sub_sin_le (k * h)
52     _ = h ^ 2 / 6 * |k| ^ 3 := by
53       rw [abs_mul, mul_pow]
54       calc
55         _ = |k| ^ 3 * |h| ^ 2 / 6 := by field_simp
56         _ = h ^ 2 / 6 * |k| ^ 3 := by rw [sq_abs]; ring
57 
58 /-- Squared scalar error in the form needed by the exact Clifford identity. -/
59 theorem sinQuot_cubic_bound_sq (k h : ℝ) :
60     (sinQuot k h - k) ^ 2 ≤ (h ^ 2 / 6) ^ 2 * k ^ 6 := by
61   have hsq := pow_le_pow_left₀ (abs_nonneg (sinQuot k h - k))
62     (sinQuot_cubic_bound k h) 2
63   have hk : (|k| ^ 3) ^ 2 = k ^ 6 := by
64     calc
65       _ = (|k| ^ 2) ^ 3 := by ring
66       _ = (k ^ 2) ^ 3 := by rw [sq_abs]
67       _ = k ^ 6 := by ring
68   simpa only [sq_abs, mul_pow, hk] using hsq
69 
70 /-- Exact homogeneous spatial weight used by the quadratic estimate. -/
71 def thirdOrderWeight (n : Mode) : ℝ :=
72   modeMomentum n 0 ^ 6 + modeMomentum n 1 ^ 6 + modeMomentum n 2 ^ 6
73 
74 theorem thirdOrderWeight_nonneg (n : Mode) : 0 ≤ thirdOrderWeight n := by
75   unfold thirdOrderWeight
76   positivity
77 
78 /-- The summand of the third-order spatial Fourier moment. -/
79 def thirdOrderModeTerm (f : CoeffL2) (n : Mode) : ℝ :=
80   thirdOrderWeight n * ‖f n‖ ^ 2
81 
82 theorem thirdOrderModeTerm_nonneg (f : CoeffL2) (n : Mode) :
83     0 ≤ thirdOrderModeTerm f n :=
84   mul_nonneg (thirdOrderWeight_nonneg n) (sq_nonneg _)
85 
86 /-- Finiteness is expressed by convergence of the actual nonnegative series. -/
87 def HasThirdOrderMoment (f : CoeffL2) : Prop :=
88   Summable (thirdOrderModeTerm f)
89 
90 /-- The exact homogeneous moment M₃, meaningful for the rate under finiteness. -/
91 def thirdOrderMoment (f : CoeffL2) : ℝ :=
92   Real.sqrt (∑' n, thirdOrderModeTerm f n)
93 
94 theorem thirdOrderMoment_nonneg (f : CoeffL2) : 0 ≤ thirdOrderMoment f :=
95   Real.sqrt_nonneg _
96 
97 theorem thirdOrderMoment_sq (f : CoeffL2) :
98     thirdOrderMoment f ^ 2 = ∑' n, thirdOrderModeTerm f n := by
99   exact Real.sq_sqrt (tsum_nonneg (thirdOrderModeTerm_nonneg f))
100 
101 theorem sq_le_one_add_sixth (x : ℝ) : x ^ 2 ≤ 1 + x ^ 6 := by
102   have h := mul_nonneg (sq_nonneg (x ^ 2 - 1)) (show 0 ≤ x ^ 2 + 1 by positivity)
103   nlinarith [sq_nonneg (x ^ 2)]
104 
105 /-- The third-order hypothesis supplies the domain needed to apply H. -/
106 theorem HasThirdOrderMoment.mem_continuumDiracDomain {f : CoeffL2}
107     (hf : HasThirdOrderMoment f) (m : ℝ) : f ∈ continuumDiracDomain m := by
108   rw [mem_continuumDiracDomain_iff_summable_weighted, summable_weighted_iff_momentum]
109   have hs : Summable (fun n => 3 * ‖f n‖ ^ 2 + thirdOrderModeTerm f n) :=
110     ((summable_coeff_norm_sq f).mul_left 3).add hf
111   apply hs.of_nonneg_of_le
112   · intro n
113     unfold momentumModeTerm momentumNormSq
114     positivity
115   · intro n
116     have h0 := sq_le_one_add_sixth (modeMomentum n 0)
117     have h1 := sq_le_one_add_sixth (modeMomentum n 1)
118     have h2 := sq_le_one_add_sixth (modeMomentum n 2)
119     have hw : momentumNormSq n ≤ 3 + thirdOrderWeight n := by
120       unfold momentumNormSq thirdOrderWeight
121       linarith
122     have hb := mul_le_mul_of_nonneg_right hw (sq_nonneg ‖f n‖)
123     simpa only [momentumModeTerm, thirdOrderModeTerm, add_mul] using hb
124 
125 /-- Lift a squared coordinate estimate using the convergent moment series. -/
126 theorem norm_le_thirdOrderMoment {f u : CoeffL2} (hf : HasThirdOrderMoment f)
127     {C : ℝ} (hC : 0 ≤ C)
128     (hb : ∀ n, ‖u n‖ ^ 2 ≤ C ^ 2 * thirdOrderModeTerm f n) :
129     ‖u‖ ≤ C * thirdOrderMoment f := by
130   have hu : Summable (fun n => ‖u n‖ ^ 2) := summable_coeff_norm_sq u
131   have hr : Summable (fun n => C ^ 2 * thirdOrderModeTerm f n) := hf.mul_left _
132   have hs := hu.tsum_le_tsum hb hr
133   have he : ‖u‖ ^ 2 = ∑' n, ‖u n‖ ^ 2 := by
134     simpa using lp.norm_rpow_eq_tsum (by norm_num : 0 < (2 : ENNReal).toReal) u
135   rw [← he, tsum_mul_left, ← thirdOrderMoment_sq] at hs
136   have hp : 0 ≤ C * thirdOrderMoment f := mul_nonneg hC (thirdOrderMoment_nonneg f)
137   exact (sq_le_sq₀ (norm_nonneg u) hp).mp (by simpa only [mul_pow] using hs)
138 
139 /-- The exact Clifford identity retains the three coordinate errors in quadrature. -/
140 theorem centered_mode_quadratic_sq (m h : ℝ) (n : Mode) (ψ : HilbertSpinor) :
141     ‖centralHilbertModeOperator m h n ψ - continuumHilbertModeOperator m n ψ‖ ^ 2 ≤
142       (h ^ 2 / 6) ^ 2 * (thirdOrderWeight n * ‖ψ‖ ^ 2) := by
143   rw [norm_centered_mode_sub_sq]
144   have h0 := sinQuot_cubic_bound_sq (modeMomentum n 0) h
145   have h1 := sinQuot_cubic_bound_sq (modeMomentum n 1) h
146   have h2 := sinQuot_cubic_bound_sq (modeMomentum n 2) h
147   have he :
148       (sinQuot (modeMomentum n 0) h - modeMomentum n 0) ^ 2 +
149       (sinQuot (modeMomentum n 1) h - modeMomentum n 1) ^ 2 +
150       (sinQuot (modeMomentum n 2) h - modeMomentum n 2) ^ 2 ≤
151       (h ^ 2 / 6) ^ 2 * thirdOrderWeight n := by
152     unfold thirdOrderWeight
153     nlinarith
154   simpa only [mul_assoc] using mul_le_mul_of_nonneg_right he (sq_nonneg ‖ψ‖)
155 
156 /-- A uniform modal perturbation envelope, valid at every real spacing. -/
157 theorem centered_mode_quadratic_bound (m h : ℝ) (n : Mode) (ψ : HilbertSpinor) :
158     ‖centralHilbertModeOperator m h n ψ - continuumHilbertModeOperator m n ψ‖ ≤
159       (h ^ 2 / 6 * Real.sqrt (thirdOrderWeight n)) * ‖ψ‖ := by
160   have hs := centered_mode_quadratic_sq m h n ψ
161   have hw := Real.sq_sqrt (thirdOrderWeight_nonneg n)
162   have hp : 0 ≤ h ^ 2 / 6 * Real.sqrt (thirdOrderWeight n) * ‖ψ‖ := by positivity
163   apply (sq_le_sq₀ (norm_nonneg _) hp).mp
164   calc
165     _ ≤ (h ^ 2 / 6) ^ 2 * (thirdOrderWeight n * ‖ψ‖ ^ 2) := hs
166     _ = (h ^ 2 / 6 * Real.sqrt (thirdOrderWeight n) * ‖ψ‖) ^ 2 := by
167       simp only [mul_pow, hw]
168       ring
169 
170 /-- Global O(h²) generator estimate on the actual maximal domain. -/
171 theorem centered_generator_quadratic_bound (m h : ℝ) (hh : h ≠ 0)
172     (f : CoeffL2) (hf : HasThirdOrderMoment f) :
173     ‖centeredCoeffOperator m h f -
174       continuumDiracOutput m ⟨f, hf.mem_continuumDiracDomain m⟩‖ ≤
175       h ^ 2 / 6 * thirdOrderMoment f := by
176   apply norm_le_thirdOrderMoment hf (by positivity)
177   intro n
178   simpa only [lp.coeFn_sub, Pi.sub_apply, centeredCoeffOperator_apply m h hh,
179     continuumDiracOutput_apply, thirdOrderModeTerm] using centered_mode_quadratic_sq m h n (f n)
180 
181 /-- The propagator estimate uses a noncommutative perturbation argument. -/
182 theorem centered_mode_propagator_quadratic_bound (m h t : ℝ) (n : Mode)
183     (ψ : HilbertSpinor) :
184     ‖centralHilbertModePropagator m h n t ψ - continuumHilbertModePropagator m n t ψ‖ ≤
185       |t| * (h ^ 2 / 6 * Real.sqrt (thirdOrderWeight n)) * ‖ψ‖ := by
186   apply modal_perturbation_bound
187     (centralHilbertModeOperator m h n) (continuumHilbertModeOperator m n)
188     (centralHilbertModeOperator_selfAdjoint m h n)
189     (continuumHilbertModeOperator_selfAdjoint m n)
190     (h ^ 2 / 6 * Real.sqrt (thirdOrderWeight n)) (by positivity)
191   intro φ
192   change ‖centralHilbertModeOperator m h n φ - continuumHilbertModeOperator m n φ‖ ≤ _
193   exact centered_mode_quadratic_bound m h n φ
194 
195 /-- The sharp global quadratic propagator estimate for arbitrary signed time. -/
196 theorem centered_propagator_quadratic_bound (m h t : ℝ) (f : CoeffL2)
197     (hf : HasThirdOrderMoment f) :
198     ‖centralCoeffPropagator m h t f - continuumCoeffPropagator m t f‖ ≤
199       (|t| * h ^ 2 / 6) * thirdOrderMoment f := by
200   apply norm_le_thirdOrderMoment hf (by positivity)
201   intro n
202   have hs := pow_le_pow_left₀ (norm_nonneg _)
203     (centered_mode_propagator_quadratic_bound m h t n (f n)) 2
204   have hw := Real.sq_sqrt (thirdOrderWeight_nonneg n)
205   simp only [lp.coeFn_sub, Pi.sub_apply, centralCoeffPropagator_apply,
206     continuumCoeffPropagator_apply]
207   calc
208     _ ≤ (|t| * (h ^ 2 / 6 * Real.sqrt (thirdOrderWeight n)) * ‖f n‖) ^ 2 := hs
209     _ = (|t| * h ^ 2 / 6) ^ 2 * thirdOrderModeTerm f n := by
210       simp only [thirdOrderModeTerm, mul_pow, hw]
211       ring
212 
213 /-- One quadratic envelope works simultaneously on every compact time interval. -/
214 theorem centered_propagator_compactTime_bound (m h T : ℝ) (_hT : 0 ≤ T)
215     (f : CoeffL2) (hf : HasThirdOrderMoment f) :
216     ∀ t ∈ Set.Icc (-T) T,
217       ‖centralCoeffPropagator m h t f - continuumCoeffPropagator m t f‖ ≤
218         (T * h ^ 2 / 6) * thirdOrderMoment f := by
219   intro t ht
220   have habs : |t| ≤ T := abs_le.mpr ht
221   have hM := thirdOrderMoment_nonneg f
222   calc
223     _ ≤ (|t| * h ^ 2 / 6) * thirdOrderMoment f :=
224       centered_propagator_quadratic_bound m h t f hf
225     _ ≤ (T * h ^ 2 / 6) * thirdOrderMoment f := by gcongr
226 
227 /-- Exact Fourier transport of the generator rate to physical torus fields. -/
228 theorem physical_generator_quadratic_bound (m h : ℝ) (hh : h ≠ 0)
229     (φ : Relativistic3DTorusFourierEvolution.TorusSpinorL2)
230     (hφ : HasThirdOrderMoment (torusFourierEquiv φ)) :
231     ‖physicalCenteredOperator m h φ - physicalDiracPMap m
232       ⟨φ, hφ.mem_continuumDiracDomain m⟩‖ ≤
233       h ^ 2 / 6 * thirdOrderMoment (torusFourierEquiv φ) := by
234   rw [← torusFourierEquiv.norm_map
235     (physicalCenteredOperator m h φ - physicalDiracPMap m
236       ⟨φ, hφ.mem_continuumDiracDomain m⟩)]
237   simp only [map_sub, torusFourierEquiv_physicalCenteredOperator_apply,
238     torusFourierEquiv_physicalDiracPMap_apply]
239   change ‖centeredCoeffOperator m h (torusFourierEquiv φ) -
240     continuumDiracOutput m ⟨torusFourierEquiv φ, hφ.mem_continuumDiracDomain m⟩‖ ≤ _
241   exact centered_generator_quadratic_bound m h hh (torusFourierEquiv φ) hφ
242 
243 /-- The same sharp signed-time rate holds in physical torus L². -/
244 theorem physical_propagator_quadratic_bound (m h t : ℝ)
245     (φ : Relativistic3DTorusFourierEvolution.TorusSpinorL2)
246     (hφ : HasThirdOrderMoment (torusFourierEquiv φ)) :
247     ‖centralTorusUnitary m h t φ - continuumTorusUnitary m t φ‖ ≤
248       (|t| * h ^ 2 / 6) * thirdOrderMoment (torusFourierEquiv φ) := by
249   rw [← torusFourierEquiv.norm_map
250     (centralTorusUnitary m h t φ - continuumTorusUnitary m t φ)]
251   simpa only [map_sub, torusFourierEquiv_centralTorusUnitary_apply,
252     torusFourierEquiv_continuumTorusUnitary_apply, centralCoeffUnitary_apply,
253     continuumCoeffUnitary_apply] using
254     centered_propagator_quadratic_bound m h t (torusFourierEquiv φ) hφ
255 
256 /-- Physical compact-time uniform estimate with its nonnegative horizon explicit. -/
257 theorem physical_propagator_compactTime_bound (m h T : ℝ) (_hT : 0 ≤ T)
258     (φ : Relativistic3DTorusFourierEvolution.TorusSpinorL2)
259     (hφ : HasThirdOrderMoment (torusFourierEquiv φ)) :
260     ∀ t ∈ Set.Icc (-T) T,
261       ‖centralTorusUnitary m h t φ - continuumTorusUnitary m t φ‖ ≤
262         (T * h ^ 2 / 6) * thirdOrderMoment (torusFourierEquiv φ) := by
263   intro t ht
264   have habs : |t| ≤ T := abs_le.mpr ht
265   have hM := thirdOrderMoment_nonneg (torusFourierEquiv φ)
266   calc
267     _ ≤ (|t| * h ^ 2 / 6) * thirdOrderMoment (torusFourierEquiv φ) :=
268       physical_propagator_quadratic_bound m h t φ hφ
269     _ ≤ (T * h ^ 2 / 6) * thirdOrderMoment (torusFourierEquiv φ) := by gcongr
270 
271 end Relativistic3DCenteredRates
272 end KomorebiPhysics

Back to source controls

Back to Physics