Fock · section of the QIQT-H book

QIQTH.Fock.WienerL2

← all sections · ← WedgeAnalyticity · GaussianMode →

Fock · entries 384–427 of 1000

Definition 384 (schwartzTranslate).  source ↗

Wiener brick 1 — the Schwartz translation operator τ_a : 𝓢(ℝ,ℂ) →L[ℂ] 𝓢(ℝ,ℂ), f ↦ f(·+a). Built via SchwartzMap.compCLM with the temperate-growth affine map x ↦ x + a (HasTemperateGrowth.id' + .const, and the moderate-decay bound ‖x‖ ≤ (1+‖a‖)(1+‖x+a‖)). The foundational operator for the L²-translate↔modulation intertwining 𝓕 ∘ τ_a = M_a ∘ 𝓕 behind Wiener’s L² Tauberian theorem.

τ a  :=  compCLM C ⋯ ⋯\tau\,a \;:=\; \mathrm{compCLM}\,\mathbb{C}\,\cdots \,\cdots

Used by schwartzTranslate_apply, boostUnitary_toLp, fourier_schwartzTranslate, fourierL2_boostUnitary.

Lemma 385 (schwartzTranslate_apply).  source ↗

((τ a) f) x=f (x+a)((\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-schwartztranslate}{\tau}\,a)\,f)\,x = f\,(x + a)

Proof. Immediate from the definitions. □\square

Used by boostUnitary_toLp, fourier_schwartzTranslate.

Lemma 386 (boostUnitary_toLp).  source ↗

Wiener brick 3 — the boost unitary IS the Schwartz translation, at L²: boostUnitary a (f.toLp) = (schwartzTranslate (−a) f).toLp (both =ᵐ θ ↦ f(θ−a), via coeFn_boostUnitary, the measure-preserving translated-ae, and schwartzTranslate_apply). This connects the QIQT rapidity-boost group to the generic Schwartz translation, so the Schwartz-level Fourier translate→modulation lemma transfers to boostUnitary (the next brick toward the intertwining 𝓕 ∘ boostUnitary_a = M_a ∘ 𝓕).

(U a) (f.toLp 2 vol)=((τ (−a)) f).toLp 2 vol(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,a)\,(f.\mathrm{toLp}\,2\,\mathrm{vol}) = ((\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-schwartztranslate}{\tau}\,(-a))\,f).\mathrm{toLp}\,2\,\mathrm{vol}

Proof. By coeFn_boostUnitary, schwartzTranslate_apply. □\square

Used by fourierL2_boostUnitary.

Definition 387 (modChar).  source ↗

The unit Fourier character ξ ↦ e^{i c ξ} (modulus 1).

χmod c ξ  :=  exp⁡ (i⋅(c⋅ξ))\chi_{\mathrm{mod}}\,c\,\xi \;:=\; \exp\,(i \cdot (c \cdot \xi))

Used by norm_modChar, continuous_modChar, memLp_modChar_smul, modL2, coeFn_modL2, norm_modL2, fourier_schwartzTranslate, modL2_sub, and 4 more.

Lemma 388 (norm_modChar).  source ↗

∥χmod c ξ∥=1\|\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modchar}{\chi_{\mathrm{mod}}}\,c\,\xi\| = 1

Proof. Immediate from the definitions. □\square

Used by memLp_modChar_smul, norm_modL2.

Lemma 389 (continuous_modChar).  source ↗

Continuous (χmod c)\mathrm{Continuous}\,(\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modchar}{\chi_{\mathrm{mod}}}\,c)

Proof. Immediate from the definitions. □\square

Used by memLp_modChar_smul.

Lemma 390 (memLp_modChar_smul).  source ↗

e^{icξ}·g ∈ L² whenever g ∈ L² (modulus-1 multiplier, via MemLp.of_le_mul).

MemLp (λξ↦χmod c ξ⋅g ξ) 2 vol\mathrm{MemLp}\,(\lambda \xi \mapsto \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modchar}{\chi_{\mathrm{mod}}}\,c\,\xi \cdot g\,\xi)\,2\,\mathrm{vol}

Proof. By norm_modChar, continuous_modChar. □\square

Used by modL2, coeFn_modL2.

Definition 391 (modL2).  source ↗

Wiener brick 2 — the L² modulation operator M_c : g ↦ (ξ ↦ e^{icξ} g(ξ)).

Used by coeFn_modL2, norm_modL2, modL2_sub, isometry_modL2, continuous_modL2, fourierL2_boostUnitary, inner_boostUnitary_eq_integral.

Lemma 392 (coeFn_modL2).  source ↗

(modL2 c g)=[vol]λξ↦χmod c ξ⋅g ξ(\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modl2}{\mathrm{modL2}}\,c\,g) =[\mathrm{vol}] \lambda \xi \mapsto \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modchar}{\chi_{\mathrm{mod}}}\,c\,\xi \cdot g\,\xi

Proof. By memLp_modChar_smul. □\square

Used by norm_modL2, modL2_sub, fourierL2_boostUnitary, inner_boostUnitary_eq_integral.

Lemma 393 (norm_modL2).  source ↗

M_c is an L²-isometry: ‖M_c g‖ = ‖g‖ (the character has modulus 1).

∥modL2 c g∥=∥g∥\|\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modl2}{\mathrm{modL2}}\,c\,g\| = \|g\|

Proof. By modChar, norm_modChar, coeFn_modL2. □\square

Used by isometry_modL2.

Lemma 394 (fourier_schwartzTranslate).  source ↗

Wiener brick 4a — the Schwartz translate→modulation identity (pointwise). 𝓕(f(·−a))(w) = e^{−2πi a w} · 𝓕f(w) — the Fourier dual of translation is modulation by the unit character modChar (−2πa). Via fourier_coe (Schwartz 𝓕 = integral 𝓕 on the coeFn) and VectorFourier.fourierIntegral_comp_add_right.

(F ((τ (−a)) f)) w=χmod (−(2⋅π⋅a)) w⋅(F f) w(\mathcal{F}\,((\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-schwartztranslate}{\tau}\,(-a))\,f))\,w = \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modchar}{\chi_{\mathrm{mod}}}\,(-(2 \cdot \pi \cdot a))\,w \cdot (\mathcal{F}\,f)\,w

Proof. By schwartzTranslate_apply. □\square

Used by fourierL2_boostUnitary.

Lemma 395 (modL2_sub).  source ↗

M_c is subtractive (companion to modL2_add), giving the isometry below.

modL2 c (g−h)=modL2 c g−modL2 c h\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modl2}{\mathrm{modL2}}\,c\,(g - h) = \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modl2}{\mathrm{modL2}}\,c\,g - \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modl2}{\mathrm{modL2}}\,c\,h

Proof. By modChar, coeFn_modL2. □\square

Used by isometry_modL2.

Lemma 396 (isometry_modL2).  source ↗

M_c is an isometry of L² (modulus-1 multiplier), hence continuous.

Isometry (modL2 c)\mathrm{Isometry}\,(\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modl2}{\mathrm{modL2}}\,c)

Proof. By norm_modL2, modL2_sub. □\square

Used by continuous_modL2.

Lemma 397 (continuous_modL2).  source ↗

Continuous (modL2 c)\mathrm{Continuous}\,(\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modl2}{\mathrm{modL2}}\,c)

Proof. By isometry_modL2. □\square

Used by fourierL2_boostUnitary.

Lemma 398 (fourierL2_boostUnitary).  source ↗

Wiener brick 4b — the L² translate→modulation intertwining. 𝓕 (boostUnitary a g) = M_{−2πa} (𝓕 g) for all g ∈ L² — the boost (a translation) becomes multiplication by the unit character under the L² Fourier unitary. Proven on the dense Schwartz range (brick 4a + toLp_fourier_eq + boostUnitary_toLp) and extended by DenseRange.equalizer (both sides continuous: 𝓕/boostUnitary are isometry-equivs, M_c is continuous_modL2).

F ((U a) g)=modL2 (−(2⋅π⋅a)) (F g)\mathcal{F}\,((\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,a)\,g) = \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modl2}{\mathrm{modL2}}\,(-(2 \cdot \pi \cdot a))\,(\mathcal{F}\,g)

Proof. By schwartzTranslate, boostUnitary_toLp, modChar, coeFn_modL2, fourier_schwartzTranslate, continuous_modL2. □\square

Used by inner_boostUnitary_eq_integral.

Lemma 399 (conj_modChar).  source ↗

The unit character conjugates to its inverse: conj (e^{icξ}) = e^{−icξ}.

(starRingEnd C) (χmod c ξ)=χmod (−c) ξ(\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modchar}{\chi_{\mathrm{mod}}}\,c\,\xi) = \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modchar}{\chi_{\mathrm{mod}}}\,(-c)\,\xi

Proof. Immediate from the definitions. □\square

Used by inner_boostUnitary_eq_integral.

Lemma 400 (inner_boostUnitary_eq_integral).  source ↗

Wiener brick 5 — the bridge. Via Plancherel (inner_fourier_eq) and the intertwining (brick 4), the boost-orbit inner product is the integral (inverse) Fourier transform of k(ξ) = conj(𝓕g₀ ξ)·𝓕h ξ ∈ L¹: ⟪boostUnitary a g₀, h⟫ = ∫ e^{+2πi a ξ}·conj(𝓕g₀ ξ)·𝓕h ξ dξ. So the orbit-orthogonality condition ∀a, ⟪…⟫ = 0 becomes the vanishing of the FT of k — the exact hypothesis of the L¹ uniqueness theorem (next brick).

⟨(U a) g0,h⟩=∫(ξ:R),χmod (2⋅π⋅a) ξ⋅((starRingEnd C) ((F g0) ξ)⋅(F h) ξ)\langle {(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,a)\,g_{0}},{h}\rangle = \int (\xi : \mathbb{R}), \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-modchar}{\chi_{\mathrm{mod}}}\,(2 \cdot \pi \cdot a)\,\xi \cdot ((\mathrm{starRingEnd}\,\mathbb{C})\,((\mathcal{F}\,g_{0})\,\xi) \cdot (\mathcal{F}\,h)\,\xi)

Proof. By modL2, coeFn_modL2, fourierL2_boostUnitary, conj_modChar. □\square

Used by fourier_correlation_eq.

Lemma 401 (fourier_correlation_eq).  source ↗

Wiener brick 6a — the reduction. The function Fourier transform of k(ξ) = conj(𝓕g₀ ξ)·𝓕h ξ at w equals the boost-orbit correlation ⟪boostUnitary (−w) g₀, h⟫ (brick 5 at a = −w, matching the 𝓕-character 𝐞(−⟪ξ,w⟫) = modChar(2π(−w))ξ). Hence (∀a, ⟪boost_a g₀,h⟫ = 0) ⟹ 𝓕 k ≡ 0.

F (λξ↦(starRingEnd C) ((F g0) ξ)⋅(F h) ξ) w=⟨(U (−w)) g0,h⟩\mathcal{F}\,(\lambda \xi \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,((\mathcal{F}\,g_{0})\,\xi) \cdot (\mathcal{F}\,h)\,\xi)\,w = \langle {(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(-w))\,g_{0}},{h}\rangle

Proof. By modChar, inner_boostUnitary_eq_integral. □\square

Used by boost_orbit_total_of_fourier_ne_zero.

Lemma 402 (ae_eq_zero_of_fourier_eq_zero).  source ↗

Wiener brick 6b — Fourier injectivity on L¹. If k ∈ L¹(ℝ) and its (function) Fourier transform vanishes identically, then k = 0 a.e. Proof: it suffices (AEEqOfIntegralContDiff) that ∫ g·k = 0 for every real smooth compactly-supported test g; package its complexification G:=↑∘g as a Schwartz map, write G = 𝓕(𝓕⁻G) (Schwartz inversion) and apply the multiplication formula ∫ 𝓕(𝓕⁻G)·k = ∫ (𝓕⁻G)·𝓕k (integral_fourierIntegral_smul_eq_flip, innerₗ symmetric) = 0 since 𝓕 k = 0.

Integrable k vol→(∀(w:R),F k w=0)→k=[vol]0\mathrm{Integrable}\,k\,\mathrm{vol} \to (\forall (w : \mathbb{R}), \mathcal{F}\,k\,w = 0) \to k =[\mathrm{vol}] 0

Proof. Immediate from the definitions. □\square

Used by boost_orbit_total_of_fourier_ne_zero, fourierL2_toLp_ne_zero_of_ne_zero.

Lemma 403 (boost_orbit_total_of_fourier_ne_zero).  source ↗

Wiener brick 7 — the Tauberian conclusion. If 𝓕 g₀ ≠ 0 a.e. and h is orthogonal to the entire boost orbit of g₀, then h = 0. Chains 6a (orbit-orthogonality ⟹ 𝓕 k ≡ 0, k=conj(𝓕g₀)·𝓕h ∈ L¹) with 6b (𝓕 k = 0 ⟹ k=ᵐ0); then 𝓕g₀≠0 a.e. forces 𝓕 h = 0 a.e. ⟹ 𝓕 h = 0 ⟹ h = 0 (𝓕 an isometry).

(∀(ξ:R),(F g0) ξ≠0)→(∀(a:R),⟨(U a) g0,h⟩=0)→h=0(\forall (\xi : \mathbb{R}), (\mathcal{F}\,g_{0})\,\xi \ne 0) \to (\forall (a : \mathbb{R}), \langle {(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,a)\,g_{0}},{h}\rangle = 0) \to h = 0

Proof. By fourier_correlation_eq, ae_eq_zero_of_fourier_eq_zero. □\square

Used by niceWedgeCyclic_of_fourier_ne_zero.

Lemma 404 (ae_ne_zero_of_analyticOnNhd).  source ↗

Wiener brick 8c — a nonzero real-analytic function is ≠ 0 a.e. The zero set of a function analytic on all of ℝ (and not identically zero) is co-discrete, hence Lebesgue-null (AnalyticOnNhd.eqOn_zero_or_eventually_ne_zero_of_preconnected + ae_restrict_le_codiscreteWithin). This is the final step turning “the boost-orbit generator’s Fourier transform is entire and ≢ 0” into the Wiener hypothesis 𝓕 g₀ ≠ 0 a.e. of brick 7.

AnalyticOnNhd R F→(∃x,F x≠0)→∀(x:R),F x≠0\mathrm{AnalyticOnNhd}\,\mathbb{R}\,F \to (\exists x, F\,x \ne 0) \to \forall (x : \mathbb{R}), F\,x \ne 0

Proof. Immediate from the definitions. □\square

Used by fourierL2_toLp_ne_zero_of_ne_zero.

Lemma 405 (integrable_exp_neg_mul_abs).  source ↗

Wiener brick 8a-foundation — exp(−b|x|) is integrable on ℝ for b > 0. The reusable both-ends exponential building block: f =O[atBot] exp(b·) and f =O[atTop] exp(−b·), each integrable at its end (exp_neg_integrableOn_Ioi + reflection), via LocallyIntegrable.integrable_of_isBigO_atBot_atTop. Dominates the 1/cosh²θ decay of Krep, giving Krep ∈ L¹ and its finite exponential moments.

0<b→Integrable (λx↦exp⁡ (−b⋅∣x∣)) vol0 < b \to \mathrm{Integrable}\,(\lambda x \mapsto \exp\,(-b \cdot |x|))\,\mathrm{vol}

Proof. Immediate from the definitions. □\square

Used by integrable_abs_mul_exp_neg_mul_abs, integrable_Krep, integrable_ftKrep.

Lemma 406 (integrable_abs_mul_exp_neg_mul_abs).  source ↗

|θ|·exp(−d|θ|) is integrable on ℝ for d > 0 — the derivative-domination building block for the FT-holomorphy (8b): |θ| ≤ (2/d)·exp((d/2)|θ|) (from t ≤ exp t) absorbs the |θ| into a slower exponential dominated by integrable_exp_neg_mul_abs (d/2).

0<d→Integrable (λθ↦∣θ∣⋅exp⁡ (−d⋅∣θ∣)) vol0 < d \to \mathrm{Integrable}\,(\lambda \theta \mapsto |\theta| \cdot \exp\,(-d \cdot |\theta|))\,\mathrm{vol}

Proof. By integrable_exp_neg_mul_abs. □\square

Used by hasDerivAt_ftKrepF.

Lemma 407 (inv_cosh_sq_le_exp).  source ↗

(cosh θ)⁻² ≤ 4·exp(−2|θ|) — from exp|θ| ≤ 2cosh θ (one of e^{±θ} equals e^{|θ|}).

(cosh⁡ θ2)−1≤4⋅exp⁡ (−2⋅∣θ∣){({\cosh\,\theta}^{2})}^{-1} \le 4 \cdot \exp\,(-2 \cdot |\theta|)

Proof. Immediate from the definitions. □\square

Used by integrable_Krep, norm_Krep_le_exp.

Lemma 408 (integrable_Krep).  source ↗

Wiener brick 8a — Krep m f ∈ L¹(ℝ) for a Schwartz test f: the localized rapidity amplitude is integrable, since ‖Krep m f θ‖ ≤ C·(cosh θ)⁻² (schwartz_Krep_decay_sq) ≤ 4C·exp(−2|θ|), dominated by the integrable exp(−2|θ|) (integrable_exp_neg_mul_abs). Makes the function Fourier transform of Krep well-defined and is the base for the L²↔L¹ agreement and the FT-holomorphy (8b).

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

Proof. By Krep_continuous, schwartz_Krep_decay_sq, integrable_exp_neg_mul_abs, inv_cosh_sq_le_exp. □\square

Used by fourierL2_Krep_ne_zero.

Definition 409 (ftKrep).  source ↗

The complexified Fourier integrand exp(−2π i θ ζ)·Krep(θ).

ftKrep m f ζ θ  :=  exp⁡ (−2⋅π⋅i⋅θ⋅ζ)⋅K m f θ\mathrm{ftKrep}\,m\,f\,\zeta\,\theta \;:=\; \exp\,(-2 \cdot \pi \cdot i \cdot \theta \cdot \zeta) \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta

Used by ftKrepF, hasDerivAt_ftKrep, norm_ftKrep, continuous_ftKrep, integrable_ftKrep, hasDerivAt_ftKrepF, ftKrepF_eq_fourier.

Definition 410 (ftKrep').  source ↗

Its ζ-derivative −2π i θ exp(−2π i θ ζ)·Krep(θ).

K^ m f ζ θ  :=  −2⋅π⋅i⋅θ⋅exp⁡ (−2⋅π⋅i⋅θ⋅ζ)⋅K m f θ\hat{K}\,m\,f\,\zeta\,\theta \;:=\; -2 \cdot \pi \cdot i \cdot \theta \cdot \exp\,(-2 \cdot \pi \cdot i \cdot \theta \cdot \zeta) \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta

Used by hasDerivAt_ftKrep, norm_ftKrep', continuous_ftKrep', hasDerivAt_ftKrepF, analyticOnNhd_ftKrepF_real.

Definition 411 (ftKrepF).  source ↗

The complexified Fourier transform F(ζ) = ∫ exp(−2π i θ ζ)·Krep(θ) dθ.

K^ m f ζ  :=  ∫(θ:R),ftKrep m f ζ θ\hat{K}\,m\,f\,\zeta \;:=\; \int (\theta : \mathbb{R}), \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrep}{\mathrm{ftKrep}}\,m\,f\,\zeta\,\theta

Used by hasDerivAt_ftKrepF, analyticOnNhd_ftKrepF_real, ftKrepF_eq_fourier, analyticOnNhd_fourier_Krep.

Lemma 412 (hasDerivAt_ftKrep).  source ↗

The integrand is ζ-holomorphic pointwise, with derivative ftKrep'.

(λζ↦ftKrep m f ζ θ)′(ζ0)=K^ m f ζ0 θ({\lambda \zeta \mapsto \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrep}{\mathrm{ftKrep}}\,m\,f\,\zeta\,\theta})'({\zeta_{0}})={\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrep}{\hat{K}}\,m\,f\,\zeta_{0}\,\theta}

Proof. By Krep. □\square

Used by hasDerivAt_ftKrepF.

Lemma 413 (ftKrep_exp_re).  source ↗

The exponent’s real part: Re(−2π i θ ζ) = 2π θ (Im ζ).

(−2⋅π⋅i⋅θ⋅ζ).re=2⋅π⋅θ⋅ζ.im(-2 \cdot \pi \cdot i \cdot \theta \cdot \zeta).\mathrm{re} = 2 \cdot \pi \cdot \theta \cdot \zeta.\mathrm{im}

Proof. Immediate from the definitions. □\square

Used by norm_ftKrep', norm_ftKrep.

Lemma 414 (norm_ftKrep').  source ↗

The norm of the integrand’s ζ-derivative.

∥K^ m f ζ θ∥=2⋅π⋅∣θ∣⋅exp⁡ (2⋅π⋅θ⋅ζ.im)⋅∥K m f θ∥\|\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrep}{\hat{K}}\,m\,f\,\zeta\,\theta\| = 2 \cdot \pi \cdot |\theta| \cdot \exp\,(2 \cdot \pi \cdot \theta \cdot \zeta.\mathrm{im}) \cdot \|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|

Proof. By ftKrep_exp_re. □\square

Used by hasDerivAt_ftKrepF.

Lemma 415 (norm_ftKrep).  source ↗

The norm of the integrand itself.

∥ftKrep m f ζ θ∥=exp⁡ (2⋅π⋅θ⋅ζ.im)⋅∥K m f θ∥\|\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrep}{\mathrm{ftKrep}}\,m\,f\,\zeta\,\theta\| = \exp\,(2 \cdot \pi \cdot \theta \cdot \zeta.\mathrm{im}) \cdot \|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|

Proof. By ftKrep_exp_re. □\square

Used by integrable_ftKrep.

Lemma 416 (norm_Krep_le_exp).  source ↗

The decay constant for Krep, factored: ‖Krep m f θ‖ ≤ C·exp(−2|θ|) for some C ≥ 0.

m≠0→∃C,0≤C∧∀(θ:R),∥K m (f) θ∥≤C⋅exp⁡ (−2⋅∣θ∣)m \ne 0 \to \exists C, 0 \le C \wedge \forall (\theta : \mathbb{R}), \|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(f)\,\theta\| \le C \cdot \exp\,(-2 \cdot |\theta|)

Proof. By schwartz_Krep_decay_sq, inv_cosh_sq_le_exp. □\square

Used by integrable_ftKrep, hasDerivAt_ftKrepF.

Lemma 417 (continuous_ftKrep).  source ↗

Continuous (K m f)→∀(ζ:C),Continuous λθ↦ftKrep m f ζ θ\mathrm{Continuous}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f) \to \forall (\zeta : \mathbb{C}), \mathrm{Continuous}\,\lambda \theta \mapsto \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrep}{\mathrm{ftKrep}}\,m\,f\,\zeta\,\theta

Proof. Immediate from the definitions. □\square

Used by integrable_ftKrep, hasDerivAt_ftKrepF.

Lemma 418 (continuous_ftKrep').  source ↗

Continuous (K m f)→∀(ζ:C),Continuous λθ↦K^ m f ζ θ\mathrm{Continuous}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f) \to \forall (\zeta : \mathbb{C}), \mathrm{Continuous}\,\lambda \theta \mapsto \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrep}{\hat{K}}\,m\,f\,\zeta\,\theta

Proof. Immediate from the definitions. □\square

Used by hasDerivAt_ftKrepF.

Lemma 419 (integrable_ftKrep).  source ↗

The integrand is integrable at any strip point |Im ζ| < 1/π.

m≠0→∀{ζ:C},∣ζ.im∣<1/π→Integrable (λθ↦ftKrep m (f) ζ θ) volm \ne 0 \to \forall \{\zeta : \mathbb{C}\}, |\zeta.\mathrm{im}| < 1 / \pi \to \mathrm{Integrable}\,(\lambda \theta \mapsto \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrep}{\mathrm{ftKrep}}\,m\,(f)\,\zeta\,\theta)\,\mathrm{vol}

Proof. By Krep, Krep_continuous, integrable_exp_neg_mul_abs, norm_ftKrep, norm_Krep_le_exp, continuous_ftKrep. □\square

Used by hasDerivAt_ftKrepF.

Lemma 420 (hasDerivAt_ftKrepF).  source ↗

Wiener brick 8b — the FT of Krep is holomorphic on the strip. At every ζ₀ with |Im ζ₀| < 1/π, F(ζ) = ∫ exp(−2π i θ ζ)·Krep(θ) dθ is complex-differentiable, with derivative ∫ ftKrep'. Via the dominated-derivative theorem (hasDerivAt_integral_of_dominated_loc_of_deriv_le, 𝕜 = ℂ): the integrand is pointwise ζ-holomorphic (hasDerivAt_ftKrep), L¹ at ζ₀ (integrable_ftKrep), and its derivative is dominated on a ball by 2πC·|θ|·exp(−d|θ|) ∈ L¹ (integrable_abs_mul_exp_neg_mul_abs).

m≠0→∀{ζ0:C},∣ζ0.im∣<1/π→(K^ m f)′(ζ0)=∫(θ:R),K^ m (f) ζ0 θm \ne 0 \to \forall \{\zeta_{0} : \mathbb{C}\}, |\zeta_{0}.\mathrm{im}| < 1 / \pi \to ({\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrepf}{\hat{K}}\,m\,f})'({\zeta_{0}})={\int (\theta : \mathbb{R}), \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrep}{\hat{K}}\,m\,(f)\,\zeta_{0}\,\theta}

Proof. By Krep, Krep_continuous, integrable_abs_mul_exp_neg_mul_abs, ftKrep, hasDerivAt_ftKrep, norm_ftKrep', norm_Krep_le_exp, continuous_ftKrep, continuous_ftKrep', integrable_ftKrep. □\square

Used by analyticOnNhd_ftKrepF_real.

Lemma 421 (analyticOnNhd_ftKrepF_real).  source ↗

Wiener brick 8b-fin — the FT of Krep, on ℝ, is real-analytic. F is holomorphic on the open strip |Im ζ| < 1/π (brick 8b), which contains ℝ; restricting to the real axis gives AnalyticOnNhd ℝ (ξ ↦ F ξ) univ (the same DifferentiableOn.analyticOnNhd + restrictScalars/ofRealCLM route as 8c′). Feeds brick 8c: combined with ≢ 0 it yields F ≠ 0 a.e. on ℝ.

m≠0→AnalyticOnNhd R (λξ↦K^ m f ξ)m \ne 0 \to \mathrm{AnalyticOnNhd}\,\mathbb{R}\,(\lambda \xi \mapsto \href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrepf}{\hat{K}}\,m\,f\,\xi)

Proof. By ftKrep', hasDerivAt_ftKrepF. □\square

Used by analyticOnNhd_fourier_Krep.

Lemma 422 (ftKrepF_eq_fourier).  source ↗

Wiener brick 8b-bridge (function FT) — F restricts to the function Fourier transform of Krep. ftKrepF m f ξ = 𝓕(Krep m f) ξ for real ξ (matching the character exp(−2πiθξ) = 𝐞(−⟨θ,ξ⟩), Real.fourier_eq/Real.fourierChar_apply). With analyticOnNhd_ftKrepF_real this gives AnalyticOnNhd ℝ (𝓕 Krep) univ.

K^ m f ξ=F (K m f) ξ\href{/browser/qiqth-fock-wienerl2#d-qiqth-fock-wienerl2-ftkrepf}{\hat{K}}\,m\,f\,\xi = \mathcal{F}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,\xi

Proof. By ftKrep. □\square

Used by analyticOnNhd_fourier_Krep.

Lemma 423 (analyticOnNhd_fourier_Krep).  source ↗

The function Fourier transform of Krep is real-analytic on ℝ (combining ftKrepF_eq_fourier with analyticOnNhd_ftKrepF_real). Combined with ≢ 0, brick 8c yields 𝓕(Krep) ≠ 0 a.e.

m≠0→AnalyticOnNhd R (λξ↦F (K m f) ξ)m \ne 0 \to \mathrm{AnalyticOnNhd}\,\mathbb{R}\,(\lambda \xi \mapsto \mathcal{F}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,\xi)

Proof. By ftKrepF, analyticOnNhd_ftKrepF_real, ftKrepF_eq_fourier. □\square

Used by fourierL2_Krep_ne_zero.

Lemma 424 (integral_smul_fourierL2_eq).  source ↗

The integral pairing identity. For g ∈ L¹∩L² and Schwartz φ: ∫ φ·⇑(𝓕_{L²}(g.toLp)) = ∫ φ·𝓕_{int}(g) — via the tempered-distribution Fourier transform (fourier_toTemperedDistribution_eq + fourier_apply + the Lp pairing toTemperedDistribution_apply) and the multiplication formula (integral_fourierIntegral_smul_eq_flip).

Integrable g vol→∀(hg2:MemLp g 2 vol)(φ:SchwartzMap R C),∫(x:R),φ x⋅(F (toLp g hg2)) x=∫(x:R),φ x⋅F g x\mathrm{Integrable}\,g\,\mathrm{vol} \to \forall (\mathrm{hg2} : \mathrm{MemLp}\,g\,2\,\mathrm{vol}) (\varphi : \mathrm{SchwartzMap}\,\mathbb{R}\,\mathbb{C}), \int (x : \mathbb{R}), \varphi\,x \cdot (\mathcal{F}\,(\mathrm{toLp}\,g\,\mathrm{hg2}))\,x = \int (x : \mathbb{R}), \varphi\,x \cdot \mathcal{F}\,g\,x

Proof. Immediate from the definitions. □\square

Used by fourierL2_toLp_ae_eq.

Lemma 425 (fourierL2_toLp_ae_eq).  source ↗

Wiener brick 8b-bridge (L²↔L¹) — the L² FT coeFn agrees a.e. with the function FT. For g ∈ L¹∩L², ⇑(𝓕_{L²}(g.toLp)) =ᵐ 𝓕_{int}(g). From the pairing identity integral_smul_fourierL2_eq (both pair equally with every Schwartz φ) + the variational lemma ae_eq_of_integral_contDiff_smul_eq (testing against real C^∞_c functions, packaged as Schwartz).

Integrable g vol→∀(hg2:MemLp g 2 vol),(F (toLp g hg2))=[vol]F g\mathrm{Integrable}\,g\,\mathrm{vol} \to \forall (\mathrm{hg2} : \mathrm{MemLp}\,g\,2\,\mathrm{vol}), (\mathcal{F}\,(\mathrm{toLp}\,g\,\mathrm{hg2})) =[\mathrm{vol}] \mathcal{F}\,g

Proof. By integral_smul_fourierL2_eq. □\square

Used by fourierL2_toLp_ne_zero_of_ne_zero.

Lemma 426 (fourierL2_toLp_ne_zero_of_ne_zero).  source ↗

The Wiener nonvanishing, assembled. For g ∈ L¹∩L² with 𝓕 g real-analytic on ℝ and g ≢ 0, the L² FT coeFn ⇑(𝓕_{L²}(g.toLp)) ≠ 0 a.e. Chains: g ≢ 0 ⟹ ∃ x, 𝓕g(x)≠0 (brick 6b contrapositive) ⟹ 𝓕 g ≠ 0 a.e. (brick 8c) ⟹ (L²↔L¹ agreement) ⇑(𝓕_{L²}(g.toLp)) ≠ 0 a.e.

Integrable g vol→∀(hg2:MemLp g 2 vol),AnalyticOnNhd R (λξ↦F g ξ)→¬g=[vol]0→∀(ξ:R),(F (toLp g hg2)) ξ≠0\mathrm{Integrable}\,g\,\mathrm{vol} \to \forall (\mathrm{hg2} : \mathrm{MemLp}\,g\,2\,\mathrm{vol}), \mathrm{AnalyticOnNhd}\,\mathbb{R}\,(\lambda \xi \mapsto \mathcal{F}\,g\,\xi) \to \neg g =[\mathrm{vol}] 0 \to \forall (\xi : \mathbb{R}), (\mathcal{F}\,(\mathrm{toLp}\,g\,\mathrm{hg2}))\,\xi \ne 0

Proof. By ae_eq_zero_of_fourier_eq_zero, ae_ne_zero_of_analyticOnNhd, fourierL2_toLp_ae_eq. □\square

Used by fourierL2_Krep_ne_zero.

Lemma 427 (fourierL2_Krep_ne_zero).  source ↗

The Wiener nonvanishing for Krep. If the localized amplitude Krep m fS of a Schwartz wedge test fS is not a.e. zero, then the L² Fourier transform of its one-particle vector is ≠ 0 a.e. — the Wiener hypothesis of brick 7, ready to feed niceWedgeCyclic_of_fourier_ne_zero.

¬K m fS=[vol]0→∀(ξ:R),(F (toLp (K m fS) ⋯ )) ξ≠0\neg \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,\mathrm{fS} =[\mathrm{vol}] 0 \to \forall (\xi : \mathbb{R}), (\mathcal{F}\,(\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,\mathrm{fS})\,\cdots ))\,\xi \ne 0

Proof. By integrable_Krep, analyticOnNhd_fourier_Krep, fourierL2_toLp_ne_zero_of_ne_zero. □\square

Used by niceWedgeCyclic_bumpW.

← all sections · ← WedgeAnalyticity · GaussianMode →