7.2. One-sided Riemann bound in Lemma 3.3🔗

The report's Lemma 3.3 states the two-sided weighted error estimate (19). The formalization proves only the one-sided upper bound that is needed later, with a unified error term for both parities that is independent of the dimension.

Definition7.2.1

uses 1

Used by 4

Reverse dependency previews

Preview

Lemma 7.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The endpoint phase is \Lambda(T) = -\tfrac{\pi|T|}{4} - \tfrac12\log(1 + \tfrac{T^2}{4}) + \tfrac{|T|}{2}\arctan\tfrac{|T|}{2}, and the dimension-free Riemann error majorant is E(T) = 3|f_T(0)| + 2|f_T(1)| + \tfrac12\log\coth\tfrac{\pi|T|}{2}, with f_T from Definition 4.1.24.

Lean code for Definition7.2.1●2 definitions

defdefined in CohnElkies/LowerBound/GammaBoundary.lean

complete

def CohnElkies.lowerEndpointPhase (T : ℝ) : ℝ

def CohnElkies.lowerEndpointPhase (T : ℝ) : ℝ

The endpoint phase `-π|T|/4 - ½ log (1 + T²/4) + (|T|/2) arctan (|T|/2)` of Lemma 3.3.

defdefined in CohnElkies/LowerBound/CenteredMax.lean

complete

def CohnElkies.lowerRiemannErrorMajorant (T : ℝ) : ℝ

def CohnElkies.lowerRiemannErrorMajorant
  (T : ℝ) : ℝ

The error majorant `3|f_T T 0| + 2|f_T T 1| + ½ log coth(π|T|/2)` of report Lemma 3.3.

Lemma7.2.2

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.24

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

For T \ne 0, with f_T from Definition 4.1.24 and \Lambda from Definition 7.2.1, one has the exact identity -\int_0^1f_T(x)\,dx = 1 + \Lambda(T).

Lean code for Lemma7.2.2●1 theorem

theoremdefined in CohnElkies/LowerBound/GammaBoundary.lean

complete

theorem CohnElkies.integral_lowerRiemannLog {T : ℝ} (hT : T ≠ 0) :
  -∫ (x : ℝ) in 0..1, CohnElkies.f_T T x =
    1 + CohnElkies.lowerEndpointPhase T

theorem CohnElkies.integral_lowerRiemannLog
  {T : ℝ} (hT : T ≠ 0) :
  -∫ (x : ℝ) in 0..1, CohnElkies.f_T T x =
    1 + CohnElkies.lowerEndpointPhase T

The Riemann-sum integral of Lemma 3.3, evaluated by the primitive above.

Proof for Lemma 7.2.2

uses 0

An elementary integration: x \mapsto x\log\sqrt{x^2 + T^2/4} - x + \tfrac{|T|}{2}\arctan\tfrac{2x}{|T|} is a primitive of f_T (CohnElkies.lowerRiemannLogPrimitive).

Lemma7.2.3

Statement uses 5

Statement dependency previews

Preview

Definition 4.1.7

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Lemma 4.1.26

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

For d \ge 2, c > 0 and T \ne 0, with \Lambda, E from Definition 7.2.1, one has the one-sided bound h_\lambda(\lambda T) \le \lambda\bigl(\log(2\pi ec^2) + \Lambda(T)\bigr) + E(T) for h_\lambda as in Definition 4.1.7 with R = c\sqrt d. Integrating against P_\sigma (Definition 4.1.8, Definition 4.1.10) gives, for 0 \le \sigma < 1, H_\sigma(0) \le \lambda M_\sigma\bigl(\log(2\pi c^2) + J_\sigma\bigr) + E_\sigma with J_\sigma = 1 + \int(P_\sigma/M_\sigma)\Lambda (Definition 4.1.24) and E_\sigma = \int P_\sigma E finite and independent of d and c: this is the upper half of (20) with an O_\sigma(1) error, Lemma 4.1.26.

Lean code for Lemma7.2.3●1 theorem

theoremdefined in CohnElkies/LowerBound/CenteredMax.lean

complete

theorem CohnElkies.lowerGammaBoundaryLog_dimension_scaled_riemann_le {d : ℕ}
  (hd : 2 ≤ d) {c T : ℝ} (hc : 0 < c) (hT : T ≠ 0) :
  CohnElkies.h_ℓ (↑d / 2) (c * √↑d) (↑d / 2 * T) ≤
    ↑d / 2 *
        (Real.log (2 * Real.pi * Real.exp 1 * c ^ 2) +
          CohnElkies.lowerEndpointPhase T) +
      CohnElkies.lowerRiemannErrorMajorant T

theorem CohnElkies.lowerGammaBoundaryLog_dimension_scaled_riemann_le
  {d : ℕ} (hd : 2 ≤ d) {c T : ℝ}
  (hc : 0 < c) (hT : T ≠ 0) :
  CohnElkies.h_ℓ (↑d / 2) (c * √↑d)
      (↑d / 2 * T) ≤
    ↑d / 2 *
        (Real.log
            (2 * Real.pi * Real.exp 1 *
              c ^ 2) +
          CohnElkies.lowerEndpointPhase
            T) +
      CohnElkies.lowerRiemannErrorMajorant
        T

Report Lemma 3.3 at the critical radius `R = c√d`.

Proof for Lemma 7.2.3

Proof uses 3

Proof dependency previews

Preview

Lemma 3.1.2

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

The same even/odd Riemann-sum computation as in the report's proof of Lemma 3.3, keeping only the upper estimates: the gamma product formulas of Lemma 3.1.3 and Lemma 3.1.2 express h_\lambda(\lambda T) through a left (even d) or midpoint (odd d) Riemann sum of f_T on [0,1], and monotonicity of f_T bounds the Riemann-sum errors by f_T(1) - f_T(0) (CohnElkies.monotone_leftRiemann_error, CohnElkies.monotone_midpointIntegral_error); the odd-dimensional endpoint correction \tfrac12\log(2\coth(\pi\lambda|T|/2)/|T|) is at most |f_T(0)| + \tfrac12\log\coth(\pi|T|/2), which makes E(T) independent of d. The identity Lemma 7.2.2 converts the integral of f_T into \Lambda, and the central bound follows by integrating against P_\sigma and using its mass M_\sigma.