5.3. Saddle geometry
Stationary radii, the centered phase, damping and moment quantities, and the damping estimates (Section 4.3: (43)–(49) and Lemmas 4.4–4.7).
Recall u_0, U from Definition 5.2.1 and set (equation (43))
u_* = -1 + \dfrac{\log\lambda}{4\lambda}. For u > -1 put \eta = 1 + u > 0,
m = \dfrac{\lambda\eta}{2}, and use \psi = (\log\Gamma)' from Definition 3.1.4, with the
branch of \log\Gamma real on the positive axis. Note
m \ge \lambda(1+u_*)/2 = \tfrac18\log\lambda
for u \ge u_*.
Lean code for Definition5.3.1●1 definition
Associated Lean declarations
-
CohnElkies.u_star[complete]
-
CohnElkies.u_star[complete]
-
defdefined in CohnElkies/UpperBound/SmallRadius.leancomplete
def CohnElkies.u_star (_ε : ℝ) (d : ℕ) : ℝ
def CohnElkies.u_star (_ε : ℝ) (d : ℕ) : ℝ
Report Lemma 4.10: the near-optimal contour height `u_* = -1 + (log λ)/(4λ)`, `λ = d/2`.
-
CohnElkies.vℓ[complete] -
CohnElkies.logRadius[complete] -
CohnElkies.saddleLogRadius_eq_digamma_add_shellDerivative[complete]
On the contour t = \lambda(T + iu), the logarithm of E_\lambda(t)r^{it}
(Definition 5.2.11) is
\tfrac{i\lambda(T+iu)}{2}\log\pi + \log\Gamma\bigl(m - \tfrac{i\lambda T}{2}\bigr)
+ \lambda h_\epsilon(T+iu) + i\lambda(T+iu)\log r,
whose T-derivative at T = 0 is
i\lambda(\tfrac12\log\pi - \tfrac12\psi(m) - \int_0^\infty w(a)a\sinh(ua)\,da + \log r)
(Lemma 5.2.5). Thus T = 0 is stationary precisely when
r = e^{v(u)}, where (equation (44))
v(u) = -\tfrac12\log\pi + \tfrac12\psi(m) + \int_0^\infty w(a)\,a\sinh(ua)\,da.
Uses Definition 5.3.1, Definition 5.2.4.
Lean code for Definition5.3.2●3 declarations
Associated Lean declarations
-
CohnElkies.vℓ[complete]
-
CohnElkies.logRadius[complete]
-
CohnElkies.saddleLogRadius_eq_digamma_add_shellDerivative[complete]
-
CohnElkies.vℓ[complete] -
CohnElkies.logRadius[complete] -
CohnElkies.saddleLogRadius_eq_digamma_add_shellDerivative[complete]
-
defdefined in CohnElkies/UpperBound/GammaPhase.leancomplete
def CohnElkies.vℓ (ε ℓ u : ℝ) : ℝ
def CohnElkies.vℓ (ε ℓ u : ℝ) : ℝ
Report (44): the stationary log radius `v_ℓ(u)`.
-
defdefined in CohnElkies/UpperBound/FourierPair.leancomplete
def CohnElkies.logRadius (ε : ℝ) (d : ℕ) (u : ℝ) : ℝ
def CohnElkies.logRadius (ε : ℝ) (d : ℕ) (u : ℝ) : ℝ
Report (83): the logarithm of the saddle radius `r(u)` in dimension `d`.
-
theoremdefined in CohnElkies/UpperBound/SmallRadius.leancomplete
theorem CohnElkies.saddleLogRadius_eq_digamma_add_shellDerivative (ε : ℝ) (d : ℕ) (u : ℝ) : CohnElkies.logRadius ε d u = -Real.log Real.pi / 2 + (↑d / 2 * (1 + u) / 2).digamma / 2 + CohnElkies.saddleSourceShellDerivative ε u
theorem CohnElkies.saddleLogRadius_eq_digamma_add_shellDerivative (ε : ℝ) (d : ℕ) (u : ℝ) : CohnElkies.logRadius ε d u = -Real.log Real.pi / 2 + (↑d / 2 * (1 + u) / 2).digamma / 2 + CohnElkies.saddleSourceShellDerivative ε u
-
CohnElkies.upperSaddleVariance[complete] -
CohnElkies.V_γ[complete] -
CohnElkies.V_s[complete] -
CohnElkies.V_B[complete]
The saddle variance is V(u) = V_\gamma - V_s + V_B with the moments of
Definition 5.3.10 (formally V = v' for v of Definition 5.3.2).
Lean code for Definition5.3.3●4 definitions
Associated Lean declarations
-
CohnElkies.upperSaddleVariance[complete]
-
CohnElkies.V_γ[complete]
-
CohnElkies.V_s[complete]
-
CohnElkies.V_B[complete]
-
CohnElkies.upperSaddleVariance[complete] -
CohnElkies.V_γ[complete] -
CohnElkies.V_s[complete] -
CohnElkies.V_B[complete]
-
defdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
def CohnElkies.upperSaddleVariance (ε ℓ δ : ℝ) : ℝ
def CohnElkies.upperSaddleVariance (ε ℓ δ : ℝ) : ℝ
The saddle variance `V_γ + (V_B - V_s)` of report (48).
-
defdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
def CohnElkies.V_γ (ℓ η : ℝ) : ℝ
def CohnElkies.V_γ (ℓ η : ℝ) : ℝ
The variance `V_γ` of the gamma density, report (48).
-
defdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
def CohnElkies.V_s (ε δ : ℝ) : ℝ
def CohnElkies.V_s (ε δ : ℝ) : ℝ
Variance `V_s` carried by the short shell on the contour of height `1 + δ`.
-
defdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
def CohnElkies.V_B (ε δ : ℝ) : ℝ
def CohnElkies.V_B (ε δ : ℝ) : ℝ
Variance `V_B` carried by the positive shell on the contour of height `1 + δ`.
For \lambda, \eta > 0 and T \in \mathbb{R}, with \mu_{\lambda,\eta} from
Definition 5.2.6, the centered log-gamma phase is (equation (45))
G_{\lambda,\eta}(T) := \int_0^\infty(e^{iaT} - 1 - iaT)\,\mu_{\lambda,\eta}(a)\,da.
Lean code for Definition5.3.4●1 definition
Associated Lean declarations
-
CohnElkies.G_ℓη[complete]
-
CohnElkies.G_ℓη[complete]
-
defdefined in CohnElkies/UpperBound/GammaPhase.leancomplete
def CohnElkies.G_ℓη (ℓ η T : ℝ) : ℂ
def CohnElkies.G_ℓη (ℓ η T : ℝ) : ℂ
Report (45): the centred log-gamma phase `G_{ℓ,η}(T) = ∫₀^∞ (e^{iaT} - 1 - iaT) dμ_ℓ(a)`.
For \lambda, \eta > 0, m = \lambda\eta/2, and T \in \mathbb{R}, the phase of
Definition 5.3.4 satisfies
e^{G_{\lambda,\eta}(T)} = \dfrac{\Gamma\bigl(m - \tfrac{i\lambda T}{2}\bigr)}{\Gamma(m)}\,e^{i\lambda T\psi(m)/2},
that is, G_{\lambda,\eta}(T) = \log\Gamma\bigl(m - \tfrac{i\lambda T}{2}\bigr) - \log\Gamma(m) + \tfrac{i\lambda T}{2}\psi(m)
(Binet-type representation; Definition 3.1.4).
Lean code for Lemma5.3.5●1 theorem
Associated Lean declarations
-
CohnElkies.exp_G_ℓη[complete]
-
CohnElkies.exp_G_ℓη[complete]
-
theoremdefined in CohnElkies/UpperBound/GammaPhase.leancomplete
theorem CohnElkies.exp_G_ℓη {ℓ η : ℝ} (hℓ : 0 < ℓ) (hη : 0 < η) (T : ℝ) : Complex.exp (CohnElkies.G_ℓη ℓ η T) = Complex.Gamma (↑ℓ * ↑η / 2 - Complex.I * (↑ℓ * ↑T / 2)) / ↑(Real.Gamma (ℓ * η / 2)) * Complex.exp (Complex.I * (↑ℓ * ↑T / 2 * ↑(ℓ * η / 2).digamma))
theorem CohnElkies.exp_G_ℓη {ℓ η : ℝ} (hℓ : 0 < ℓ) (hη : 0 < η) (T : ℝ) : Complex.exp (CohnElkies.G_ℓη ℓ η T) = Complex.Gamma (↑ℓ * ↑η / 2 - Complex.I * (↑ℓ * ↑T / 2)) / ↑(Real.Gamma (ℓ * η / 2)) * Complex.exp (Complex.I * (↑ℓ * ↑T / 2 * ↑(ℓ * η / 2).digamma))
Report (45): `exp G_{ℓ,η}(T) = Γ(m - i b)/Γ(m) · e^{i b ψ(m)}` with `m = ℓη/2`, `b = ℓT/2`.
Apply the Malmstén–Binet integral representation of \log\Gamma,
\log\Gamma(z+w) - \log\Gamma(z) - w\psi(z) = \int_0^\infty (e^{-ws} - 1 + ws)\,\dfrac{e^{-zs}}{s(1-e^{-s})}\,ds
(\operatorname{Re} z > 0, \operatorname{Re}(z+w) > 0), with z = m, w = -i\lambda T/2,
and substitute a = \lambda s/2. (The formalization proves the exponentiated identity through
the Euler product of \Gamma: truncating the geometric series in
1/(1 - e^{-2a/\lambda}) gives the ratios \Gamma_N(m - ib)/\Gamma_N(m) of the partial
products, which converge to the gamma ratio.)
The gamma damping is
D_\gamma(T) := -\operatorname{Re}G_{\lambda,\eta}(T) = \int_0^\infty(1 - \cos(aT))\,\mu_{\lambda,\eta}(a)\,da
(Definition 5.3.4).
Lean code for Definition5.3.6●1 definition
Associated Lean declarations
-
CohnElkies.D_γ[complete]
-
CohnElkies.D_γ[complete]
-
defdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
def CohnElkies.D_γ (ℓ η T : ℝ) : ℝ
def CohnElkies.D_γ (ℓ η T : ℝ) : ℝ
`D_γ(T) = ∫₀^∞ (1 - cos (aT)) μ_{λ,η}(a) da`, the gamma damping of report (45).
D_\gamma(T) \ge 0 for every T (Definition 5.3.6): the gamma function in the
Mellin envelope always damps the integrand away from T = 0.
Lean code for Lemma5.3.7●1 theorem
Associated Lean declarations
-
CohnElkies.upperGammaDamping_nonneg[complete]
-
CohnElkies.upperGammaDamping_nonneg[complete]
-
theoremdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
theorem CohnElkies.upperGammaDamping_nonneg {ℓ η : ℝ} (hℓ : 0 < ℓ) (T : ℝ) : 0 ≤ CohnElkies.D_γ ℓ η T
theorem CohnElkies.upperGammaDamping_nonneg {ℓ η : ℝ} (hℓ : 0 < ℓ) (T : ℝ) : 0 ≤ CohnElkies.D_γ ℓ η T
1 - \cos(aT) \ge 0 and \mu_{\lambda,\eta} > 0.
Normalize E_\lambda(\lambda(T+iu))r^{i\lambda T} by the positive number
E_\lambda(i\lambda u) = \pi^{-\lambda u/2}\Gamma(m)e^{\lambda h_\epsilon(iu)} and set
r = e^{v(u)}.
The linear terms cancel by the saddle equation, and (36) gives (equations (46), (47))
\mathcal{L}_u(T) := \log\dfrac{E_\lambda(\lambda(T+iu))}{E_\lambda(i\lambda u)} + i\lambda Tv(u),
which equals
G_{\lambda,\eta}(T) + \lambda\int_0^\infty w(a)\cosh(ua)(\cos(aT)-1)\,da
+ i\lambda\int_0^\infty w(a)\sinh(ua)(aT - \sin(aT))\,da.
Uses Definition 5.3.2, Definition 5.3.4 and
Lemma 5.3.5.
Lean code for Definition5.3.8●1 definition
Associated Lean declarations
-
CohnElkies.L_u[complete]
-
CohnElkies.L_u[complete]
-
defdefined in CohnElkies/UpperBound/GammaPhase.leancomplete
def CohnElkies.L_u (ε ℓ u T : ℝ) : ℂ
def CohnElkies.L_u (ε ℓ u T : ℝ) : ℂ
The centred saddle phase `L_u(T)` of report (46): gamma part plus shell part.
-
CohnElkies.D_u[complete] -
CohnElkies.saddleSourceContourDamping[complete]
The total damping is (equation (47))
D_u(T) := -\operatorname{Re}\mathcal{L}_u(T) = D_\gamma(T)
+ \lambda\int_0^\infty w(a)\cosh(ua)(1 - \cos(aT))\,da
(Definition 5.3.8, Definition 5.3.6). Equation (47) isolates the
main difficulty: w_s reduces D_u, while w_B increases it. We must prove D_u(T) > 0
for every T \ne 0 and V(u) > 0 for every u \ge u_*.
Lean code for Definition5.3.9●2 definitions
Associated Lean declarations
-
CohnElkies.D_u[complete]
-
CohnElkies.saddleSourceContourDamping[complete]
-
CohnElkies.D_u[complete] -
CohnElkies.saddleSourceContourDamping[complete]
-
defdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
def CohnElkies.D_u (ε ℓ δ T : ℝ) : ℝ
def CohnElkies.D_u (ε ℓ δ T : ℝ) : ℝ
The total damping `D_u = D_γ + D_B - D_s` of report (47).
-
defdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
def CohnElkies.saddleSourceContourDamping (ε ℓ u T : ℝ) : ℝ
def CohnElkies.saddleSourceContourDamping (ε ℓ u T : ℝ) : ℝ
The damping exponent `D(u, T) = D_γ + D_B - D_s` of the contour `z = λ(1 + u) - iλT`, report (46) and (49).
-
CohnElkies.V_γ[complete] -
CohnElkies.M₃_γ[complete] -
CohnElkies.M₃[complete]
The quadratic and cubic sizes of the phase are measured by (equation (48))
V_\gamma = \dfrac1\lambda\int_0^\infty a^2\mu_{\lambda,\eta}(a)\,da,
M_3 = \dfrac1\lambda\int_0^\infty a^3\mu_{\lambda,\eta}(a)\,da
+ \int_0^\infty\bigl(|w_s(a)| + w_B(a)\bigr)a^3\cosh(ua)\,da
(Definition 5.2.6, Definition 5.2.3).
Lean code for Definition5.3.10●3 definitions
Associated Lean declarations
-
CohnElkies.V_γ[complete]
-
CohnElkies.M₃_γ[complete]
-
CohnElkies.M₃[complete]
-
CohnElkies.V_γ[complete] -
CohnElkies.M₃_γ[complete] -
CohnElkies.M₃[complete]
-
defdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
def CohnElkies.V_γ (ℓ η : ℝ) : ℝ
def CohnElkies.V_γ (ℓ η : ℝ) : ℝ
The variance `V_γ` of the gamma density, report (48).
-
defdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
def CohnElkies.M₃_γ (ℓ η : ℝ) : ℝ
def CohnElkies.M₃_γ (ℓ η : ℝ) : ℝ
The third moment `M₃_γ` of the gamma density, report (48).
-
defdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
def CohnElkies.M₃ (ε ℓ δ : ℝ) : ℝ
def CohnElkies.M₃ (ε ℓ δ : ℝ) : ℝ
The saddle third moment `M₃_γ + (M₃_B - M₃_s)` of report (48).
-
CohnElkies.D_s[complete] -
CohnElkies.D_B[complete] -
CohnElkies.V_s[complete] -
CohnElkies.V_B[complete]
The shell contributions are (equation (49))
D_s(T) = \lambda\int_{a_0}^A|w_s(a)|\cosh(ua)(1-\cos(aT))\,da,
D_B(T) = \lambda\int_B^{B+1}w_B(a)\cosh(ua)(1-\cos(aT))\,da,
V_s = \int_{a_0}^A|w_s(a)|a^2\cosh(ua)\,da, V_B = \int_B^{B+1}w_B(a)a^2\cosh(ua)\,da
(Definition 5.2.2, Definition 5.2.3). In particular
D_u = D_\gamma - D_s + D_B and V(u) = V_\gamma - V_s + V_B
(Definition 5.3.9, Definition 5.3.3).
Lean code for Definition5.3.11●4 definitions
Associated Lean declarations
-
CohnElkies.D_s[complete]
-
CohnElkies.D_B[complete]
-
CohnElkies.V_s[complete]
-
CohnElkies.V_B[complete]
-
CohnElkies.D_s[complete] -
CohnElkies.D_B[complete] -
CohnElkies.V_s[complete] -
CohnElkies.V_B[complete]
-
defdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
def CohnElkies.D_s (ε ℓ δ T : ℝ) : ℝ
def CohnElkies.D_s (ε ℓ δ T : ℝ) : ℝ
Damping `D_s(T)` produced by the short shell on the contour of height `1 + δ`.
-
defdefined in CohnElkies/UpperBound/Envelope.leancomplete
def CohnElkies.D_B (ε ℓ δ T : ℝ) : ℝ
def CohnElkies.D_B (ε ℓ δ T : ℝ) : ℝ
Damping `D_B(T)` produced by the positive shell on the contour of height `1 + δ`.
-
defdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
def CohnElkies.V_s (ε δ : ℝ) : ℝ
def CohnElkies.V_s (ε δ : ℝ) : ℝ
Variance `V_s` carried by the short shell on the contour of height `1 + δ`.
-
defdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
def CohnElkies.V_B (ε δ : ℝ) : ℝ
def CohnElkies.V_B (ε δ : ℝ) : ℝ
Variance `V_B` carried by the positive shell on the contour of height `1 + δ`.
For every \lambda > 0, u > -1 and T \in \mathbb{R}, the quantities of
Definition 5.3.8, Definition 5.3.3 and Definition 5.3.10
satisfy (equation (50))
\Bigl|\mathcal{L}_u(T) + \dfrac{\lambda V(u)}{2}T^2\Bigr| \le \dfrac{\lambda M_3}{6}|T|^3.
Lean code for Lemma5.3.12●1 theorem
Associated Lean declarations
-
CohnElkies.norm_L_u_add_le[complete]
-
CohnElkies.norm_L_u_add_le[complete]
-
theoremdefined in CohnElkies/UpperBound/GammaPhase.leancomplete
theorem CohnElkies.norm_L_u_add_le {ε ℓ u : ℝ} (hε : 0 < ε) (hℓ : 0 < ℓ) (hu : -1 < u) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) (T : ℝ) : ‖CohnElkies.L_u ε ℓ u T + ↑ℓ * ↑(CohnElkies.V_u ε ℓ u) / 2 * ↑T ^ 2‖ ≤ ℓ * CohnElkies.M₃ ε ℓ (u - 1) / 6 * |T| ^ 3
theorem CohnElkies.norm_L_u_add_le {ε ℓ u : ℝ} (hε : 0 < ε) (hℓ : 0 < ℓ) (hu : -1 < u) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) (T : ℝ) : ‖CohnElkies.L_u ε ℓ u T + ↑ℓ * ↑(CohnElkies.V_u ε ℓ u) / 2 * ↑T ^ 2‖ ≤ ℓ * CohnElkies.M₃ ε ℓ (u - 1) / 6 * |T| ^ 3
The globally valid Taylor estimates e^{ix} - 1 - ix = -x^2/2 + O(|x|^3) and
x - \sin x = O(|x|^3), applied to (45) and (46) with |\sinh(ua)| \le \cosh(ua).
-
CohnElkies.upperGammaVariance_bounds[complete] -
CohnElkies.upperGammaThirdMoment_bounds[complete]
For \lambda, \eta > 0 the gamma moments of Definition 5.3.10 satisfy (equations
(51)–(52))
\dfrac{1}{2\eta} \le V_\gamma \le \dfrac{1}{2\eta} + \dfrac{1}{\lambda\eta^2},
\dfrac{1}{2\eta^2} \le \dfrac1\lambda\int_0^\infty a^3\mu_{\lambda,\eta}(a)\,da \le \dfrac{1}{2\eta^2} + \dfrac{2}{\lambda\eta^3}.
Lean code for Lemma5.3.13●2 theorems
Associated Lean declarations
-
CohnElkies.upperGammaVariance_bounds[complete]
-
CohnElkies.upperGammaThirdMoment_bounds[complete]
-
CohnElkies.upperGammaVariance_bounds[complete] -
CohnElkies.upperGammaThirdMoment_bounds[complete]
-
theoremdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
theorem CohnElkies.upperGammaVariance_bounds {ℓ η : ℝ} (hℓ : 0 < ℓ) (hη : 0 < η) : 1 / (2 * η) ≤ CohnElkies.V_γ ℓ η ∧ CohnElkies.V_γ ℓ η ≤ 1 / (2 * η) + 1 / (ℓ * η ^ 2)
theorem CohnElkies.upperGammaVariance_bounds {ℓ η : ℝ} (hℓ : 0 < ℓ) (hη : 0 < η) : 1 / (2 * η) ≤ CohnElkies.V_γ ℓ η ∧ CohnElkies.V_γ ℓ η ≤ 1 / (2 * η) + 1 / (ℓ * η ^ 2)
Report (48): `1/(2η) ≤ V_γ ≤ 1/(2η) + 1/(λη²)`.
-
theoremdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
theorem CohnElkies.upperGammaThirdMoment_bounds {ℓ η : ℝ} (hℓ : 0 < ℓ) (hη : 0 < η) : 1 / (2 * η ^ 2) ≤ CohnElkies.M₃_γ ℓ η ∧ CohnElkies.M₃_γ ℓ η ≤ 1 / (2 * η ^ 2) + 2 / (ℓ * η ^ 3)
theorem CohnElkies.upperGammaThirdMoment_bounds {ℓ η : ℝ} (hℓ : 0 < ℓ) (hη : 0 < η) : 1 / (2 * η ^ 2) ≤ CohnElkies.M₃_γ ℓ η ∧ CohnElkies.M₃_γ ℓ η ≤ 1 / (2 * η ^ 2) + 2 / (ℓ * η ^ 3)
Report (48): `1/(2η²) ≤ M₃_γ ≤ 1/(2η²) + 2/(λη³)`.
Both follow from x \le e^x - 1 \le xe^x applied to the density \mu_{\lambda,\eta} of
Definition 5.2.6 (the report instead inserts uniform trigamma and
polygamma estimates into the polygamma expressions of the moments).
For \lambda, \eta > 0 and all T (equation (53)),
D_\gamma(T) \ge \dfrac{\lambda}{8e}\min\Bigl(\dfrac{T^2}{\eta}, |T|\Bigr)
(Definition 5.3.6).
Lean code for Lemma5.3.14●1 theorem
Associated Lean declarations
-
CohnElkies.upperGammaDamping_lower_bound[complete]
-
CohnElkies.upperGammaDamping_lower_bound[complete]
-
theoremdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
theorem CohnElkies.upperGammaDamping_lower_bound {ℓ η : ℝ} (hℓ : 0 < ℓ) (hη : 0 < η) (T : ℝ) : ℓ / (8 * Real.exp 1) * min (T ^ 2 / η) |T| ≤ CohnElkies.D_γ ℓ η T
theorem CohnElkies.upperGammaDamping_lower_bound {ℓ η : ℝ} (hℓ : 0 < ℓ) (hη : 0 < η) (T : ℝ) : ℓ / (8 * Real.exp 1) * min (T ^ 2 / η) |T| ≤ CohnElkies.D_γ ℓ η T
Report (45): `λ/(8e) · min (T²/η, |T|) ≤ D_γ(T)`.
1 - e^{-x} \le x in (37) gives \mu_{\lambda,\eta}(a) \ge \lambda e^{-\eta a}/(2a^2). For
T \ne 0 take L = \min(\eta^{-1}, |T|^{-1}); on 0 < a < L both e^{-\eta a} and
(1-\cos(aT))/(a^2T^2) are bounded below by absolute positive constants, so
D_\gamma(T) \ge c\lambda T^2L, which is (53).
Lemma 4.4 and (51)–(53) control the gamma contribution and cubic remainder. For u_* \le u \le U the negative
shell removes at most a (1 - c\epsilon)-fraction of the gamma damping, while w_B contributes
nonnegative damping.
For every 0 < \epsilon \le 1/4, \lambda > 0 and -1 < u \le U, the total damping of
Definition 5.3.9 satisfies (equation (55))
D_u(T) \ge 2\epsilon D_\gamma(T) for all T.
Lean code for Lemma5.3.15●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
theorem CohnElkies.upperFirstBranchSaddleDamping_lower_bound {ε ℓ u : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hℓ : 0 < ℓ) (hulower : -1 < u) (huupper : u ≤ 1 + ε / 2) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) (T : ℝ) : 2 * ε * CohnElkies.D_γ ℓ (1 + u) T ≤ CohnElkies.saddleSourceContourDamping ε ℓ u T
theorem CohnElkies.upperFirstBranchSaddleDamping_lower_bound {ε ℓ u : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hℓ : 0 < ℓ) (hulower : -1 < u) (huupper : u ≤ 1 + ε / 2) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) (T : ℝ) : 2 * ε * CohnElkies.D_γ ℓ (1 + u) T ≤ CohnElkies.saddleSourceContourDamping ε ℓ u T
Report (49): on the first branch the saddle damping dominates `2ε D_γ`.
Integrating (54) of Lemma 5.2.7 against 1 - \cos(aT) \ge 0 shows that the
negative shell removes at most a (1-2\epsilon)-fraction of the gamma damping, and the
contribution of w_B is nonnegative, so
D_u(T) \ge D_\gamma(T) - (1-2\epsilon)\int_{a_0}^A(1-\cos(aT))\mu_{\lambda,\eta}(a)\,da
\ge 2\epsilon D_\gamma(T).
For every 0 < \epsilon \le 1/4, \lambda > 0 and -1 < u \le U, with \eta = 1 + u,
the variances of Definition 5.3.11 and Definition 5.3.3
satisfy (equation (56))
V_s \le (1 - 2\epsilon)V_\gamma, hence V(u) \ge 2\epsilon V_\gamma \ge \dfrac{\epsilon}{\eta} > 0.
Lean code for Lemma5.3.16●3 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/SaddleContour.leancomplete
theorem CohnElkies.upperFirstBranch_shortVariance_le_gamma {ε ℓ u : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hℓ : 0 < ℓ) (hulower : -1 < u) (huupper : u ≤ 1 + ε / 2) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) : CohnElkies.V_s ε (u - 1) ≤ (1 - 2 * ε) * CohnElkies.V_γ ℓ (1 + u)
theorem CohnElkies.upperFirstBranch_shortVariance_le_gamma {ε ℓ u : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hℓ : 0 < ℓ) (hulower : -1 < u) (huupper : u ≤ 1 + ε / 2) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) : CohnElkies.V_s ε (u - 1) ≤ (1 - 2 * ε) * CohnElkies.V_γ ℓ (1 + u)
Report §4.3: on the first branch the short shell carries at most `(1 - 2ε)` of the gamma variance.
-
theoremdefined in CohnElkies/UpperBound/SaddleContour.leancomplete
theorem CohnElkies.upperFirstBranch_saddleSourceGaussianVariance_lower_bound {ε ℓ u : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hℓ : 0 < ℓ) (hulower : -1 < u) (huupper : u ≤ 1 + ε / 2) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) : 2 * ε * CohnElkies.V_γ ℓ (1 + u) ≤ CohnElkies.V_u ε ℓ u
theorem CohnElkies.upperFirstBranch_saddleSourceGaussianVariance_lower_bound {ε ℓ u : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hℓ : 0 < ℓ) (hulower : -1 < u) (huupper : u ≤ 1 + ε / 2) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) : 2 * ε * CohnElkies.V_γ ℓ (1 + u) ≤ CohnElkies.V_u ε ℓ u
-
theoremdefined in CohnElkies/UpperBound/SaddleContour.leancomplete
theorem CohnElkies.eventually_saddleSourceGaussianVariance_firstBranch_pos : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 < ℓ → ∀ (u : ℝ), -1 < u → u ≤ 1 + ε / 2 → 0 < CohnElkies.V_u ε ℓ u
theorem CohnElkies.eventually_saddleSourceGaussianVariance_firstBranch_pos : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 < ℓ → ∀ (u : ℝ), -1 < u → u ≤ 1 + ε / 2 → 0 < CohnElkies.V_u ε ℓ u
Integrating (54) of Lemma 5.2.7 against a^2/\lambda gives
V_s \le (1 - 2\epsilon)V_\gamma, hence V(u) \ge 2\epsilon V_\gamma + V_B \ge \epsilon/\eta by
(51) of Lemma 5.3.13.
There is \epsilon_0 > 0 such that, for every 0 < \epsilon < \epsilon_0, there are
constants C_\epsilon, \lambda_\epsilon > 0 with: for every \lambda \ge \lambda_\epsilon and
u_* \le u \le U (equation (57)), M_3 \le C_\epsilon V(u) (Definition 5.3.10,
Definition 5.3.3); moreover \lambda\eta \ge (\log\lambda)/4 on this range
(Definition 5.3.1).
Lean code for Lemma5.3.17●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/SaddleTails.leancomplete
theorem CohnElkies.upperFirstBranch_saddleSourceThirdMoment_scaled_le {ε ℓ u : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hℓ : 0 < ℓ) (hulower : -1 < u) (huupper : u ≤ 1 + ε / 2) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) (hscale : 1 ≤ ℓ * (1 + u)) : (1 + u) ^ 2 * CohnElkies.M₃ ε ℓ (u - 1) ≤ CohnElkies.saddleSourceFirstBranchThirdMomentCoefficient ε
theorem CohnElkies.upperFirstBranch_saddleSourceThirdMoment_scaled_le {ε ℓ u : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hℓ : 0 < ℓ) (hulower : -1 < u) (huupper : u ≤ 1 + ε / 2) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) (hscale : 1 ≤ ℓ * (1 + u)) : (1 + u) ^ 2 * CohnElkies.M₃ ε ℓ (u - 1) ≤ CohnElkies.saddleSourceFirstBranchThirdMomentCoefficient ε
For u_* \le u \le U the positive-shell variance satisfies
V_B \le (B+1)^2Qe^{(U-1)(B+1)} = O_\epsilon(1), and since \lambda\eta \ge (\log\lambda)/4 and
\eta \le 2 + \epsilon/2, (51) gives V(u) \le V_\gamma + V_B = O_\epsilon(\eta^{-1}), while
V(u) \ge \epsilon/\eta by Lemma 5.3.16. Similarly (54) bounds the
negative-shell third moment by the gamma third moment \frac1\lambda\int a^3\mu_{\lambda,\eta},
the positive-shell third moment is O_\epsilon(1), and (52) of Lemma 5.3.13
gives M_3 = O_\epsilon(\eta^{-2}) = O_\epsilon(V(u)).
When u > U, the factor \cosh(ua) in (47) can make w_s overwhelm the gamma contribution.
Put \delta = u - 1. For T \ne 0 the ratios D_s(T)/(\lambda\min(T^2,1)) and
D_B(T)/(\lambda\min(T^2,1)) have respective sizes at most C_0e^{\delta A} and at least
Qe^{\delta B}, so the separation in Lemma 4.2 makes w_B dominate w_s throughout u \ge U.
The interval support of w_B prevents frequency resonances: a shell concentrated at one a
would have D_B(T) = 0 whenever aT \in 2\pi\mathbb{Z}, whereas (equation (58))
\int_B^{B+1}(1 - \cos(aT))\,da = 1 - \operatorname{sinc}(T/2)\cos\bigl((B+\tfrac12)T\bigr),
\operatorname{sinc}(x) = \sin(x)/x, and 1 - |\operatorname{sinc}(T/2)| \asymp \min(T^2,1), so
(58) is
positive for every T \ne 0, uniformly at small and large frequencies. Define the separation
error \rho_\epsilon = (A + a_0^{-1})Q^{-1}\exp\bigl(-\tfrac{\epsilon}{2}(B-A)\bigr)
= C_0Q^{-1}e^{-(U-1)(B-A)};
Lemma 5.2.10 gives \rho_\epsilon = O(e^{-c/\epsilon^2}) = o(1) as
\epsilon \downarrow 0.
For \lambda \ge 0, u = 1 + \delta \ge 1 and all T, the shell dampings of
Definition 5.3.11 satisfy (equations (59)–(60))
D_s(T) \le \lambda C_0e^{\delta A}\min(T^2, 1) and
D_B(T) \ge \dfrac{\lambda}{50}Qe^{\delta B}\min(T^2, 1), with C_0 = A + a_0^{-1}
(Definition 5.2.1).
Lean code for Lemma5.3.18●2 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
theorem CohnElkies.upperShortShellDamping_global_bound {ε ℓ δ T : ℝ} (hε : 0 < ε) (hℓ : 0 ≤ ℓ) (hδ : 0 ≤ δ) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) : CohnElkies.D_s ε ℓ δ T ≤ ℓ * CohnElkies.upperShellShortCoefficient ε * Real.exp (δ * CohnElkies.Aε ε) * min (T ^ 2) 1
theorem CohnElkies.upperShortShellDamping_global_bound {ε ℓ δ T : ℝ} (hε : 0 < ε) (hℓ : 0 ≤ ℓ) (hδ : 0 ≤ δ) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) (hmargin : ∀ a ∈ Set.Icc (CohnElkies.a₀ε ε) (CohnElkies.Aε ε), 0 ≤ CohnElkies.bε ε a) : CohnElkies.D_s ε ℓ δ T ≤ ℓ * CohnElkies.upperShellShortCoefficient ε * Real.exp (δ * CohnElkies.Aε ε) * min (T ^ 2) 1
Report (59): the short shell contributes at most `λ (A + a₀⁻¹) e^{δA} min(T², 1)`. -
theoremdefined in CohnElkies/UpperBound/Envelope.leancomplete
theorem CohnElkies.positiveShellDamping_lower_bound {ε ℓ δ T : ℝ} (hε : 0 < ε) (hℓ : 0 ≤ ℓ) (hδ : 0 ≤ δ) : ℓ / 50 * CohnElkies.Qε ε * Real.exp (δ * CohnElkies.Bε ε) * min (T ^ 2) 1 ≤ CohnElkies.D_B ε ℓ δ T
theorem CohnElkies.positiveShellDamping_lower_bound {ε ℓ δ T : ℝ} (hε : 0 < ε) (hℓ : 0 ≤ ℓ) (hδ : 0 ≤ δ) : ℓ / 50 * CohnElkies.Qε ε * Real.exp (δ * CohnElkies.Bε ε) * min (T ^ 2) 1 ≤ CohnElkies.D_B ε ℓ δ T
Report (60): `D_B(T) ≥ c λ Q e^{δB} min(T², 1)`.
For u = 1 + \delta the explicit densities satisfy |w_s(a)|\cosh(ua) \ll e^{\delta a}/a^2 and
w_B(a)\cosh(ua) \asymp Qe^{\delta a} on their supports. If |T| \le 1,
1 - \cos(aT) = O(a^2T^2)
gives D_s(T) \ll \lambda T^2\int_{a_0}^Ae^{\delta a}\,da \ll \lambda Ae^{\delta A}T^2; if
|T| \ge 1,
1 - \cos(aT) = O(1) gives
D_s(T) \ll \lambda e^{\delta A}\int_{a_0}^Aa^{-2}\,da \ll \lambda a_0^{-1}e^{\delta A}.
These give (59). On the positive shell, (58) yields
D_B(T) \gg \lambda Qe^{\delta B}\int_B^{B+1}(1-\cos(aT))\,da
\gg \lambda Qe^{\delta B}\min(T^2,1),
which is (60).
There is \epsilon_0 > 0 such that, for every 0 < \epsilon < \epsilon_0, every
\lambda \ge 0, every u \ge U and every T \in \mathbb{R} (equations (61)–(62)),
D_s(T) \le \dfrac{1}{100}D_B(T), hence D_u(T) \ge D_\gamma(T) + \dfrac{99}{100}D_B(T)
(Definition 5.3.11, Definition 5.3.9).
Lean code for Lemma5.3.19●2 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
theorem CohnElkies.eventually_upper_shortShell_domination : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 ≤ ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → ∀ (T : ℝ), CohnElkies.D_s ε ℓ δ T ≤ 1 / 100 * CohnElkies.D_B ε ℓ δ T
theorem CohnElkies.eventually_upper_shortShell_domination : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 ≤ ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → ∀ (T : ℝ), CohnElkies.D_s ε ℓ δ T ≤ 1 / 100 * CohnElkies.D_B ε ℓ δ T
Report (61): the short-shell damping is at most `1/100` of the positive-shell damping.
-
theoremdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
theorem CohnElkies.eventually_upperSaddleDamping_gamma_add_shell : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 < ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → ∀ (T : ℝ), CohnElkies.D_γ ℓ (2 + δ) T + 99 / 100 * CohnElkies.D_B ε ℓ δ T ≤ CohnElkies.D_u ε ℓ δ T
theorem CohnElkies.eventually_upperSaddleDamping_gamma_add_shell : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 < ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → ∀ (T : ℝ), CohnElkies.D_γ ℓ (2 + δ) T + 99 / 100 * CohnElkies.D_B ε ℓ δ T ≤ CohnElkies.D_u ε ℓ δ T
For T \ne 0, division of (59) by (60) (Lemma 5.3.18) gives
D_s(T)/D_B(T) \ll C_0Q^{-1}e^{-\delta(B-A)} \le \rho_\epsilon, and
Lemma 5.2.10 makes the right side less than 1/100 for small \epsilon;
at T = 0 both damping terms vanish. Then D_u = D_\gamma - D_s + D_B proves (62).
For u = 1 + \delta \ge 1 the positive-shell variance of Definition 5.3.11
satisfies (equation (64))
\tfrac12B^2Qe^{\delta B} \le V_B \le (B+1)^2Qe^{\delta(B+1)}.
Lean code for Lemma5.3.20●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
theorem CohnElkies.upperPositiveShellVariance_bounds {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 ≤ δ) : 1 / 2 * CohnElkies.Bε ε ^ 2 * CohnElkies.Qε ε * Real.exp (δ * CohnElkies.Bε ε) ≤ CohnElkies.V_B ε δ ∧ CohnElkies.V_B ε δ ≤ (CohnElkies.Bε ε + 1) ^ 2 * CohnElkies.Qε ε * Real.exp (δ * (CohnElkies.Bε ε + 1))
theorem CohnElkies.upperPositiveShellVariance_bounds {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 ≤ δ) : 1 / 2 * CohnElkies.Bε ε ^ 2 * CohnElkies.Qε ε * Real.exp (δ * CohnElkies.Bε ε) ≤ CohnElkies.V_B ε δ ∧ CohnElkies.V_B ε δ ≤ (CohnElkies.Bε ε + 1) ^ 2 * CohnElkies.Qε ε * Real.exp (δ * (CohnElkies.Bε ε + 1))
Report (45): two-sided bounds for the positive-shell variance `V_B`.
Integrate w_B(a)\cosh(ua) \asymp Qe^{\delta a} against a^2 over [B, B+1].
There is \epsilon_0 > 0 such that, for every 0 < \epsilon < \epsilon_0, there is
C_\epsilon > 0 with: for every \lambda \ge 1 and u \ge U (equations (63), (65)–(66)),
V_s \le \dfrac{1}{100}V_B, hence
V_\gamma + \dfrac{99}{100}V_B \le V(u) \le V_\gamma + V_B and V(u) > 0, and
M_3 \le C_\epsilon V(u) (Definition 5.3.3, Definition 5.3.10,
Definition 5.3.11).
Lean code for Lemma5.3.21●4 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/ShellEstimates.leancomplete
theorem CohnElkies.eventually_upper_shortShellVariance_domination : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (δ : ℝ), ε / 2 ≤ δ → CohnElkies.V_s ε δ ≤ 1 / 100 * CohnElkies.V_B ε δ
theorem CohnElkies.eventually_upper_shortShellVariance_domination : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (δ : ℝ), ε / 2 ≤ δ → CohnElkies.V_s ε δ ≤ 1 / 100 * CohnElkies.V_B ε δ
The short-shell variance is at most `1/100` of the positive-shell variance.
-
theoremdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
theorem CohnElkies.eventually_upperSaddleVariance_bounds : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 < ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → 1 / (2 * (2 + δ)) + 99 / 100 * CohnElkies.V_B ε δ ≤ CohnElkies.upperSaddleVariance ε ℓ δ ∧ CohnElkies.upperSaddleVariance ε ℓ δ ≤ 1 / (2 * (2 + δ)) + 1 / (ℓ * (2 + δ) ^ 2) + CohnElkies.V_B ε δ
theorem CohnElkies.eventually_upperSaddleVariance_bounds : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 < ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → 1 / (2 * (2 + δ)) + 99 / 100 * CohnElkies.V_B ε δ ≤ CohnElkies.upperSaddleVariance ε ℓ δ ∧ CohnElkies.upperSaddleVariance ε ℓ δ ≤ 1 / (2 * (2 + δ)) + 1 / (ℓ * (2 + δ) ^ 2) + CohnElkies.V_B ε δ
-
theoremdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
theorem CohnElkies.eventually_upperSaddleVariance_pos : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 < ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → 0 < CohnElkies.upperSaddleVariance ε ℓ δ
theorem CohnElkies.eventually_upperSaddleVariance_pos : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 < ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → 0 < CohnElkies.upperSaddleVariance ε ℓ δ
-
theoremdefined in CohnElkies/UpperBound/SaddleDamping.leancomplete
theorem CohnElkies.eventually_upperSaddleThirdMoment_le_variance : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 1 ≤ ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → CohnElkies.M₃ ε ℓ δ ≤ (2 + 100 / 99 * CohnElkies.upperSaddleShellThirdCoefficient ε) * CohnElkies.upperSaddleVariance ε ℓ δ
theorem CohnElkies.eventually_upperSaddleThirdMoment_le_variance : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 1 ≤ ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → CohnElkies.M₃ ε ℓ δ ≤ (2 + 100 / 99 * CohnElkies.upperSaddleShellThirdCoefficient ε) * CohnElkies.upperSaddleVariance ε ℓ δ
Report (48): the saddle third moment is dominated by the saddle variance.
Comparing the quadratic coefficients of (59) and (60) gives V_s = O(\rho_\epsilon V_B), with
\rho_\epsilon < 1/100 for small \epsilon by Lemma 5.2.10; then
V(u) = V_\gamma - V_s + V_B gives (63). Since \delta \ge \epsilon/2,
V_B \gg B^2Qe^{\epsilon B/2} = B^2e^{\epsilon B/8} \gg 1 by
Lemma 5.3.20, while V_\gamma \ll \eta^{-1} \ll 1 by (51); thus
V_\gamma = O(V_B). Since a \le A on the negative shell,
\int_{a_0}^A|w_s|a^3\cosh(ua) \le AV_s \ll A\rho_\epsilon V_B, while a \le B+1 bounds the
positive-shell third moment by (B+1)V_B; this proves (65). Finally, since
\eta \ge 2 + \epsilon/2, (51)–(52) of Lemma 5.3.13 bound the gamma third
moment by O(V_\gamma); the shell third moments are O_\epsilon(V_B), and V_\gamma = O(V_B),
V_B \asymp V(u) give M_3 = O_\epsilon(V(u)), which is (66).
Set T_0 = (2(B+1))^{-1}. To bound the tails of the saddle integral for u \ge U, we sharpen
the damping on three frequency ranges: |T| \le T_0, where D_u is quadratic;
T_0 \le |T| \le \eta, where w_B supplies a uniform positive floor; and |T| \ge \eta, where
the gamma contribution also grows linearly.
There is \epsilon_0 > 0 such that, for every 0 < \epsilon < \epsilon_0, every
\lambda > 0 and every u \ge U, with \delta = u - 1 and T_0 = (2(B+1))^{-1}
(equations (67)–(69)), the damping D_u of Definition 5.3.9 admits the
pointwise splitting
(1+|T|^3)e^{-D_u(T)} \le (1+|T|^3)e^{-\frac{\lambda V(u)}{100e}T^2}
+ e^{-\Xi}\Bigl((1+|T|^3)e^{-\frac{\lambda}{8e(2+\delta)}T^2} + (1+|T|^3)e^{-\frac{\lambda}{8e}|T|}\Bigr)
for all T \in \mathbb{R}, with the barrier \Xi = \dfrac{99}{5000}\lambda Qe^{\delta B}T_0^2:
on |T| \le T_0 the damping is Gaussian with rate proportional to \lambda V(u), and for
|T| \ge T_0 it exceeds the shell barrier \Xi plus the gamma damping D_\gamma
(quadratic up to |T| \approx \eta, linear beyond).
Lean code for Lemma5.3.22●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/GaussianError.leancomplete
theorem CohnElkies.eventually_secondBranch_damping_pointwise : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 < ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → ∀ (T : ℝ), CohnElkies.saddleGaussianTailWeight T * Real.exp (-CohnElkies.saddleSourceContourDamping ε ℓ (1 + δ) T) ≤ CohnElkies.saddleGaussianTailWeight T * Real.exp (-CohnElkies.secondBranchRate ε ℓ δ * T ^ 2) + Real.exp (-CohnElkies.secondBranchBarrier ε ℓ δ) * (CohnElkies.saddleGaussianTailWeight T * Real.exp (-CohnElkies.secondBranchGammaRate ℓ δ * T ^ 2) + CohnElkies.saddleGaussianTailWeight T * Real.exp (-CohnElkies.secondBranchLinearRate ℓ * |T|))
theorem CohnElkies.eventually_secondBranch_damping_pointwise : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (ℓ : ℝ), 0 < ℓ → ∀ (δ : ℝ), ε / 2 ≤ δ → ∀ (T : ℝ), CohnElkies.saddleGaussianTailWeight T * Real.exp (-CohnElkies.saddleSourceContourDamping ε ℓ (1 + δ) T) ≤ CohnElkies.saddleGaussianTailWeight T * Real.exp (-CohnElkies.secondBranchRate ε ℓ δ * T ^ 2) + Real.exp (-CohnElkies.secondBranchBarrier ε ℓ δ) * (CohnElkies.saddleGaussianTailWeight T * Real.exp (-CohnElkies.secondBranchGammaRate ℓ δ * T ^ 2) + CohnElkies.saddleGaussianTailWeight T * Real.exp (-CohnElkies.secondBranchLinearRate ℓ * |T|))
Splitting `e^{-D_u}` into the local Gaussian and the barrier-suppressed outer part.
If |T| \le T_0, then |aT| \le 1/2 on [B,B+1], so 1 - \cos(aT) \asymp a^2T^2 and
D_B(T) \asymp \lambda V_BT^2. Since \eta \ge 2 + \epsilon/2 and |T| \le \eta, (53) and (51)
of Lemma 5.3.14 and Lemma 5.3.13 give
D_\gamma(T) \gg \lambda T^2/\eta \gg \lambda V_\gamma T^2. Combining these through (62) of
Lemma 5.3.19 and (63) of Lemma 5.3.21 proves (67). If
T_0 \le |T| \le \eta, then \min(T^2,1) \ge T_0^2, so (62) and (60)
(Lemma 5.3.18) give
D_u(T) \gg \lambda T_0^2Qe^{\delta B} \gg_\epsilon \lambda Qe^{\delta B}, which is (68). If
|T| \ge \eta, then \min(T^2,1) = 1 and (53) gives D_\gamma(T) \gg \lambda|T|; adding the
positive shell through (62) and (60) yields (69).