Generated by gen_inner_sum.py: the table of Ê_in on [3, 20].

def Zeta5Irrational.tInL : List ℚ

The 126 rational endpoints of the 125 inner-range linear pieces.

Equations

• One or more equations did not get rendered due to their size.

def Zeta5Irrational.kInL : List ℤ

Integer allocation levels chosen for the 125 inner-range pieces.

Equations

• One or more equations did not get rendered due to their size.

def Zeta5Irrational.aInL : List ℚ

Rational slopes of the 125 inner-range linear pieces.

Equations

• One or more equations did not get rendered due to their size.

def Zeta5Irrational.bInL : List ℚ

Rational intercepts of the 125 inner-range linear pieces.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Zeta5Irrational.tIn (i : ℕ) : ℝ

The ith inner-range endpoint as a real number; zero outside the table.

Equations

• Zeta5Irrational.tIn i = ↑(Zeta5Irrational.tInL.getD i 0)

def Zeta5Irrational.kIn (i : ℕ) : ℤ

The allocation level for inner piece i; zero outside the table.

Equations

• Zeta5Irrational.kIn i = Zeta5Irrational.kInL.getD i 0

noncomputable def Zeta5Irrational.gIn (i : ℕ) (x : ℝ) : ℝ

The affine bound on inner piece i, with coefficients from aInL and bInL.

Equations

• Zeta5Irrational.gIn i x = ↑(Zeta5Irrational.aInL.getD i 0) * x + ↑(Zeta5Irrational.bInL.getD i 0)

theorem Zeta5Irrational.tIn_mono (i : ℕ) : i < 125 → tIn i < tIn (i + 1)

theorem Zeta5Irrational.inner_table (i : ℕ) : i < 125 → ∀ x ∈ Set.Ico (tIn i) (tIn (i + 1)), Ein x (kIn i) = gIn i x

theorem Zeta5Irrational.inner_table_k (i : ℕ) : i < 125 → ∀ x ∈ Set.Ico (tIn i) (tIn (i + 1)), -2 * ↑⌊x⌋₊ - 6 ≤ kIn i ∧ kIn i ≤ 8 * ↑⌊x⌋₊ + 20