The inner tail: -L_p ≤ p (x F(x) + 27/16) + O(x²)

For an explicit level k (the rounded minimiser of the quadratic majorant) the discrete bound of inner_Lp_le is at most p (x F(x) + 27/16) + C(x), where F(x) = 4λ + 2λ{x} - 12λ{αx}, λ = 37/40, α = 3/40, x = K/p.

Elementary facts

theorem Zeta5Irrational.sum_range_tri (t : ℚ) (L : ℕ) : ∑ i ∈ Finset.range L, (t - 2 * ↑i) / 2 = ↑L * (t - ↑L + 1) / 2

theorem Zeta5Irrational.psiR_le (k β : ℤ) : psiR k β ≤ ↑(k - β + 1) ^ 2 / 8

theorem Zeta5Irrational.sum_aCnt {p m v : ℕ} (hm : 2 * m + 1 = p) (hv : v < p) : ∑ c ∈ Finset.Icc 1 m, aCnt p v c = v

theorem Zeta5Irrational.aCnt_range {p m v c : ℕ} (hm : 2 * m + 1 = p) (hv : v < p) (_hc1 : 1 ≤ c) (hcm : c ≤ m) : (if m < v then 1 else 0) ≤ aCnt p v c ∧ aCnt p v c ≤ (if m < v then 1 else 0) + 1

theorem Zeta5Irrational.popoviciu {ι : Type u_1} (s : Finset ι) (φ : ι → ℝ) (L : ℝ) (hφ : ∀ c ∈ s, L ≤ φ c ∧ φ c ≤ L + 7) (hs : 0 < s.card) : ∑ c ∈ s, φ c ^ 2 ≤ (∑ c ∈ s, φ c) ^ 2 / ↑s.card + 49 * ↑s.card / 4

Popoviciu: values in an interval of length 7 have ∑ φ² ≤ (∑ φ)²/m + 49m/4.

noncomputable def Zeta5Irrational.Jc (u : ℝ) : ℝ

The continuous layer function J(u) = ∑_{j ≤ 1000} (u - j/2)⁺.

Equations

• Zeta5Irrational.Jc u = ∑ j ∈ Finset.Icc 1 1000, max 0 (u - ↑j / 2)

theorem Zeta5Irrational.layer_eq {p : ℕ} (hp : 0 < p) (h : ℕ) : layer p 1000 ↑h = ↑p * Jc (↑h / ↑p)

theorem Zeta5Irrational.two_Jc_eq {u : ℝ} (hu0 : 0 ≤ u) (hu : u ≤ 500) : 2 * Jc u = 2 * u ^ 2 - u + Int.fract (2 * u) * (1 - Int.fract (2 * u)) / 2

2 J(u) = 2u² - u + η(1 - η)/2 with η = {2u}, for 0 ≤ u ≤ 500.

theorem Zeta5Irrational.phi_bounds {p m v v' c : ℕ} (hm : 2 * m + 1 = p) (hv : v < p) (hv' : v' < p) (hc1 : 1 ≤ c) (hcm : c ≤ m) : ((6 * if m < v' then 1 else 0) - if m < v then 1 else 0) - 1 ≤ 6 * ↑(aCnt p v' c) - ↑(aCnt p v c) ∧ 6 * ↑(aCnt p v' c) - ↑(aCnt p v c) ≤ ((6 * if m < v' then 1 else 0) - if m < v then 1 else 0) - 1 + 7

theorem Zeta5Irrational.hIn_le_sq (n p : ℕ) (k τ : ℤ) (hk : k = τ + (12 * ↑(3 * n / p) - 2 * ↑(40 * n / p) - 4) - 1) (a a' : ℕ) : hIn n p k a a' ≤ (↑τ - (6 * ↑a' - ↑a)) ^ 2 / 8

theorem Zeta5Irrational.layer_le {p : ℕ} (hp0 : 0 < p) (H : ℕ) (hu500 : ↑H / ↑p ≤ 500) : 2 * layer p 1000 ↑H ≤ 2 * ↑H ^ 2 / ↑p - ↑H + ↑p / 8

theorem Zeta5Irrational.quad_le {hR SR m τ : ℝ} (hm0 : 0 < m) (h1 : τ ≤ (SR + 2 * hR) / m + 1 / 2) (h2 : (SR + 2 * hR) / m + 1 / 2 < τ + 1) : -hR * τ + (m * τ ^ 2 - 2 * τ * SR + SR ^ 2 / m) / 4 ≤ -hR * SR / m - hR ^ 2 / m + m / 16

theorem Zeta5Irrational.diff_le {hR SR p : ℝ} (hp : 1 < p) (hh0 : 0 ≤ hR) (hhS : 0 ≤ hR + SR) : 2 * hR ^ 2 / p - hR ^ 2 / ((p - 1) / 2) - hR * SR / ((p - 1) / 2) + 2 * hR * SR / p ≤ 0

noncomputable def Zeta5Irrational.Ftail (x : ℝ) : ℝ

F(x) = 4λ + 2λ{x} - 12λ{αx}.

Equations

• Zeta5Irrational.Ftail x = 4 * (37 / 40) + 2 * (37 / 40) * Int.fract x - 12 * (37 / 40) * Int.fract (3 / 40 * x)

noncomputable def Zeta5Irrational.Ctail (n p : ℕ) : ℝ

The additive error of the tail bound.

Equations

• Zeta5Irrational.Ctail n p = 4 * (37 * ↑n) / ↑p + ↑(Zeta5Irrational.ktopI n p - Zeta5Irrational.kloI n p) * ↑(Zeta5Irrational.L0I n p) + 2 * Zeta5Irrational.Bmax n p + 1

theorem Zeta5Irrational.tail_class_sum_le (n p v v' : ℕ) (k τ : ℤ) (hodd : 2 * (p / 2) + 1 = p) (hvp : v < p) (hv'p : v' < p) (hm : 0 < p / 2) (hk : k = τ + (12 * ↑(3 * n / p) - 2 * ↑(40 * n / p) - 4) - 1) : 2 * ∑ c ∈ Finset.Icc 1 (p / 2), hIn n p k (aCnt p v c) (aCnt p v' c) ≤ (↑(p / 2) * ↑τ ^ 2 - 2 * ↑τ * (6 * ↑v' - ↑v) + (6 * ↑v' - ↑v) ^ 2 / ↑(p / 2) + 49 * ↑(p / 2) / 4) / 4

Sum the quadratic class bound using the seven-unit range of the counts.

noncomputable def Zeta5Irrational.tailLevel (n p : ℕ) : ℤ

The integral level obtained by rounding the quadratic minimizer.

Equations

• Zeta5Irrational.tailLevel n p = ⌊(6 * ↑(3 * n % p) - ↑(40 * n % p) + 2 * (37 * ↑n)) / ↑(p / 2) + 1 / 2⌋ + (12 * ↑(3 * n / p) - 2 * ↑(40 * n / p) - 4) - 1

theorem Zeta5Irrational.tailLevel_mem (n p : ℕ) (hodd : 2 * (p / 2) + 1 = p) (hp7 : 7 ≤ p) (hin : 3 * p ≤ 40 * n) : kloI n p ≤ tailLevel n p ∧ tailLevel n p ≤ ktopI n p

The rounded minimizer lies in the admissible interval of integral levels.

theorem Zeta5Irrational.tail_Lp_le {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 33 ≤ n) (hodd : 2 * (p / 2) + 1 = p) (hp7 : 7 ≤ p) (hsmall : ¬p * Mcut ≤ 40 * n) (hin : 3 * p ≤ 40 * n) (hsq : 2 * (40 * n) < p ^ 2) (hdeg : 5 + 2 * (18 * n + 2 * (37 * n)) - 2 * (40 * n) + 1 < p ^ 2) : -↑(Lp n p) ≤ ↑p * (40 * ↑n / ↑p * Ftail (40 * ↑n / ↑p) + 27 / 16) + Ctail n p

The tail bound: -L_p ≤ p (x F(x) + 27/16) + C.