Helpers for the piece tables

On a piece where ⌊x⌋, ⌊αx⌋, ⌊2λx⌋ are constant, Ê_in(x, k) and Ê_out(x) are explicit combinations of the interval counts c_{ij}({x}, {αx}); the counts have closed forms.

theorem Zeta5Irrational.nat_floor_of_bounds {x : ℝ} {q : ℕ} (h1 : ↑q ≤ x) (h2 : x < ↑q + 1) : ⌊x⌋₊ = q

theorem Zeta5Irrational.fract_of_bounds {x : ℝ} {q : ℕ} (h1 : ↑q ≤ x) (h2 : x < ↑q + 1) : Int.fract x = x - ↑q

theorem Zeta5Irrational.two_Jc_lin {u : ℝ} (μ : ℕ) (h1 : ↑μ ≤ 2 * u) (h2 : 2 * u < ↑μ + 1) (hu : u ≤ 500) : 2 * Jc u = 2 * ↑μ * u - ↑μ * (↑μ + 1) / 2

theorem Zeta5Irrational.psiR_eq (k β : ℤ) : psiR k β = ↑(lrow k β) * (↑(k - β) - ↑(lrow k β) + 1) / 2

ψ in closed form.

Closed forms of the interval counts

theorem Zeta5Irrational.cc00 {f g : ℝ} : ccount f g 0 0 = 1 / 2

theorem Zeta5Irrational.cc01 {f g : ℝ} (hg0 : 0 ≤ g) (hg1 : g < 1) : ccount f g 0 1 = min g (1 / 2)

theorem Zeta5Irrational.cc02 {f g : ℝ} (hg1 : g < 1) : ccount f g 0 2 = max 0 (g - 1 / 2)

theorem Zeta5Irrational.cc10 {f g : ℝ} (hf0 : 0 ≤ f) (hf1 : f < 1) : ccount f g 1 0 = min f (1 / 2)

theorem Zeta5Irrational.cc20 {f g : ℝ} (hf1 : f < 1) : ccount f g 2 0 = max 0 (f - 1 / 2)

theorem Zeta5Irrational.cc11 {f g : ℝ} (hf0 : 0 ≤ f) (hf1 : f < 1) (hg0 : 0 ≤ g) : ccount f g 1 1 = min (min f g) (1 / 2)

theorem Zeta5Irrational.cc12 {f g : ℝ} (hg1 : g < 1) : ccount f g 1 2 = max 0 (min f (1 / 2) + g - 1)

theorem Zeta5Irrational.cc21 {f g : ℝ} (hf1 : f < 1) : ccount f g 2 1 = max 0 (min g (1 / 2) + f - 1)

theorem Zeta5Irrational.cc22 {f g : ℝ} (hg1 : g < 1) : ccount f g 2 2 = max 0 (min f g - 1 / 2)

theorem Zeta5Irrational.Ein_expand {x : ℝ} (k : ℤ) {q q' μ : ℕ} (hq1 : ↑q ≤ x) (hq2 : x < ↑q + 1) (hr1 : ↑q' ≤ 3 / 40 * x) (hr2 : 3 / 40 * x < ↑q' + 1) (hm1 : ↑μ ≤ 2 * (37 / 40 * x)) (hm2 : 2 * (37 / 40 * x) < ↑μ + 1) (hx : x ≤ 400) : Ein x k = -2 * (37 / 40 * x) * ↑q + 12 * (37 / 40 * x) * ↑q' + (2 * ↑μ * (37 / 40 * x) - ↑μ * (↑μ + 1) / 2) - 37 / 40 * x * ↑k + 2 * ∑ i : Fin 3, ∑ j : Fin 3, bIn q q' k i j * ccount (x - ↑q) (3 / 40 * x - ↑q') i j

Ê_in on a piece.

theorem Zeta5Irrational.Eout_expand {x : ℝ} {q q' μ : ℕ} (hq1 : ↑q ≤ x) (hq2 : x < ↑q + 1) (hr1 : ↑q' ≤ 3 / 40 * x) (hr2 : 3 / 40 * x < ↑q' + 1) (hm1 : ↑μ ≤ 2 * (37 / 40 * x)) (hm2 : 2 * (37 / 40 * x) < ↑μ + 1) (hx : x ≤ 400) : Eout x = -2 * (37 / 40 * x) * ↑q + (2 * ↑μ * (37 / 40 * x) - ↑μ * (↑μ + 1) / 2) - 2 * ∑ i : Fin 3, ∑ j : Fin 3, bGO q i j * ccount (x - ↑q) (3 / 40 * x - ↑q') i j + max 0 (13 / 10 * x - 2)

Ê_out on a piece.

theorem Zeta5Irrational.toNat_cast_q (a : ℤ) : ↑a.toNat = max (↑a) 0