GaussianMode · section of the QIQT-H book
QIQTH.GaussianMode ← all sections · ← WienerL2 · HregExplicitKG →
GaussianMode · entries 428–444 of 1000
Definition 428 (gaussC). source ↗
Normalization constant C = (ℏ√π)^{−1/2} of the Gaussian reference profile.
g a u s s C : = ( ( ℏ ⋅ π ) ) − 1 \mathrm{gaussC} \;:=\; {(\sqrt (\hbar \cdot \sqrt \pi))}^{-1} gaussC := ( ( ℏ ⋅ π )) − 1 Used by gaussModegaussC_sq_mul_sqrtgaussMode_normSqgaussMode_conj_mulgaussMode_integrablegaussMode_calibrationgaussC_posgaussMode_norm
Definition 429 (gaussMode). source ↗
The Gaussian wave-packet reference profile g₀(θ) = C·exp(−θ²/2 − iθ).
g 0 θ : = ( g a u s s C ℏ ) ⋅ exp ( ( − θ 2 / 2 ) − θ ⋅ i ) g_{0}\,\theta \;:=\; (\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussc}{\mathrm{gaussC}}\,\hbar) \cdot \exp\,((-{\theta}^{2} / 2) - \theta \cdot i) g 0 θ := ( gaussC ℏ ) ⋅ exp (( − θ 2 /2 ) − θ ⋅ i ) Used by gaussMode'gaussMode_normSqgaussMode_conj_mulgaussMode_integrablegaussMode_calibrationgaussMode_normgaussMode_continuousgaussMode_hasDerivAt
Definition 430 (gaussMode'). source ↗
Its derivative profile g₀'(θ) = g₀(θ)·(−θ − i).
g a u s s M o d e ′ θ : = g 0 ℏ θ ⋅ ( − θ − i ) \mathrm{gaussMode}^{\prime}\,\theta \;:=\; \href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar\,\theta \cdot (-\theta - i) gaussMode ′ θ := g 0 ℏ θ ⋅ ( − θ − i ) Used by gaussMode_conj_mulgaussMode_integrablegaussMode_calibrationgaussMode_hasDerivAtgaussMode'_continuousgaussMode'_norm_leqiqt_gr_freefield_completeqiqt_gr_freefield_gaussian
Lemma 431 (gaussC_sq_mul_sqrt). source ↗
C²·√π = 1/ℏ for ℏ > 0 — the calibration arithmetic.
0 < ℏ → g a u s s C ℏ 2 ⋅ π = 1 / ℏ 0 < \hbar \to {\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussc}{\mathrm{gaussC}}\,\hbar}^{2} \cdot \sqrt \pi = 1 / \hbar 0 < ℏ → gaussC ℏ 2 ⋅ π = 1/ℏ Proof. Immediate from the definitions. □ \square □
Used by gaussMode_calibration
Lemma 432 (gaussMode_normSq). source ↗
normSq(g₀ θ) = C²·e^{−θ²} — the Gaussian envelope.
n o r m S q ( g 0 ℏ θ ) = g a u s s C ℏ 2 ⋅ exp ( − θ 2 ) \mathrm{normSq}\,(\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar\,\theta) = {\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussc}{\mathrm{gaussC}}\,\hbar}^{2} \cdot \exp\,(-{\theta}^{2}) normSq ( g 0 ℏ θ ) = gaussC ℏ 2 ⋅ exp ( − θ 2 ) Proof. Immediate from the definitions. □ \square □
Used by gaussMode_conj_mulgaussMode_normgaussMode_sq_integrable
Lemma 433 (gaussMode_conj_mul). source ↗
The pointwise boost-charge density: conj(g₀ θ)·g₀'(θ) = ↑(C²·e^{−θ²})·(−θ − i).
( s t a r R i n g E n d C ) ( g 0 ℏ θ ) ⋅ g a u s s M o d e ′ ℏ θ = ( g a u s s C ℏ 2 ⋅ exp ( − θ 2 ) ) ⋅ ( − θ − i ) (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar\,\theta) \cdot \href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{\mathrm{gaussMode}^{\prime}}\,\hbar\,\theta = ({\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussc}{\mathrm{gaussC}}\,\hbar}^{2} \cdot \exp\,(-{\theta}^{2})) \cdot (-\theta - i) ( starRingEnd C ) ( g 0 ℏ θ ) ⋅ gaussMode ′ ℏ θ = ( gaussC ℏ 2 ⋅ exp ( − θ 2 )) ⋅ ( − θ − i ) Proof. By gaussMode_normSq□ \square □
Used by gaussMode_integrablegaussMode_calibration
Lemma 434 (gaussMode_integrable). source ↗
The boost-charge integrand is integrable (Gaussian × polynomial).
I n t e g r a b l e ( λ θ ↦ ( s t a r R i n g E n d C ) ( g 0 ℏ θ ) ⋅ g a u s s M o d e ′ ℏ θ ) v o l \mathrm{Integrable}\,(\lambda \theta \mapsto (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar\,\theta) \cdot \href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{\mathrm{gaussMode}^{\prime}}\,\hbar\,\theta)\,\mathrm{vol} Integrable ( λ θ ↦ ( starRingEnd C ) ( g 0 ℏ θ ) ⋅ gaussMode ′ ℏ θ ) vol Proof. By gaussCgaussMode_conj_mul□ \square □
Used by gaussMode_calibration
Lemma 435 (gaussMode_calibration). source ↗
The Gaussian profile satisfies the calibration (−2π ∫ conj(g₀)·g₀').im = 2π/ℏ. Combined with localized_mode_hTkk, the per-generator hTkk is fully discharged for the canonical Gaussian localization.
0 < ℏ → ( − ( 2 ⋅ π ⋅ ∫ ( θ : R ) , ( s t a r R i n g E n d C ) ( g 0 ℏ θ ) ⋅ g a u s s M o d e ′ ℏ θ ) ) . i m = 2 ⋅ π / ℏ 0 < \hbar \to (-(2 \cdot \pi \cdot \int (\theta : \mathbb{R}), (\mathrm{starRingEnd}\,\mathbb{C})\,(\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar\,\theta) \cdot \href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{\mathrm{gaussMode}^{\prime}}\,\hbar\,\theta)).\mathrm{im} = 2 \cdot \pi / \hbar 0 < ℏ → ( − ( 2 ⋅ π ⋅ ∫ ( θ : R ) , ( starRingEnd C ) ( g 0 ℏ θ ) ⋅ gaussMode ′ ℏ θ )) . im = 2 ⋅ π /ℏ Proof. By gaussCgaussC_sq_mul_sqrtgaussMode_conj_mulgaussMode_integrable□ \square □
Used by qiqt_gr_freefield_completeqiqt_gr_freefield_gaussian
Lemma 436 (gaussC_pos). source ↗
0 < ℏ → 0 < g a u s s C ℏ 0 < \hbar \to 0 < \href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussc}{\mathrm{gaussC}}\,\hbar 0 < ℏ → 0 < gaussC ℏ Proof. Immediate from the definitions. □ \square □
Used by gaussMode_normgaussMode'_norm_le
Lemma 437 (gaussMode_norm). source ↗
‖g₀(θ)‖ = C·e^{−θ²/2} (from normSq = C²e^{−θ²}).
0 < ℏ → ∀ ( θ : R ) , ∥ g 0 ℏ θ ∥ = g a u s s C ℏ ⋅ exp ( − θ 2 / 2 ) 0 < \hbar \to \forall (\theta : \mathbb{R}), \|\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar\,\theta\| = \href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussc}{\mathrm{gaussC}}\,\hbar \cdot \exp\,(-{\theta}^{2} / 2) 0 < ℏ → ∀ ( θ : R ) , ∥ g 0 ℏ θ ∥ = gaussC ℏ ⋅ exp ( − θ 2 /2 ) Proof. By gaussMode_normSqgaussC_pos□ \square □
Used by gaussMode'_norm_legaussMode_integrable_fn
Lemma 438 (gaussMode_continuous). source ↗
C o n t i n u o u s ( g 0 ℏ ) \mathrm{Continuous}\,(\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar) Continuous ( g 0 ℏ ) Proof. By gaussC□ \square □
Used by gaussMode'_continuousgaussMode_memLpgaussMode_integrable_fn
Lemma 439 (gaussMode_hasDerivAt). source ↗
( g 0 ℏ ) ′ ( θ ) = g a u s s M o d e ′ ℏ θ ({\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar})'({\theta})={\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{\mathrm{gaussMode}^{\prime}}\,\hbar\,\theta} ( g 0 ℏ ) ′ ( θ ) = gaussMode ′ ℏ θ Proof. By gaussC□ \square □
Used by qiqt_gr_freefield_completeqiqt_gr_freefield_gaussian
Lemma 440 (gaussMode'_continuous). source ↗
C o n t i n u o u s ( g a u s s M o d e ′ ℏ ) \mathrm{Continuous}\,(\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{\mathrm{gaussMode}^{\prime}}\,\hbar) Continuous ( gaussMode ′ ℏ ) Proof. By gaussModegaussMode_continuous□ \square □
Used by qiqt_gr_freefield_completeqiqt_gr_freefield_gaussian
Lemma 441 (gaussMode'_norm_le). source ↗
‖g₀'(θ)‖ ≤ C, via 1 + θ² ≤ e^{θ²} so e^{−θ²/2}√(θ²+1) ≤ 1.
0 < ℏ → ∀ ( θ : R ) , ∥ g a u s s M o d e ′ ℏ θ ∥ ≤ g a u s s C ℏ 0 < \hbar \to \forall (\theta : \mathbb{R}), \|\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{\mathrm{gaussMode}^{\prime}}\,\hbar\,\theta\| \le \href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussc}{\mathrm{gaussC}}\,\hbar 0 < ℏ → ∀ ( θ : R ) , ∥ gaussMode ′ ℏ θ ∥ ≤ gaussC ℏ Proof. By gaussModegaussC_posgaussMode_norm□ \square □
Used by qiqt_gr_freefield_completeqiqt_gr_freefield_gaussian
Lemma 442 (gaussMode_sq_integrable). source ↗
I n t e g r a b l e ( λ θ ↦ ∥ g 0 ℏ θ ∥ 2 ) v o l \mathrm{Integrable}\,(\lambda \theta \mapsto {\|\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar\,\theta\|}^{2})\,\mathrm{vol} Integrable ( λ θ ↦ ∥ g 0 ℏ θ ∥ 2 ) vol Proof. By gaussCgaussMode_normSq□ \square □
Used by gaussMode_memLp
Lemma 443 (gaussMode_memLp). source ↗
M e m L p ( g 0 ℏ ) 2 v o l \mathrm{MemLp}\,(\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar)\,2\,\mathrm{vol} MemLp ( g 0 ℏ ) 2 vol Proof. By gaussMode_continuousgaussMode_sq_integrable□ \square □
Used by qiqt_gr_freefield_completeqiqt_gr_freefield_gaussian
Lemma 444 (gaussMode_integrable_fn). source ↗
0 < ℏ → I n t e g r a b l e ( g 0 ℏ ) v o l 0 < \hbar \to \mathrm{Integrable}\,(\href{/browser/qiqth-gaussianmode#d-qiqth-wedgekmstogr-gaussmode}{g_{0}}\,\hbar)\,\mathrm{vol} 0 < ℏ → Integrable ( g 0 ℏ ) vol Proof. By gaussCgaussMode_normgaussMode_continuous□ \square □
Used by qiqt_gr_freefield_completeqiqt_gr_freefield_gaussian
← all sections · ← WienerL2 · HregExplicitKG →