Fock · section of the QIQT-H book

QIQTH.Fock.Localization

← all sections · ← FreeFieldHFlux · OneParticle →

Fock · entries 236–269 of 1000

Definition 236 (V).  source ↗

1+1D Minkowski spacetime (coordinates (t, x) = (z 0, z 1)).

V  :=  Fin 2→RV \;:=\; \mathrm{Fin}\,2 \to \mathbb{R}

Used by inner_KrepL2, inner_KrepL2_general, inner_boostUnitary_KrepL2, symm_edge_eq_shifted, symm_edge_eq_inner, kmsFun, kmsFun_ofReal, kmsFun_ofReal_eq_inner, and 158 more.

Definition 237 (minkowskiDot).  source ↗

The Minkowski pairing η(p, x) = p₀x₀ − p₁x₁ (signature (+,−)).

η p x  :=  p 0⋅x 0−p 1⋅x 1\eta\,p\,x \;:=\; p\,0 \cdot x\,0 - p\,1 \cdot x\,1

Used by minkowskiFourier_smul, minkowskiFourier_bumpCW, minkowskiDot_boost, minkowskiFourier, minkowskiFourier_boost, minkowskiFourier_zero, continuous_minkowskiDot_fst, continuous_minkowskiDot_snd, and 5 more.

Definition 238 (massShell).  source ↗

The positive mass shell in rapidity coordinates: p_m(θ) = (m cosh θ, m sinh θ).

MS m θ  :=  ![m⋅cosh⁡ θ,m⋅sinh⁡ θ]\mathrm{MS}\,m\,\theta \;:=\; ![m \cdot \cosh\,\theta , m \cdot \sinh\,\theta]

Used by Krep_smul, Krep_bumpCW_zero, massShell_zero, massShell_one, massShell_boost, Krep, Krep_boost, Krep_zero, and 8 more.

Definition 239 (lorentzBoost).  source ↗

The proper rapidity-a Lorentz boost on V.

L a z  :=  ![cosh⁡ a⋅z 0+sinh⁡ a⋅z 1,sinh⁡ a⋅z 0+cosh⁡ a⋅z 1]\mathrm{L}\,a\,z \;:=\; ![\cosh\,a \cdot z\,0 + \sinh\,a \cdot z\,1 , \sinh\,a \cdot z\,0 + \cosh\,a \cdot z\,1]

Used by lorentzBoost_zero, lorentzBoost_one, massShell_boost, minkowskiDot_boost, lorentzBoostₗ_apply, measurePreserving_lorentzBoost, measurableEmbedding_lorentzBoost, boostTest, and 6 more.

Lemma 240 (massShell_zero).  source ↗

MS m θ 0=m⋅cosh⁡ θ\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-massshell}{\mathrm{MS}}\,m\,\theta\,0 = m \cdot \cosh\,\theta

Proof. Immediate from the definitions. □\square

Used by massShell_boost.

Lemma 241 (massShell_one).  source ↗

MS m θ 1=m⋅sinh⁡ θ\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-massshell}{\mathrm{MS}}\,m\,\theta\,1 = m \cdot \sinh\,\theta

Proof. Immediate from the definitions. □\square

Used by massShell_boost.

Lemma 242 (lorentzBoost_zero).  source ↗

L a z 0=cosh⁡ a⋅z 0+sinh⁡ a⋅z 1\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a\,z\,0 = \cosh\,a \cdot z\,0 + \sinh\,a \cdot z\,1

Proof. Immediate from the definitions. □\square

Used by massShell_boost.

Lemma 243 (lorentzBoost_one).  source ↗

L a z 1=sinh⁡ a⋅z 0+cosh⁡ a⋅z 1\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a\,z\,1 = \sinh\,a \cdot z\,0 + \cosh\,a \cdot z\,1

Proof. Immediate from the definitions. □\square

Used by massShell_boost.

Lemma 244 (massShell_boost).  source ↗

The boost shifts rapidity on the mass shell: Λ_a (p_m θ) = p_m (θ + a). This is the geometric heart of boost-equivariance (the boost acts as translation θ ↦ θ + a on the shell).

L a (MS m θ)=MS m (θ+a)\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-massshell}{\mathrm{MS}}\,m\,\theta) = \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-massshell}{\mathrm{MS}}\,m\,(\theta + a)

Proof. By massShell_zero, massShell_one, lorentzBoost_zero, lorentzBoost_one. □\square

Used by Krep_boost.

Lemma 245 (minkowskiDot_boost).  source ↗

The Minkowski pairing is boost-invariant: η(Λ_a p, Λ_a x) = η(p, x).

η (L a p) (L a x)=η p x\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskidot}{\eta}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a\,p)\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a\,x) = \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskidot}{\eta}\,p\,x

Proof. Immediate from the definitions. □\square

Used by minkowskiFourier_boost.

Definition 246 (lorentzBoostMat).  source ↗

The boost matrix [[cosh a, sinh a], [sinh a, cosh a]].

lorentzBoostMat a  :=  !![cosh⁡ a,sinh⁡ a;sinh⁡ a,cosh⁡ a]\mathrm{lorentzBoostMat}\,a \;:=\; !![\cosh\,a , \sinh\,a ; \sinh\,a , \cosh\,a]

Used by lorentzBoostₗ, lorentzBoostₗ_apply, det_lorentzBoost.

Definition 247 (lorentzBoostₗ).  source ↗

The boost packaged as an ℝ-linear endomorphism of V (via its standard matrix). Typed on Fin 2 → ℝ (rather than the abbrev V) so the volume Haar instance synthesizes for the measure change-of-variables.

L a  :=  toLin′ (lorentzBoostMat a)\mathrm{L}\,a \;:=\; \mathrm{toLin}^{\prime}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboostmat}{\mathrm{lorentzBoostMat}}\,a)

Used by lorentzBoostₗ_apply, det_lorentzBoost, measurePreserving_lorentzBoost, lorentzBoostLE, measurableEmbedding_lorentzBoost.

Lemma 248 (lorentzBoostₗ_apply).  source ↗

(L a) z=L a z(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a)\,z = \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a\,z

Proof. By lorentzBoostMat. □\square

Used by measurePreserving_lorentzBoost, measurableEmbedding_lorentzBoost.

Lemma 249 (det_lorentzBoost).  source ↗

The boost is unimodular: det Λ_a = cosh²a − sinh²a = 1 — the change of variables y = Λ_a x in the spacetime Fourier integral has unit Jacobian (no measure correction).

det (L a)=1\mathrm{det}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a) = 1

Proof. By lorentzBoostMat. □\square

Used by measurePreserving_lorentzBoost.

Lemma 250 (measurePreserving_lorentzBoost).  source ↗

The boost preserves the Lebesgue volume (unit Jacobian) — the measure-preservation needed for the Fourier change of variables in boost-equivariance. (Stated on Fin 2 → ℝ explicitly so the volume Haar instance synthesizes; V is the same type but the reducible abbrev blocks instance search.)

MeasurePreserving (L a) vol vol\mathrm{MeasurePreserving}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a)\,\mathrm{vol}\,\mathrm{vol}

Proof. By lorentzBoostₗ, lorentzBoostₗ_apply, det_lorentzBoost. □\square

Used by minkowskiFourier_boost.

Definition 251 (lorentzBoostLE).  source ↗

The boost as a (continuous) linear equivalence of Fin 2 → ℝ — gives a measurable embedding.

Used by measurableEmbedding_lorentzBoost.

Lemma 252 (measurableEmbedding_lorentzBoost).  source ↗

The boost is a measurable embedding (it is a continuous linear equivalence).

MeasurableEmbedding (L a)\mathrm{MeasurableEmbedding}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a)

Proof. By lorentzBoostₗ, lorentzBoostₗ_apply, lorentzBoostLE. □\square

Used by minkowskiFourier_boost.

Definition 253 (minkowskiFourier).  source ↗

The Minkowski-space Fourier transform f̂_M(p) = ∫ e^{−i η(p,x)} f(x) dx, with the Minkowski pairing in the exponent (signature (+,−); soundness trap #2).

F f p  :=  ∫(x:V),exp⁡ (−i⋅(η p x))⋅f x\mathcal{F}\,f\,p \;:=\; \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \exp\,(-i \cdot (\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskidot}{\eta}\,p\,x)) \cdot f\,x

Used by minkowskiFourier_smul, Krep_smul, minkowskiFourier_bumpCW, Krep_bumpCW_zero, minkowskiFourier_boost, Krep, Krep_boost, minkowskiFourier_zero, and 7 more.

Definition 254 (boostTest).  source ↗

The boost action on test functions (β_a f)(x) = f(Λ_a x).

ϕB a f x  :=  f (L a x)\phi_{B}\,a\,f\,x \;:=\; f\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a\,x)

Used by inner_boostUnitary_KrepL2, symm_edge_eq_inner, kmsFun_ofReal_eq_inner, memLp_Krep_boostTest, boost, minkowskiFourier_boost, Krep_boost, boostUnitary_KrepL2, and 2 more.

Lemma 255 (minkowskiFourier_boost).  source ↗

Boost-equivariance of the localization (Fourier) map: f̂_M ∘ β_a = U_a ∘ f̂_M, i.e. (β_a f)^_M(p) = f̂_M(Λ_a p). A clean change of variables y = Λ_a x (unit Jacobian, the boost is volume-preserving and a measurable embedding) plus the Minkowski-pairing boost-invariance. This is the Phase-1c keystone: it makes the localization intertwine the spacetime boost with the one-particle action. Holds for ANY f (no integrability hypothesis — MeasurePreserving.integral_comp).

F (ϕB a f) p=F f (L a p)\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskifourier}{\mathcal{F}}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-boosttest}{\phi_{B}}\,a\,f)\,p = \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskifourier}{\mathcal{F}}\,f\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-lorentzboost}{\mathrm{L}}\,a\,p)

Proof. By minkowskiDot, minkowskiDot_boost, measurePreserving_lorentzBoost, measurableEmbedding_lorentzBoost. □\square

Used by Krep_boost.

Definition 256 (Krep).  source ↗

The localized rapidity amplitude (K f)(θ) = 2^{-1/2} · f̂_M(p_m θ) — the value of the localization map on the positive mass shell, in rapidity coordinates (before the L² packaging). The 1/√2 is the invariant-measure normalization dp/(2ω) = dθ/2 (soundness trap #1: omitting it scales the symplectic form by 2).

K m f θ  :=  1/2⋅F f (MS m θ)K\,m\,f\,\theta \;:=\; 1 / \sqrt 2 \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskifourier}{\mathcal{F}}\,f\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-massshell}{\mathrm{MS}}\,m\,\theta)

Used by inner_KrepL2, inner_KrepL2_general, inner_boostUnitary_KrepL2, symm_edge_eq_shifted, symm_edge_eq_inner, kmsFun_ofReal, kmsFun_ofReal_eq_inner, kmsFun_sub_I, and 68 more.

Lemma 257 (Krep_boost).  source ↗

The localization is boost-covariant at the amplitude level: boosting the spacetime test function translates the localized rapidity amplitude, (K (β_a f))(θ) = (K f)(θ + a). So the Lorentz boost acts on the localized one-particle amplitude as the rapidity translation θ ↦ θ + a — exactly the action implemented by the one-particle unitary OneParticle.boostUnitary. Immediate from the Phase-1c keystone minkowskiFourier_boost and the shell geometry massShell_boost.

K m (ϕB a f) θ=K m f (θ+a)\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-boosttest}{\phi_{B}}\,a\,f)\,\theta = \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,(\theta + a)

Proof. By massShell, lorentzBoost, massShell_boost, minkowskiFourier, minkowskiFourier_boost. □\square

Used by inner_boostUnitary_KrepL2, memLp_Krep_boostTest, boostUnitary_KrepL2, boostUnitary_mapsTo_wedgeGenSet.

Lemma 258 (minkowskiFourier_zero).  source ↗

The Minkowski-Fourier transform of the zero function is zero.

F (λx↦0) p=0\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskifourier}{\mathcal{F}}\,(\lambda x \mapsto 0)\,p = 0

Proof. By minkowskiDot. □\square

Used by Krep_zero.

Lemma 259 (Krep_zero).  source ↗

The localized amplitude of the zero function is the zero function.

(K m λx↦0)=0(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,\lambda x \mapsto 0) = 0

Proof. By massShell, minkowskiFourier, minkowskiFourier_zero. □\square

Used by zero_vec.

Lemma 260 (continuous_minkowskiDot_fst).  source ↗

p ↦ η(p,x) is continuous.

Continuous λp↦η p x\mathrm{Continuous}\,\lambda p \mapsto \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskidot}{\eta}\,p\,x

Proof. Immediate from the definitions. □\square

Used by minkowskiFourier_continuous.

Lemma 261 (continuous_minkowskiDot_snd).  source ↗

x ↦ η(p,x) is continuous.

Continuous λx↦η p x\mathrm{Continuous}\,\lambda x \mapsto \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskidot}{\eta}\,p\,x

Proof. Immediate from the definitions. □\square

Used by minkowskiFourier_continuous.

Lemma 262 (minkowskiFourier_continuous).  source ↗

The Minkowski-Fourier transform of an integrable function is continuous (Riemann–Lebesgue continuity, via dominated convergence; the exponential has modulus one and f dominates).

Integrable f vol→Continuous (F f)\mathrm{Integrable}\,f\,\mathrm{vol} \to \mathrm{Continuous}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskifourier}{\mathcal{F}}\,f)

Proof. By minkowskiDot, continuous_minkowskiDot_fst, continuous_minkowskiDot_snd. □\square

Used by Krep_continuous.

Lemma 263 (continuous_massShell).  source ↗

The mass-shell embedding θ ↦ p_m(θ) is continuous.

Continuous (MS m)\mathrm{Continuous}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-massshell}{\mathrm{MS}}\,m)

Proof. Immediate from the definitions. □\square

Used by Krep_continuous.

Lemma 264 (Krep_continuous).  source ↗

The localized rapidity amplitude is continuous for an integrable test function, hence (part (a) of MemLp) almost-everywhere strongly measurable. The remaining part (b) — the L² bound from Schwartz–Fourier decay on the mass shell — is the isolated multi-week analytic core.

Integrable f vol→Continuous (K m f)\mathrm{Integrable}\,f\,\mathrm{vol} \to \mathrm{Continuous}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)

Proof. By massShell, minkowskiFourier, minkowskiFourier_continuous, continuous_massShell. □\square

Used by Krep_bumpCW_ne_zero_of, Krep_aestronglyMeasurable, integrable_Krep, integrable_ftKrep, hasDerivAt_ftKrepF.

Lemma 265 (Krep_aestronglyMeasurable).  source ↗

Integrable f vol→AEStronglyMeasurable (K m f) vol\mathrm{Integrable}\,f\,\mathrm{vol} \to \mathrm{AEStronglyMeasurable}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,\mathrm{vol}

Proof. By Krep_continuous. □\square

Used by Krep_memLp_of_decay.

Lemma 266 (one_add_sq_le_cosh_sq).  source ↗

The mass-shell hyperbola dominates the parabola: 1 + θ² ≤ cosh²θ (since cosh²=1+sinh² and θ² ≤ sinh²θ).

1+θ2≤cosh⁡ θ21 + {\theta}^{2} \le {\cosh\,\theta}^{2}

Proof. Immediate from the definitions. □\square

Used by integrable_cosh_inv_sq.

Lemma 267 (integrable_cosh_inv_sq).  source ↗

1/cosh² is integrable on ℝ (dominated by the Cauchy density (1+θ²)⁻¹).

Integrable (λθ↦(cosh⁡ θ2)−1) vol\mathrm{Integrable}\,(\lambda \theta \mapsto {({\cosh\,\theta}^{2})}^{-1})\,\mathrm{vol}

Proof. By one_add_sq_le_cosh_sq. □\square

Used by memLp_cosh_inv.

Lemma 268 (memLp_cosh_inv).  source ↗

1/cosh ∈ L²(ℝ) — the comparison function for the localized-amplitude boundedness.

MemLp (λθ↦(cosh⁡ θ)−1) 2 vol\mathrm{MemLp}\,(\lambda \theta \mapsto {(\cosh\,\theta)}^{-1})\,2\,\mathrm{vol}

Proof. By integrable_cosh_inv_sq. □\square

Used by Krep_memLp_of_decay.

Lemma 269 (Krep_memLp_of_decay).  source ↗

Boundedness from a 1/cosh decay bound: if the localized rapidity amplitude is dominated by C/cosh θ, then it lies in L²(ℝ). This reduces the MemLp obligation of LocalTest to the sharp pointwise Fourier-decay estimate ‖(K f)(θ)‖ ≤ C/cosh θ — the genuine remaining analytic content (the Fourier transform of a smooth test function decays on the mass shell). The integrability is fully discharged here.

Integrable f vol→∀{C:R},(∀(θ:R),∥K m f θ∥≤C⋅(cosh⁡ θ)−1)→MemLp (K m f) 2 vol\mathrm{Integrable}\,f\,\mathrm{vol} \to \forall \{C : \mathbb{R}\}, (\forall (\theta : \mathbb{R}), \|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\| \le C \cdot {(\cosh\,\theta)}^{-1}) \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol}

Proof. By Krep_aestronglyMeasurable, memLp_cosh_inv. □\square

Used by schwartz_Krep_memLp.

← all sections · ← FreeFieldHFlux · OneParticle →