Fock · section of the QIQT-H book

QIQTH.Fock.SchwartzDecay

← all sections · ← OneParticleBW · WedgeAnalyticity →

Fock · entries 320–325 of 1000

Definition 320 (minkBilin).  source ↗

The continuous bilinear Minkowski pairing rescaled by 1/(2π): L v w = (v₀ w₀ − v₁ w₁) / (2π). Writing the bespoke minkowskiFourier as a VectorFourier.fourierIntegral for this L lets us borrow Mathlib’s Fourier-decay machinery.

η  :=  (1/(2⋅π))⋅((proj 0).smulRight (proj 0)−(proj 1).smulRight (proj 1))\eta \;:=\; (1 / (2 \cdot \pi)) \cdot ((\mathrm{proj}\,0).\mathrm{smulRight}\,(\mathrm{proj}\,0) - (\mathrm{proj}\,1).\mathrm{smulRight}\,(\mathrm{proj}\,1))

Used by minkBilin_apply, minkowskiFourier_eq_fourierIntegral, schwartz_Krep_memLp, schwartz_Krep_decay_sq.

Lemma 321 (minkBilin_apply).  source ↗

(η v) w=(v 0⋅w 0−v 1⋅w 1)/(2⋅π)(\href{/browser/qiqth-fock-schwartzdecay#d-qiqth-fock-localization-minkbilin}{\eta}\,v)\,w = (v\,0 \cdot w\,0 - v\,1 \cdot w\,1) / (2 \cdot \pi)

Proof. Immediate from the definitions. □\square

Used by minkowskiFourier_eq_fourierIntegral, schwartz_Krep_memLp, schwartz_Krep_decay_sq.

Lemma 322 (minkowskiFourier_eq_fourierIntegral).  source ↗

Bridge: the bespoke Minkowski-Fourier transform IS a VectorFourier.fourierIntegral for the bilinear form minkBilin (with the standard 2π Fourier character). This is what lets us import Mathlib’s decay estimates.

F f p=F e vol η.toLinearMap12 f p\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskifourier}{\mathcal{F}}\,f\,p = \mathcal{F}\,\mathrm{e}\,\mathrm{vol}\,\href{/browser/qiqth-fock-schwartzdecay#d-qiqth-fock-localization-minkbilin}{\eta}.\mathrm{toLinearMap}_{12}\,f\,p

Proof. By minkowskiDot, minkBilin_apply. □\square

Used by schwartz_Krep_memLp, schwartz_Krep_decay_sq.

Lemma 323 (abs_sinh_le_cosh).  source ↗

|sinh θ| ≤ cosh θ.

∣sinh⁡ θ∣≤cosh⁡ θ|\sinh\,\theta| \le \cosh\,\theta

Proof. Immediate from the definitions. □\square

Used by schwartz_Krep_memLp, schwartz_Krep_decay_sq.

Lemma 324 (schwartz_Krep_memLp).  source ↗

General Schwartz 1/cosh decay of the localized amplitude. For any Schwartz f and m ≠ 0, ‖Krep m f θ‖ ≤ C · (cosh θ)⁻¹ with C = 4πS / (√2·|m|), where S = ∫‖f‖ + ∫‖D f‖ is a finite Schwartz constant. Hence Krep m f ∈ L²(ℝ).

m≠0→MemLp (K m f) 2 volm \ne 0 \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol}

Proof. By massShell, minkowskiFourier, Krep_memLp_of_decay, minkBilin, minkBilin_apply, minkowskiFourier_eq_fourierIntegral, abs_sinh_le_cosh. □\square

Used by fourierL2_Krep_ne_zero.

Lemma 325 (schwartz_Krep_decay_sq).  source ↗

General Schwartz 1/cosh² decay of the localized amplitude (one derivative more than schwartz_Krep_memLp). For any Schwartz f and m ≠ 0, ‖Krep m f θ‖ ≤ 16π²·S₂/(√2·m²) · (cosh θ)⁻² with S₂ = ∫‖f‖ + ∫‖Df‖ + ∫‖D²f‖. The (cosh θ)⁻² decay (via the n = 2 Fourier-decay estimate) is what makes the horizon amplitude L¹ and differentiable at the bifurcation surface x = 0 (the softer Route-B regularity).

m≠0→∀(θ:R),∥K m (f) θ∥≤16⋅π2⋅(((∫(v:V),∥f v∥)+∫(v:V),∥D R 1 (f) v∥)+∫(v:V),∥D R 2 (f) v∥)/(2⋅m2)⋅(cosh⁡ θ2)−1m \ne 0 \to \forall (\theta : \mathbb{R}), \|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(f)\,\theta\| \le 16 \cdot {\pi}^{2} \cdot (((\int (v : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|f\,v\|) + \int (v : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|\mathrm{D}\,\mathbb{R}\,1\,(f)\,v\|) + \int (v : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|\mathrm{D}\,\mathbb{R}\,2\,(f)\,v\|) / (\sqrt 2 \cdot {m}^{2}) \cdot {({\cosh\,\theta}^{2})}^{-1}

Proof. By massShell, minkowskiFourier, minkBilin, minkBilin_apply, minkowskiFourier_eq_fourierIntegral, abs_sinh_le_cosh. □\square

Used by integrable_Krep, norm_Krep_le_exp.

← all sections · ← OneParticleBW · WedgeAnalyticity →