Fock · section of the QIQT-H book
QIQTH.Fock.BoostKMS ← all sections · ← EinsteinFieldEquation · CyclicWitness →
Fock · entries 94–208 of 1000
Lemma 94 (inner_KrepL2). source ↗
The L² inner product of two wedge modes as a concrete rapidity integral. ⟪KrepL2 f, KrepL2 g⟫ = ∫ conj(Krep m f θ)·Krep m g θ dθ (via L2.inner_def + MemLp.coeFn_toLp).
⟨ t o L p ( K m f ) h f , t o L p ( K m g ) h g ⟩ = ∫ ( θ : R ) , ( s t a r R i n g E n d C ) ( K m f θ ) ⋅ K m g θ \langle {\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,\mathrm{hf}},{\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,\mathrm{hg}}\rangle = \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta) \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta ⟨ toLp ( K m f ) hf , toLp ( K m g ) hg ⟩ = ∫ ( θ : R ) , ( starRingEnd C ) ( K m f θ ) ⋅ K m g θ Proof. Immediate from the definitions. □ \square □
Used by inner_boostUnitary_KrepL2norm_toLp_Krep_eq_sqrt
Lemma 95 (inner_KrepL2_general). source ↗
The L² inner product of a wedge mode against an ARBITRARY h ∈ L² as a concrete integral : ⟪KrepL2 f, h⟫ = ∫ conj(Krep m f θ)·h(θ) dθ. The concrete form of the Reeh–Schlieder totality condition: {KrepL2 f : f nice} is total iff the only h with ∫ conj(Krep f)·h = 0 for all nice f is h = 0.
⟨ t o L p ( K m f ) h f , h ⟩ = ∫ ( θ : R ) , ( s t a r R i n g E n d C ) ( K m f θ ) ⋅ h θ \langle {\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,\mathrm{hf}},{h}\rangle = \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta) \cdot h\,\theta ⟨ toLp ( K m f ) hf , h ⟩ = ∫ ( θ : R ) , ( starRingEnd C ) ( K m f θ ) ⋅ h θ Proof. Immediate from the definitions. □ \square □
Used by niceWedge_isCyclic_of_total_integralniceWedgeCyclic_of_fourier_ne_zero
Lemma 96 (inner_boostUnitary_KrepL2). source ↗
The real-axis edge. ⟪KrepL2 g, boostUnitary a (KrepL2 f)⟫ = ∫ conj(Krep m g θ)·Krep m f (θ−a) dθ. Combines boostUnitary_KrepL2 (boost acts by boostTest), inner_KrepL2, and the amplitude boost- covariance Krep m (boostTest (−a) f) θ = Krep m f (θ−a). This is the orbit correlation f(t) = ⟪η, V_t ξ⟫ of StripKMSrvd (with V_t = boostUnitary a, a the rapidity).
M e m L p ( K m ( ϕ B ( − a ) f ) ) 2 v o l → ⟨ t o L p ( K m g ) h g , ( U a ) ( t o L p ( K m f ) h f ) ⟩ = ∫ ( θ : R ) , ( s t a r R i n g E n d C ) ( K m g θ ) ⋅ K m f ( θ − a ) \mathrm{MemLp}\,(\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))\,2\,\mathrm{vol} \to \langle {\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,\mathrm{hg}},{(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,a)\,(\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,\mathrm{hf})}\rangle = \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta) \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,(\theta - a) MemLp ( K m ( ϕ B ( − a ) f )) 2 vol → ⟨ toLp ( K m g ) hg , ( U a ) ( toLp ( K m f ) hf ) ⟩ = ∫ ( θ : R ) , ( starRingEnd C ) ( K m g θ ) ⋅ K m f ( θ − a ) Proof. By inner_KrepL2Krep_boostboostUnitary_KrepL2□ \square □
Used by symm_edge_eq_inner
Lemma 97 (symm_edge_eq_shifted). source ↗
Symmetric ↔ shifted edge (change of variables θ ↦ θ+πt). The KMS function’s symmetric real-axis form equals the boost-orbit form: ∫ conj(Krep g (θ+πt))·Krep f (θ−πt) dθ = ∫ conj(Krep g θ)·Krep f (θ−2πt) dθ (translation invariance).
∫ ( θ : R ) , ( s t a r R i n g E n d C ) ( K m g ( θ + π ⋅ t ) ) ⋅ K m f ( θ − π ⋅ t ) = ∫ ( θ : R ) , ( s t a r R i n g E n d C ) ( K m g θ ) ⋅ K m f ( θ − 2 ⋅ π ⋅ t ) \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,(\theta + \pi \cdot t)) \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,(\theta - \pi \cdot t) = \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta) \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,(\theta - 2 \cdot \pi \cdot t) ∫ ( θ : R ) , ( starRingEnd C ) ( K m g ( θ + π ⋅ t )) ⋅ K m f ( θ − π ⋅ t ) = ∫ ( θ : R ) , ( starRingEnd C ) ( K m g θ ) ⋅ K m f ( θ − 2 ⋅ π ⋅ t ) Proof. Immediate from the definitions. □ \square □
Used by symm_edge_eq_inner
Lemma 98 (symm_edge_eq_inner). source ↗
The KMS top edge f(t) = ⟪η, V_t ξ⟫ in symmetric (KMS-function) form. Combining symm_edge_eq_shifted and inner_boostUnitary_KrepL2: the symmetric integral ∫ conj(Krep g (θ+πt))·Krep f (θ−πt) dθ — the t-real value of the KMS function F(z)=∫ conj(KrepCont g (θ+πz̄))·KrepCont f (θ−πz) — equals ⟪KrepL2 g, boostUnitary(2πt) (KrepL2 f)⟫. (Boost sign +2π here; StripKMSrvd’s V_t=boostUnitary(−2π·) is matched by orienting t.)
M e m L p ( K m ( ϕ B ( − ( 2 ⋅ π ⋅ t ) ) f ) ) 2 v o l → ∫ ( θ : R ) , ( s t a r R i n g E n d C ) ( K m g ( θ + π ⋅ t ) ) ⋅ K m f ( θ − π ⋅ t ) = ⟨ t o L p ( K m g ) h g , ( U ( 2 ⋅ π ⋅ t ) ) ( t o L p ( K m f ) h f ) ⟩ \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-boosttest}{\phi_{B}}\,(-(2 \cdot \pi \cdot t))\,f))\,2\,\mathrm{vol} \to \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,(\theta + \pi \cdot t)) \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,(\theta - \pi \cdot t) = \langle {\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,\mathrm{hg}},{(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,(\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,\mathrm{hf})}\rangle MemLp ( K m ( ϕ B ( − ( 2 ⋅ π ⋅ t )) f )) 2 vol → ∫ ( θ : R ) , ( starRingEnd C ) ( K m g ( θ + π ⋅ t )) ⋅ K m f ( θ − π ⋅ t ) = ⟨ toLp ( K m g ) hg , ( U ( 2 ⋅ π ⋅ t )) ( toLp ( K m f ) hf ) ⟩ Proof. By inner_boostUnitary_KrepL2symm_edge_eq_shifted□ \square □
Used by kmsFun_ofReal_eq_inner
Definition 99 (kmsFun). source ↗
The KMS function F(z) = ∫ conj(KrepCont g (conj(θ+πz)))·KrepCont f (θ−πz) dθ — the candidate StripKMSrvd witness. H^#(θ+πz) = conj(H(conj(θ+πz))) with H = KrepCont g, Ξ = KrepCont f; for z in the strip {−1<Im z<0} both factors are evaluated with imaginary part in (0,π) (the good damping region).
Used by kmsFun_ofRealkmsFun_ofReal_eq_innerkmsFun_sub_IkmsFun_differentiableAtkmsFun_differentiableOnkmsFunCut_tendsto_closednorm_kmsFun_sub_kmsFunCut_lekmsFun_add_left
Lemma 100 (kmsFun_ofReal). source ↗
The KMS function on the real axis equals the symmetric integral (via KrepCont_ofReal): the real-axis arguments are real, so each KrepCont collapses to Krep and the inner conjugation is trivial.
F m f g t = ∫ ( θ : R ) , ( s t a r R i n g E n d C ) ( K m g ( θ + π ⋅ t ) ) ⋅ K m f ( θ − π ⋅ t ) \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g\,t = \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,(\theta + \pi \cdot t)) \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,(\theta - \pi \cdot t) F m f g t = ∫ ( θ : R ) , ( starRingEnd C ) ( K m g ( θ + π ⋅ t )) ⋅ K m f ( θ − π ⋅ t ) Proof. By KrepContKrepCont_ofReal□ \square □
Used by kmsFun_ofReal_eq_innerkmsFun_sub_I
Lemma 101 (kmsFun_ofReal_eq_inner). source ↗
The KMS top edge for kmsFun : F(t) = ⟪KrepL2 g, boostUnitary(2πt) (KrepL2 f)⟫ (kmsFun_ofReal ∘ symm_edge_eq_inner).
M e m L p ( K m ( ϕ B ( − ( 2 ⋅ π ⋅ t ) ) f ) ) 2 v o l → F m f g t = ⟨ t o L p ( K m g ) h g , ( U ( 2 ⋅ π ⋅ t ) ) ( t o L p ( K m f ) h f ) ⟩ \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-boosttest}{\phi_{B}}\,(-(2 \cdot \pi \cdot t))\,f))\,2\,\mathrm{vol} \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g\,t = \langle {\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,\mathrm{hg}},{(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,(\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,\mathrm{hf})}\rangle MemLp ( K m ( ϕ B ( − ( 2 ⋅ π ⋅ t )) f )) 2 vol → F m f g t = ⟨ toLp ( K m g ) hg , ( U ( 2 ⋅ π ⋅ t )) ( toLp ( K m f ) hf ) ⟩ Proof. By symm_edge_eq_innerkmsFun_ofReal□ \square □
Used by bcf_apply_eq_topbcf_apply_eq_bot
Lemma 102 (kmsFun_sub_I). source ↗
The KMS bottom edge F(t−i) = conj(F(t)) (for real f,g). At z=t−i the iπ-shift puts both KrepCont arguments at imaginary part +π, so KrepCont_add_pi_I (A3) collapses each to conj(Krep …): F(t−i) = ∫ Krep g(θ+πt)·conj(Krep f(θ−πt)) dθ = conj(F(t)). With the top edge (kmsFun_ofReal_eq_inner) and ⟪V_t ξ,η⟫ = conj⟪η,V_t ξ⟫, this is the bottom-edge requirement f(t−i) = ⟪V_t ξ,η⟫ of StripKMSrvd.
( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → ∀ ( t : R ) , F m f g ( t − i ) = ( s t a r R i n g E n d C ) ( F m f g t ) (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(f\,x) = f\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(g\,x) = g\,x) \to \forall (t : \mathbb{R}), \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g\,(t - i) = (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g\,t) ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → ∀ ( t : R ) , F m f g ( t − i ) = ( starRingEnd C ) ( F m f g t ) Proof. By kmsFun_ofRealKrepKrepContKrepCont_add_pi_I□ \square □
Used by bcf_apply_eq_bot
Lemma 103 (differentiable_reflKrepCont). source ↗
The reflected amplitude u ↦ conj(KrepCont g(conj u)) is entire (Schwarz reflection: conj∘F∘conj is holomorphic when F is). Via DifferentiableAt.star_conj + differentiable_KrepCont. This is the g factor H^# of the KMS-function integrand — the holomorphy ingredient for kmsFun.
C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → D i f f e r e n t i a b l e C λ u ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) u ) ) \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \mathrm{Differentiable}\,\mathbb{C}\,\lambda u \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,u)) Continuous g → HasCompactSupport g → Differentiable C λ u ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) u )) Proof. By differentiable_KrepCont□ \square □
Used by differentiable_kmsIntegrandhasDerivAt_kmsIntegrand_zcontinuous_deriv_reflKrepCont
Lemma 104 (norm_reflKrepCont_le). source ↗
Strip-decay of the reflected amplitude ‖reflKrep(u)‖ = ‖KrepCont g(conj u)‖ for −π ≤ Im u ≤ 0 (so Im(conj u) ∈ [0,π]): ≤ (1/√2)(∫‖g‖)·exp(−(m sin(−Im u)δ)·cosh(Re u)). The g-factor bound for the kmsFun integrand (reflKrep(θ+πz), where Im(θ+πz)=π Im z ∈(−π,0) for z in the strip).
0 ≤ m → ∀ { g : V → C } , C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { u : C } , − π ≤ u . i m → u . i m ≤ 0 → ∥ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) u ) ) ∥ ≤ ( 1 / 2 ⋅ ∫ ( x : V ) , ∥ g x ∥ ) ⋅ exp ( − ( m ⋅ sin ( − u . i m ) ⋅ δ ) ⋅ cosh u . r e ) 0 \le m \to \forall \{g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \forall \{\delta : \mathbb{R}\}, (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{u : \mathbb{C}\}, -\pi \le u.\mathrm{im} \to u.\mathrm{im} \le 0 \to \|(\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,u))\| \le (1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|g\,x\|) \cdot \exp\,(-(m \cdot \sin\,(-u.\mathrm{im}) \cdot \delta) \cdot \cosh\,u.\mathrm{re}) 0 ≤ m → ∀ { g : V → C } , Continuous g → HasCompactSupport g → ∀ { δ : R } , ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { u : C } , − π ≤ u . im → u . im ≤ 0 → ∥ ( starRingEnd C ) ( K C m g (( starRingEnd C ) u )) ∥ ≤ ( 1/ 2 ⋅ ∫ ( x : V ) , ∥ g x ∥ ) ⋅ exp ( − ( m ⋅ sin ( − u . im ) ⋅ δ ) ⋅ cosh u . re ) Proof. By norm_KrepCont_le_exp_decay_gen□ \square □
Used by integrable_kmsIntegrandnorm_term2_le
Lemma 105 (deriv_reflKrepCont_eq). source ↗
The derivative of the reflected amplitude: deriv(u ↦ conj(KrepCont g(conj u))) u = conj(deriv(KrepCont g)(conj u)) (Schwarz reflection, HasDerivAt.conj_conj).
C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ ( u : C ) , D ( λ u ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) u ) ) ) u = ( s t a r R i n g E n d C ) ( D ( K C m g ) ( ( s t a r R i n g E n d C ) u ) ) \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \forall (u : \mathbb{C}), \mathrm{D}\,(\lambda u \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,u)))\,u = (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{D}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g)\,((\mathrm{starRingEnd}\,\mathbb{C})\,u)) Continuous g → HasCompactSupport g → ∀ ( u : C ) , D ( λ u ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) u ))) u = ( starRingEnd C ) ( D ( K C m g ) (( starRingEnd C ) u )) Proof. By differentiable_KrepCont□ \square □
Used by norm_deriv_reflKrepCont_le
Lemma 106 (norm_deriv_reflKrepCont_le). source ↗
Strip-decay of the reflected amplitude’s derivative : ‖deriv reflKrep(u)‖ = ‖deriv KrepCont g(conj u)‖ ≤ (1/√2)·|m|·cosh(Re u)·exp(−(m sin(−Im u)δ)·cosh(Re u))·∫(|x₀|+|x₁|)‖g‖ for −π≤Im u≤0. The deriv reflKrep factor bound for the kmsFun integrand’s z-derivative.
0 ≤ m → ∀ { g : V → C } , C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { u : C } , − π ≤ u . i m → u . i m ≤ 0 → ∥ D ( λ u ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) u ) ) ) u ∥ ≤ 1 / 2 ⋅ ( ∣ m ∣ ⋅ cosh u . r e ⋅ exp ( − ( m ⋅ sin ( − u . i m ) ⋅ δ ) ⋅ cosh u . r e ) ⋅ ∫ ( x : V ) , ( ∣ x 0 ∣ + ∣ x 1 ∣ ) ⋅ ∥ g x ∥ ) 0 \le m \to \forall \{g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \forall \{\delta : \mathbb{R}\}, (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{u : \mathbb{C}\}, -\pi \le u.\mathrm{im} \to u.\mathrm{im} \le 0 \to \|\mathrm{D}\,(\lambda u \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,u)))\,u\| \le 1 / \sqrt 2 \cdot (|m| \cdot \cosh\,u.\mathrm{re} \cdot \exp\,(-(m \cdot \sin\,(-u.\mathrm{im}) \cdot \delta) \cdot \cosh\,u.\mathrm{re}) \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (|x\,0| + |x\,1|) \cdot \|g\,x\|) 0 ≤ m → ∀ { g : V → C } , Continuous g → HasCompactSupport g → ∀ { δ : R } , ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { u : C } , − π ≤ u . im → u . im ≤ 0 → ∥ D ( λ u ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) u ))) u ∥ ≤ 1/ 2 ⋅ ( ∣ m ∣ ⋅ cosh u . re ⋅ exp ( − ( m ⋅ sin ( − u . im ) ⋅ δ ) ⋅ cosh u . re ) ⋅ ∫ ( x : V ) , ( ∣ x 0∣ + ∣ x 1∣ ) ⋅ ∥ g x ∥ ) Proof. By deriv_reflKrepCont_eqnorm_deriv_KrepCont_le_exp_decay□ \square □
Used by norm_term1_le
Lemma 107 (differentiable_kmsIntegrand). source ↗
The kmsFun integrand is entire in z (for f,g continuous with compact support). The g-factor conj(KrepCont g(conj(θ+πz))) = differentiable_reflKrepCont ∘ (affine), the f-factor KrepCont f(θ−πz) = differentiable_KrepCont ∘ (affine); the product is differentiable. This is the per-θ (h_diff) ingredient for the parametric-integral holomorphy of F (DiffContOnCl).
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 g → H a s C o m p a c t S u p p o r t g → ∀ ( θ : R ) , D i f f e r e n t i a b l e C λ z ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) ( θ + π ⋅ z ) ) ) ⋅ K C m f ( θ − π ⋅ z ) \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \forall (\theta : \mathbb{R}), \mathrm{Differentiable}\,\mathbb{C}\,\lambda z \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,(\theta + \pi \cdot z))) \cdot \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta - \pi \cdot z) Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ ( θ : R ) , Differentiable C λ z ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) ( θ + π ⋅ z ))) ⋅ K C m f ( θ − π ⋅ z ) Proof. By differentiable_reflKrepContdifferentiable_KrepCont□ \square □
Used by kmsFunCut_continuousOn
Lemma 108 (hasDerivAt_kmsIntegrand_z). source ↗
The kmsFun integrand’s z-derivative (product/chain rule): for fixed θ, the integrand conj(KrepCont g(conj(θ+πz)))·KrepCont f(θ−πz) has derivative [deriv reflKrep(θ+πz)·π]·KrepCont f(θ−πz) + reflKrep(θ+πz)·[deriv KrepCont f(θ−πz)·(−π)]. The h_diff ingredient (with explicit value, for the domination bound) of the dominated-derivative theorem for kmsFun’s holomorphy.
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 g → H a s C o m p a c t S u p p o r t g → ∀ ( θ : R ) ( z : C ) , ( λ z ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) ( θ + π ⋅ z ) ) ) ⋅ K C m f ( θ − π ⋅ z ) ) ′ ( z ) = D ( λ u ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) u ) ) ) ( θ + π ⋅ z ) ⋅ π ⋅ K C m f ( θ − π ⋅ z ) + ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) ( θ + π ⋅ z ) ) ) ⋅ ( D ( K C m f ) ( θ − π ⋅ z ) ⋅ − π ) \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \forall (\theta : \mathbb{R}) (z : \mathbb{C}), ({\lambda z \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,(\theta + \pi \cdot z))) \cdot \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta - \pi \cdot z)})'({z})={\mathrm{D}\,(\lambda u \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,u)))\,(\theta + \pi \cdot z) \cdot \pi \cdot \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta - \pi \cdot z) + (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,(\theta + \pi \cdot z))) \cdot (\mathrm{D}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f)\,(\theta - \pi \cdot z) \cdot -\pi)} Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ ( θ : R ) ( z : C ) , ( λ z ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) ( θ + π ⋅ z ))) ⋅ K C m f ( θ − π ⋅ z ) ) ′ ( z ) = D ( λ u ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) u ))) ( θ + π ⋅ z ) ⋅ π ⋅ K C m f ( θ − π ⋅ z ) + ( starRingEnd C ) ( K C m g (( starRingEnd C ) ( θ + π ⋅ z ))) ⋅ ( D ( K C m f ) ( θ − π ⋅ z ) ⋅ − π ) Proof. By differentiable_reflKrepContdifferentiable_KrepCont□ \square □
Used by kmsFun_differentiableAtkmsFunCut_differentiableAt
Lemma 109 (norm_two_term_le). source ↗
Norm decomposition of the integrand z-derivative value (from hasDerivAt_kmsIntegrand_z) into its four factors: ‖A·π·C + B·(D·(−π))‖ ≤ π·‖A‖·‖C‖ + π·‖B‖·‖D‖.
∥ A ⋅ π ⋅ C + B ⋅ ( D ⋅ − π ) ∥ ≤ π ⋅ ( ∥ A ∥ ⋅ ∥ C ∥ ) + π ⋅ ( ∥ B ∥ ⋅ ∥ D ∥ ) \|A \cdot \pi \cdot C + B \cdot (D \cdot -\pi)\| \le \pi \cdot (\|A\| \cdot \|C\|) + \pi \cdot (\|B\| \cdot \|D\|) ∥ A ⋅ π ⋅ C + B ⋅ ( D ⋅ − π ) ∥ ≤ π ⋅ ( ∥ A ∥ ⋅ ∥ C ∥ ) + π ⋅ ( ∥ B ∥ ⋅ ∥ D ∥ ) Proof. Immediate from the definitions. □ \square □
Used by kmsIntegrand_deriv_bound
Lemma 110 (continuous_kmsIntegrand_in_theta). source ↗
The kmsFun integrand is continuous in θ (for fixed z) — the measurability (hF_meas) ingredient for the parametric-integral holomorphy of F. KrepCont is continuous (entire), composed with the continuous θ-maps θ↦conj(θ+πz), θ↦θ−πz, and conj.
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 g → H a s C o m p a c t S u p p o r t g → ∀ ( z : C ) , C o n t i n u o u s λ θ ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) ( θ + π ⋅ z ) ) ) ⋅ K C m f ( θ − π ⋅ z ) \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \forall (z : \mathbb{C}), \mathrm{Continuous}\,\lambda \theta \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,(\theta + \pi \cdot z))) \cdot \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta - \pi \cdot z) Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ ( z : C ) , Continuous λ θ ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) ( θ + π ⋅ z ))) ⋅ K C m f ( θ − π ⋅ z ) Proof. By differentiable_KrepCont□ \square □
Used by integrable_kmsIntegrandkmsFun_differentiableAtkmsFunCut_differentiableAtkmsFunCut_continuousOn
Lemma 111 (continuous_deriv_reflKrepCont). source ↗
deriv reflKrep is continuous (reflKrep entire ⟹ deriv analytic ⟹ continuous).
C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → C o n t i n u o u s ( D λ u ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) u ) ) ) \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \mathrm{Continuous}\,(\mathrm{D}\,\lambda u \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,u))) Continuous g → HasCompactSupport g → Continuous ( D λ u ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) u ))) Proof. By differentiable_reflKrepCont□ \square □
Used by continuous_kmsIntegrand_deriv_in_theta
Lemma 112 (continuous_kmsIntegrand_deriv_in_theta). source ↗
The kmsFun integrand’s z-derivative value is continuous in θ — the hF'_meas (derivative measurability) ingredient. Each of the four factors is continuous in θ.
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 g → H a s C o m p a c t S u p p o r t g → ∀ ( z : C ) , C o n t i n u o u s λ θ ↦ D ( λ u ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) u ) ) ) ( θ + π ⋅ z ) ⋅ π ⋅ K C m f ( θ − π ⋅ z ) + ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) ( θ + π ⋅ z ) ) ) ⋅ ( D ( K C m f ) ( θ − π ⋅ z ) ⋅ − π ) \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \forall (z : \mathbb{C}), \mathrm{Continuous}\,\lambda \theta \mapsto \mathrm{D}\,(\lambda u \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,u)))\,(\theta + \pi \cdot z) \cdot \pi \cdot \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta - \pi \cdot z) + (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,(\theta + \pi \cdot z))) \cdot (\mathrm{D}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f)\,(\theta - \pi \cdot z) \cdot -\pi) Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ ( z : C ) , Continuous λ θ ↦ D ( λ u ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) u ))) ( θ + π ⋅ z ) ⋅ π ⋅ K C m f ( θ − π ⋅ z ) + ( starRingEnd C ) ( K C m g (( starRingEnd C ) ( θ + π ⋅ z ))) ⋅ ( D ( K C m f ) ( θ − π ⋅ z ) ⋅ − π ) Proof. By continuous_deriv_reflKrepContdifferentiable_KrepContcontinuous_deriv_KrepCont□ \square □
Used by kmsFun_differentiableAtkmsFunCut_differentiableAt
Lemma 113 (integrable_kmsIntegrand). source ↗
hF_int — the kmsFun integrand is integrable in θz (−1<Im z<0). ‖integrand‖ = ‖reflKrep(θ+πz)‖·‖KrepCont f(θ−πz)‖ ≤ C_g·(C_f·exp(−(mσδf)·cosh(θ−π Re z))) (the g-factor bounded, the f-factor decaying, σ=sin(−π Im z)>0), dominated by an integrable translate of exp(−c·cosh).
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { \deltaf \deltag : R } , 0 < \deltaf → 0 < \deltag → ( ∀ ( x : V ) , f x ≠ 0 → \deltaf ≤ x 1 − x 0 ∧ \deltaf ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → \deltag ≤ x 1 − x 0 ∧ \deltag ≤ x 1 + x 0 ) → ∀ { z : C } , − 1 < z . i m → z . i m < 0 → I n t e g r a b l e ( λ θ ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) ( θ + π ⋅ z ) ) ) ⋅ K C m f ( θ − π ⋅ z ) ) v o l 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \forall \{\deltaf \deltag : \mathbb{R}\}, 0 < \deltaf \to 0 < \deltag \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), f\,x \ne 0 \to \deltaf \le x\,1 - x\,0 \wedge \deltaf \le x\,1 + x\,0) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), g\,x \ne 0 \to \deltag \le x\,1 - x\,0 \wedge \deltag \le x\,1 + x\,0) \to \forall \{z : \mathbb{C}\}, -1 < z.\mathrm{im} \to z.\mathrm{im} < 0 \to \mathrm{Integrable}\,(\lambda \theta \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,(\theta + \pi \cdot z))) \cdot \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta - \pi \cdot z))\,\mathrm{vol} 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { \deltaf \deltag : R } , 0 < \deltaf → 0 < \deltag → ( ∀ ( x : V ) , f x = 0 → \deltaf ≤ x 1 − x 0 ∧ \deltaf ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → \deltag ≤ x 1 − x 0 ∧ \deltag ≤ x 1 + x 0 ) → ∀ { z : C } , − 1 < z . im → z . im < 0 → Integrable ( λ θ ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) ( θ + π ⋅ z ))) ⋅ K C m f ( θ − π ⋅ z )) vol Proof. By norm_reflKrepCont_lecontinuous_kmsIntegrand_in_thetaintegrable_exp_neg_const_mul_coshsin_neg_pi_mul_posnorm_KrepCont_le_exp_decay_gen□ \square □
Used by kmsFun_differentiableAtkmsFunCut_differentiableAt
Lemma 114 (exists_sin_min). source ↗
Decay-rate lower bound over a strip-interior ball. If closedBall z₀ ε ⊆ {−1<Im<0}, the decay rate σ(z)=sin(−π·Im z) has a positive lower bound σmin on the ball (continuous positive fn on a compact set attains a positive min). The c₀ for cosh_shift_exp_le in the h_bound assembly.
0 < ε → ( ∀ z ∈ B ˉ z 0 ε , − 1 < z . i m ∧ z . i m < 0 ) → ∃ σ m i n , 0 < σ m i n ∧ ∀ z ∈ B ˉ z 0 ε , σ m i n ≤ sin ( − ( π ⋅ z . i m ) ) 0 < \varepsilon \to (\forall z\in \bar{B}\,z_{0}\,\varepsilon, -1 < z.\mathrm{im} \wedge z.\mathrm{im} < 0) \to \exists \sigma\mathrm{min}, 0 < \sigma\mathrm{min} \wedge \forall z\in \bar{B}\,z_{0}\,\varepsilon, \sigma\mathrm{min} \le \sin\,(-(\pi \cdot z.\mathrm{im})) 0 < ε → ( ∀ z ∈ B ˉ z 0 ε , − 1 < z . im ∧ z . im < 0 ) → ∃ σ min , 0 < σ min ∧ ∀ z ∈ B ˉ z 0 ε , σ min ≤ sin ( − ( π ⋅ z . im )) Proof. By sin_neg_pi_mul_pos□ \square □
Used by kmsFun_differentiableAtkmsFunCut_differentiableAt
Lemma 115 (norm_term1_le). source ↗
h_bound term 1‖deriv reflKrep(θ+πz)‖·‖KrepCont f(θ−πz)‖ ≤ Cdg·Cf·(e^{πR}·cosh θ·exp(−κ·cosh θ)) (κ = m σmin δ e^{−πR}), via prod_norm_bound_cosh_shift (the deriv reflKrep factor decays in cosh(θ+π Re z), the KrepCont f factor is bounded by Cf).
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { z : C } , − 1 < z . i m → z . i m < 0 → ∀ { σ m i n R : R } , 0 < σ m i n → σ m i n ≤ sin ( − ( π ⋅ z . i m ) ) → ∣ z . r e ∣ ≤ R → ∀ ( θ : R ) , ∥ D ( λ u ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) u ) ) ) ( θ + π ⋅ z ) ∥ ⋅ ∥ K C m f ( θ − π ⋅ z ) ∥ ≤ 1 / 2 ⋅ ( ∣ m ∣ ⋅ ∫ ( x : V ) , ( ∣ x 0 ∣ + ∣ x 1 ∣ ) ⋅ ∥ g x ∥ ) ⋅ ( 1 / 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ ) ⋅ ( exp ( π ⋅ R ) ⋅ cosh θ ⋅ exp ( − ( m ⋅ σ m i n ⋅ δ ⋅ exp ( − ( π ⋅ R ) ) ⋅ cosh θ ) ) ) 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{z : \mathbb{C}\}, -1 < z.\mathrm{im} \to z.\mathrm{im} < 0 \to \forall \{\sigma\mathrm{min} R : \mathbb{R}\}, 0 < \sigma\mathrm{min} \to \sigma\mathrm{min} \le \sin\,(-(\pi \cdot z.\mathrm{im})) \to |z.\mathrm{re}| \le R \to \forall (\theta : \mathbb{R}), \|\mathrm{D}\,(\lambda u \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,u)))\,(\theta + \pi \cdot z)\| \cdot \|\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta - \pi \cdot z)\| \le 1 / \sqrt 2 \cdot (|m| \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (|x\,0| + |x\,1|) \cdot \|g\,x\|) \cdot (1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|f\,x\|) \cdot (\exp\,(\pi \cdot R) \cdot \cosh\,\theta \cdot \exp\,(-(m \cdot \sigma\mathrm{min} \cdot \delta \cdot \exp\,(-(\pi \cdot R)) \cdot \cosh\,\theta))) 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { z : C } , − 1 < z . im → z . im < 0 → ∀ { σ min R : R } , 0 < σ min → σ min ≤ sin ( − ( π ⋅ z . im )) → ∣ z . re ∣ ≤ R → ∀ ( θ : R ) , ∥ D ( λ u ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) u ))) ( θ + π ⋅ z ) ∥ ⋅ ∥ K C m f ( θ − π ⋅ z ) ∥ ≤ 1/ 2 ⋅ ( ∣ m ∣ ⋅ ∫ ( x : V ) , ( ∣ x 0∣ + ∣ x 1∣ ) ⋅ ∥ g x ∥ ) ⋅ ( 1/ 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ ) ⋅ ( exp ( π ⋅ R ) ⋅ cosh θ ⋅ exp ( − ( m ⋅ σ min ⋅ δ ⋅ exp ( − ( π ⋅ R )) ⋅ cosh θ ))) Proof. By norm_deriv_reflKrepCont_lesin_neg_pi_mul_posprod_norm_bound_cosh_shiftnorm_KrepCont_le_exp_decay_gen□ \square □
Used by kmsIntegrand_deriv_bound
Lemma 116 (norm_term2_le). source ↗
h_bound term 2‖reflKrep(θ+πz)‖·‖deriv KrepCont f(θ−πz)‖ ≤ Cdf·Cg·(e^{πR}·cosh θ·exp(−κ·cosh θ)) (mirror of term 1, with the deriv on the f-factor: deriv KrepCont f decaying in cosh(θ−π Re z), reflKrep bounded by Cg).
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { z : C } , − 1 < z . i m → z . i m < 0 → ∀ { σ m i n R : R } , 0 < σ m i n → σ m i n ≤ sin ( − ( π ⋅ z . i m ) ) → ∣ z . r e ∣ ≤ R → ∀ ( θ : R ) , ∥ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) ( θ + π ⋅ z ) ) ) ∥ ⋅ ∥ D ( K C m f ) ( θ − π ⋅ z ) ∥ ≤ 1 / 2 ⋅ ( ∣ m ∣ ⋅ ∫ ( x : V ) , ( ∣ x 0 ∣ + ∣ x 1 ∣ ) ⋅ ∥ f x ∥ ) ⋅ ( 1 / 2 ⋅ ∫ ( x : V ) , ∥ g x ∥ ) ⋅ ( exp ( π ⋅ R ) ⋅ cosh θ ⋅ exp ( − ( m ⋅ σ m i n ⋅ δ ⋅ exp ( − ( π ⋅ R ) ) ⋅ cosh θ ) ) ) 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{z : \mathbb{C}\}, -1 < z.\mathrm{im} \to z.\mathrm{im} < 0 \to \forall \{\sigma\mathrm{min} R : \mathbb{R}\}, 0 < \sigma\mathrm{min} \to \sigma\mathrm{min} \le \sin\,(-(\pi \cdot z.\mathrm{im})) \to |z.\mathrm{re}| \le R \to \forall (\theta : \mathbb{R}), \|(\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,(\theta + \pi \cdot z)))\| \cdot \|\mathrm{D}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f)\,(\theta - \pi \cdot z)\| \le 1 / \sqrt 2 \cdot (|m| \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (|x\,0| + |x\,1|) \cdot \|f\,x\|) \cdot (1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|g\,x\|) \cdot (\exp\,(\pi \cdot R) \cdot \cosh\,\theta \cdot \exp\,(-(m \cdot \sigma\mathrm{min} \cdot \delta \cdot \exp\,(-(\pi \cdot R)) \cdot \cosh\,\theta))) 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { z : C } , − 1 < z . im → z . im < 0 → ∀ { σ min R : R } , 0 < σ min → σ min ≤ sin ( − ( π ⋅ z . im )) → ∣ z . re ∣ ≤ R → ∀ ( θ : R ) , ∥ ( starRingEnd C ) ( K C m g (( starRingEnd C ) ( θ + π ⋅ z ))) ∥ ⋅ ∥ D ( K C m f ) ( θ − π ⋅ z ) ∥ ≤ 1/ 2 ⋅ ( ∣ m ∣ ⋅ ∫ ( x : V ) , ( ∣ x 0∣ + ∣ x 1∣ ) ⋅ ∥ f x ∥ ) ⋅ ( 1/ 2 ⋅ ∫ ( x : V ) , ∥ g x ∥ ) ⋅ ( exp ( π ⋅ R ) ⋅ cosh θ ⋅ exp ( − ( m ⋅ σ min ⋅ δ ⋅ exp ( − ( π ⋅ R )) ⋅ cosh θ ))) Proof. By norm_reflKrepCont_lesin_neg_pi_mul_posprod_norm_bound_cosh_shiftnorm_deriv_KrepCont_le_exp_decay□ \square □
Used by kmsIntegrand_deriv_bound
Lemma 117 (kmsIntegrand_deriv_bound). source ↗
The h_bound pointwise content : ‖F'(z,θ)‖ ≤ π·(Cdg·Cf + Cdf·Cg)·(e^{πR}·cosh θ·exp(−κ·cosh θ)), κ = m σmin δ e^{−πR} — a z-independent (for the ball) integrable-in-θ bound on the integrand z-derivative. Combines norm_two_term_le + norm_term1_le + norm_term2_le.
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { z : C } , − 1 < z . i m → z . i m < 0 → ∀ { σ m i n R : R } , 0 < σ m i n → σ m i n ≤ sin ( − ( π ⋅ z . i m ) ) → ∣ z . r e ∣ ≤ R → ∀ ( θ : R ) , ∥ D ( λ u ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) u ) ) ) ( θ + π ⋅ z ) ⋅ π ⋅ K C m f ( θ − π ⋅ z ) + ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) ( θ + π ⋅ z ) ) ) ⋅ ( D ( K C m f ) ( θ − π ⋅ z ) ⋅ − π ) ∥ ≤ π ⋅ ( ( 1 / 2 ⋅ ( ∣ m ∣ ⋅ ∫ ( x : V ) , ( ∣ x 0 ∣ + ∣ x 1 ∣ ) ⋅ ∥ g x ∥ ) ⋅ ( 1 / 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ ) + 1 / 2 ⋅ ( ∣ m ∣ ⋅ ∫ ( x : V ) , ( ∣ x 0 ∣ + ∣ x 1 ∣ ) ⋅ ∥ f x ∥ ) ⋅ ( 1 / 2 ⋅ ∫ ( x : V ) , ∥ g x ∥ ) ) ⋅ ( exp ( π ⋅ R ) ⋅ cosh θ ⋅ exp ( − ( m ⋅ σ m i n ⋅ δ ⋅ exp ( − ( π ⋅ R ) ) ⋅ cosh θ ) ) ) ) 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{z : \mathbb{C}\}, -1 < z.\mathrm{im} \to z.\mathrm{im} < 0 \to \forall \{\sigma\mathrm{min} R : \mathbb{R}\}, 0 < \sigma\mathrm{min} \to \sigma\mathrm{min} \le \sin\,(-(\pi \cdot z.\mathrm{im})) \to |z.\mathrm{re}| \le R \to \forall (\theta : \mathbb{R}), \|\mathrm{D}\,(\lambda u \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,u)))\,(\theta + \pi \cdot z) \cdot \pi \cdot \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta - \pi \cdot z) + (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,(\theta + \pi \cdot z))) \cdot (\mathrm{D}\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f)\,(\theta - \pi \cdot z) \cdot -\pi)\| \le \pi \cdot ((1 / \sqrt 2 \cdot (|m| \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (|x\,0| + |x\,1|) \cdot \|g\,x\|) \cdot (1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|f\,x\|) + 1 / \sqrt 2 \cdot (|m| \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (|x\,0| + |x\,1|) \cdot \|f\,x\|) \cdot (1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|g\,x\|)) \cdot (\exp\,(\pi \cdot R) \cdot \cosh\,\theta \cdot \exp\,(-(m \cdot \sigma\mathrm{min} \cdot \delta \cdot \exp\,(-(\pi \cdot R)) \cdot \cosh\,\theta)))) 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { z : C } , − 1 < z . im → z . im < 0 → ∀ { σ min R : R } , 0 < σ min → σ min ≤ sin ( − ( π ⋅ z . im )) → ∣ z . re ∣ ≤ R → ∀ ( θ : R ) , ∥ D ( λ u ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) u ))) ( θ + π ⋅ z ) ⋅ π ⋅ K C m f ( θ − π ⋅ z ) + ( starRingEnd C ) ( K C m g (( starRingEnd C ) ( θ + π ⋅ z ))) ⋅ ( D ( K C m f ) ( θ − π ⋅ z ) ⋅ − π ) ∥ ≤ π ⋅ (( 1/ 2 ⋅ ( ∣ m ∣ ⋅ ∫ ( x : V ) , ( ∣ x 0∣ + ∣ x 1∣ ) ⋅ ∥ g x ∥ ) ⋅ ( 1/ 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ ) + 1/ 2 ⋅ ( ∣ m ∣ ⋅ ∫ ( x : V ) , ( ∣ x 0∣ + ∣ x 1∣ ) ⋅ ∥ f x ∥ ) ⋅ ( 1/ 2 ⋅ ∫ ( x : V ) , ∥ g x ∥ )) ⋅ ( exp ( π ⋅ R ) ⋅ cosh θ ⋅ exp ( − ( m ⋅ σ min ⋅ δ ⋅ exp ( − ( π ⋅ R )) ⋅ cosh θ )))) Proof. By norm_two_term_lenorm_term1_lenorm_term2_le□ \square □
Used by kmsFun_differentiableAtkmsFunCut_differentiableAt
Lemma 118 (kmsFun_differentiableAt). source ↗
kmsFun m f g is differentiable at every interior strip point−1<Im z₀<0), for f,g continuous with compact support strictly inside the wedge (uniform margin δ>0). The holomorphy half of DiffContOnCl. Assembles the six dominated-derivative hypotheses (hF_meas, hF_int, hF'_meas, h_diff, h_bound, bound_integrable — all proven) over a strip-interior ball (with σ_min from exists_sin_min, R from the ball).
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { z 0 : C } , − 1 < z 0 . i m → z 0 . i m < 0 → D i f f e r e n t i a b l e A t C ( F m f g ) z 0 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{z_{0} : \mathbb{C}\}, -1 < z_{0}.\mathrm{im} \to z_{0}.\mathrm{im} < 0 \to \mathrm{DifferentiableAt}\,\mathbb{C}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g)\,z_{0} 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { z 0 : C } , − 1 < z 0 . im → z 0 . im < 0 → DifferentiableAt C ( F m f g ) z 0 Proof. By hasDerivAt_kmsIntegrand_zcontinuous_kmsIntegrand_in_thetacontinuous_kmsIntegrand_deriv_in_thetaintegrable_kmsIntegrandexists_sin_minkmsIntegrand_deriv_boundKrepContintegrable_cosh_mul_exp_neg_const_mul_cosh□ \square □
Used by kmsFun_differentiableOn
Lemma 119 (kmsFun_differentiableOn). source ↗
kmsFun m f g is holomorphic on the whole open strip{−1<Im z<0} — the DifferentiableOn half of DiffContOnCl, an immediate corollary of kmsFun_differentiableAt (the strip is open, so DifferentiableAt at each point gives DifferentiableWithinAt).
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → D i f f e r e n t i a b l e O n C ( F m f g ) ( i m − 1 ′ ( − 1 , 0 ) ) 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \mathrm{DifferentiableOn}\,\mathbb{C}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g)\,(\mathrm{im} ^{-1}{}' ({-1},{0})) 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → DifferentiableOn C ( F m f g ) ( im − 1 ′ ( − 1 , 0 )) Proof. By kmsFun_differentiableAt□ \square □
Used by stripKMSrvd_closure
Definition 120 (kmsFunCut). source ↗
θ-truncated KMS function (cutoff R): the same integrand as kmsFun, but integrated over the compact rapidity window θ ∈ [−R,R]. The truncation device (GPT-5.5): the compact θ-domain makes kmsFunCut R holomorphic on the open strip, continuous on the closed strip, and trivially BOUNDED there — with no logarithmic blow-up — so Hadamard three-lines bounds it by the edge constant B for every R, and R→∞ (dominated convergence) transfers the bound to kmsFun.
Used by norm_kmsFunCut_lekmsFunCut_differentiableAtkmsFunCut_differentiableOnkmsFunCut_continuousOnkmsFunCut_ofRealkmsFunCut_sub_Inorm_kmsFunCut_diff_ofReal_lenorm_kmsFunCut_diff_sub_I_le
Lemma 121 (norm_kmsFunCut_le). source ↗
Trivial closed-strip bound for kmsFunCut (Im z ∈ [−1,0], R ≥ 0): ‖kmsFunCut R z‖ ≤ C_g·C_f·2R with C_h = (1/√2)∫‖h‖. Each KrepCont factor has argument imaginary part −π·Im z ∈ [0,π], so the plain bound norm_KrepCont_le_const applies; integrate the constant C_g·C_f over [−R,R] (measure 2R). This is the BddAbove Hadamard needs — finite for each R, the log-blowup absent.
0 ≤ m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 ≤ δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { R : R } , 0 ≤ R → ∀ { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → ∥ k m s m f g R z ∥ ≤ ( 1 / 2 ⋅ ∫ ( x : V ) , ∥ g x ∥ ) ⋅ ( 1 / 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ ) ⋅ ( 2 ⋅ R ) 0 \le m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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 (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall \{R : \mathbb{R}\}, 0 \le R \to \forall \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \|\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,R\,z\| \le (1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|g\,x\|) \cdot (1 / \sqrt 2 \cdot \int (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \|f\,x\|) \cdot (2 \cdot R) 0 ≤ m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 ≤ δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ { R : R } , 0 ≤ R → ∀ { z : C } , − 1 ≤ z . im → z . im ≤ 0 → ∥ kms m f g R z ∥ ≤ ( 1/ 2 ⋅ ∫ ( x : V ) , ∥ g x ∥ ) ⋅ ( 1/ 2 ⋅ ∫ ( x : V ) , ∥ f x ∥ ) ⋅ ( 2 ⋅ R ) Proof. By KrepContnorm_KrepCont_le_const□ \square □
Used by norm_kmsFunCut_diff_le
Lemma 122 (kmsFunCut_differentiableAt). source ↗
kmsFunCut Rc is differentiable at every interior strip point−1<Im z₀<0) — the open-strip (DifferentiableOn) half of DiffContOnCl for the truncated function. Same dominated-derivative assembly as kmsFun_differentiableAt, but over the restricted measure volume.restrict [−Rc,Rc]; the interior σ-damped bound (kmsIntegrand_deriv_bound) and integrability transfer to the restricted measure via .integrableOn.
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ ( R c : R ) { z 0 : C } , − 1 < z 0 . i m → z 0 . i m < 0 → D i f f e r e n t i a b l e A t C ( k m s m f g R c ) z 0 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall (\mathrm{Rc} : \mathbb{R}) \{z_{0} : \mathbb{C}\}, -1 < z_{0}.\mathrm{im} \to z_{0}.\mathrm{im} < 0 \to \mathrm{DifferentiableAt}\,\mathbb{C}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,\mathrm{Rc})\,z_{0} 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ ( Rc : R ) { z 0 : C } , − 1 < z 0 . im → z 0 . im < 0 → DifferentiableAt C ( kms m f g Rc ) z 0 Proof. By hasDerivAt_kmsIntegrand_zcontinuous_kmsIntegrand_in_thetacontinuous_kmsIntegrand_deriv_in_thetaintegrable_kmsIntegrandexists_sin_minkmsIntegrand_deriv_boundKrepContintegrable_cosh_mul_exp_neg_const_mul_cosh□ \square □
Used by kmsFunCut_differentiableOn
Lemma 123 (kmsFunCut_differentiableOn). source ↗
kmsFunCut Rc is holomorphic on the open strip{−1<Im z<0} — the DifferentiableOn half of DiffContOnCl for the truncated function (immediate from kmsFunCut_differentiableAt).
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ ( R c : R ) , D i f f e r e n t i a b l e O n C ( k m s m f g R c ) ( i m − 1 ′ ( − 1 , 0 ) ) 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall (\mathrm{Rc} : \mathbb{R}), \mathrm{DifferentiableOn}\,\mathbb{C}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,\mathrm{Rc})\,(\mathrm{im} ^{-1}{}' ({-1},{0})) 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ ( Rc : R ) , DifferentiableOn C ( kms m f g Rc ) ( im − 1 ′ ( − 1 , 0 )) Proof. By kmsFunCut_differentiableAt□ \square □
Used by norm_kmsFunCut_diff_le
Lemma 124 (kmsFunCut_continuousOn). source ↗
kmsFunCut Rc is continuous on the CLOSED strip{−1≤Im z≤0} — the ContinuousOn half of DiffContOnCl. This is where the θ-truncation pays off: the integrand is dominated by the constant C_g·C_f uniformly on the closed strip (no degeneration, since ‖KrepCont‖ ≤ C for Im arg ∈ [0,π]), which is integrable on the finite-measure window [−Rc,Rc]; continuousOn_of_dominated + the integrand’s z-continuity (differentiable_kmsIntegrand) close it.
0 ≤ m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 ≤ δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ ( R c : R ) , C o n t i n u o u s O n ( k m s m f g R c ) ( i m − 1 ′ [ − 1 , 0 ] ) 0 \le m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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 (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), g\,x \ne 0 \to \delta \le x\,1 - x\,0 \wedge \delta \le x\,1 + x\,0) \to \forall (\mathrm{Rc} : \mathbb{R}), \mathrm{ContinuousOn}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,\mathrm{Rc})\,(\mathrm{im} ^{-1}{}' [{-1},{0}]) 0 ≤ m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 ≤ δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ∀ ( Rc : R ) , ContinuousOn ( kms m f g Rc ) ( im − 1 ′ [ − 1 , 0 ]) Proof. By differentiable_kmsIntegrandcontinuous_kmsIntegrand_in_thetaKrepContnorm_KrepCont_le_const□ \square □
Used by norm_kmsFunCut_diff_le
Lemma 125 (kmsFunCut_ofReal). source ↗
kmsFunCut on the real axisKrepCont→Krep collapse as kmsFun_ofReal, over [−R,R].
k m s m f g R t = ∫ ( θ : R ) i n [ − R , R ] , ( s t a r R i n g E n d C ) ( K m g ( θ + π ⋅ t ) ) ⋅ K m f ( θ − π ⋅ t ) \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,R\,t = \int (\theta : \mathbb{R}) in [{-R},{R}], (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,(\theta + \pi \cdot t)) \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,(\theta - \pi \cdot t) kms m f g R t = ∫ ( θ : R ) in [ − R , R ] , ( starRingEnd C ) ( K m g ( θ + π ⋅ t )) ⋅ K m f ( θ − π ⋅ t ) Proof. By KrepContKrepCont_ofReal□ \square □
Used by kmsFunCut_sub_Inorm_kmsFunCut_diff_ofReal_le
Lemma 126 (kmsFunCut_sub_I). source ↗
kmsFunCut bottom edgeF(t−i) = conj F(t) (real f,g) — same iπ-shift collapse as kmsFun_sub_I, over [−R,R].
( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → ∀ ( R t : R ) , k m s m f g R ( t − i ) = ( s t a r R i n g E n d C ) ( k m s m f g R t ) (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(f\,x) = f\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(g\,x) = g\,x) \to \forall (R t : \mathbb{R}), \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,R\,(t - i) = (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,R\,t) ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → ∀ ( R t : R ) , kms m f g R ( t − i ) = ( starRingEnd C ) ( kms m f g R t ) Proof. By kmsFunCut_ofRealKrepKrepContKrepCont_add_pi_I□ \square □
Used by norm_kmsFunCut_diff_sub_I_le
Lemma 127 (norm_le_of_strip_edges). source ↗
Abstract Hadamard-on-the-strip bound. A function Φ holomorphic on the open strip {−1<Im z<0}, continuous and bounded on the closed strip, with both boundary lines ≤ b, satisfies ‖Φ z‖ ≤ b everywhere in the closed strip. Rotate w↦−i·w onto verticalClosedStrip 0 1 and apply Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip' (edge consts b,b, b^(1−s)·b^s=b). The reusable core of the truncation argument (used for kmsFunCut and for the annular differences kmsFunCut S − kmsFunCut R).
D i f f e r e n t i a b l e O n C Φ ( i m − 1 ′ ( − 1 , 0 ) ) → C o n t i n u o u s O n Φ ( i m − 1 ′ [ − 1 , 0 ] ) → B d d A b o v e ( n o r m ∘ Φ ′ ′ i m − 1 ′ [ − 1 , 0 ] ) → ( ∀ ( t : R ) , ∥ Φ t ∥ ≤ b ) → ( ∀ ( t : R ) , ∥ Φ ( t − i ) ∥ ≤ b ) → ∀ { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → ∥ Φ z ∥ ≤ b \mathrm{DifferentiableOn}\,\mathbb{C}\,\Phi\,(\mathrm{im} ^{-1}{}' ({-1},{0})) \to \mathrm{ContinuousOn}\,\Phi\,(\mathrm{im} ^{-1}{}' [{-1},{0}]) \to \mathrm{BddAbove}\,(\mathrm{norm} \circ \Phi '' \mathrm{im} ^{-1}{}' [{-1},{0}]) \to (\forall (t : \mathbb{R}), \|\Phi\,t\| \le b) \to (\forall (t : \mathbb{R}), \|\Phi\,(t - i)\| \le b) \to \forall \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \|\Phi\,z\| \le b DifferentiableOn C Φ ( im − 1 ′ ( − 1 , 0 )) → ContinuousOn Φ ( im − 1 ′ [ − 1 , 0 ]) → BddAbove ( norm ∘ Φ ′′ im − 1 ′ [ − 1 , 0 ]) → ( ∀ ( t : R ) , ∥Φ t ∥ ≤ b ) → ( ∀ ( t : R ) , ∥Φ ( t − i ) ∥ ≤ b ) → ∀ { z : C } , − 1 ≤ z . im → z . im ≤ 0 → ∥Φ z ∥ ≤ b Proof. Immediate from the definitions. □ \square □
Used by norm_kmsFunCut_diff_le
Lemma 128 (real_L2_inner_le). source ↗
Real Cauchy–Schwarz for nonnegative L² functions: ∫ u·v ≤ √(∫u²)·√(∫v²). Hölder p=q=2.
M e m L p u 2 μ → M e m L p v 2 μ → 0 ≤ [ μ ] u → 0 ≤ [ μ ] v → ∫ ( θ : R ) , u θ ⋅ v θ ∂ μ ≤ ( ∫ ( θ : R ) , u θ 2 ∂ μ ) ⋅ ( ∫ ( θ : R ) , v θ 2 ∂ μ ) \mathrm{MemLp}\,u\,2\,\mu \to \mathrm{MemLp}\,v\,2\,\mu \to 0 \le [\mu] u \to 0 \le [\mu] v \to \int (\theta : \mathbb{R}), u\,\theta \cdot v\,\theta \partial \mu \le \sqrt (\int (\theta : \mathbb{R}), {u\,\theta}^{2} \partial \mu) \cdot \sqrt (\int (\theta : \mathbb{R}), {v\,\theta}^{2} \partial \mu) MemLp u 2 μ → MemLp v 2 μ → 0 ≤ [ μ ] u → 0 ≤ [ μ ] v → ∫ ( θ : R ) , u θ ⋅ v θ ∂ μ ≤ ( ∫ ( θ : R ) , u θ 2 ∂ μ ) ⋅ ( ∫ ( θ : R ) , v θ 2 ∂ μ ) Proof. Immediate from the definitions. □ \square □
Used by tail_term_le
Lemma 129 (tail_term_le). source ↗
One shifted-tail term : with the cutoff indicator tied to the FIRST factor’s shift +c, ∫ 1_{R<|θ+c|}·‖Krep h₁(θ+c)‖·‖Krep h₂(θ+d)‖ ≤ T_{h₁}(R)·‖Krep h₂‖₂. Real Cauchy–Schwarz (real_L2_inner_le) on 1_{·}·‖Krep h₁(·+c)‖ and ‖Krep h₂(·+d)‖, then translation-invariance (integral_add_right_eq_self) turns each shifted slice integral into the t-independent tail / full norm.
M e m L p ( K m h 1 ) 2 v o l → M e m L p ( K m h 2 ) 2 v o l → ∀ ( R c d : R ) , ∫ ( θ : R ) , { θ ∣ R < ∣ θ + c ∣ } .1 1 θ ⋅ ( ∥ K m h 1 ( θ + c ) ∥ ⋅ ∥ K m h 2 ( θ + d ) ∥ ) ≤ ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m h 1 θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m h 2 θ ∥ 2 ) \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,h_{1})\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,h_{2})\,2\,\mathrm{vol} \to \forall (R c d : \mathbb{R}), \int (\theta : \mathbb{R}), \{\theta|R < |\theta + c|\}.\mathbf{1}\,1\,\theta \cdot (\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,h_{1}\,(\theta + c)\| \cdot \|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,h_{2}\,(\theta + d)\|) \le \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,h_{1}\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,h_{2}\,\theta\|}^{2}) MemLp ( K m h 1 ) 2 vol → MemLp ( K m h 2 ) 2 vol → ∀ ( R c d : R ) , ∫ ( θ : R ) , { θ ∣ R < ∣ θ + c ∣ } . 1 1 θ ⋅ ( ∥ K m h 1 ( θ + c ) ∥ ⋅ ∥ K m h 2 ( θ + d ) ∥ ) ≤ ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m h 1 θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m h 2 θ ∥ 2 ) Proof. By real_L2_inner_le□ \square □
Used by tail_integral_le
Lemma 130 (tail_geom). source ↗
Shifted-tail geometry (the crux of the annular bound): if |θ| > R then |θ+a| > R or |θ−a| > R. Since 2|θ| = |(θ+a)+(θ−a)| ≤ |θ+a|+|θ−a|, both ≤ R would force |θ| ≤ R. This is why the scalar KMS product has uniformly small edge tails even though the individual L² slices do not.
R < ∣ θ ∣ → R < ∣ θ + a ∣ ∨ R < ∣ θ − a ∣ R < |\theta| \to R < |\theta + a| \vee R < |\theta - a| R < ∣ θ ∣ → R < ∣ θ + a ∣ ∨ R < ∣ θ − a ∣ Proof. Immediate from the definitions. □ \square □
Used by tail_integral_le
Lemma 131 (tail_integral_le). source ↗
The full tail integral bound ∫_{|θ|>R} ‖Krep g(θ+πt)‖·‖Krep f(θ−πt)‖ ≤ ε_R, UNIFORM in t, with ε_R = T_g(R)·‖Krep f‖₂ + T_f(R)·‖Krep g‖₂. Split the {|θ|>R} indicator by tail_geom into the two shifted tails and apply tail_term_le to each. The scalar product’s edge tail is t-uniform — the heart of the annular-difference route to closed-strip continuity.
M e m L p ( K m f ) 2 v o l → M e m L p ( K m g ) 2 v o l → ∀ ( R : R ) , ∫ ( θ : R ) , { θ ∣ R < ∣ θ ∣ } .1 1 θ ⋅ ( ∥ K m g ( θ + π ⋅ t ) ∥ ⋅ ∥ K m f ( θ − π ⋅ t ) ∥ ) ≤ ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m g θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) + ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m f θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m g θ ∥ 2 ) \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,2\,\mathrm{vol} \to \forall (R : \mathbb{R}), \int (\theta : \mathbb{R}), \{\theta|R < |\theta|\}.\mathbf{1}\,1\,\theta \cdot (\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,(\theta + \pi \cdot t)\| \cdot \|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,(\theta - \pi \cdot t)\|) \le \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) + \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta\|}^{2}) MemLp ( K m f ) 2 vol → MemLp ( K m g ) 2 vol → ∀ ( R : R ) , ∫ ( θ : R ) , { θ ∣ R < ∣ θ ∣ } . 1 1 θ ⋅ ( ∥ K m g ( θ + π ⋅ t ) ∥ ⋅ ∥ K m f ( θ − π ⋅ t ) ∥ ) ≤ ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m g θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) + ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m f θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m g θ ∥ 2 ) Proof. By tail_term_letail_geom□ \square □
Used by norm_kmsFunCut_diff_ofReal_le
Lemma 132 (norm_kmsFunCut_diff_ofReal_le). source ↗
Annular top-edge bound (S ≥ R): ‖kmsFunCut S t − kmsFunCut R t‖ ≤ ε_R UNIFORMLY in t. The difference is ∫ (1_{Icc(−S,S)} − 1_{Icc(−R,R)})·I whose integrand has norm ≤ 1_{|θ|>R}·w pointwise (I is the real-axis integrand, w=‖I‖; on |θ|≤R it cancels, on R<|θ|≤S it is I, beyond S it is 0); then norm_integral_le_integral_norm + integral_mono + tail_integral_le.
M e m L p ( K m f ) 2 v o l → M e m L p ( K m g ) 2 v o l → ∀ { R S : R } , R ≤ S → ∥ k m s m f g S t − k m s m f g R t ∥ ≤ ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m g θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) + ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m f θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m g θ ∥ 2 ) \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,2\,\mathrm{vol} \to \forall \{R S : \mathbb{R}\}, R \le S \to \|\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,S\,t - \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,R\,t\| \le \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) + \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta\|}^{2}) MemLp ( K m f ) 2 vol → MemLp ( K m g ) 2 vol → ∀ { R S : R } , R ≤ S → ∥ kms m f g S t − kms m f g R t ∥ ≤ ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m g θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) + ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m f θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m g θ ∥ 2 ) Proof. By kmsFunCut_ofRealtail_integral_le□ \square □
Used by norm_kmsFunCut_diff_sub_I_lenorm_kmsFunCut_diff_le
Lemma 133 (norm_kmsFunCut_diff_sub_I_le). source ↗
Annular bottom-edge bound (S ≥ R, real f,g): same ε_R as the top edge, via kmsFunCut_sub_I (F(t−i)=conj F(t)) ⟹ the difference is the conjugate of the top-edge difference, equal norm.
( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → M e m L p ( K m f ) 2 v o l → M e m L p ( K m g ) 2 v o l → ∀ { R S : R } , R ≤ S → ∥ k m s m f g S ( t − i ) − k m s m f g R ( t − i ) ∥ ≤ ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m g θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) + ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m f θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m g θ ∥ 2 ) (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(f\,x) = f\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(g\,x) = g\,x) \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,2\,\mathrm{vol} \to \forall \{R S : \mathbb{R}\}, R \le S \to \|\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,S\,(t - i) - \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,R\,(t - i)\| \le \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) + \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta\|}^{2}) ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → MemLp ( K m f ) 2 vol → MemLp ( K m g ) 2 vol → ∀ { R S : R } , R ≤ S → ∥ kms m f g S ( t − i ) − kms m f g R ( t − i ) ∥ ≤ ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m g θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) + ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m f θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m g θ ∥ 2 ) Proof. By kmsFunCut_sub_Inorm_kmsFunCut_diff_ofReal_le□ \square □
Used by norm_kmsFunCut_diff_le
Lemma 134 (norm_kmsFunCut_diff_le). source ↗
The annular difference is ≤ ε_R on the WHOLE closed strip (S ≥ R). kmsFunCut S − kmsFunCut R is DiffContOnCl + bounded (difference of two such), and both boundary lines are ≤ ε_R (norm_kmsFunCut_diff_ofReal_le/_sub_I_le); norm_le_of_strip_edges propagates the edge bound inward. Combined with ε_R → 0 this is the uniform-Cauchy property of {kmsFunCut n} on the closed strip.
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g 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 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → M e m L p ( K m f ) 2 v o l → M e m L p ( K m g ) 2 v o l → ∀ { R S : R } , 0 ≤ R → R ≤ S → ∀ { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → ∥ k m s m f g S z − k m s m f g R z ∥ ≤ ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m g θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) + ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m f θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m g θ ∥ 2 ) 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,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 (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(g\,x) = g\,x) \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,2\,\mathrm{vol} \to \forall \{R S : \mathbb{R}\}, 0 \le R \to R \le S \to \forall \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \|\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,S\,z - \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,R\,z\| \le \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) + \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta\|}^{2}) 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → MemLp ( K m f ) 2 vol → MemLp ( K m g ) 2 vol → ∀ { R S : R } , 0 ≤ R → R ≤ S → ∀ { z : C } , − 1 ≤ z . im → z . im ≤ 0 → ∥ kms m f g S z − kms m f g R z ∥ ≤ ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m g θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) + ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m f θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m g θ ∥ 2 ) Proof. By norm_kmsFunCut_lekmsFunCut_differentiableOnkmsFunCut_continuousOnnorm_le_of_strip_edgesnorm_kmsFunCut_diff_ofReal_lenorm_kmsFunCut_diff_sub_I_le□ \square □
Used by norm_kmsFun_sub_kmsFunCut_le
Lemma 135 (integrable_kmsFun_integrand_closed). source ↗
The kmsFun integrand is integrable at every CLOSED-strip z (−1≤Im z≤0). Both slices are L² via memLp_KrepCont_affine_closed (arg Im = −π·Im z ∈ [0,π], including the edges), so the product is integrable by AM-GM and the integrand by integrable_norm_iff. This is the per-z input that makes kmsFunCut n z → kmsFun z hold up to the boundary.
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g 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 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → M e m L p ( K m f ) 2 v o l → M e m L p ( K m g ) 2 v o l → ∀ { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → I n t e g r a b l e ( λ θ ↦ ( s t a r R i n g E n d C ) ( K C m g ( ( s t a r R i n g E n d C ) ( θ + π ⋅ z ) ) ) ⋅ K C m f ( θ − π ⋅ z ) ) v o l 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,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 (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(g\,x) = g\,x) \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,2\,\mathrm{vol} \to \forall \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \mathrm{Integrable}\,(\lambda \theta \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,g\,((\mathrm{starRingEnd}\,\mathbb{C})\,(\theta + \pi \cdot z))) \cdot \href{/browser/qiqth-fock-wedgeanalyticity#d-qiqth-fock-wedgeanalyticity-krepcont}{K_{\mathbb{C}}}\,m\,f\,(\theta - \pi \cdot z))\,\mathrm{vol} 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → MemLp ( K m f ) 2 vol → MemLp ( K m g ) 2 vol → ∀ { z : C } , − 1 ≤ z . im → z . im ≤ 0 → Integrable ( λ θ ↦ ( starRingEnd C ) ( K C m g (( starRingEnd C ) ( θ + π ⋅ z ))) ⋅ K C m f ( θ − π ⋅ z )) vol Proof. By memLp_KrepCont_affine_closed□ \square □
Used by kmsFunCut_tendsto_closedkmsFun_add_leftkmsFun_add_right
Lemma 136 (kmsFunCut_tendsto_closed). source ↗
kmsFunCut n z → kmsFun z up to the boundaryz, tendsto_setIntegral_of_monotone (⋃ₙ[−n,n]=ℝ) with the closed-strip integrability integrable_kmsFun_integrand_closed.
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g 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 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → M e m L p ( K m f ) 2 v o l → M e m L p ( K m g ) 2 v o l → ∀ { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → T e n d s t o ( λ n ↦ k m s m f g ( n ) z ) a t T o p ( N ( F m f g z ) ) 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,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 (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(g\,x) = g\,x) \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,2\,\mathrm{vol} \to \forall \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \mathrm{Tendsto}\,(\lambda n \mapsto \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,(n)\,z)\,\mathrm{atTop}\,(\mathcal{N}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g\,z)) 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → MemLp ( K m f ) 2 vol → MemLp ( K m g ) 2 vol → ∀ { z : C } , − 1 ≤ z . im → z . im ≤ 0 → Tendsto ( λn ↦ kms m f g ( n ) z ) atTop ( N ( F m f g z )) Proof. By integrable_kmsFun_integrand_closedKrepCont□ \square □
Used by norm_kmsFun_sub_kmsFunCut_le
Lemma 137 (norm_kmsFun_sub_kmsFunCut_le). source ↗
Uniform error ‖kmsFun z − kmsFunCut R z‖ ≤ ε_R on the closed strip (R ≥ 0). Pass S→∞ to the limit in norm_kmsFunCut_diff_le via kmsFunCut_tendsto_closed + le_of_tendsto.
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g 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 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → M e m L p ( K m f ) 2 v o l → M e m L p ( K m g ) 2 v o l → ∀ { R : R } , 0 ≤ R → ∀ { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → ∥ F m f g z − k m s m f g R z ∥ ≤ ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m g θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) + ( ∫ ( θ : R ) i n { θ ∣ R < ∣ θ ∣ } , ∥ K m f θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m g θ ∥ 2 ) 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,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 (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(g\,x) = g\,x) \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,2\,\mathrm{vol} \to \forall \{R : \mathbb{R}\}, 0 \le R \to \forall \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \|\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g\,z - \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,R\,z\| \le \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) + \sqrt (\int (\theta : \mathbb{R}) in \{\theta|R < |\theta|\}, {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) \cdot \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g\,\theta\|}^{2}) 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → MemLp ( K m f ) 2 vol → MemLp ( K m g ) 2 vol → ∀ { R : R } , 0 ≤ R → ∀ { z : C } , − 1 ≤ z . im → z . im ≤ 0 → ∥ F m f g z − kms m f g R z ∥ ≤ ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m g θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) + ( ∫ ( θ : R ) in { θ ∣ R < ∣ θ ∣ } , ∥ K m f θ ∥ 2 ) ⋅ ( ∫ ( θ : R ) , ∥ K m g θ ∥ 2 ) Proof. By norm_kmsFunCut_diff_lekmsFunCut_tendsto_closed□ \square □
Used by norm_kmsFun_le_norm_mul
Lemma 138 (kmsFunCut_zero). source ↗
kmsFunCut m f g 0 z = 0 — the cutoff window [−0,0] = {0} has measure zero.
k m s m f g 0 z = 0 \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfuncut}{\mathrm{kms}}\,m\,f\,g\,0\,z = 0 kms m f g 0 z = 0 Proof. By KrepCont□ \square □
Used by norm_kmsFun_le_norm_mul
Lemma 139 (kmsFun_add_left). source ↗
kmsFun is additive in the f slotf₁,f₂,g with MemLp amplitudes). KrepCont_add distributes the f-factor; the outer integral splits by integral_add (each summand integrable via integrable_kmsFun_integrand_closed).
0 < m → ∀ { f 1 f 2 g : V → C } , 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 o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g 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 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → 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 g ) 2 v o l → ∀ { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → F m ( f 1 + f 2 ) g z = F m f 1 g z + F m f 2 g z 0 < m \to \forall \{f_{1} f_{2} g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f_{1} \to \mathrm{HasCompactSupport}\,f_{1} \to \mathrm{Continuous}\,f_{2} \to \mathrm{HasCompactSupport}\,f_{2} \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \forall \{\delta : \mathbb{R}\}, 0 < \delta \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \mathrm{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{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}), g\,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})\,(\mathrm{f}\,x) = \mathrm{f}\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{f}\,x) = \mathrm{f}\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(g\,x) = g\,x) \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\,g)\,2\,\mathrm{vol} \to \forall \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,(f_{1} + f_{2})\,g\,z = \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f_{1}\,g\,z + \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f_{2}\,g\,z 0 < m → ∀ { f 1 f 2 g : V → C } , Continuous f 1 → HasCompactSupport f 1 → Continuous f 2 → HasCompactSupport f 2 → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → MemLp ( K m f 1 ) 2 vol → MemLp ( K m f 2 ) 2 vol → MemLp ( K m g ) 2 vol → ∀ { z : C } , − 1 ≤ z . im → z . im ≤ 0 → F m ( f 1 + f 2 ) g z = F m f 1 g z + F m f 2 g z Proof. By integrable_kmsFun_integrand_closedKrepContKrepCont_add□ \square □
Used by kmsFun_sub_left
Lemma 140 (kmsFun_add_right). source ↗
kmsFun is additive in the g slotkmsFun_add_left but on the conjugated g-factor (KrepCont_add + map_add for conj).
0 < m → ∀ { f g 1 g 2 : 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 → C o n t i n u o u s g 1 → H a s C o m p a c t S u p p o r t g 1 → C o n t i n u o u s g 2 → H a s C o m p a c t S u p p o r t g 2 → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g 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 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → M e m L p ( K m f ) 2 v o l → M e m L p ( K m g 1 ) 2 v o l → M e m L p ( K m g 2 ) 2 v o l → ∀ { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → F m f ( g 1 + g 2 ) z = F m f g 1 z + F m f g 2 z 0 < m \to \forall \{f g_{1} g_{2} : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g_{1} \to \mathrm{HasCompactSupport}\,g_{1} \to \mathrm{Continuous}\,g_{2} \to \mathrm{HasCompactSupport}\,g_{2} \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{g}\,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{g}\,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 (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{g}\,x) = \mathrm{g}\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{g}\,x) = \mathrm{g}\,x) \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{1})\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{2})\,2\,\mathrm{vol} \to \forall \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,(g_{1} + g_{2})\,z = \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g_{1}\,z + \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g_{2}\,z 0 < m → ∀ { f g 1 g 2 : V → C } , Continuous f → HasCompactSupport f → Continuous g 1 → HasCompactSupport g 1 → Continuous g 2 → HasCompactSupport g 2 → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → MemLp ( K m f ) 2 vol → MemLp ( K m g 1 ) 2 vol → MemLp ( K m g 2 ) 2 vol → ∀ { z : C } , − 1 ≤ z . im → z . im ≤ 0 → F m f ( g 1 + g 2 ) z = F m f g 1 z + F m f g 2 z Proof. By integrable_kmsFun_integrand_closedKrepContKrepCont_add□ \square □
Used by kmsFun_sub_right
Lemma 141 (kmsFun_sub_left). source ↗
f-slot subtraction identitykmsFun m (f₁−f₂) g = kmsFun m f₁ g − kmsFun m f₂ g on the closed strip (from kmsFun_add_left; f₁−f₂ is again nice — δ-margin on the union of supports, real, MemLp).
0 < m → ∀ { f 1 f 2 g : V → C } , 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 o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g 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 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → 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 g ) 2 v o l → ∀ { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → F m ( f 1 − f 2 ) g z = F m f 1 g z − F m f 2 g z 0 < m \to \forall \{f_{1} f_{2} g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f_{1} \to \mathrm{HasCompactSupport}\,f_{1} \to \mathrm{Continuous}\,f_{2} \to \mathrm{HasCompactSupport}\,f_{2} \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \to \forall \{\delta : \mathbb{R}\}, 0 < \delta \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \mathrm{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{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}), g\,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})\,(\mathrm{f}\,x) = \mathrm{f}\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{f}\,x) = \mathrm{f}\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(g\,x) = g\,x) \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\,g)\,2\,\mathrm{vol} \to \forall \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,(f_{1} - f_{2})\,g\,z = \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f_{1}\,g\,z - \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f_{2}\,g\,z 0 < m → ∀ { f 1 f 2 g : V → C } , Continuous f 1 → HasCompactSupport f 1 → Continuous f 2 → HasCompactSupport f 2 → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → MemLp ( K m f 1 ) 2 vol → MemLp ( K m f 2 ) 2 vol → MemLp ( K m g ) 2 vol → ∀ { z : C } , − 1 ≤ z . im → z . im ≤ 0 → F m ( f 1 − f 2 ) g z = F m f 1 g z − F m f 2 g z Proof. By kmsFun_add_leftmemLp_Krep_sub□ \square □
Used by norm_kmsFun_sub_le
Lemma 142 (kmsFun_sub_right). source ↗
g-slot subtraction identitykmsFun m f (g₁−g₂) = kmsFun m f g₁ − kmsFun m f g₂ (from kmsFun_add_right; g₁−g₂ is again nice).
0 < m → ∀ { f g 1 g 2 : 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 → C o n t i n u o u s g 1 → H a s C o m p a c t S u p p o r t g 1 → C o n t i n u o u s g 2 → H a s C o m p a c t S u p p o r t g 2 → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g 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 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → M e m L p ( K m f ) 2 v o l → M e m L p ( K m g 1 ) 2 v o l → M e m L p ( K m g 2 ) 2 v o l → ∀ { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → F m f ( g 1 − g 2 ) z = F m f g 1 z − F m f g 2 z 0 < m \to \forall \{f g_{1} g_{2} : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g_{1} \to \mathrm{HasCompactSupport}\,g_{1} \to \mathrm{Continuous}\,g_{2} \to \mathrm{HasCompactSupport}\,g_{2} \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{g}\,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{g}\,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 (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{g}\,x) = \mathrm{g}\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{g}\,x) = \mathrm{g}\,x) \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{1})\,2\,\mathrm{vol} \to \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{2})\,2\,\mathrm{vol} \to \forall \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,(g_{1} - g_{2})\,z = \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g_{1}\,z - \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g_{2}\,z 0 < m → ∀ { f g 1 g 2 : V → C } , Continuous f → HasCompactSupport f → Continuous g 1 → HasCompactSupport g 1 → Continuous g 2 → HasCompactSupport g 2 → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → MemLp ( K m f ) 2 vol → MemLp ( K m g 1 ) 2 vol → MemLp ( K m g 2 ) 2 vol → ∀ { z : C } , − 1 ≤ z . im → z . im ≤ 0 → F m f ( g 1 − g 2 ) z = F m f g 1 z − F m f g 2 z Proof. By kmsFun_add_rightmemLp_Krep_sub□ \square □
Used by norm_kmsFun_sub_le
Lemma 143 (norm_toLp_Krep_eq_sqrt). source ↗
L²-norm of a one-particle vector as an integral‖KrepL2 f‖ = √(∫‖Krep m f‖²). Via inner_KrepL2 (⟪KrepL2 f, KrepL2 f⟫ = ∫ conj(Krep f)·Krep f = ↑∫‖Krep f‖²) and inner_self_eq_norm_sq. The bridge from the analytic strip bound (in ∫‖Krep‖²) to the Hilbert norms ‖ξ‖,‖η‖ for the closure/threading argument.
∥ t o L p ( K m f ) h f ∥ = ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,\mathrm{hf}\| = \sqrt (\int (\theta : \mathbb{R}), {\|\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta\|}^{2}) ∥ toLp ( K m f ) hf ∥ = ( ∫ ( θ : R ) , ∥ K m f θ ∥ 2 ) Proof. By inner_KrepL2□ \square □
Used by norm_kmsFun_le_norm_mul
Lemma 144 (minkowskiFourier_smul). source ↗
minkowskiFourier is ℂ-homogeneous in the test function(c·f)^_M = c·f̂_M.
F ( λ x ↦ c ⋅ f x ) p = c ⋅ F f p \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskifourier}{\mathcal{F}}\,(\lambda x \mapsto c \cdot f\,x)\,p = c \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-minkowskifourier}{\mathcal{F}}\,f\,p F ( λ x ↦ c ⋅ f x ) p = c ⋅ F f p Proof. By minkowskiDot□ \square □
Used by Krep_smul
Lemma 145 (Krep_smul). source ↗
Krep is ℂ-homogeneous in the test functionKrep m (c·f) = c·Krep m f.
( K m λ x ↦ c ⋅ f x ) = λ θ ↦ c ⋅ K m f θ (\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,\lambda x \mapsto c \cdot f\,x) = \lambda \theta \mapsto c \cdot \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f\,\theta ( K m λ x ↦ c ⋅ f x ) = λ θ ↦ c ⋅ K m f θ Proof. By minkowskiFourier_smulmassShellminkowskiFourier□ \square □
Used by vec_smul
Lemma 146 (KrepL2_add). source ↗
KrepL2 respects additionKrepL2(f₁+f₂) = KrepL2 f₁ + KrepL2 f₂ in L². MemLp.toLp_add + MemLp.toLp_eq_toLp_iff (Krep(f₁+f₂) =ᵐ Krep f₁ + Krep f₂, Krep_add). With KrepL2_sub and the real scalar law, this makes {KrepL2 f : f nice} an ℝ-subspace, so span_ℝ adds nothing: every span element is a single KrepL2 of a nice function — collapsing the closure threading to single nice generator pairs.
t o L p ( K m ( f 1 + f 2 ) ) ⋯ = t o L p ( K m f 1 ) h f 1 L + t o L p ( K m f 2 ) h f 2 L \mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(f_{1} + f_{2}))\,\cdots = \mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{1})\,\mathrm{hf}_{1}L + \mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2})\,\mathrm{hf}_{2}L toLp ( K m ( f 1 + f 2 )) ⋯ = toLp ( K m f 1 ) hf 1 L + toLp ( K m f 2 ) hf 2 L Proof. By Krep_add□ \square □
Used by vec_add
Lemma 147 (KrepL2_sub). source ↗
KrepL2 respects subtractionKrepL2(f₁−f₂) = KrepL2 f₁ − KrepL2 f₂ in L². MemLp.toLp_sub + MemLp.toLp_eq_toLp_iff (the Lp elements agree since Krep(f₁−f₂) =ᵐ Krep f₁ − Krep f₂, Krep_sub). Lets ‖KrepL2(Fₙ−Fₘ)‖ = ‖ξₙ − ξₘ‖ → 0 drive the closure Cauchy argument.
t o L p ( K m ( f 1 − f 2 ) ) ⋯ = t o L p ( K m f 1 ) h f 1 L − t o L p ( K m f 2 ) h f 2 L \mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,(f_{1} - f_{2}))\,\cdots = \mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{1})\,\mathrm{hf}_{1}L - \mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2})\,\mathrm{hf}_{2}L toLp ( K m ( f 1 − f 2 )) ⋯ = toLp ( K m f 1 ) hf 1 L − toLp ( K m f 2 ) hf 2 L Proof. By Krep_sub□ \square □
Used by norm_kmsFun_sub_le
Lemma 148 (norm_kmsFun_le_norm_mul). source ↗
Strip bound in Hilbert norms : ‖kmsFun z‖ ≤ 2·‖KrepL2 g‖·‖KrepL2 f‖ on the closed strip. The R=0 annular constant ε₀ rewritten via {0<|θ|} =ᵐ ℝ and norm_toLp_Krep_eq_sqrt. The Cauchy–Schwarz-type bound ‖F z‖ ≤ C·‖η‖·‖ξ‖ controlling the span-closure threading.
0 < m → ∀ { f g : 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 → C o n t i n u o u s g → H a s C o m p a c t S u p p o r t g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g 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 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → ∀ ( h f L : M e m L p ( K m f ) 2 v o l ) ( h g L : M e m L p ( K m g ) 2 v o l ) { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → ∥ F m f g z ∥ ≤ 2 ⋅ ∥ t o L p ( K m g ) h g L ∥ ⋅ ∥ t o L p ( K m f ) h f L ∥ 0 < m \to \forall \{f g : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to \mathrm{Continuous}\,g \to \mathrm{HasCompactSupport}\,g \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}), g\,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 (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(g\,x) = g\,x) \to \forall (\mathrm{hfL} : \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol}) (\mathrm{hgL} : \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,2\,\mathrm{vol}) \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \|\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g\,z\| \le 2 \cdot \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g)\,\mathrm{hgL}\| \cdot \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,\mathrm{hfL}\| 0 < m → ∀ { f g : V → C } , Continuous f → HasCompactSupport f → Continuous g → HasCompactSupport g → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → ∀ ( hfL : MemLp ( K m f ) 2 vol ) ( hgL : MemLp ( K m g ) 2 vol ) { z : C } , − 1 ≤ z . im → z . im ≤ 0 → ∥ F m f g z ∥ ≤ 2 ⋅ ∥ toLp ( K m g ) hgL ∥ ⋅ ∥ toLp ( K m f ) hfL ∥ Proof. By kmsFunCutnorm_kmsFun_sub_kmsFunCut_lekmsFunCut_zeronorm_toLp_Krep_eq_sqrt□ \square □
Used by norm_kmsFun_sub_le
Lemma 149 (norm_kmsFun_sub_le). source ↗
Difference bound (closure Cauchy keystone) : on the closed strip, ‖kmsFun f₁ g₁ z − kmsFun f₂ g₂ z‖ ≤ 2‖KrepL2 g₁‖·‖KrepL2 f₁ − KrepL2 f₂‖ + 2‖KrepL2 g₁ − KrepL2 g₂‖·‖KrepL2 f₂‖. Difference identity (kmsFun_sub_left/right) ⟹ kmsFun_{f₁−f₂,g₁}+kmsFun_{f₂,g₁−g₂}, each bounded by norm_kmsFun_le_norm_mul and rewritten via KrepL2_sub. The controlling estimate for the BCF Cauchy net.
0 < m → ∀ { f 1 f 2 g 1 g 2 : V → C } , 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 o n t i n u o u s g 1 → H a s C o m p a c t S u p p o r t g 1 → C o n t i n u o u s g 2 → H a s C o m p a c t S u p p o r t g 2 → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , f x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x ≠ 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g 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 ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → ( ∀ ( x : V ) , ( s t a r R i n g E n d C ) ( g x ) = g x ) → ∀ ( h f 1 L : M e m L p ( K m f 1 ) 2 v o l ) ( h f 2 L : M e m L p ( K m f 2 ) 2 v o l ) ( h g 1 L : M e m L p ( K m g 1 ) 2 v o l ) ( h g 2 L : M e m L p ( K m g 2 ) 2 v o l ) { z : C } , − 1 ≤ z . i m → z . i m ≤ 0 → ∥ F m f 1 g 1 z − F m f 2 g 2 z ∥ ≤ 2 ⋅ ∥ t o L p ( K m g 1 ) h g 1 L ∥ ⋅ ∥ t o L p ( K m f 1 ) h f 1 L − t o L p ( K m f 2 ) h f 2 L ∥ + 2 ⋅ ∥ t o L p ( K m g 1 ) h g 1 L − t o L p ( K m g 2 ) h g 2 L ∥ ⋅ ∥ t o L p ( K m f 2 ) h f 2 L ∥ 0 < m \to \forall \{f_{1} f_{2} g_{1} g_{2} : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}\}, \mathrm{Continuous}\,f_{1} \to \mathrm{HasCompactSupport}\,f_{1} \to \mathrm{Continuous}\,f_{2} \to \mathrm{HasCompactSupport}\,f_{2} \to \mathrm{Continuous}\,g_{1} \to \mathrm{HasCompactSupport}\,g_{1} \to \mathrm{Continuous}\,g_{2} \to \mathrm{HasCompactSupport}\,g_{2} \to \forall \{\delta : \mathbb{R}\}, 0 < \delta \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), \mathrm{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{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{g}\,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{g}\,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})\,(\mathrm{f}\,x) = \mathrm{f}\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{f}\,x) = \mathrm{f}\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{g}\,x) = \mathrm{g}\,x) \to (\forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{g}\,x) = \mathrm{g}\,x) \to \forall (\mathrm{hf}_{1}L : \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{1})\,2\,\mathrm{vol}) (\mathrm{hf}_{2}L : \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2})\,2\,\mathrm{vol}) (\mathrm{hg}_{1}L : \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{1})\,2\,\mathrm{vol}) (\mathrm{hg}_{2}L : \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{2})\,2\,\mathrm{vol}) \{z : \mathbb{C}\}, -1 \le z.\mathrm{im} \to z.\mathrm{im} \le 0 \to \|\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f_{1}\,g_{1}\,z - \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f_{2}\,g_{2}\,z\| \le 2 \cdot \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{1})\,\mathrm{hg}_{1}L\| \cdot \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{1})\,\mathrm{hf}_{1}L - \mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2})\,\mathrm{hf}_{2}L\| + 2 \cdot \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{1})\,\mathrm{hg}_{1}L - \mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{2})\,\mathrm{hg}_{2}L\| \cdot \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2})\,\mathrm{hf}_{2}L\| 0 < m → ∀ { f 1 f 2 g 1 g 2 : V → C } , Continuous f 1 → HasCompactSupport f 1 → Continuous f 2 → HasCompactSupport f 2 → Continuous g 1 → HasCompactSupport g 1 → Continuous g 2 → HasCompactSupport g 2 → ∀ { δ : R } , 0 < δ → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , f x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , g x = 0 → δ ≤ x 1 − x 0 ∧ δ ≤ x 1 + x 0 ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( f x ) = f x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → ( ∀ ( x : V ) , ( starRingEnd C ) ( g x ) = g x ) → ∀ ( hf 1 L : MemLp ( K m f 1 ) 2 vol ) ( hf 2 L : MemLp ( K m f 2 ) 2 vol ) ( hg 1 L : MemLp ( K m g 1 ) 2 vol ) ( hg 2 L : MemLp ( K m g 2 ) 2 vol ) { z : C } , − 1 ≤ z . im → z . im ≤ 0 → ∥ F m f 1 g 1 z − F m f 2 g 2 z ∥ ≤ 2 ⋅ ∥ toLp ( K m g 1 ) hg 1 L ∥ ⋅ ∥ toLp ( K m f 1 ) hf 1 L − toLp ( K m f 2 ) hf 2 L ∥ + 2 ⋅ ∥ toLp ( K m g 1 ) hg 1 L − toLp ( K m g 2 ) hg 2 L ∥ ⋅ ∥ toLp ( K m f 2 ) hf 2 L ∥ Proof. By kmsFun_sub_leftkmsFun_sub_rightKrepL2_subnorm_kmsFun_le_norm_mulmemLp_Krep_sub□ \square □
Used by dist_kmsBCF_le
Lemma 150 (memLp_Krep_boostTest). source ↗
Boost-translate preserves L² : MemLp (Krep m (boostTest a f)) 2 from MemLp (Krep m f) 2, since Krep m (boostTest a f) = Krep m f ∘ (·+a) (Krep_boost) and translation is measure-preserving.
M e m L p ( K m f ) 2 v o l → ∀ ( a : R ) , M e m L p ( K m ( ϕ B a f ) ) 2 v o l \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f)\,2\,\mathrm{vol} \to \forall (a : \mathbb{R}), \mathrm{MemLp}\,(\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))\,2\,\mathrm{vol} MemLp ( K m f ) 2 vol → ∀ ( a : R ) , MemLp ( K m ( ϕ B a f )) 2 vol Proof. By Krep_boost□ \square □
Used by bcf_apply_eq_topbcf_apply_eq_bot
Definition 151 (kmsBCF). source ↗
(c1) The KMS witness as a bounded continuous function on the closed strip (nice f,g). Continuous via kmsFun_continuousOn_closed, bounded by 2‖KrepL2 g‖·‖KrepL2 f‖ via norm_kmsFun_le_norm_mul. The vehicle for the uniform-Cauchy limit (norm_kmsFun_sub_le) in the span-closure threading to StripKMSrvd 𝒦_W.
Used by kmsBCF_applydist_kmsBCF_lekmsBCF_congrbcfbcf_congrdist_bcf_lebcf_apply_eq_topbcf_apply_eq_bot
Lemma 152 (kmsBCF_apply). source ↗
( F h m h f h f c h g h g c h δ h m f h m g h f r h g r h f L h g L ) z = F m f g z (\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsbcf}{F}\,\mathrm{hm}\,\mathrm{hf}\,\mathrm{hfc}\,\mathrm{hg}\,\mathrm{hgc}\,h\delta\,\mathrm{hmf}\,\mathrm{hmg}\,\mathrm{hfr}\,\mathrm{hgr}\,\mathrm{hfL}\,\mathrm{hgL})\,z = \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsfun}{F}\,m\,f\,g\,z ( F hm hf hfc hg hgc h δ hmf hmg hfr hgr hfL hgL ) z = F m f g z Proof. Immediate from the definitions. □ \square □
Used by dist_kmsBCF_lekmsBCF_congrbcf_apply_eq_topbcf_apply_eq_botstripKMSrvd_closure
Lemma 153 (dist_kmsBCF_le). source ↗
(c2) BCF Cauchy-control step : dist (kmsBCF f₁ g₁) (kmsBCF f₂ g₂) ≤ the difference bound. Via BoundedContinuousFunction.dist_le + the pointwise norm_kmsFun_sub_le. (Common margin δ.)
d i s t ( F h m h f 1 h f 1 c h g 1 h g 1 c h δ h m f 1 h m g 1 h f 1 r h g 1 r h f 1 L h g 1 L ) ( F h m h f 2 h f 2 c h g 2 h g 2 c h δ h m f 2 h m g 2 h f 2 r h g 2 r h f 2 L h g 2 L ) ≤ 2 ⋅ ∥ t o L p ( K m g 1 ) h g 1 L ∥ ⋅ ∥ t o L p ( K m f 1 ) h f 1 L − t o L p ( K m f 2 ) h f 2 L ∥ + 2 ⋅ ∥ t o L p ( K m g 1 ) h g 1 L − t o L p ( K m g 2 ) h g 2 L ∥ ⋅ ∥ t o L p ( K m f 2 ) h f 2 L ∥ \mathrm{dist}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsbcf}{F}\,\mathrm{hm}\,\mathrm{hf}_{1}\,\mathrm{hf}_{1}c\,\mathrm{hg}_{1}\,\mathrm{hg}_{1}c\,h\delta\,\mathrm{hmf}_{1}\,\mathrm{hmg}_{1}\,\mathrm{hf}_{1}r\,\mathrm{hg}_{1}r\,\mathrm{hf}_{1}L\,\mathrm{hg}_{1}L)\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsbcf}{F}\,\mathrm{hm}\,\mathrm{hf}_{2}\,\mathrm{hf}_{2}c\,\mathrm{hg}_{2}\,\mathrm{hg}_{2}c\,h\delta\,\mathrm{hmf}_{2}\,\mathrm{hmg}_{2}\,\mathrm{hf}_{2}r\,\mathrm{hg}_{2}r\,\mathrm{hf}_{2}L\,\mathrm{hg}_{2}L) \le 2 \cdot \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{1})\,\mathrm{hg}_{1}L\| \cdot \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{1})\,\mathrm{hf}_{1}L - \mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2})\,\mathrm{hf}_{2}L\| + 2 \cdot \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{1})\,\mathrm{hg}_{1}L - \mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,g_{2})\,\mathrm{hg}_{2}L\| \cdot \|\mathrm{toLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,f_{2})\,\mathrm{hf}_{2}L\| dist ( F hm hf 1 hf 1 c hg 1 hg 1 c h δ hmf 1 hmg 1 hf 1 r hg 1 r hf 1 L hg 1 L ) ( F hm hf 2 hf 2 c hg 2 hg 2 c h δ hmf 2 hmg 2 hf 2 r hg 2 r hf 2 L hg 2 L ) ≤ 2 ⋅ ∥ toLp ( K m g 1 ) hg 1 L ∥ ⋅ ∥ toLp ( K m f 1 ) hf 1 L − toLp ( K m f 2 ) hf 2 L ∥ + 2 ⋅ ∥ toLp ( K m g 1 ) hg 1 L − toLp ( K m g 2 ) hg 2 L ∥ ⋅ ∥ toLp ( K m f 2 ) hf 2 L ∥ Proof. By kmsFunnorm_kmsFun_sub_lekmsBCF_apply□ \square □
Used by dist_bcf_le
Lemma 154 (kmsBCF_congr). source ↗
kmsBCF is independent of the margin δkmsFun m f g, which has no δ). Lets the closure Cauchy sequence over approximants with shrinking margins δₙ→0 be compared at a common (minimal) δ via dist_kmsBCF_le.
F h m h f h f c h g h g c h δ h m f h m g h f r h g r h f L h g L = F h m h f h f c h g h g c h δ ′ h m f ′ h m g ′ h f r h g r h f L h g L \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsbcf}{F}\,\mathrm{hm}\,\mathrm{hf}\,\mathrm{hfc}\,\mathrm{hg}\,\mathrm{hgc}\,h\delta\,\mathrm{hmf}\,\mathrm{hmg}\,\mathrm{hfr}\,\mathrm{hgr}\,\mathrm{hfL}\,\mathrm{hgL} = \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsbcf}{F}\,\mathrm{hm}\,\mathrm{hf}\,\mathrm{hfc}\,\mathrm{hg}\,\mathrm{hgc}\,h\delta'\,\mathrm{hmf}^{\prime}\,\mathrm{hmg}^{\prime}\,\mathrm{hfr}\,\mathrm{hgr}\,\mathrm{hfL}\,\mathrm{hgL} F hm hf hfc hg hgc h δ hmf hmg hfr hgr hfL hgL = F hm hf hfc hg hgc h δ ′ hmf ′ hmg ′ hfr hgr hfL hgL Proof. By kmsFunkmsBCF_apply□ \square □
Used by bcf_congr
Lemma 155 (NiceTest). source ↗
A nice wedge test function : the bundled data for a one-particle generator of the wedge standard subspace — continuous, compactly supported, real, with a δ-margin inside the wedge, and L² on-shell amplitude. This is the standard AQFT wedge-localization core class (compactly-supported δ-margin functions), closed under ±, so the generators {NiceTest.vec} already form an ℝ-subspace — and the BW/KMS extension over closure(span(niceWedgeGenSet)) reduces to a closure limit over single nice generator PAIRS (no density theorem; the kmsBCF Cauchy limit closes the span).
R → T y p e \mathbb{R} \to Type R → T y p e Proof. Immediate from the definitions. □ \square □
Used by mkfcontcptδhδmarginreal
Lemma 156 (mk). source ↗
{ m : R } → ( 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 → N i c e T e s t m \{m : \mathbb{R}\} \to (f : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V} \to \mathbb{C}) \to \mathrm{Continuous}\,f \to \mathrm{HasCompactSupport}\,f \to (\delta : \mathbb{R}) \to 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 \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest}{\mathrm{NiceTest}}\,m { m : R } → ( 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 → NiceTest m Proof. Immediate from the definitions. □ \square □
Used by addboostzerosmulbumpNiceTestW
Definition 157 (f). source ↗
the underlying test function
f m s e l f : = s e l f .1 f\,m\,\mathrm{self} \;:=\; \mathrm{self}.1 f m self := self .1 Used by contcptmarginrealmemLpvecaddvec_add
Lemma 158 (cont). source ↗
C o n t i n u o u s s e l f . f \mathrm{Continuous}\,\mathrm{self}.f Continuous self . f Proof. Immediate from the definitions. □ \square □
Used by vec_addbcfbcf_congrdist_bcf_lebcf_apply_eq_topbcf_apply_eq_botstripKMSrvd_closure
Lemma 159 (cpt). source ↗
H a s C o m p a c t S u p p o r t s e l f . f \mathrm{HasCompactSupport}\,\mathrm{self}.f HasCompactSupport self . f Proof. Immediate from the definitions. □ \square □
Used by vec_addbcfbcf_congrdist_bcf_lebcf_apply_eq_topbcf_apply_eq_botstripKMSrvd_closure
Definition 160 (δ). source ↗
the wedge margin
δ m s e l f : = s e l f .4 \delta\,m\,\mathrm{self} \;:=\; \mathrm{self}.4 δ m self := self .4 Used by hδmarginaddmargin_lebcfbcf_congrdist_bcf_lebcf_apply_eq_top
Lemma 161 (hδ). source ↗
0 < s e l f . δ 0 < \mathrm{self}.\delta 0 < self . δ Proof. Immediate from the definitions. □ \square □
Used by bcf_congrdist_bcf_lesmulstripKMSrvd_closure
Lemma 162 (margin). source ↗
s e l f . f x ≠ 0 → s e l f . δ ≤ x 1 − x 0 ∧ s e l f . δ ≤ x 1 + x 0 \mathrm{self}.f\,x \ne 0 \to \mathrm{self}.\delta \le x\,1 - x\,0 \wedge \mathrm{self}.\delta \le x\,1 + x\,0 self . f x = 0 → self . δ ≤ x 1 − x 0 ∧ self . δ ≤ x 1 + x 0 Proof. Immediate from the definitions. □ \square □
Used by margin_le
Lemma 163 (real). source ↗
( s t a r R i n g E n d C ) ( s e l f . f x ) = s e l f . f x (\mathrm{starRingEnd}\,\mathbb{C})\,(\mathrm{self}.f\,x) = \mathrm{self}.f\,x ( starRingEnd C ) ( self . f x ) = self . f x Proof. Immediate from the definitions. □ \square □
Used by bcfbcf_congrdist_bcf_lebcf_apply_eq_topbcf_apply_eq_botstripKMSrvd_closure
Lemma 164 (memLp). source ↗
M e m L p ( K m s e l f . f ) 2 v o l \mathrm{MemLp}\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,\mathrm{self}.f)\,2\,\mathrm{vol} MemLp ( K m self . f ) 2 vol Proof. Immediate from the definitions. □ \square □
Used by vecvec_addbcfbcf_congrdist_bcf_lebcf_apply_eq_topbcf_apply_eq_botvec_boost
Definition 165 (vec). source ↗
The one-particle vector KrepL2 f ∈ L² of a nice test function.
Used by vec_adddist_bcf_lebcf_cauchySeqbcf_apply_eq_topbcf_apply_eq_botniceWedgeGenSetmem_niceWedgeGenSetniceWedgeGenSet_add_mem
Definition 166 (add). source ↗
Nice tests are closed under addition (margin → min, support → union): the sum is again nice. The structural engine behind span_ℝ(niceWedgeGenSet) = niceWedgeGenSet.
a d d m N 1 N 2 : = { f : = N 1 . f + N 2 . f , c o n t : = ⋯ , c p t : = ⋯ , δ : = min ( N 1 . δ , N 2 . δ ) , h δ : = ⋯ , m a r g i n : = ⋯ , r e a l : = ⋯ , m e m L p : = ⋯ } \mathrm{add}\,m\,N_{1}\,N_{2} \;:=\; \{f :=N_{1}.f + N_{2}.f , \mathrm{cont} :=\cdots , \mathrm{cpt} :=\cdots , \delta :=\min({N_{1}.\delta},{N_{2}.\delta}) , h\delta :=\cdots , \mathrm{margin} :=\cdots , \mathrm{real} :=\cdots , \mathrm{memLp} :=\cdots \} add m N 1 N 2 := { f := N 1 . f + N 2 . f , cont := ⋯ , cpt := ⋯ , δ := min ( N 1 . δ , N 2 . δ ) , h δ := ⋯ , margin := ⋯ , real := ⋯ , memLp := ⋯ } Used by vec_addniceWedgeGenSet_add_mem
Lemma 167 (vec_add). source ↗
NiceTest.add realizes Hilbert-space addition(N₁.add N₂).vec = N₁.vec + N₂.vec (via KrepL2_add).
( N 1 . a d d N 2 ) . v e c = N 1 . v e c + N 2 . v e c (N_{1}.\mathrm{add}\,N_{2}).\mathrm{vec} = N_{1}.\mathrm{vec} + N_{2}.\mathrm{vec} ( N 1 . add N 2 ) . vec = N 1 . vec + N 2 . vec Proof. By KrepL2_addfcontcptmemLp□ \square □
Used by niceWedgeGenSet_add_mem
Lemma 168 (margin_le). source ↗
Margin monotonicity : a nice test’s δ-margin also holds at any smaller δ₀ ≤ δ. Lets a pair of nice tests with different margins be compared at the common (smaller) margin.
δ 0 ≤ N . δ → ∀ ( x : V ) , N . f x ≠ 0 → δ 0 ≤ x 1 − x 0 ∧ δ 0 ≤ x 1 + x 0 \delta_{0} \le N.\delta \to \forall (x : \href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-v}{V}), N.f\,x \ne 0 \to \delta_{0} \le x\,1 - x\,0 \wedge \delta_{0} \le x\,1 + x\,0 δ 0 ≤ N . δ → ∀ ( x : V ) , N . f x = 0 → δ 0 ≤ x 1 − x 0 ∧ δ 0 ≤ x 1 + x 0 Proof. By margin□ \square □
Used by bcf_congrdist_bcf_lestripKMSrvd_closure
Definition 169 (bcf). source ↗
The KMS witness BCF for a pair of nice tests (N in the ξ slot, M in the η slot), built at the common margin min N.δ M.δ. The NiceTest-bundled form of kmsBCF, the vehicle for the Cauchy limit.
b c f m N M : = F h m ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ \mathrm{bcf}\,m\,N\,M \;:=\; \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsbcf}{F}\,\mathrm{hm}\,\cdots \,\cdots \,\cdots \,\cdots \,\cdots \,\cdots \,\cdots \,\cdots \,\cdots \,\cdots \,\cdots bcf m N M := F hm ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Used by bcf_congrdist_bcf_lebcf_cauchySeqbcf_apply_eq_topbcf_apply_eq_botstripKMSrvd_closure
Lemma 170 (bcf_congr). source ↗
NiceTest.bcf at an arbitrary common margin δ'kmsBCF, kmsBCF_congr).
b c f h m N M = F h m ⋯ ⋯ ⋯ ⋯ h δ ′ h m f ′ h m g ′ ⋯ ⋯ ⋯ ⋯ \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest-bcf}{\mathrm{bcf}}\,\mathrm{hm}\,N\,M = \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-kmsbcf}{F}\,\mathrm{hm}\,\cdots \,\cdots \,\cdots \,\cdots \,h\delta'\,\mathrm{hmf}^{\prime}\,\mathrm{hmg}^{\prime}\,\cdots \,\cdots \,\cdots \,\cdots bcf hm N M = F hm ⋯ ⋯ ⋯ ⋯ h δ ′ hmf ′ hmg ′ ⋯ ⋯ ⋯ ⋯ Proof. By kmsBCF_congrδhδmargin_le□ \square □
Used by dist_bcf_le
Lemma 171 (dist_bcf_le). source ↗
(c2, NiceTest form) BCF Cauchy-control : dist (N₁.kmsBCF M₁) (N₂.kmsBCF M₂) is bounded by the Hilbert-norm difference bound, reconciling the per-pair margins at the four-way minimum via NiceTest.bcf_congr, then dist_kmsBCF_le. The keystone for the closure Cauchy sequence.
d i s t ( b c f h m N 1 M 1 ) ( b c f h m N 2 M 2 ) ≤ 2 ⋅ ∥ M 1 . v e c ∥ ⋅ ∥ N 1 . v e c − N 2 . v e c ∥ + 2 ⋅ ∥ M 1 . v e c − M 2 . v e c ∥ ⋅ ∥ N 2 . v e c ∥ \mathrm{dist}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest-bcf}{\mathrm{bcf}}\,\mathrm{hm}\,N_{1}\,M_{1})\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest-bcf}{\mathrm{bcf}}\,\mathrm{hm}\,N_{2}\,M_{2}) \le 2 \cdot \|M_{1}.\mathrm{vec}\| \cdot \|N_{1}.\mathrm{vec} - N_{2}.\mathrm{vec}\| + 2 \cdot \|M_{1}.\mathrm{vec} - M_{2}.\mathrm{vec}\| \cdot \|N_{2}.\mathrm{vec}\| dist ( bcf hm N 1 M 1 ) ( bcf hm N 2 M 2 ) ≤ 2 ⋅ ∥ M 1 . vec ∥ ⋅ ∥ N 1 . vec − N 2 . vec ∥ + 2 ⋅ ∥ M 1 . vec − M 2 . vec ∥ ⋅ ∥ N 2 . vec ∥ Proof. By kmsBCFdist_kmsBCF_lefcontcptδhδrealmemLpmargin_lebcf_congr□ \square □
Used by bcf_cauchySeq
Lemma 172 (bcf_cauchySeq). source ↗
(c2→limit) The KMS-witness BCFs of L²-convergent approximants form a Cauchy sequence. If (N n).vec → ξ and (M n).vec → η in L², then n ↦ (N n).bcf (M n) is CauchySeq in closedStrip →ᵇ ℂ — from NiceTest.dist_bcf_le (the product difference bound) plus boundedness of the convergent norm sequences and Cauchyness of the vectors. Since closedStrip →ᵇ ℂ is a CompleteSpace, this Cauchy sequence converges (next step), giving the closure KMS witness.
T e n d s t o ( λ n ↦ ( N n ) . v e c ) a t T o p ( N ξ ) → T e n d s t o ( λ n ↦ ( M n ) . v e c ) a t T o p ( N η ) → C a u c h y S e q λ n ↦ b c f h m ( N n ) ( M n ) \mathrm{Tendsto}\,(\lambda n \mapsto (N\,n).\mathrm{vec})\,\mathrm{atTop}\,(\mathcal{N}\,\xi) \to \mathrm{Tendsto}\,(\lambda n \mapsto (M\,n).\mathrm{vec})\,\mathrm{atTop}\,(\mathcal{N}\,\eta) \to \mathrm{CauchySeq}\,\lambda n \mapsto \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest-bcf}{\mathrm{bcf}}\,\mathrm{hm}\,(N\,n)\,(M\,n) Tendsto ( λn ↦ ( N n ) . vec ) atTop ( N ξ ) → Tendsto ( λn ↦ ( M n ) . vec ) atTop ( N η ) → CauchySeq λn ↦ bcf hm ( N n ) ( M n ) Proof. By dist_bcf_le□ \square □
Used by stripKMSrvd_closure
Lemma 173 (bcf_apply_eq_top). source ↗
(c4) BCF top edge : at a closed-strip point z with (z:ℂ) = t (real), N.bcf M z = ⟪M.vec, boostUnitary(2πt) N.vec⟫ — the StripKMSrvd top-boundary value, via kmsFun_ofReal_eq_inner.
z = t → ( b c f h m N M ) z = ⟨ M . v e c , ( U ( 2 ⋅ π ⋅ t ) ) N . v e c ⟩ z = t \to (\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest-bcf}{\mathrm{bcf}}\,\mathrm{hm}\,N\,M)\,z = \langle {M.\mathrm{vec}},{(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,N.\mathrm{vec}}\rangle z = t → ( bcf hm N M ) z = ⟨ M . vec , ( U ( 2 ⋅ π ⋅ t )) N . vec ⟩ Proof. By kmsFunkmsFun_ofReal_eq_innermemLp_Krep_boostTestkmsBCFkmsBCF_applyfcontcptδrealmemLp□ \square □
Used by stripKMSrvd_closure
Lemma 174 (bcf_apply_eq_bot). source ↗
(c4) BCF bottom edge : at a closed-strip point z with (z:ℂ) = t − i, N.bcf M z = ⟪boostUnitary(2πt) N.vec, M.vec⟫ — the StripKMSrvd bottom-boundary value, via kmsFun_sub_I + inner_conj_symm.
z = t − i → ( b c f h m N M ) z = ⟨ ( U ( 2 ⋅ π ⋅ t ) ) N . v e c , M . v e c ⟩ z = t - i \to (\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest-bcf}{\mathrm{bcf}}\,\mathrm{hm}\,N\,M)\,z = \langle {(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,N.\mathrm{vec}},{M.\mathrm{vec}}\rangle z = t − i → ( bcf hm N M ) z = ⟨ ( U ( 2 ⋅ π ⋅ t )) N . vec , M . vec ⟩ Proof. By kmsFunkmsFun_ofReal_eq_innerkmsFun_sub_ImemLp_Krep_boostTestkmsBCFkmsBCF_applyfcontcptδrealmemLpKrep□ \square □
Used by stripKMSrvd_closure
Definition 175 (niceWedgeGenSet). source ↗
The nice-core wedge generating set : the one-particle vectors KrepL2 f from nice wedge test functions. The standard BW wedge-localization core; an ℝ-subspace as a set (closed under ± via NiceTest.add/vec_add), so span_ℝ of it adds nothing.
G m : = r a n g e λ N ↦ N . v e c \mathcal{G}\,m \;:=\; \mathrm{range}\,\lambda N \mapsto N.\mathrm{vec} G m := range λ N ↦ N . vec Used by mem_niceWedgeGenSetniceWedgeGenSet_add_memboostUnitary_mapsTo_niceWedgeGenSetzero_mem_niceWedgeGenSetniceWedgeGenSet_smul_memniceWedgeSubmoduleniceWedgeClosedSubmodule_coeniceWedge_isCyclic_of_dense
Lemma 176 (mem_niceWedgeGenSet). source ↗
Membership unfolding for niceWedgeGenSet: ξ is a nice generator iff it is some NiceTest.vec.
ξ ∈ G m ↔ ∃ N , N . v e c = ξ \xi \in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m \leftrightarrow \exists N, N.\mathrm{vec} = \xi ξ ∈ G m ↔ ∃ N , N . vec = ξ Proof. Immediate from the definitions. □ \square □
Used by stripKMSrvd_closure
Lemma 177 (niceWedgeGenSet_add_mem). source ↗
niceWedgeGenSet is closed under additionNiceTest.add), the set-level statement that it is already an ℝ-subspace (so span_ℝ collapses to it).
ξ ∈ G m → η ∈ G m → ξ + η ∈ G m \xi \in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m \to \eta \in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m \to \xi + \eta \in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m ξ ∈ G m → η ∈ G m → ξ + η ∈ G m Proof. By NiceTestvecaddvec_add□ \square □
Used by niceWedgeSubmodule
Definition 178 (boost). source ↗
The boost of a nice test is again nice (the standard wedge-localization core is boost-invariant). f := boostTest(−a) N.f; the wedge margin δ rescales to δ·e^{−|a|} > 0 (the boost scales the lightcone coords by e^{∓a}), continuity/compact-support transport through the boost homeomorphism, realness and L² are preserved (memLp_Krep_boostTest via Krep_boost).
b o o s t m N a : = { f : = ϕ B ( − a ) N . f , c o n t : = ⋯ , c p t : = ⋯ , δ : = N . δ ⋅ exp ( − ∣ a ∣ ) , h δ : = ⋯ , m a r g i n : = ⋯ , r e a l : = ⋯ , m e m L p : = ⋯ } \mathrm{boost}\,m\,N\,a \;:=\; \{f :=\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-boosttest}{\phi_{B}}\,(-a)\,N.f , \mathrm{cont} :=\cdots , \mathrm{cpt} :=\cdots , \delta :=N.\delta \cdot \exp\,(-|a|) , h\delta :=\cdots , \mathrm{margin} :=\cdots , \mathrm{real} :=\cdots , \mathrm{memLp} :=\cdots \} boost m N a := { f := ϕ B ( − a ) N . f , cont := ⋯ , cpt := ⋯ , δ := N . δ ⋅ exp ( − ∣ a ∣ ) , h δ := ⋯ , margin := ⋯ , real := ⋯ , memLp := ⋯ } Used by vec_boostboostUnitary_mapsTo_niceWedgeGenSetniceWedgeCyclic_of_fourier_ne_zero
Lemma 179 (vec_boost). source ↗
NiceTest.boost realizes the boost unitaryboostUnitary a N.vec = (N.boost a).vec (boostUnitary_KrepL2).
( U a ) N . v e c = ( N . b o o s t a ) . v e c (\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,a)\,N.\mathrm{vec} = (N.\mathrm{boost}\,a).\mathrm{vec} ( U a ) N . vec = ( N . boost a ) . vec Proof. By fmemLpboostUnitary_KrepL2□ \square □
Used by boostUnitary_mapsTo_niceWedgeGenSetniceWedgeCyclic_of_fourier_ne_zero
Lemma 180 (boostUnitary_mapsTo_niceWedgeGenSet). source ↗
The nice-core wedge generating set is boost-closed : boostUnitary a maps niceWedgeGenSet m into itself. Supplies the 𝒦-invariance hInv for the +2π nice-core BW discharge (oneParticleBW_niceWedge).
M a p s T o ( ( U a ) ) ( G m ) ( G m ) \mathrm{MapsTo}\,((\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,a))\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m)\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m) MapsTo (( U a )) ( G m ) ( G m ) Proof. By NiceTestvecboostvec_boost□ \square □
Used by oneParticleBW_niceWedge
Definition 181 (zero). source ↗
The zero nice test (f = 0): witnesses NiceTest m is inhabited and 0 ∈ niceWedgeGenSet.
z e r o m : = { f : = λ x ↦ 0 , c o n t : = _ p r o o f _ 1 , c p t : = _ p r o o f _ 2 , δ : = 1 , h δ : = _ p r o o f _ 3 , m a r g i n : = _ p r o o f _ 4 , r e a l : = _ p r o o f _ 5 , m e m L p : = ⋯ } \mathrm{zero}\,m \;:=\; \{f :=\lambda x \mapsto 0 , \mathrm{cont} :=\mathrm{\_proof\_1} , \mathrm{cpt} :=\mathrm{\_proof\_2} , \delta :=1 , h\delta :=\mathrm{\_proof\_3} , \mathrm{margin} :=\mathrm{\_proof\_4} , \mathrm{real} :=\mathrm{\_proof\_5} , \mathrm{memLp} :=\cdots \} zero m := { f := λ x ↦ 0 , cont := _proof_1 , cpt := _proof_2 , δ := 1 , h δ := _proof_3 , margin := _proof_4 , real := _proof_5 , memLp := ⋯ } Used by zero_veczero_mem_niceWedgeGenSet
Definition 182 (smul). source ↗
Real-scalar multiple of a nice test (c·f): again nice (c·f ≠ 0 ⟹ f ≠ 0, so the margin holds at the same δ; realness uses c real).
s m u l m c N : = { f : = λ x ↦ c ⋅ N . f x , c o n t : = ⋯ , c p t : = ⋯ , δ : = N . δ , h δ : = ⋯ , m a r g i n : = ⋯ , r e a l : = ⋯ , m e m L p : = ⋯ } \mathrm{smul}\,m\,c\,N \;:=\; \{f :=\lambda x \mapsto c \cdot N.f\,x , \mathrm{cont} :=\cdots , \mathrm{cpt} :=\cdots , \delta :=N.\delta , h\delta :=\cdots , \mathrm{margin} :=\cdots , \mathrm{real} :=\cdots , \mathrm{memLp} :=\cdots \} smul m c N := { f := λ x ↦ c ⋅ N . f x , cont := ⋯ , cpt := ⋯ , δ := N . δ , h δ := ⋯ , margin := ⋯ , real := ⋯ , memLp := ⋯ } Used by vec_smulniceWedgeGenSet_smul_mem
Lemma 183 (zero_vec). source ↗
(NiceTest.zero m).vec = 0.
( z e r o m ) . v e c = 0 (\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest-zero}{\mathrm{zero}}\,m).\mathrm{vec} = 0 ( zero m ) . vec = 0 Proof. By fmemLpVKrepKrep_zero□ \square □
Used by zero_mem_niceWedgeGenSet
Lemma 184 (vec_smul). source ↗
NiceTest.smul realizes Hilbert-space real-scalar multiplication(N.smul c).vec = c • N.vec.
( s m u l c N ) . v e c = c ⋅ N . v e c (\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest-smul}{\mathrm{smul}}\,c\,N).\mathrm{vec} = c \cdot N.\mathrm{vec} ( smul c N ) . vec = c ⋅ N . vec Proof. By Krep_smulfmemLpVKrep□ \square □
Used by niceWedgeGenSet_smul_mem
Lemma 185 (zero_mem_niceWedgeGenSet). source ↗
0 ∈ niceWedgeGenSet.
0 ∈ G m 0 \in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m 0 ∈ G m Proof. By NiceTestveczerozero_vec□ \square □
Used by niceWedgeSubmodule
Lemma 186 (niceWedgeGenSet_smul_mem). source ↗
niceWedgeGenSet is closed under real-scalar multiplication.
ξ ∈ G m → c ⋅ ξ ∈ G m \xi \in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m \to c \cdot \xi \in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m ξ ∈ G m → c ⋅ ξ ∈ G m Proof. By NiceTestvecsmulvec_smul□ \square □
Used by niceWedgeSubmodule
Definition 187 (niceWedgeSubmodule). source ↗
niceWedgeGenSet is an ℝ-subspaceSubmodule): closed under +, real •, and contains 0. Hence span_ℝ (niceWedgeGenSet) = niceWedgeGenSet as a set (niceWedgeGenSet_span_eq), so the nice-core ClosedSubmodule is literally closure (niceWedgeGenSet m).
n i c e W e d g e S u b m o d u l e m : = { c a r r i e r : = G m , a d d _ m e m ′ : = ⋯ , z e r o _ m e m ′ : = ⋯ , s m u l _ m e m ′ : = ⋯ } \mathrm{niceWedgeSubmodule}\,m \;:=\; \{\mathrm{carrier} :=\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m , \mathrm{add\_mem}^{\prime} :=\cdots , \mathrm{zero\_mem}^{\prime} :=\cdots , \mathrm{smul\_mem}^{\prime} :=\cdots \} niceWedgeSubmodule m := { carrier := G m , add_mem ′ := ⋯ , zero_mem ′ := ⋯ , smul_mem ′ := ⋯ } Used by niceWedgeClosedSubmoduleniceWedgeClosedSubmodule_coe
Definition 188 (niceWedgeClosedSubmodule). source ↗
The nice-core wedge subspace as a ClosedSubmodule ℝ — the carrier object of the (would-be) wedge standard subspace, whose underlying set is exactly closure (niceWedgeGenSet m). This is the S-carrier the Reeh–Schlieder standardness (separating + cyclic) would be proved about; the carrier itself is elementary (the topological closure of the nice ℝ-subspace).
K m : = ( n i c e W e d g e S u b m o d u l e m ) . c l o s u r e \mathcal{K}\,m \;:=\; (\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgesubmodule}{\mathrm{niceWedgeSubmodule}}\,m).\mathrm{closure} K m := ( niceWedgeSubmodule m ) . closure Used by niceWedgeClosedSubmodule_coeniceWedgeStandardSubspaceniceWedge_isCyclic_of_denseniceWedge_isCyclic_of_totalniceWedge_isCyclic_of_total_integralniceWedge_isSeparating_of_no_complex_lineoneParticleBW_niceWedge_of_standardNiceWedgeSeparating
Lemma 189 (niceWedgeClosedSubmodule_coe). source ↗
The carrier set of niceWedgeClosedSubmodule m is closure (niceWedgeGenSet m).
( K m ) = G m ‾ (\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m) = \overline{{\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m}} ( K m ) = G m Proof. By niceWedgeSubmodule□ \square □
Used by niceWedge_isCyclic_of_denseoneParticleBW_niceWedge_of_standardniceWedgeSeparating_pos_mass
Definition 190 (niceWedgeStandardSubspace). source ↗
The nice-core wedge standard subspace, GIVEN the Reeh–Schlieder properties (separating + cyclic). Carrier = niceWedgeClosedSubmodule m (= closure (niceWedgeGenSet m)). Separating and cyclic are the two — and only two — remaining inputs: the genuine Reeh–Schlieder frontier, isolated here as named hypotheses (the carrier and everything else is elementary and built).
K m : = { c l : = K m , I s S e p a r a t i n g : = h s e p , I s C y c l i c : = h c y c } \mathcal{K}\,m \;:=\; \{\mathrm{cl} :=\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m , \mathrm{IsSeparating} :=\mathrm{hsep} , \mathrm{IsCyclic} :=\mathrm{hcyc}\} K m := { cl := K m , IsSeparating := hsep , IsCyclic := hcyc } Used by oneParticleBW_niceWedge_of_standardoneParticleBW_niceWedge_reehSchliederoneParticleBW_niceWedge_unconditionalfreeField_modularEnergy_eq_boostChargefreeField_oneParticle_hFluxfreeField_component_hFluxfreeField_kd_conclusionqiqt_gr_freefield
Lemma 191 (ClosedSubmodule_sup_mulI_invariant). source ↗
K ⊔ iK is i-invariant(K ⊔ K.mulI).mulI = K ⊔ K.mulI (mulI_sup + mulI_mulI_eq + sup_comm). Term-mode (exact) absorbs the mulI instance-diamond that defeats rw.
( K K . m u l I ) . m u l I = K K . m u l I (KK.\mathrm{mulI}).\mathrm{mulI} = KK.\mathrm{mulI} ( K K . mulI ) . mulI = K K . mulI Proof. Immediate from the definitions. □ \square □
Used by ClosedSubmodule_sup_mulI_eq_top_of_dense
Lemma 192 (closedSubmodule_smul_I_mem). source ↗
An i-invariant real closed submodule is closed under i• : S.mulI = S, x ∈ S ⟹ I • x ∈ S.
S . m u l I = S → ∀ { x : ( L p C 2 v o l ) } , x ∈ S → i ⋅ x ∈ S S.\mathrm{mulI} = S \to \forall \{x : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})\}, x \in S \to i \cdot x \in S S . mulI = S → ∀ { x : ( Lp C 2 vol )} , x ∈ S → i ⋅ x ∈ S Proof. Immediate from the definitions. □ \square □
Used by closedSubmodule_smul_complex_mem
Lemma 193 (closedSubmodule_smul_complex_mem). source ↗
An i-invariant real closed submodule is closed under ℂ-scalar multiplication (a complex subspace): c • x ∈ S for c : ℂ, via c • x = c.re • x + c.im • (I • x).
S . m u l I = S → ∀ { x : ( L p C 2 v o l ) } , x ∈ S → ∀ ( c : C ) , c ⋅ x ∈ S S.\mathrm{mulI} = S \to \forall \{x : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})\}, x \in S \to \forall (c : \mathbb{C}), c \cdot x \in S S . mulI = S → ∀ { x : ( Lp C 2 vol )} , x ∈ S → ∀ ( c : C ) , c ⋅ x ∈ S Proof. By closedSubmodule_smul_I_mem□ \square □
Used by ClosedSubmodule_sup_mulI_eq_top_of_dense
Lemma 194 (ClosedSubmodule_sup_mulI_eq_top_of_dense). source ↗
General cyclicity from density : for ANY real closed submodule K and generating set G ⊆ K whose complex span is dense, K ⊔ K.mulI = ⊤. K ⊔ K.mulI is i-invariant (a closed ℂ-subspace) ⊇ G ⊇ closure of its dense ℂ-span = ⊤. The reusable engine: applies to the right wedge (niceWedgeGenSet), and to the complement Kᗮ for the dual separating reduction.
∀ G ⊆ K , D e n s e ( s p a n C G ) → K K . m u l I = ⊤ \forall G\subseteq K, \mathrm{Dense}\,(\mathrm{span}\,\mathbb{C}\,G) \to KK.\mathrm{mulI} = \top ∀ G ⊆ K , Dense ( span C G ) → K K . mulI = ⊤ Proof. By ClosedSubmodule_sup_mulI_invariantclosedSubmodule_smul_complex_mem□ \square □
Used by niceWedge_isCyclic_of_dense
Lemma 195 (niceWedge_isCyclic_of_dense). source ↗
The cyclic frontier in natural Reeh–Schlieder form : the nice-core wedge subspace is CYCLIC (hcyc) as soon as the complex span of the nice one-particle vectors is dense in L²(ℝ). Instance of ClosedSubmodule_sup_mulI_eq_top_of_dense with G = niceWedgeGenSet m ⊆ K = niceWedgeClosedSubmodule m (niceWedgeClosedSubmodule_coe + subset_closure). This converts the lattice identity hcyc into the standard analytic statement Dense (span_ℂ (niceWedgeGenSet m)) — the Reeh–Schlieder wedge-totality.
D e n s e ( s p a n C ( G m ) ) → K m ( K m ) . m u l I = ⊤ \mathrm{Dense}\,(\mathrm{span}\,\mathbb{C}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m)) \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m).\mathrm{mulI} = \top Dense ( span C ( G m )) → K m ( K m ) . mulI = ⊤ Proof. By niceWedgeClosedSubmodule_coeClosedSubmodule_sup_mulI_eq_top_of_dense□ \square □
Used by niceWedge_isCyclic_of_total
Lemma 196 (niceWedge_dense_of_total). source ↗
Density from totality (the sharpest analytic form) : span_ℂ (niceWedgeGenSet m) is dense as soon as the nice wedge generators are TOTAL — no nonzero h ∈ L²(ℝ) is orthogonal to every KrepL2 f. Pure Hilbert-space machinery on the complex orthogonal complement (orthogonal_eq_bot_iff / topologicalClosure_eq_top_iff), which on Lp ℂ 2 is the unambiguous InnerProductSpace ℂ — NO instance diamond. Chains with niceWedge_isCyclic_of_dense: the cyclic Reeh–Schlieder frontier is now exactly “{KrepL2 f : f nice} is total in L²(ℝ)” — the canonical wedge-totality statement.
( ∀ ( h : ( L p C 2 v o l ) ) , ( ∀ ( N : N i c e T e s t m ) , ⟨ N . v e c , h ⟩ = 0 ) → h = 0 ) → D e n s e ( s p a n C ( G m ) ) (\forall (h : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), (\forall (N : \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest}{\mathrm{NiceTest}}\,m), \langle {N.\mathrm{vec}},{h}\rangle = 0) \to h = 0) \to \mathrm{Dense}\,(\mathrm{span}\,\mathbb{C}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m)) ( ∀ ( h : ( Lp C 2 vol )) , ( ∀ ( N : NiceTest m ) , ⟨ N . vec , h ⟩ = 0 ) → h = 0 ) → Dense ( span C ( G m )) Proof. Immediate from the definitions. □ \square □
Used by niceWedge_isCyclic_of_total
Lemma 197 (niceWedge_isCyclic_of_total). source ↗
Cyclicity from totality : the nice-core wedge subspace is cyclic as soon as {KrepL2 f : f nice} is total in L²(ℝ) (niceWedge_dense_of_total ∘ niceWedge_isCyclic_of_dense). The cyclic Reeh–Schlieder frontier in its canonical, sharpest form — no instance plumbing, no density bookkeeping.
( ∀ ( h : ( L p C 2 v o l ) ) , ( ∀ ( N : N i c e T e s t m ) , ⟨ N . v e c , h ⟩ = 0 ) → h = 0 ) → K m ( K m ) . m u l I = ⊤ (\forall (h : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), (\forall (N : \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest}{\mathrm{NiceTest}}\,m), \langle {N.\mathrm{vec}},{h}\rangle = 0) \to h = 0) \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m).\mathrm{mulI} = \top ( ∀ ( h : ( Lp C 2 vol )) , ( ∀ ( N : NiceTest m ) , ⟨ N . vec , h ⟩ = 0 ) → h = 0 ) → K m ( K m ) . mulI = ⊤ Proof. By niceWedge_isCyclic_of_denseniceWedge_dense_of_total□ \square □
Used by niceWedge_isCyclic_of_total_integral
Lemma 198 (niceWedge_isCyclic_of_total_integral). source ↗
Cyclicity from totality, in fully EXPLICIT integral form (the precise Reeh–Schlieder statement): cyclic as soon as the only h ∈ L²(ℝ) with ∫ conj(Krep m f θ)·h(θ) dθ = 0 for every nice wedge f is h = 0. Via inner_KrepL2_general (⟪KrepL2 f, h⟫ = ∫ conj(Krep f)·h). This is the cyclic frontier as a concrete integral-vanishing condition on the on-shell amplitudes — the textbook wedge-totality, no abstraction.
( ∀ ( h : ( L p C 2 v o l ) ) , ( ∀ ( N : N i c e T e s t m ) , ∫ ( θ : R ) , ( s t a r R i n g E n d C ) ( K m N . f θ ) ⋅ h θ = 0 ) → h = 0 ) → K m ( K m ) . m u l I = ⊤ (\forall (h : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), (\forall (N : \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicetest}{\mathrm{NiceTest}}\,m), \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-fock-localization#d-qiqth-fock-localization-krep}{K}\,m\,N.f\,\theta) \cdot h\,\theta = 0) \to h = 0) \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m).\mathrm{mulI} = \top ( ∀ ( h : ( Lp C 2 vol )) , ( ∀ ( N : NiceTest m ) , ∫ ( θ : R ) , ( starRingEnd C ) ( K m N . f θ ) ⋅ h θ = 0 ) → h = 0 ) → K m ( K m ) . mulI = ⊤ Proof. By inner_KrepL2_generalmemLpvecniceWedge_isCyclic_of_total□ \square □
Used by oneParticleBW_niceWedge_reehSchliederoneParticleBW_niceWedge_unconditionalfreeField_modularEnergy_eq_boostChargefreeField_oneParticle_hFluxfreeField_component_hFluxfreeField_kd_conclusionqiqt_gr_freefield
Lemma 199 (closedSubmodule_smul_I_mem_of_mem_mulI). source ↗
v ∈ K.mulI ⟹ I • v ∈ KmulI membership direction, via mem_mapEquiv_iff + I⁻¹ = -I + the real-subspace closure (I•v = (-1)•((-I)•v)). Uses the unambiguous ℂ scalarSMulCLE — NO ℝ-instance tangle (unlike the ᗮ route). The engine for the DIRECT separating reduction.
v ∈ K . m u l I → i ⋅ v ∈ K v \in K.\mathrm{mulI} \to i \cdot v \in K v ∈ K . mulI → i ⋅ v ∈ K Proof. Immediate from the definitions. □ \square □
Used by niceWedge_isSeparating_of_no_complex_line
Lemma 200 (niceWedge_isSeparating_of_no_complex_line). source ↗
The separating frontier in DIRECT form (sidestepping the ᗮ instance tangle): the nice-core wedge subspace is SEPARATING (hsep) as soon as it contains NO nonzero complex line — the only v with both v ∈ K and I • v ∈ K is v = 0. Via mem_inf + closedSubmodule_smul_I_mem_of_mem_mulI, all on the unambiguous ℂ mulI (no orthogonal complement, no ℝ-inner-product diamond). For the free field this is the non-degeneracy of the one-particle symplectic form (Pauli–Jordan) — the dual analytic Reeh–Schlieder input.
( ∀ v ∈ K m , i ⋅ v ∈ K m → v = 0 ) → K m ( K m ) . m u l I = ⊥ (\forall v\in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m, i \cdot v \in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m \to v = 0) \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m).\mathrm{mulI} = \bot ( ∀ v ∈ K m , i ⋅ v ∈ K m → v = 0 ) → K m ( K m ) . mulI = ⊥ Proof. By closedSubmodule_smul_I_mem_of_mem_mulI□ \square □
Used by oneParticleBW_niceWedge_reehSchliederoneParticleBW_niceWedge_unconditionalfreeField_modularEnergy_eq_boostChargefreeField_oneParticle_hFluxfreeField_component_hFluxfreeField_kd_conclusionqiqt_gr_freefield
Lemma 201 (stripKMSrvd_closure). source ↗
(c3+c4) The RvD Def 3.4 KMS witness extended to the CLOSURE of the nice generators , axiom-free. For ξ, η ∈ closure (niceWedgeGenSet m) there is a bounded function F, holomorphic on the open strip and continuous to its closure, with the boost-KMS boundary values F(t) = ⟪η, V(2πt) ξ⟫, F(t−i) = ⟪V(2πt) ξ, η⟫. Construction: pick nice approximants Nₙ.vec → ξ, Mₙ.vec → η; their witness BCFs (Nₙ).bcf (Mₙ) form a Cauchy sequence (bcf_cauchySeq) with limit b in the complete space closedStrip →ᵇ ℂ; F := dite-extend b by 0 off the strip. …
0 < m → ∀ { ξ η : ( L p C 2 v o l ) } , ξ ∈ G m ‾ → η ∈ G m ‾ → ∃ F , D i f f C o n t O n C l C F ( i m − 1 ′ ( − 1 , 0 ) ) ∧ ( ∃ C , ∀ ( z : C ) , ∥ F z ∥ ≤ C ) ∧ ( ∀ ( t : R ) , F t = ⟨ η , ( U ( 2 ⋅ π ⋅ t ) ) ξ ⟩ ) ∧ ∀ ( t : R ) , F ( t − i ) = ⟨ ( U ( 2 ⋅ π ⋅ t ) ) ξ , η ⟩ 0 < m \to \forall \{\xi \eta : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})\}, \xi \in \overline{{\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m}} \to \eta \in \overline{{\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m}} \to \exists F, \mathrm{DiffContOnCl}\,\mathbb{C}\,F\,(\mathrm{im} ^{-1}{}' ({-1},{0})) \wedge (\exists C, \forall (z : \mathbb{C}), \|F\,z\| \le C) \wedge (\forall (t : \mathbb{R}), F\,t = \langle {\eta},{(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,\xi}\rangle) \wedge \forall (t : \mathbb{R}), F\,(t - i) = \langle {(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,\xi},{\eta}\rangle 0 < m → ∀ { ξ η : ( Lp C 2 vol )} , ξ ∈ G m → η ∈ G m → ∃ F , DiffContOnCl C F ( im − 1 ′ ( − 1 , 0 )) ∧ ( ∃ C , ∀ ( z : C ) , ∥ F z ∥ ≤ C ) ∧ ( ∀ ( t : R ) , F t = ⟨ η , ( U ( 2 ⋅ π ⋅ t )) ξ ⟩) ∧ ∀ ( t : R ) , F ( t − i ) = ⟨ ( U ( 2 ⋅ π ⋅ t )) ξ , η ⟩ Proof. By kmsFunkmsFun_differentiableOnkmsBCFkmsBCF_applyNiceTestfcontcptδhδrealmemLpvecmargin_lebcfbcf_cauchySeqbcf_apply_eq_topbcf_apply_eq_botmem_niceWedgeGenSet□ \square □
Used by stripKMSrvd_boostUnitaryniceWedgeSeparating_pos_mass
Lemma 202 (stripKMSrvd_boostUnitary). source ↗
StripKMSrvd (RvD Def 3.4) for the boost group on the FULL wedge standard subspacet ↦ V(2πt) satisfies the RvD half-strip KMS condition on closure (niceWedgeGenSet m) — the standard wedge subspace. Immediate packaging of stripKMSrvd_closure (each generator pair gets the bounded-holomorphic KMS witness). This is the object RvD Theorem 3.8 consumes to identify the boost generator with the modular Hamiltonian — now a THEOREM, not a labelled hKMS hypothesis.
0 < m → S t r i p K M S r v d ( λ t ↦ ( U ( 2 ⋅ π ⋅ t ) ) ) ( G m ‾ ) 0 < m \to \href{/browser/qiqth-fock-oneparticlebw#d-qiqth-fock-oneparticlebw-stripkmsrvd}{\mathrm{StripKMSrvd}}\,(\lambda t \mapsto (\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t)))\,(\overline{{\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m}}) 0 < m → StripKMSrvd ( λ t ↦ ( U ( 2 ⋅ π ⋅ t ))) ( G m ) Proof. By stripKMSrvd_closure□ \square □
Used by oneParticleBW_niceWedge
Lemma 203 (oneParticleBW_niceWedge). source ↗
One-particle Bisognano–Wichmann for the nice-core wedge subspace — hKMS DISCHARGED at the constructed +2π sign , axiom-free. For a standard subspace S whose carrier is the nice-core wedge subspace closure (niceWedgeGenSet m) and the rapidity-boost group V t = boostUnitary(2πt), the modular flow IS the boost: modUnitary S t = V t. The genuine RvD Def 3.4 KMS condition (hKMS) is no longer a labelled hypothesis — it is supplied by the machine-checked stripKMSrvd_boostUnitary; the 𝒦-invariance by boostUnitary_mapsTo_niceWedgeGenSet (+ Set.MapsTo.closure); the contraction-group structure by the boost group laws. …
0 < m → ∀ ( S : S t a n d a r d S u b s p a c e ( L p C 2 v o l ) ) ( V : R → ( L p C 2 v o l ) → L [ C ] ( L p C 2 v o l ) ) , S . c l = G m ‾ → ( ∀ ( t : R ) ( x : ( L p C 2 v o l ) ) , ( V t ) x = ( U ( 2 ⋅ π ⋅ t ) ) x ) → ∀ ( t : R ) , Δ S t = V t 0 < m \to \forall (S : \mathrm{StandardSubspace}\,(\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})) (V : \mathbb{R} \to (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol}) \to L[\mathbb{C}] (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), S.\mathrm{cl} = \overline{{\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgegenset}{\mathcal{G}}\,m}} \to (\forall (t : \mathbb{R}) (x : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), (V\,t)\,x = (\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,x) \to \forall (t : \mathbb{R}), \href{/browser/qiqth-standardsubspacemodularflow#d-qiqth-standardsubspacemodular-modunitary}{\Delta}\,S\,t = V\,t 0 < m → ∀ ( S : StandardSubspace ( Lp C 2 vol )) ( V : R → ( Lp C 2 vol ) → L [ C ] ( Lp C 2 vol )) , S . cl = G m → ( ∀ ( t : R ) ( x : ( Lp C 2 vol )) , ( V t ) x = ( U ( 2 ⋅ π ⋅ t )) x ) → ∀ ( t : R ) , Δ S t = V t Proof. By boostUnitary_mapsTo_niceWedgeGenSetstripKMSrvd_boostUnitaryboostUnitary_add_applyboostUnitary_zero_applycontinuous_boostUnitary_applyStripKMSrvdoneParticleBW_completeprojKmem_K_iff_projKgaussSmeargaussSmear_mem_K□ \square □
Used by oneParticleBW_niceWedge_of_standard
Lemma 204 (oneParticleBW_niceWedge_of_standard). source ↗
The nice-core wedge BW, conditional ONLY on Reeh–Schlieder (separating + cyclic). For the boost V t = boostUnitary(2πt), the modular flow of the nice-core wedge standard subspace IS the boost. Combines niceWedgeStandardSubspace with oneParticleBW_niceWedge, making explicit that the ENTIRE remaining gap to an unconditional free-field one-particle BW is the two Reeh–Schlieder properties (the cited frontier) — every analytic input (the KMS condition, the 𝒦-invariance, the boost-group structure) is discharged.
0 < m → ∀ ( V : R → ( L p C 2 v o l ) → L [ C ] ( L p C 2 v o l ) ) , ( ∀ ( t : R ) ( x : ( L p C 2 v o l ) ) , ( V t ) x = ( U ( 2 ⋅ π ⋅ t ) ) x ) → ∀ ( h s e p : K m ( K m ) . m u l I = ⊥ ) ( h c y c : K m ( K m ) . m u l I = ⊤ ) ( t : R ) , Δ ( K m h s e p h c y c ) t = V t 0 < m \to \forall (V : \mathbb{R} \to (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol}) \to L[\mathbb{C}] (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), (\forall (t : \mathbb{R}) (x : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), (V\,t)\,x = (\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,x) \to \forall (\mathrm{hsep} : \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m).\mathrm{mulI} = \bot ) (\mathrm{hcyc} : \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m).\mathrm{mulI} = \top ) (t : \mathbb{R}), \href{/browser/qiqth-standardsubspacemodularflow#d-qiqth-standardsubspacemodular-modunitary}{\Delta}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgestandardsubspace}{\mathcal{K}}\,m\,\mathrm{hsep}\,\mathrm{hcyc})\,t = V\,t 0 < m → ∀ ( V : R → ( Lp C 2 vol ) → L [ C ] ( Lp C 2 vol )) , ( ∀ ( t : R ) ( x : ( Lp C 2 vol )) , ( V t ) x = ( U ( 2 ⋅ π ⋅ t )) x ) → ∀ ( hsep : K m ( K m ) . mulI = ⊥ ) ( hcyc : K m ( K m ) . mulI = ⊤ ) ( t : R ) , Δ ( K m hsep hcyc ) t = V t Proof. By niceWedgeClosedSubmodule_coeoneParticleBW_niceWedge□ \square □
Used by oneParticleBW_niceWedge_reehSchlieder
Definition 205 (NiceWedgeSeparating). source ↗
The Reeh–Schlieder SEPARATING condition (the nice-core wedge subspace has no nonzero complex line): the only v with v ∈ K and I•v ∈ K is v = 0 — the one-particle symplectic non-degeneracy (Pauli–Jordan). One of the two analytic facts the free-field one-particle BW rests on; named here as a first-class goal for an analytic proof.
N i c e W e d g e S e p a r a t i n g m : = ∀ v ∈ K m , i ⋅ v ∈ K m → v = 0 \mathrm{NiceWedgeSeparating}\,m \;:=\; \forall v\in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m, i \cdot v \in \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeclosedsubmodule}{\mathcal{K}}\,m \to v = 0 NiceWedgeSeparating m := ∀ v ∈ K m , i ⋅ v ∈ K m → v = 0 Used by oneParticleBW_niceWedge_reehSchliederniceWedgeSeparating_pos_mass
Definition 206 (NiceWedgeCyclic). source ↗
The Reeh–Schlieder CYCLIC condition (wedge-totality of the on-shell amplitudes): the only h ∈ L²(ℝ) with ∫ conj(Krep m f θ)·h(θ) dθ = 0 for every nice wedge f is h = 0 — Paley–Wiener / edge-of-the-wedge. The other analytic fact the free-field one-particle BW rests on.
Used by niceWedgeCyclic_of_fourier_ne_zerooneParticleBW_niceWedge_reehSchliederniceWedgeCyclic_bumpWniceWedgeCyclic_of_bumpW_fourier_ne_zeroniceWedgeCyclic_pos_mass
Lemma 207 (niceWedgeCyclic_of_fourier_ne_zero). source ↗
NiceWedgeCyclic from the Wiener–Tauberian theorem.N₀ whose one-particle Fourier transform is nonzero almost everywhere. Proof: h ⊥ every nice generator ⟹ h ⊥ the whole rapidity-boost orbit of N₀ (boosts of a nice generator are nice generators, NiceTest.vec_boost; the orthogonality is the integral via inner_KrepL2_general); then the complete L²-Wiener theorem (boost_orbit_total_of_fourier_ne_zero) forces h = 0. This reduces the entire cyclic Reeh–Schlieder input to the SINGLE concrete analytic fact 𝓕(N₀.vec) ≠ 0 a.e. — no edge-of-the-wedge analyticity.
( ∀ ( ξ : R ) , ( F N 0 . v e c ) ξ ≠ 0 ) → N i c e W e d g e C y c l i c m (\forall (\xi : \mathbb{R}), (\mathcal{F}\,N_{0}.\mathrm{vec})\,\xi \ne 0) \to \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgecyclic}{\mathrm{NiceWedgeCyclic}}\,m ( ∀ ( ξ : R ) , ( F N 0 . vec ) ξ = 0 ) → NiceWedgeCyclic m Proof. By inner_KrepL2_generalfmemLpboostvec_boostKrepboostUnitaryboost_orbit_total_of_fourier_ne_zero□ \square □
Used by niceWedgeCyclic_bumpW
Lemma 208 (oneParticleBW_niceWedge_reehSchlieder). source ↗
THE free-field one-particle Bisognano–Wichmann, reduced to its TWO analytic Reeh–Schlieder inputs. modUnitary S t = boostUnitary(2πt) for the nice-core wedge standard subspace, given ONLY the two named Reeh–Schlieder conditions: NiceWedgeSeparating m (no complex line / Pauli–Jordan) and NiceWedgeCyclic m (wedge-totality / Paley–Wiener). NO lattice, NO instance, NO labelled-KMS hypotheses remain: every structural step (the KMS condition, the 𝒦-invariance, the boost group, the standard-subspace construction, BOTH Reeh–Schlieder lattice reductions) is machine-checked and axiom-free. …
0 < m → ∀ ( V : R → ( L p C 2 v o l ) → L [ C ] ( L p C 2 v o l ) ) , ( ∀ ( t : R ) ( x : ( L p C 2 v o l ) ) , ( V t ) x = ( U ( 2 ⋅ π ⋅ t ) ) x ) → ∀ ( h s e p : N i c e W e d g e S e p a r a t i n g m ) ( h c y c : N i c e W e d g e C y c l i c m ) ( t : R ) , Δ ( K m ⋯ ⋯ ) t = V t 0 < m \to \forall (V : \mathbb{R} \to (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol}) \to L[\mathbb{C}] (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), (\forall (t : \mathbb{R}) (x : (\mathrm{Lp}\,\mathbb{C}\,2\,\mathrm{vol})), (V\,t)\,x = (\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(2 \cdot \pi \cdot t))\,x) \to \forall (\mathrm{hsep} : \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgeseparating}{\mathrm{NiceWedgeSeparating}}\,m) (\mathrm{hcyc} : \href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgecyclic}{\mathrm{NiceWedgeCyclic}}\,m) (t : \mathbb{R}), \href{/browser/qiqth-standardsubspacemodularflow#d-qiqth-standardsubspacemodular-modunitary}{\Delta}\,(\href{/browser/qiqth-fock-boostkms#d-qiqth-fock-boostkms-nicewedgestandardsubspace}{\mathcal{K}}\,m\,\cdots \,\cdots )\,t = V\,t 0 < m → ∀ ( V : R → ( Lp C 2 vol ) → L [ C ] ( Lp C 2 vol )) , ( ∀ ( t : R ) ( x : ( Lp C 2 vol )) , ( V t ) x = ( U ( 2 ⋅ π ⋅ t )) x ) → ∀ ( hsep : NiceWedgeSeparating m ) ( hcyc : NiceWedgeCyclic m ) ( t : R ) , Δ ( K m ⋯ ⋯ ) t = V t Proof. By oneParticleBW_niceWedge_of_standard□ \square □
Used by oneParticleBW_niceWedge_unconditional
← all sections · ← EinsteinFieldEquation · CyclicWitness →