Fock · section of the QIQT-H book
QIQTH.Fock.WedgeAnalyticity ← all sections · ← SchwartzDecay · WienerL2 →
Fock · entries 326–383 of 1000
Definition 326 (minkowskiDotℂ). source ↗
Complex Minkowski pairing p · x = p₀x₀ − p₁x₁ for a complex momentum p and a real point x.
η p x : = p 0 ⋅ ( x 0 ) − p 1 ⋅ ( x 1 ) \eta\,p\,x \;:=\; p\,0 \cdot (x\,0) - p\,1 \cdot (x\,1) η p x := p 0 ⋅ ( x 0 ) − p 1 ⋅ ( x 1 ) Used by KrepContminkowskiDotℂ_massShellℂ_ofRealKrepCont_ofRealkernelhasDerivAt_minkowskiDotℂ_massShellℂhasDerivAt_kernelcontinuous_kernel_in_xnorm_kernel_le
Definition 327 (massShellℂ). source ↗
The complexified mass shell p_m(ζ) = (m cosh ζ, m sinh ζ) (ℂ-valued momentum at complex rapidity ζ). On the real axis it is massShell m θ; it satisfies p_m(ζ+iπ) = −p_m(ζ).
M S m ζ : = ! [ m ⋅ c o s h ζ , m ⋅ s i n h ζ ] \mathrm{MS}\,m\,\zeta \;:=\; ![m \cdot \mathrm{cosh}\,\zeta , m \cdot \mathrm{sinh}\,\zeta] MS m ζ := ! [ m ⋅ cosh ζ , m ⋅ sinh ζ ] Used by KrepContmassShellℂ_ofRealmassShellℂ_add_pi_IminkowskiDotℂ_massShellℂ_ofRealKrepCont_ofRealkernelhasDerivAt_minkowskiDotℂ_massShellℂhasDerivAt_kernel
Definition 328 (KrepCont). source ↗
The analytically continued localized amplitude (K_ℂ f)(ζ) = 2^{-1/2}·∫ e^{−i·p_m(ζ)·x} f(x) dx.
Used by kmsFunkmsFun_ofRealkmsFun_sub_Idifferentiable_reflKrepContnorm_reflKrepCont_lederiv_reflKrepCont_eqnorm_deriv_reflKrepCont_ledifferentiable_kmsIntegrand
Lemma 329 (massShellℂ_ofReal). source ↗
On the real axis the complexified mass shell is the real one: p_m(θ) = massShell m θ (cast to ℂ).
M S m ( θ ) i = ( M S m θ i ) \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-massshell}{\mathrm{MS}}\,m\,(\theta)\,i = (\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-massshell}{\mathrm{MS}}\,m\,\theta\,i) MS m ( θ ) i = ( MS m θ i ) Proof. Immediate from the definitions. □ \square □
Used by minkowskiDotℂ_massShellℂ_ofReal
Lemma 330 (massShellℂ_add_pi_I). source ↗
The iπ-shift identity p_m(ζ + iπ) = −p_m(ζ) — the analytic engine of the boundary conjugation ψ_f(θ+iπ) = conj(ψ_f(θ)). Immediate from cosh(ζ+iπ)=−cosh ζ, sinh(ζ+iπ)=−sinh ζ.
M S m ( ζ + π ⋅ i ) = − M S m ζ \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-massshell}{\mathrm{MS}}\,m\,(\zeta + \pi \cdot i) = -\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-massshell}{\mathrm{MS}}\,m\,\zeta MS m ( ζ + π ⋅ i ) = − MS m ζ Proof. Immediate from the definitions. □ \square □
Used by kernel_add_pi_I
Lemma 331 (minkowskiDotℂ_massShellℂ_ofReal). source ↗
The complex pairing on the real-axis mass shell is the real pairing (cast to ℂ).
η ( M S m θ ) x = ( η ( M S m θ ) x ) \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-minkowskidot}{\eta}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-massshell}{\mathrm{MS}}\,m\,\theta)\,x = (\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskidot}{\eta}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-massshell}{\mathrm{MS}}\,m\,\theta)\,x) η ( MS m θ ) x = ( η ( MS m θ ) x ) Proof. By massShellℂ_ofReal□ \square □
Used by KrepCont_ofRealkernel_add_pi_I
Lemma 332 (KrepCont_ofReal). source ↗
A1a — real-axis agreement. The continued amplitude restricted to the real rapidity axis is the original localized amplitude: (K_ℂ f)(θ) = (K f)(θ).
K C m f θ = K m f θ \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,\theta = \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta K C m f θ = K m f θ Proof. By minkowskiDotmassShellminkowskiFourierminkowskiDotℂmassShellℂminkowskiDotℂ_massShellℂ_ofReal□ \square □
Used by kmsFun_ofRealkmsFunCut_ofRealKrepCont_add_pi_IKrep_addmemLp_KrepCont_affine_closed
Lemma 333 (cosh_ofReal_add_ofReal_mul_I). source ↗
cosh(θ + iλ) = cosh θ cos λ + i sinh θ sin λ (real/imaginary split at a complex rapidity).
c o s h ( θ + λ ⋅ i ) = ( cosh θ ⋅ cos λ ) + ( sinh θ ⋅ sin λ ) ⋅ i \mathrm{cosh}\,(\theta + \lambda \cdot i) = (\cosh\,\theta \cdot \cos\,\lambda) + (\sinh\,\theta \cdot \sin\,\lambda) \cdot i cosh ( θ + λ ⋅ i ) = ( cosh θ ⋅ cos λ ) + ( sinh θ ⋅ sin λ ) ⋅ i Proof. Immediate from the definitions. □ \square □
Used by norm_kernel_eq
Lemma 334 (sinh_ofReal_add_ofReal_mul_I). source ↗
sinh(θ + iλ) = sinh θ cos λ + i cosh θ sin λ.
s i n h ( θ + λ ⋅ i ) = ( sinh θ ⋅ cos λ ) + ( cosh θ ⋅ sin λ ) ⋅ i \mathrm{sinh}\,(\theta + \lambda \cdot i) = (\sinh\,\theta \cdot \cos\,\lambda) + (\cosh\,\theta \cdot \sin\,\lambda) \cdot i sinh ( θ + λ ⋅ i ) = ( sinh θ ⋅ cos λ ) + ( cosh θ ⋅ sin λ ) ⋅ i Proof. Immediate from the definitions. □ \square □
Used by norm_kernel_eq
Definition 335 (kernel). source ↗
The analytic-continuation kernel K(ζ, x) = exp(−i·p_m(ζ)·x).
k e r n e l m x ζ : = exp ( − i ⋅ η ( M S m ζ ) x ) \mathrm{kernel}\,m\,x\,\zeta \;:=\; \exp\,(-i \cdot \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-minkowskidot}{\eta}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-massshell}{\mathrm{MS}}\,m\,\zeta)\,x) kernel m x ζ := exp ( − i ⋅ η ( MS m ζ ) x ) Used by hasDerivAt_kernelkernelDerivhasDerivAt_kernel_mulcontinuous_kernel_in_xnorm_kernel_lenorm_kernelDeriv_lecontinuous_kernelDeriv_in_xhasDerivAt_KrepCont
Lemma 336 (hasDerivAt_minkowskiDotℂ_massShellℂ). source ↗
The ζ-derivative of the complex pairing p_m(ζ)·x = m coshζ·x₀ − m sinhζ·x₁ is m sinhζ·x₀ − m coshζ·x₁.
( λ ζ ↦ η ( M S m ζ ) x ) ′ ( ζ ) = m ⋅ s i n h ζ ⋅ ( x 0 ) − m ⋅ c o s h ζ ⋅ ( x 1 ) ({\lambda \zeta \mapsto \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-minkowskidot}{\eta}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-massshell}{\mathrm{MS}}\,m\,\zeta)\,x})'({\zeta})={m \cdot \mathrm{sinh}\,\zeta \cdot (x\,0) - m \cdot \mathrm{cosh}\,\zeta \cdot (x\,1)} ( λ ζ ↦ η ( MS m ζ ) x ) ′ ( ζ ) = m ⋅ sinh ζ ⋅ ( x 0 ) − m ⋅ cosh ζ ⋅ ( x 1 ) Proof. Immediate from the definitions. □ \square □
Used by hasDerivAt_kernel
Lemma 337 (hasDerivAt_kernel). source ↗
A1b (pointwise). For each x, the kernel ζ ↦ K(ζ,x) is complex-differentiable everywhere, with dK/dζ = K(ζ,x)·(−i·(m sinhζ·x₀ − m coshζ·x₁)) — the chain rule through exp. So for each fixed x the integrand is entire in the rapidity parameter (the per-x half of the dominated-convergence holomorphy argument).
( k e r n e l m x ) ′ ( ζ ) = k e r n e l m x ζ ⋅ ( − i ⋅ ( m ⋅ s i n h ζ ⋅ ( x 0 ) − m ⋅ c o s h ζ ⋅ ( x 1 ) ) ) ({\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x})'({\zeta})={\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,\zeta \cdot (-i \cdot (m \cdot \mathrm{sinh}\,\zeta \cdot (x\,0) - m \cdot \mathrm{cosh}\,\zeta \cdot (x\,1)))} ( kernel m x ) ′ ( ζ ) = kernel m x ζ ⋅ ( − i ⋅ ( m ⋅ sinh ζ ⋅ ( x 0 ) − m ⋅ cosh ζ ⋅ ( x 1 ))) Proof. By minkowskiDotℂmassShellℂhasDerivAt_minkowskiDotℂ_massShellℂ□ \square □
Used by hasDerivAt_kernel_mul
Definition 338 (kernelDeriv). source ↗
The integrand-derivative value K'(ζ,x) = K(ζ,x)·(−i·(m sinhζ·x₀ − m coshζ·x₁)).
K ′ m x ζ : = k e r n e l m x ζ ⋅ ( − i ⋅ ( m ⋅ s i n h ζ ⋅ ( x 0 ) − m ⋅ c o s h ζ ⋅ ( x 1 ) ) ) \mathrm{K}'\,m\,x\,\zeta \;:=\; \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,\zeta \cdot (-i \cdot (m \cdot \mathrm{sinh}\,\zeta \cdot (x\,0) - m \cdot \mathrm{cosh}\,\zeta \cdot (x\,1))) K ′ m x ζ := kernel m x ζ ⋅ ( − i ⋅ ( m ⋅ sinh ζ ⋅ ( x 0 ) − m ⋅ cosh ζ ⋅ ( x 1 ))) Used by hasDerivAt_kernel_mulnorm_kernelDeriv_lecontinuous_kernelDeriv_in_xhasDerivAt_KrepContdifferentiable_KrepContderiv_KrepCont_eqnorm_kernelDeriv_le_exp_decaynorm_deriv_KrepCont_le_exp_decay
Lemma 339 (hasDerivAt_kernel_mul). source ↗
The full integrand ζ ↦ K(ζ,x)·f(x) is complex-differentiable, derivative K'(ζ,x)·f(x) (the h_diff ingredient for the dominated parametric-derivative assembly).
( λ ζ ↦ k e r n e l m x ζ ⋅ f x ) ′ ( ζ ) = K ′ m x ζ ⋅ f x ({\lambda \zeta \mapsto \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,\zeta \cdot f\,x})'({\zeta})={\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernelderiv}{\mathrm{K}{}'}\,m\,x\,\zeta \cdot f\,x} ( λ ζ ↦ kernel m x ζ ⋅ f x ) ′ ( ζ ) = K ′ m x ζ ⋅ f x Proof. By hasDerivAt_kernel□ \square □
Used by hasDerivAt_KrepCont
Lemma 340 (continuous_kernel_in_x). source ↗
The kernel is continuous in x (for fixed ζ) — gives ae-strong-measurability of the integrand.
C o n t i n u o u s λ x ↦ k e r n e l m x ζ \mathrm{Continuous}\,\lambda x \mapsto \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,\zeta Continuous λ x ↦ kernel m x ζ Proof. By minkowskiDotℂmassShellℂ□ \square □
Used by continuous_kernelDeriv_in_xhasDerivAt_KrepContKrepCont_add
Lemma 341 (norm_exp_le_exp_norm). source ↗
‖exp z‖ ≤ e^{‖z‖} and ‖exp(−z)‖ ≤ e^{‖z‖} (from ‖exp z‖ = e^{Re z} and ±Re z ≤ ‖z‖).
∥ exp z ∥ ≤ exp ∥ z ∥ \|\exp\,z\| \le \exp\,\|z\| ∥ exp z ∥ ≤ exp ∥ z ∥ Proof. Immediate from the definitions. □ \square □
Used by norm_exp_neg_le_exp_normnorm_cosh_lenorm_sinh_lenorm_kernel_le
Lemma 342 (norm_exp_neg_le_exp_norm). source ↗
∥ exp ( − z ) ∥ ≤ exp ∥ z ∥ \|\exp\,(-z)\| \le \exp\,\|z\| ∥ exp ( − z ) ∥ ≤ exp ∥ z ∥ Proof. By norm_exp_le_exp_norm□ \square □
Used by norm_cosh_lenorm_sinh_le
Lemma 343 (norm_cosh_le). source ↗
‖cosh ζ‖ ≤ e^{‖ζ‖} (crude growth bound from cosh ζ = (e^ζ + e^{−ζ})/2).
∥ c o s h ζ ∥ ≤ exp ∥ ζ ∥ \|\mathrm{cosh}\,\zeta\| \le \exp\,\|\zeta\| ∥ cosh ζ ∥ ≤ exp ∥ ζ ∥ Proof. By norm_exp_le_exp_normnorm_exp_neg_le_exp_norm□ \square □
Used by norm_kernel_lenorm_kernelDeriv_le
Lemma 344 (norm_cosh_le_cosh_re). source ↗
‖cosh ζ‖ ≤ cosh(Re ζ) (sharp real-part bound, ‖e^{±ζ}‖ = e^{±Re ζ}).
∥ c o s h ζ ∥ ≤ cosh ζ . r e \|\mathrm{cosh}\,\zeta\| \le \cosh\,\zeta.\mathrm{re} ∥ cosh ζ ∥ ≤ cosh ζ . re Proof. Immediate from the definitions. □ \square □
Used by norm_kernelDeriv_le_exp_decay
Lemma 345 (norm_sinh_le_cosh_re). source ↗
‖sinh ζ‖ ≤ cosh(Re ζ) (sharp real-part bound).
∥ s i n h ζ ∥ ≤ cosh ζ . r e \|\mathrm{sinh}\,\zeta\| \le \cosh\,\zeta.\mathrm{re} ∥ sinh ζ ∥ ≤ cosh ζ . re Proof. Immediate from the definitions. □ \square □
Used by norm_kernelDeriv_le_exp_decay
Lemma 346 (norm_sinh_le). source ↗
‖sinh ζ‖ ≤ e^{‖ζ‖} (crude growth bound from sinh ζ = (e^ζ − e^{−ζ})/2).
∥ s i n h ζ ∥ ≤ exp ∥ ζ ∥ \|\mathrm{sinh}\,\zeta\| \le \exp\,\|\zeta\| ∥ sinh ζ ∥ ≤ exp ∥ ζ ∥ Proof. By norm_exp_le_exp_normnorm_exp_neg_le_exp_norm□ \square □
Used by norm_kernel_lenorm_kernelDeriv_le
Lemma 347 (norm_term_le). source ↗
A bound for a term (m·c)·a − (m·s)·b with ‖c‖,‖s‖ ≤ e^r: ≤ |m|·e^r·(|a|+|b|). Used for both the pairing p_m(ζ)·x (c,s = cosh,sinh) and its ζ-derivative (c,s = sinh,cosh).
∥ c ∥ ≤ exp r → ∥ s ∥ ≤ exp r → ∀ ( a b : R ) , ∥ m ⋅ c ⋅ a − m ⋅ s ⋅ b ∥ ≤ ∣ m ∣ ⋅ exp r ⋅ ( ∣ a ∣ + ∣ b ∣ ) \|c\| \le \exp\,r \to \|s\| \le \exp\,r \to \forall (a b : \mathbb{R}), \|m \cdot c \cdot a - m \cdot s \cdot b\| \le |m| \cdot \exp\,r \cdot (|a| + |b|) ∥ c ∥ ≤ exp r → ∥ s ∥ ≤ exp r → ∀ ( ab : R ) , ∥ m ⋅ c ⋅ a − m ⋅ s ⋅ b ∥ ≤ ∣ m ∣ ⋅ exp r ⋅ ( ∣ a ∣ + ∣ b ∣ ) Proof. Immediate from the definitions. □ \square □
Used by norm_kernel_lenorm_kernelDeriv_le
Lemma 348 (norm_kernel_le). source ↗
‖K(ζ,x)‖ ≤ exp(|m|·e^{‖ζ‖}·(|x₀|+|x₁|)) (kernel growth bound; ‖exp(−i·D)‖ ≤ exp‖D‖, ‖D‖ bound).
∥ k e r n e l m x ζ ∥ ≤ exp ( ∣ m ∣ ⋅ exp ∥ ζ ∥ ⋅ ( ∣ x 0 ∣ + ∣ x 1 ∣ ) ) \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,\zeta\| \le \exp\,(|m| \cdot \exp\,\|\zeta\| \cdot (|x\,0| + |x\,1|)) ∥ kernel m x ζ ∥ ≤ exp ( ∣ m ∣ ⋅ exp ∥ ζ ∥ ⋅ ( ∣ x 0∣ + ∣ x 1∣ )) Proof. By minkowskiDotℂmassShellℂnorm_exp_le_exp_normnorm_cosh_lenorm_sinh_lenorm_term_le□ \square □
Used by norm_kernelDeriv_le
Lemma 349 (norm_kernelDeriv_le). source ↗
‖K'(ζ,x)‖ ≤ exp(B)·B with B = |m|·e^{‖ζ‖}·(|x₀|+|x₁|) (the integrand-derivative growth bound).
∥ K ′ m x ζ ∥ ≤ exp ( ∣ m ∣ ⋅ exp ∥ ζ ∥ ⋅ ( ∣ x 0 ∣ + ∣ x 1 ∣ ) ) ⋅ ( ∣ m ∣ ⋅ exp ∥ ζ ∥ ⋅ ( ∣ x 0 ∣ + ∣ x 1 ∣ ) ) \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernelderiv}{\mathrm{K}{}'}\,m\,x\,\zeta\| \le \exp\,(|m| \cdot \exp\,\|\zeta\| \cdot (|x\,0| + |x\,1|)) \cdot (|m| \cdot \exp\,\|\zeta\| \cdot (|x\,0| + |x\,1|)) ∥ K ′ m x ζ ∥ ≤ exp ( ∣ m ∣ ⋅ exp ∥ ζ ∥ ⋅ ( ∣ x 0∣ + ∣ x 1∣ )) ⋅ ( ∣ m ∣ ⋅ exp ∥ ζ ∥ ⋅ ( ∣ x 0∣ + ∣ x 1∣ )) Proof. By kernelnorm_cosh_lenorm_sinh_lenorm_term_lenorm_kernel_le□ \square □
Used by hasDerivAt_KrepCont
Lemma 350 (continuous_kernelDeriv_in_x). source ↗
The integrand-derivative is continuous in x (for fixed ζ) — gives measurability.
C o n t i n u o u s λ x ↦ K ′ m x ζ \mathrm{Continuous}\,\lambda x \mapsto \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernelderiv}{\mathrm{K}{}'}\,m\,x\,\zeta Continuous λ x ↦ K ′ m x ζ Proof. By kernelcontinuous_kernel_in_x□ \square □
Used by hasDerivAt_KrepCont
Lemma 351 (hasDerivAt_KrepCont). source ↗
A1b-ii-β — holomorphy of KrepCont. For f continuous with compact support, ζ ↦ KrepCont m f ζ is complex-differentiable at every ζ₀, with derivative (1/√2)·∫ K'(ζ₀,x)·f(x). Proven by the dominated parametric-derivative theorem (𝕜 = ℂ): the per-x derivative is hasDerivAt_kernel_mul, and the ball-domination uses norm_kernelDeriv_le + the compact bound ‖x‖ ≤ M on tsupport f.
C o n t i n u o u s f → H a s C o m p a c t S u p p o r t f → ∀ ( ζ 0 : C ) , ( K C m f ) ′ ( ζ 0 ) = 1 / 2 ⋅ ∫ ( x : V ) , K ′ m x ζ 0 ⋅ f x \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \forall (\zeta_{0} : \mathbb{C}), ({\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f})'({\zeta_{0}})={1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernelderiv}{\mathrm{K}{}'}\,m\,x\,\zeta_{0} \cdot f\,x} Continuous f → HasCompactSupport f → ∀ ( ζ 0 : C ) , ( K C m f ) ′ ( ζ 0 ) = 1/ 2 ⋅ ∫ ( x : V ) , K ′ m x ζ 0 ⋅ f x Proof. By kernelhasDerivAt_kernel_mulcontinuous_kernel_in_xnorm_kernelDeriv_lecontinuous_kernelDeriv_in_x□ \square □
Used by differentiable_KrepContderiv_KrepCont_eq
Lemma 352 (differentiable_KrepCont). source ↗
A1b — KrepCont m f is entire for f continuous with compact support.
C o n t i n u o u s f → H a s C o m p a c t S u p p o r t f → D i f f e r e n t i a b l e C ( K C m f ) \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Differentiable}\,\mathbb{C}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f) Continuous f → HasCompactSupport f → Differentiable C ( K C m f ) Proof. By kernelDerivhasDerivAt_KrepCont□ \square □
Used by differentiable_reflKrepContderiv_reflKrepCont_eqdifferentiable_kmsIntegrandhasDerivAt_kmsIntegrand_zcontinuous_kmsIntegrand_in_thetacontinuous_kmsIntegrand_deriv_in_thetacontinuous_deriv_KrepContmemLp_KrepCont_affine
Lemma 353 (continuous_deriv_KrepCont). source ↗
deriv (KrepCont m f) is continuousAnalyticAt.deriv). The measurability ingredient (hF'_meas) for the dominated-derivative theorem.
C o n t i n u o u s f → H a s C o m p a c t S u p p o r t f → C o n t i n u o u s ( D ( K C m f ) ) \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,(\mathrm{D}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f)) Continuous f → HasCompactSupport f → Continuous ( D ( K C m f )) Proof. By differentiable_KrepCont□ \square □
Used by continuous_kmsIntegrand_deriv_in_theta
Lemma 354 (deriv_KrepCont_eq). source ↗
The rapidity-derivative of KrepCont m f as an integral: (K_ℂ f)'(ζ) = 2^{-1/2}·∫ K'(ζ,x)·f(x) dx.
C o n t i n u o u s f → H a s C o m p a c t S u p p o r t f → ∀ ( ζ : C ) , D ( K C m f ) ζ = 1 / 2 ⋅ ∫ ( x : V ) , K ′ m x ζ ⋅ f x \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \forall (\zeta : \mathbb{C}), \mathrm{D}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f)\,\zeta = 1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernelderiv}{\mathrm{K}{}'}\,m\,x\,\zeta \cdot f\,x Continuous f → HasCompactSupport f → ∀ ( ζ : C ) , D ( K C m f ) ζ = 1/ 2 ⋅ ∫ ( x : V ) , K ′ m x ζ ⋅ f x Proof. By hasDerivAt_KrepCont□ \square □
Used by norm_deriv_KrepCont_le_exp_decay
Lemma 355 (kernel_add_pi_I). source ↗
The kernel’s iπ-boundary conjugation: K(θ+iπ, x) = conj(K(θ, x)). Engine: p_m(θ+iπ) = −p_m(θ) and p_m(θ)·x real, so exp(−i·(−p_m(θ)·x)) = conj(exp(−i·p_m(θ)·x)).
k e r n e l m x ( θ + π ⋅ i ) = ( s t a r R i n g E n d C ) ( k e r n e l m x θ ) \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,(\theta + \pi \cdot i) = (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,\theta) kernel m x ( θ + π ⋅ i ) = ( starRingEnd C ) ( kernel m x θ ) Proof. By minkowskiDotmassShellminkowskiDotℂmassShellℂmassShellℂ_add_pi_IminkowskiDotℂ_massShellℂ_ofReal□ \square □
Used by KrepCont_add_pi_I
Lemma 356 (KrepCont_add_pi_I). source ↗
A3 — boundary conjugation of the continued amplitude. For real f, ψ_f(θ+iπ) = conj(ψ_f(θ)) (= conj(Krep m f θ)). This is the relation that turns the top edge ⟪η, V_t ξ⟫ into the KMS bottom edge ⟪V_t ξ, η⟫.
( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( f x ) = f x ) → ∀ ( θ : R ) , K C m f ( θ + π ⋅ i ) = ( s t a r R i n g E n d C ) ( K m f θ ) (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(f\,x) = f\,x) \to \forall (\theta : \mathbb{R}), \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta + \pi \cdot i) = (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta) ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ∀ ( θ : R ) , K C m f ( θ + π ⋅ i ) = ( starRingEnd C ) ( K m f θ ) Proof. By minkowskiDotℂmassShellℂKrepCont_ofRealkernel_add_pi_I□ \square □
Used by kmsFun_sub_IkmsFunCut_sub_ImemLp_KrepCont_affine_closed
Lemma 357 (sq_div_eight_le_cosh). source ↗
θ²/8 ≤ cosh θ — a crude quadratic lower bound (cosh θ ≥ e^{|θ|}/2 ≥ (1+|θ|/2)²/2 ≥ θ²/8), the comparison feeding the Gaussian domination of the wedge-mode strip decay.
θ 2 / 8 ≤ cosh θ {\theta}^{2} / 8 \le \cosh\,\theta θ 2 /8 ≤ cosh θ Proof. Immediate from the definitions. □ \square □
Used by integrable_exp_neg_const_mul_cosh
Lemma 358 (integrable_exp_neg_const_mul_cosh). source ↗
A2 (decay building block). θ ↦ exp(−c·cosh θ) is integrable over ℝ for c > 0 — by Gaussian domination exp(−c cosh θ) ≤ exp(−(c/8)·θ²) (sq_div_eight_le_cosh). The θ-integrability that the interior-λ strip decay of the wedge mode reduces to (the damping exponent is ∝ −cosh θ).
0 < c → I n t e g r a b l e ( λ θ ↦ exp ( − ( c ⋅ cosh θ ) ) ) v o l 0 < c \to \mathrm{Integrable}\,(\lambda \theta \mapsto \exp\,(-(c \cdot \cosh\,\theta)))\,\mathrm{vol} 0 < c → Integrable ( λ θ ↦ exp ( − ( c ⋅ cosh θ ))) vol Proof. By sq_div_eight_le_cosh□ \square □
Used by integrable_kmsIntegrandintegrable_cosh_mul_exp_neg_const_mul_coshmemLp_KrepCont_affine
Lemma 359 (abs_sinh_le_cosh). source ↗
|sinh θ| ≤ cosh θ (cosh±sinh = e^{±θ} ≥ 0).
∣ sinh θ ∣ ≤ cosh θ |\sinh\,\theta| \le \cosh\,\theta ∣ sinh θ ∣ ≤ cosh θ Proof. Immediate from the definitions. □ \square □
Used by cosh_add_le_exp_abs_mulexp_neg_abs_mul_le_cosh_add
Lemma 360 (cosh_add_abs_sinh). source ↗
cosh s + |sinh s| = e^{|s|} and cosh s − |sinh s| = e^{−|s|}.
cosh s + ∣ sinh s ∣ = exp ∣ s ∣ \cosh\,s + |\sinh\,s| = \exp\,|s| cosh s + ∣ sinh s ∣ = exp ∣ s ∣ Proof. Immediate from the definitions. □ \square □
Used by cosh_add_le_exp_abs_mul
Lemma 361 (cosh_sub_abs_sinh). source ↗
cosh s − ∣ sinh s ∣ = exp ( − ∣ s ∣ ) \cosh\,s - |\sinh\,s| = \exp\,(-|s|) cosh s − ∣ sinh s ∣ = exp ( − ∣ s ∣ ) Proof. Immediate from the definitions. □ \square □
Used by exp_neg_abs_mul_le_cosh_add
Lemma 362 (cosh_add_le_exp_abs_mul). source ↗
cosh(θ+s) ≤ e^{|s|}·cosh θ
cosh ( θ + s ) ≤ exp ∣ s ∣ ⋅ cosh θ \cosh\,(\theta + s) \le \exp\,|s| \cdot \cosh\,\theta cosh ( θ + s ) ≤ exp ∣ s ∣ ⋅ cosh θ Proof. By abs_sinh_le_coshcosh_add_abs_sinh□ \square □
Used by cosh_shift_exp_le
Lemma 363 (exp_neg_abs_mul_le_cosh_add). source ↗
e^{−|s|}·cosh θ ≤ cosh(θ+s)
exp ( − ∣ s ∣ ) ⋅ cosh θ ≤ cosh ( θ + s ) \exp\,(-|s|) \cdot \cosh\,\theta \le \cosh\,(\theta + s) exp ( − ∣ s ∣ ) ⋅ cosh θ ≤ cosh ( θ + s ) Proof. By abs_sinh_le_coshcosh_sub_abs_sinh□ \square □
Used by cosh_shift_exp_le
Lemma 364 (sin_neg_pi_mul_pos). source ↗
0 < sin(−π·w) for −1 < w < 0 (the decay rate σ = sin(−π·Im z) is positive on the open strip).
− 1 < w → w < 0 → 0 < sin ( − ( π ⋅ w ) ) -1 < w \to w < 0 \to 0 < \sin\,(-(\pi \cdot w)) − 1 < w → w < 0 → 0 < sin ( − ( π ⋅ w )) Proof. Immediate from the definitions. □ \square □
Used by integrable_kmsIntegrandexists_sin_minnorm_term1_lenorm_term2_le
Lemma 365 (cosh_shift_exp_le). source ↗
The shifted cosh·exp made uniform. For |s| ≤ S, 0 < c₀ ≤ c: cosh(θ+s)·exp(−c·cosh(θ+s)) ≤ e^S·cosh θ·exp(−c₀·e^{−S}·cosh θ). The core estimate that turns the shifting-peak strip decay (s = πRe z over a z-ball) into a z-uniform integrable-in-θ bound.
∣ s ∣ ≤ S → 0 < c 0 → c 0 ≤ c → cosh ( θ + s ) ⋅ exp ( − ( c ⋅ cosh ( θ + s ) ) ) ≤ exp S ⋅ cosh θ ⋅ exp ( − ( c 0 ⋅ exp ( − S ) ⋅ cosh θ ) ) |s| \le S \to 0 < c_{0} \to c_{0} \le c \to \cosh\,(\theta + s) \cdot \exp\,(-(c \cdot \cosh\,(\theta + s))) \le \exp\,S \cdot \cosh\,\theta \cdot \exp\,(-(c_{0} \cdot \exp\,(-S) \cdot \cosh\,\theta)) ∣ s ∣ ≤ S → 0 < c 0 → c 0 ≤ c → cosh ( θ + s ) ⋅ exp ( − ( c ⋅ cosh ( θ + s ))) ≤ exp S ⋅ cosh θ ⋅ exp ( − ( c 0 ⋅ exp ( − S ) ⋅ cosh θ )) Proof. By cosh_add_le_exp_abs_mulexp_neg_abs_mul_le_cosh_add□ \square □
Used by prod_norm_bound_cosh_shift
Lemma 366 (prod_norm_bound_cosh_shift). source ↗
The h_bound core estimate. A cosh(θ+s)·exp(−c·cosh(θ+s))-decaying factor (na) times a bounded factor (nb ≤ Cb), made z-uniform: na·nb ≤ Cd·Cb·(e^S·cosh θ·exp(−c₀·e^{−S}·cosh θ)). Both terms of the kmsFun integrand z-derivative reduce to this (via the four factor bounds + cosh_shift_exp_le).
n a ≤ C d ⋅ ( cosh ( θ + s ) ⋅ exp ( − ( c ⋅ cosh ( θ + s ) ) ) ) → n b ≤ C b → 0 ≤ n b → 0 ≤ C b → 0 ≤ C d → ∣ s ∣ ≤ S → 0 < c 0 → c 0 ≤ c → n a ⋅ n b ≤ C d ⋅ C b ⋅ ( exp S ⋅ cosh θ ⋅ exp ( − ( c 0 ⋅ exp ( − S ) ⋅ cosh θ ) ) ) \mathrm{na} \le \mathrm{Cd} \cdot (\cosh\,(\theta + s) \cdot \exp\,(-(c \cdot \cosh\,(\theta + s)))) \to \mathrm{nb} \le \mathrm{Cb} \to 0 \le \mathrm{nb} \to 0 \le \mathrm{Cb} \to 0 \le \mathrm{Cd} \to |s| \le S \to 0 < c_{0} \to c_{0} \le c \to \mathrm{na} \cdot \mathrm{nb} \le \mathrm{Cd} \cdot \mathrm{Cb} \cdot (\exp\,S \cdot \cosh\,\theta \cdot \exp\,(-(c_{0} \cdot \exp\,(-S) \cdot \cosh\,\theta))) na ≤ Cd ⋅ ( cosh ( θ + s ) ⋅ exp ( − ( c ⋅ cosh ( θ + s )))) → nb ≤ Cb → 0 ≤ nb → 0 ≤ Cb → 0 ≤ Cd → ∣ s ∣ ≤ S → 0 < c 0 → c 0 ≤ c → na ⋅ nb ≤ Cd ⋅ Cb ⋅ ( exp S ⋅ cosh θ ⋅ exp ( − ( c 0 ⋅ exp ( − S ) ⋅ cosh θ ))) Proof. By cosh_shift_exp_le□ \square □
Used by norm_term1_lenorm_term2_le
Lemma 367 (integrable_cosh_mul_exp_neg_const_mul_cosh). source ↗
A2 (derivative-decay building block). s ↦ cosh s·exp(−c·cosh s) is integrable over ℝ for c > 0. The integrand-derivative bound (‖kernelDeriv‖ ≲ cosh(s)·exp(−c·cosh s), the cosh polynomial factor against the double-exponential damping) reduces to this. Via cosh s ≤ (1/c)·exp((c/2)cosh s) (Real.two_mul_le_exp) ⟹ cosh s·exp(−c cosh s) ≤ (1/c)·exp(−(c/2)cosh s).
0 < c → I n t e g r a b l e ( λ s ↦ cosh s ⋅ exp ( − ( c ⋅ cosh s ) ) ) v o l 0 < c \to \mathrm{Integrable}\,(\lambda s \mapsto \cosh\,s \cdot \exp\,(-(c \cdot \cosh\,s)))\,\mathrm{vol} 0 < c → Integrable ( λ s ↦ cosh s ⋅ exp ( − ( c ⋅ cosh s ))) vol Proof. By integrable_exp_neg_const_mul_cosh□ \square □
Used by kmsFun_differentiableAtkmsFunCut_differentiableAt
Lemma 368 (norm_kernel_eq). source ↗
The exact kernel modulus on the strip: ‖K(θ+iλ,x)‖ = exp(m sinλ·(sinhθ·x₀ − coshθ·x₁)).
∥ k e r n e l m x ( θ + λ ⋅ i ) ∥ = exp ( m ⋅ sin λ ⋅ ( sinh θ ⋅ x 0 − cosh θ ⋅ x 1 ) ) \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,(\theta + \lambda \cdot i)\| = \exp\,(m \cdot \sin\,\lambda \cdot (\sinh\,\theta \cdot x\,0 - \cosh\,\theta \cdot x\,1)) ∥ kernel m x ( θ + λ ⋅ i ) ∥ = exp ( m ⋅ sin λ ⋅ ( sinh θ ⋅ x 0 − cosh θ ⋅ x 1 )) Proof. By minkowskiDotℂmassShellℂcosh_ofReal_add_ofReal_mul_Isinh_ofReal_add_ofReal_mul_I□ \square □
Used by norm_kernel_eq'norm_kernel_le_exp_decay
Lemma 369 (norm_kernel_eq'). source ↗
The exact kernel modulus at a general complex ζ: ‖K(ζ,x)‖ = exp(m sin(Im ζ)·(sinh(Re ζ)·x₀ − cosh(Re ζ)·x₁)) (rewrite ζ = Re ζ + i·Im ζ, then norm_kernel_eq).
∥ k e r n e l m x ζ ∥ = exp ( m ⋅ sin ζ . i m ⋅ ( sinh ζ . r e ⋅ x 0 − cosh ζ . r e ⋅ x 1 ) ) \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,\zeta\| = \exp\,(m \cdot \sin\,\zeta.\mathrm{im} \cdot (\sinh\,\zeta.\mathrm{re} \cdot x\,0 - \cosh\,\zeta.\mathrm{re} \cdot x\,1)) ∥ kernel m x ζ ∥ = exp ( m ⋅ sin ζ . im ⋅ ( sinh ζ . re ⋅ x 0 − cosh ζ . re ⋅ x 1 )) Proof. By norm_kernel_eq□ \square □
Used by norm_kernel_le_exp_decay'
Lemma 370 (norm_kernel_le_exp_decay). source ↗
Pointwise strip-decay of the kernel. For x with wedge margin δ (δ ≤ x₁∓x₀) and 0≤λ≤π, ‖K(θ+iλ,x)‖ ≤ exp(−(m sinλ δ)·coshθ) — double-exponential decay in θ for interior λ.
0 ≤ m → ∀ { x : V } { δ : R } , δ ≤ x 1 − x 0 → δ ≤ x 1 + x 0 → ∀ { θ λ : R } , 0 ≤ λ → λ ≤ π → ∥ k e r n e l m x ( θ + λ ⋅ i ) ∥ ≤ exp ( − ( m ⋅ sin λ ⋅ δ ) ⋅ cosh θ ) 0 \le m \to \forall \{x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}\} \{\delta : \mathbb{R}\}, \delta \le x\,1 - x\,0 \to \delta \le x\,1 + x\,0 \to \forall \{\theta \lambda : \mathbb{R}\}, 0 \le \lambda \to \lambda \le \pi \to \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,(\theta + \lambda \cdot i)\| \le \exp\,(-(m \cdot \sin\,\lambda \cdot \delta) \cdot \cosh\,\theta) 0 ≤ m → ∀ { x : V } { δ : R } , δ ≤ x 1 − x 0 → δ ≤ x 1 + x 0 → ∀ { θ λ : R } , 0 ≤ λ → λ ≤ π → ∥ kernel m x ( θ + λ ⋅ i ) ∥ ≤ exp ( − ( m ⋅ sin λ ⋅ δ ) ⋅ cosh θ ) Proof. By norm_kernel_eq□ \square □
Used by norm_KrepCont_le_exp_decay
Lemma 371 (norm_kernel_le_exp_decay'). source ↗
Pointwise strip-decay of the kernel at a general ζ (0 ≤ Im ζ ≤ π, x with wedge margin δ): ‖K(ζ,x)‖ ≤ exp(−(m sin(Im ζ) δ)·cosh(Re ζ)). The general-ζ form powering the z-derivative decay.
0 ≤ m → ∀ { x : V } { δ : R } , δ ≤ x 1 − x 0 → δ ≤ x 1 + x 0 → ∀ { ζ : C } , 0 ≤ ζ . i m → ζ . i m ≤ π → ∥ k e r n e l m x ζ ∥ ≤ exp ( − ( m ⋅ sin ζ . i m ⋅ δ ) ⋅ cosh ζ . r e ) 0 \le m \to \forall \{x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}\} \{\delta : \mathbb{R}\}, \delta \le x\,1 - x\,0 \to \delta \le x\,1 + x\,0 \to \forall \{\zeta : \mathbb{C}\}, 0 \le \zeta.\mathrm{im} \to \zeta.\mathrm{im} \le \pi \to \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernel}{\mathrm{kernel}}\,m\,x\,\zeta\| \le \exp\,(-(m \cdot \sin\,\zeta.\mathrm{im} \cdot \delta) \cdot \cosh\,\zeta.\mathrm{re}) 0 ≤ m → ∀ { x : V } { δ : R } , δ ≤ x 1 − x 0 → δ ≤ x 1 + x 0 → ∀ { ζ : C } , 0 ≤ ζ . im → ζ . im ≤ π → ∥ kernel m x ζ ∥ ≤ exp ( − ( m ⋅ sin ζ . im ⋅ δ ) ⋅ cosh ζ . re ) Proof. By norm_kernel_eq'□ \square □
Used by norm_kernelDeriv_le_exp_decay
Lemma 372 (norm_kernelDeriv_le_exp_decay). source ↗
Pointwise strip-decay of kernelDeriv at a general ζ : ‖K'(ζ,x)‖ ≤ exp(−c·cosh(Re ζ))·|m|· cosh(Re ζ)·(|x₀|+|x₁|) (c = m sin(Im ζ) δ). Kernel decay (norm_kernel_le_exp_decay') × poly bound (‖poly‖ ≤ |m|·cosh(Re ζ)·(|x₀|+|x₁|) via norm_sinh/cosh_le_cosh_re). The cosh(Re ζ) polynomial factor against the double-exponential damping — the integrand of the z-derivative domination.
0 ≤ m → ∀ { x : V } { δ : R } , δ ≤ x 1 − x 0 → δ ≤ x 1 + x 0 → ∀ { ζ : C } , 0 ≤ ζ . i m → ζ . i m ≤ π → ∥ K ′ m x ζ ∥ ≤ exp ( − ( m ⋅ sin ζ . i m ⋅ δ ) ⋅ cosh ζ . r e ) ⋅ ( ∣ m ∣ ⋅ cosh ζ . r e ⋅ ( ∣ x 0 ∣ + ∣ x 1 ∣ ) ) 0 \le m \to \forall \{x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}\} \{\delta : \mathbb{R}\}, \delta \le x\,1 - x\,0 \to \delta \le x\,1 + x\,0 \to \forall \{\zeta : \mathbb{C}\}, 0 \le \zeta.\mathrm{im} \to \zeta.\mathrm{im} \le \pi \to \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-kernelderiv}{\mathrm{K}{}'}\,m\,x\,\zeta\| \le \exp\,(-(m \cdot \sin\,\zeta.\mathrm{im} \cdot \delta) \cdot \cosh\,\zeta.\mathrm{re}) \cdot (|m| \cdot \cosh\,\zeta.\mathrm{re} \cdot (|x\,0| + |x\,1|)) 0 ≤ m → ∀ { x : V } { δ : R } , δ ≤ x 1 − x 0 → δ ≤ x 1 + x 0 → ∀ { ζ : C } , 0 ≤ ζ . im → ζ . im ≤ π → ∥ K ′ m x ζ ∥ ≤ exp ( − ( m ⋅ sin ζ . im ⋅ δ ) ⋅ cosh ζ . re ) ⋅ ( ∣ m ∣ ⋅ cosh ζ . re ⋅ ( ∣ x 0∣ + ∣ x 1∣ )) Proof. By kernelnorm_cosh_le_cosh_renorm_sinh_le_cosh_renorm_kernel_le_exp_decay'□ \square □
Used by norm_deriv_KrepCont_le_exp_decay
Lemma 373 (norm_KrepCont_le_exp_decay). source ↗
A2 (step 1) — pointwise strip-decay of the continued amplitude. For wedge-supported f (uniform margin δ via exists_wedge_margin) and 0≤λ≤π, ‖KrepCont m f (θ+iλ)‖ ≤ (1/√2)·(∫‖f‖)·exp(−(m sinλ δ)·coshθ). The decay factor (double-exponential in θ for interior λ) is what makes KrepCont m f (·+iλ) ∈ L².
0 ≤ m → ∀ { f : V → C } , C o n t i n u o u s f → H a s C o m p a c t S u p p o r t f → ∀ { δ : R } , ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { θ λ : R } , 0 ≤ λ → λ ≤ π → ∥ K C m f ( θ + λ ⋅ i ) ∥ ≤ ( 1 / 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ ) ⋅ exp ( − ( m ⋅ sin λ ⋅ δ ) ⋅ cosh θ ) 0 \le m \to \forall \{f : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \forall \{\delta : \mathbb{R}\}, (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), f\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{\theta \lambda : \mathbb{R}\}, 0 \le \lambda \to \lambda \le \pi \to \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta + \lambda \cdot i)\| \le (1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|f\,x\|) \cdot \exp\,(-(m \cdot \sin\,\lambda \cdot \delta) \cdot \cosh\,\theta) 0 ≤ m → ∀ { f : V → C } , Continuous f → HasCompactSupport f → ∀ { δ : R } , ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { θ λ : R } , 0 ≤ λ → λ ≤ π → ∥ K C m f ( θ + λ ⋅ i ) ∥ ≤ ( 1/ 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ ) ⋅ exp ( − ( m ⋅ sin λ ⋅ δ ) ⋅ cosh θ ) Proof. By minkowskiDotℂmassShellℂkernelnorm_kernel_le_exp_decay□ \square □
Used by norm_KrepCont_le_exp_decay_gen
Lemma 374 (norm_deriv_KrepCont_le_exp_decay). source ↗
Pointwise strip-decay of deriv KrepCont. For wedge-supported f (margin δ) and 0≤Im ζ≤π, ‖deriv(KrepCont m f) ζ‖ ≤ (1/√2)·|m|·cosh(Re ζ)·exp(−c·cosh(Re ζ))·∫(|x₀|+|x₁|)‖f‖ (c=m sin(Im ζ)δ). The z-derivative norm bound: cosh(Re ζ)·exp(−c·cosh(Re ζ)) decay (× a finite constant).
0 ≤ m → ∀ { f : V → C } , C o n t i n u o u s f → H a s C o m p a c t S u p p o r t f → ∀ { δ : R } , ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { ζ : C } , 0 ≤ ζ . i m → ζ . i m ≤ π → ∥ D ( K C m f ) ζ ∥ ≤ 1 / 2 ⋅ ( ∣ m ∣ ⋅ cosh ζ . r e ⋅ exp ( − ( m ⋅ sin ζ . i m ⋅ δ ) ⋅ cosh ζ . r e ) ⋅ ∫ ( x : V ) , ( ∣ x 0 ∣ + ∣ x 1 ∣ ) ⋅ ∥ f x ∥ ) 0 \le m \to \forall \{f : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \forall \{\delta : \mathbb{R}\}, (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), f\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{\zeta : \mathbb{C}\}, 0 \le \zeta.\mathrm{im} \to \zeta.\mathrm{im} \le \pi \to \|\mathrm{D}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f)\,\zeta\| \le 1 / \sqrt 2 \cdot (|m| \cdot \cosh\,\zeta.\mathrm{re} \cdot \exp\,(-(m \cdot \sin\,\zeta.\mathrm{im} \cdot \delta) \cdot \cosh\,\zeta.\mathrm{re}) \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (|x\,0| + |x\,1|) \cdot \|f\,x\|) 0 ≤ m → ∀ { f : V → C } , Continuous f → HasCompactSupport f → ∀ { δ : R } , ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { ζ : C } , 0 ≤ ζ . im → ζ . im ≤ π → ∥ D ( K C m f ) ζ ∥ ≤ 1/ 2 ⋅ ( ∣ m ∣ ⋅ cosh ζ . re ⋅ exp ( − ( m ⋅ sin ζ . im ⋅ δ ) ⋅ cosh ζ . re ) ⋅ ∫ ( x : V ) , ( ∣ x 0∣ + ∣ x 1∣ ) ⋅ ∥ f x ∥ ) Proof. By kernelDerivderiv_KrepCont_eqnorm_kernelDeriv_le_exp_decay□ \square □
Used by norm_deriv_reflKrepCont_lenorm_term2_le
Lemma 375 (norm_KrepCont_le_exp_decay_gen). source ↗
Pointwise strip-decay of KrepCont at a general complex argument w (0≤Im w≤π, f wedge-supported): ‖KrepCont m f w‖ ≤ (1/√2)·(∫‖f‖)·exp(−(m sin(Im w)δ)·cosh(Re w)) (rewrite w = Re w + i·Im w).
0 ≤ m → ∀ { f : V → C } , C o n t i n u o u s f → H a s C o m p a c t S u p p o r t f → ∀ { δ : R } , ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { w : C } , 0 ≤ w . i m → w . i m ≤ π → ∥ K C m f w ∥ ≤ ( 1 / 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ ) ⋅ exp ( − ( m ⋅ sin w . i m ⋅ δ ) ⋅ cosh w . r e ) 0 \le m \to \forall \{f : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \forall \{\delta : \mathbb{R}\}, (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), f\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{w : \mathbb{C}\}, 0 \le w.\mathrm{im} \to w.\mathrm{im} \le \pi \to \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,w\| \le (1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|f\,x\|) \cdot \exp\,(-(m \cdot \sin\,w.\mathrm{im} \cdot \delta) \cdot \cosh\,w.\mathrm{re}) 0 ≤ m → ∀ { f : V → C } , Continuous f → HasCompactSupport f → ∀ { δ : R } , ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { w : C } , 0 ≤ w . im → w . im ≤ π → ∥ K C m f w ∥ ≤ ( 1/ 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ ) ⋅ exp ( − ( m ⋅ sin w . im ⋅ δ ) ⋅ cosh w . re ) Proof. By norm_KrepCont_le_exp_decay□ \square □
Used by norm_reflKrepCont_leintegrable_kmsIntegrandnorm_term1_lenorm_KrepCont_le_constmemLp_KrepCont_affine
Lemma 376 (norm_KrepCont_le_const). source ↗
Plain KrepCont bound on the closed strip (0≤Im w≤π, f wedge-supported with δ≥0): ‖KrepCont m f w‖ ≤ (1/√2)·∫‖f‖ — the strip-damping factor exp(−(m sin(Im w)δ)·cosh(Re w)) ≤ 1 since its exponent is ≤ 0 (sin(Im w)≥0 on [0,π], m,δ,cosh ≥ 0). This Re-uniform constant bound is what makes the truncated KMS integral trivially bounded on the closed strip (no log-blowup).
0 ≤ m → ∀ { f : V → C } , C o n t i n u o u s f → H a s C o m p a c t S u p p o r t f → ∀ { δ : R } , 0 ≤ δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { w : C } , 0 ≤ w . i m → w . i m ≤ π → ∥ K C m f w ∥ ≤ 1 / 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ 0 \le m \to \forall \{f : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \forall \{\delta : \mathbb{R}\}, 0 \le \delta \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), f\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{w : \mathbb{C}\}, 0 \le w.\mathrm{im} \to w.\mathrm{im} \le \pi \to \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,w\| \le 1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|f\,x\| 0 ≤ m → ∀ { f : V → C } , Continuous f → HasCompactSupport f → ∀ { δ : R } , 0 ≤ δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { w : C } , 0 ≤ w . im → w . im ≤ π → ∥ K C m f w ∥ ≤ 1/ 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ Proof. By norm_KrepCont_le_exp_decay_gen□ \square □
Used by norm_kmsFunCut_lekmsFunCut_continuousOn
Lemma 377 (memLp_KrepCont_affine). source ↗
A2 (step 2′) — affine-argument L² membership. For m > 0, wedge-supported f, and a complex offset c₀ with Im c₀ ∈ (0,π), the slice θ ↦ KrepCont m f (θ + c₀) is in L²(dθ). The argument’s imaginary part is the constant Im c₀ (strip-interior ⟹ sin > 0), and the real part is θ + Re c₀; pointwise domination by C·exp(−c·cosh(θ+Re c₀)) (norm_KrepCont_le_exp_decay_gen) against the L² translate of C·exp(−c·cosh) (measurePreserving_add_right). Generalizes memLp_KrepCont_strip to a real shift of the strip slice — the form the two boost-KMS slices take.
0 < m → ∀ { f : V → C } , C o n t i n u o u s f → H a s C o m p a c t S u p p o r t f → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { c 0 : C } , 0 < c 0 . i m → c 0 . i m < π → M e m L p ( λ θ ↦ K C m f ( θ + c 0 ) ) 2 v o l 0 < m \to \forall \{f : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \forall \{\delta : \mathbb{R}\}, 0 < \delta \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), f\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{c_{0} : \mathbb{C}\}, 0 < c_{0}.\mathrm{im} \to c_{0}.\mathrm{im} < \pi \to \mathrm{MemLp}\,(\lambda \theta \mapsto \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta + c_{0}))\,2\,\mathrm{vol} 0 < m → ∀ { f : V → C } , Continuous f → HasCompactSupport f → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { c 0 : C } , 0 < c 0 . im → c 0 . im < π → MemLp ( λ θ ↦ K C m f ( θ + c 0 )) 2 vol Proof. By differentiable_KrepContintegrable_exp_neg_const_mul_coshnorm_KrepCont_le_exp_decay_gen□ \square □
Used by memLp_KrepCont_affine_closed
Lemma 378 (KrepCont_add). source ↗
KrepCont is additive in the test functionf₁,f₂): the defining integral ∫ kernel·f is linear in f, with each kernel·fᵢ integrable (continuous, compact support). The sesquilinearity foundation for threading stripKMSrvd_pair over the wedge span.
C o n t i n u o u s f 1 → H a s C o m p a c t S u p p o r t f 1 → C o n t i n u o u s f 2 → H a s C o m p a c t S u p p o r t f 2 → ∀ ( ζ : C ) , K C m ( f 1 + f 2 ) ζ = K C m f 1 ζ + K C m f 2 ζ \mathrm{Continuous}\,f_{1} \to \mathrm{HasCompactSupport}\,f_{1} \to \mathrm{Continuous}\,f_{2} \to \mathrm{HasCompactSupport}\,f_{2} \to \forall (\zeta : \mathbb{C}), \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,(f_{1} + f_{2})\,\zeta = \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f_{1}\,\zeta + \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f_{2}\,\zeta Continuous f 1 → HasCompactSupport f 1 → Continuous f 2 → HasCompactSupport f 2 → ∀ ( ζ : C ) , K C m ( f 1 + f 2 ) ζ = K C m f 1 ζ + K C m f 2 ζ Proof. By minkowskiDotℂmassShellℂkernelcontinuous_kernel_in_x□ \square □
Used by kmsFun_add_leftkmsFun_add_rightKrep_add
Lemma 379 (Krep_add). source ↗
Krep (real axis) is additive in the test functionKrepCont_add at real argument (KrepCont_ofReal). Used for the MemLp closure of the wedge-test class under +/− in the span-closure threading.
C o n t i n u o u s f 1 → H a s C o m p a c t S u p p o r t f 1 → C o n t i n u o u s f 2 → H a s C o m p a c t S u p p o r t f 2 → ∀ ( θ : R ) , K m ( f 1 + f 2 ) θ = K m f 1 θ + K m f 2 θ \mathrm{Continuous}\,f_{1} \to \mathrm{HasCompactSupport}\,f_{1} \to \mathrm{Continuous}\,f_{2} \to \mathrm{HasCompactSupport}\,f_{2} \to \forall (\theta : \mathbb{R}), \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(f_{1} + f_{2})\,\theta = \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{1}\,\theta + \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2}\,\theta Continuous f 1 → HasCompactSupport f 1 → Continuous f 2 → HasCompactSupport f 2 → ∀ ( θ : R ) , K m ( f 1 + f 2 ) θ = K m f 1 θ + K m f 2 θ Proof. By KrepContKrepCont_ofRealKrepCont_add□ \square □
Used by KrepL2_addKrep_submemLp_Krep_add
Lemma 380 (Krep_sub). source ↗
Krep (real axis) respects subtractionKrep m (f₁−f₂) = Krep m f₁ − Krep m f₂ (from Krep_add).
C o n t i n u o u s f 1 → H a s C o m p a c t S u p p o r t f 1 → C o n t i n u o u s f 2 → H a s C o m p a c t S u p p o r t f 2 → ∀ ( θ : R ) , K m ( f 1 − f 2 ) θ = K m f 1 θ − K m f 2 θ \mathrm{Continuous}\,f_{1} \to \mathrm{HasCompactSupport}\,f_{1} \to \mathrm{Continuous}\,f_{2} \to \mathrm{HasCompactSupport}\,f_{2} \to \forall (\theta : \mathbb{R}), \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(f_{1} - f_{2})\,\theta = \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{1}\,\theta - \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2}\,\theta Continuous f 1 → HasCompactSupport f 1 → Continuous f 2 → HasCompactSupport f 2 → ∀ ( θ : R ) , K m ( f 1 − f 2 ) θ = K m f 1 θ − K m f 2 θ Proof. By Krep_add□ \square □
Used by KrepL2_submemLp_Krep_sub
Lemma 381 (memLp_Krep_add). source ↗
MemLp closure under additionMemLp (Krep m (f₁+f₂)) 2 from MemLp (Krep m fᵢ) 2, via Krep_add (Krep(f₁+f₂)=Krep f₁+Krep f₂) + MemLp.add. The additive companion of memLp_Krep_sub; together they make the nice one-particle vectors {KrepL2 f} closed under ±, i.e. an ℝ-subspace.
C o n t i n u o u s f 1 → H a s C o m p a c t S u p p o r t f 1 → C o n t i n u o u s f 2 → H a s C o m p a c t S u p p o r t f 2 → M e m L p ( K m f 1 ) 2 v o l → M e m L p ( K m f 2 ) 2 v o l → M e m L p ( K m ( f 1 + f 2 ) ) 2 v o l \mathrm{Continuous}\,f_{1} \to \mathrm{HasCompactSupport}\,f_{1} \to \mathrm{Continuous}\,f_{2} \to \mathrm{HasCompactSupport}\,f_{2} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{1})\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2})\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(f_{1} + f_{2}))\,2\,\mathrm{vol} Continuous f 1 → HasCompactSupport f 1 → Continuous f 2 → HasCompactSupport f 2 → MemLp ( K m f 1 ) 2 vol → MemLp ( K m f 2 ) 2 vol → MemLp ( K m ( f 1 + f 2 )) 2 vol Proof. By Krep_add□ \square □
Used by KrepL2_add
Lemma 382 (memLp_Krep_sub). source ↗
MemLp closure under subtractionMemLp (Krep m (f₁−f₂)) 2 from MemLp (Krep m fᵢ) 2, via Krep_sub (Krep(f₁−f₂)=Krep f₁−Krep f₂) + MemLp.sub.
C o n t i n u o u s f 1 → H a s C o m p a c t S u p p o r t f 1 → C o n t i n u o u s f 2 → H a s C o m p a c t S u p p o r t f 2 → M e m L p ( K m f 1 ) 2 v o l → M e m L p ( K m f 2 ) 2 v o l → M e m L p ( K m ( f 1 − f 2 ) ) 2 v o l \mathrm{Continuous}\,f_{1} \to \mathrm{HasCompactSupport}\,f_{1} \to \mathrm{Continuous}\,f_{2} \to \mathrm{HasCompactSupport}\,f_{2} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{1})\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2})\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(f_{1} - f_{2}))\,2\,\mathrm{vol} Continuous f 1 → HasCompactSupport f 1 → Continuous f 2 → HasCompactSupport f 2 → MemLp ( K m f 1 ) 2 vol → MemLp ( K m f 2 ) 2 vol → MemLp ( K m ( f 1 − f 2 )) 2 vol Proof. By Krep_sub□ \square □
Used by kmsFun_sub_leftkmsFun_sub_rightKrepL2_subnorm_kmsFun_sub_le
Lemma 383 (memLp_KrepCont_affine_closed). source ↗
Affine-argument L² membership on the CLOSED strip Im c₀ ∈ [0,π]. Extends memLp_KrepCont_affine to the two boundary heights: at Im c₀ = 0 the slice is a real-axis translate Krep m f(·+Re c₀) (KrepCont_ofReal), at Im c₀ = π it is the conjugate conj(Krep m f(·+Re c₀)) (KrepCont_add_pi_I, MemLp.star) — both in L² via the MemLp (Krep m f) 2 hypothesis; the interior is memLp_KrepCont_affine. This supplies the edge L² slices needed to integrate the kmsFun integrand up to the boundary.
0 < m → ∀ { f : V → C } , C o n t i n u o u s f → H a s C o m p a c t S u p p o r t f → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( f x ) = f x ) → M e m L p ( K m f ) 2 v o l → ∀ { c 0 : C } , 0 ≤ c 0 . i m → c 0 . i m ≤ π → M e m L p ( λ θ ↦ K C m f ( θ + c 0 ) ) 2 v o l 0 < m \to \forall \{f : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \forall \{\delta : \mathbb{R}\}, 0 < \delta \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), f\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(f\,x) = f\,x) \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \forall \{c_{0} : \mathbb{C}\}, 0 \le c_{0}.\mathrm{im} \to c_{0}.\mathrm{im} \le \pi \to \mathrm{MemLp}\,(\lambda \theta \mapsto \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta + c_{0}))\,2\,\mathrm{vol} 0 < m → ∀ { f : V → C } , Continuous f → HasCompactSupport f → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → MemLp ( K m f ) 2 vol → ∀ { c 0 : C } , 0 ≤ c 0 . im → c 0 . im ≤ π → MemLp ( λ θ ↦ K C m f ( θ + c 0 )) 2 vol Proof. By KrepCont_ofRealKrepCont_add_pi_ImemLp_KrepCont_affine□ \square □
Used by integrable_kmsFun_integrand_closed
← all sections · ← SchwartzDecay · WienerL2 →