The inner-range allocation (water filling)

Classes c ≠ 0 with integer offsets β c (the row weights of class c are i + β c / 2). At a level k (weights < k/2), class c receives lrow k (β c) = ⌈(k - β c)/2⌉⁺ rows. We take the largest feasible level kf ∈ [klo, ktop] (at most h - L0min rows used) and put the remaining rows into the zero class. Then

• the allocation is valid for inner_bound_cap (the zero-class condition),
• ∑ wcap ≥ Φ(kf) - B₀, with Φ(k) = h k/2 - ∑_c ψ(k, β c) concave in k,
• Φ(kf) ≥ Φ(k) - (k - klo) L0min/2 for every k ∈ [klo, ktop].

def Zeta5Irrational.lrow (k β : ℤ) : ℕ

The number of rows of offset β below the level k: ⌈(k - β)/2⌉⁺.

Equations

• Zeta5Irrational.lrow k β = ((k - β + 1) / 2).toNat

theorem Zeta5Irrational.lrow_ge (k β : ℤ) : (↑k - ↑β) / 2 ≤ ↑(lrow k β)

theorem Zeta5Irrational.lrow_lt {k β : ℤ} {i : ℕ} (hi : i < lrow k β) : 2 * ↑i + ↑β < ↑k

theorem Zeta5Irrational.lrow_le_max (k β : ℤ) : ↑(lrow k β) + ↑β / 2 ≤ max (↑β) (↑k + 1) / 2

theorem Zeta5Irrational.lrow_mono {k k' : ℤ} (h : k ≤ k') (β : ℤ) : lrow k β ≤ lrow k' β

theorem Zeta5Irrational.lrow_succ (k β : ℤ) : lrow (k + 1) β = lrow k β ∨ lrow (k + 1) β = lrow k β + 1 ∧ 2 * ↑(lrow k β) + β = k

noncomputable def Zeta5Irrational.psiR (k β : ℤ) : ℚ

ψ(k, β) = ∑_{i < lrow} (k/2 - i - β/2).

Equations

• Zeta5Irrational.psiR k β = ∑ i ∈ Finset.range (Zeta5Irrational.lrow k β), (↑k - 2 * ↑i - ↑β) / 2

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

def Zeta5Irrational.rowsK {m : ℕ} (β : Fin (m + 1) → ℤ) (k : ℤ) : ℕ

Rows used at level k.

Equations

• Zeta5Irrational.rowsK β k = ∑ c ∈ Finset.univ.erase 0, Zeta5Irrational.lrow k (β c)

noncomputable def Zeta5Irrational.PhiK {m : ℕ} (β : Fin (m + 1) → ℤ) (h : ℕ) (k : ℤ) : ℚ

Φ(k) = h k / 2 - ∑ ψ.

Equations

• Zeta5Irrational.PhiK β h k = ↑h * ↑k / 2 - ∑ c ∈ Finset.univ.erase 0, Zeta5Irrational.psiR k (β c)

theorem Zeta5Irrational.PhiK_succ {m : ℕ} (β : Fin (m + 1) → ℤ) (h : ℕ) (k : ℤ) : PhiK β h (k + 1) = PhiK β h k + (↑h - ↑(rowsK β (k + 1))) / 2

theorem Zeta5Irrational.rowsK_mono {m : ℕ} (β : Fin (m + 1) → ℤ) {k k' : ℤ} (h : k ≤ k') : rowsK β k ≤ rowsK β k'

noncomputable def Zeta5Irrational.kfSel {m : ℕ} (β : Fin (m + 1) → ℤ) (h L0min : ℕ) (klo ktop : ℤ) : ℤ

The chosen level.

Equations

• Zeta5Irrational.kfSel β h L0min klo ktop = klo + ↑(Nat.findGreatest (fun (j : ℕ) => Zeta5Irrational.rowsK β (klo + ↑j) + L0min ≤ h) (ktop - klo).toNat)

theorem Zeta5Irrational.kfSel_feasible {m : ℕ} (β : Fin (m + 1) → ℤ) (h L0min : ℕ) (klo ktop : ℤ) (hlo : rowsK β klo + L0min ≤ h) : rowsK β (kfSel β h L0min klo ktop) + L0min ≤ h

theorem Zeta5Irrational.kfSel_ge {m : ℕ} (β : Fin (m + 1) → ℤ) (h L0min : ℕ) (klo ktop : ℤ) : klo ≤ kfSel β h L0min klo ktop

theorem Zeta5Irrational.kfSel_le {m : ℕ} (β : Fin (m + 1) → ℤ) (h L0min : ℕ) (klo ktop : ℤ) (hk : klo ≤ ktop) : kfSel β h L0min klo ktop ≤ ktop

theorem Zeta5Irrational.kfSel_max {m : ℕ} (β : Fin (m + 1) → ℤ) (h L0min : ℕ) (klo ktop : ℤ) {k : ℤ} (hk1 : kfSel β h L0min klo ktop < k) (hk2 : k ≤ ktop) : h < rowsK β k + L0min

theorem Zeta5Irrational.PhiK_le_kf {m : ℕ} (β : Fin (m + 1) → ℤ) (h L0min : ℕ) (klo ktop : ℤ) (hlo : rowsK β klo + L0min ≤ h) {k : ℤ} (hk1 : klo ≤ k) (hk2 : k ≤ ktop) : PhiK β h k ≤ PhiK β h (kfSel β h L0min klo ktop) + ↑(k - klo) * ↑L0min / 2

Concavity comparison: Φ(k) ≤ Φ(kf) + (k - klo) L0min / 2 on [klo, ktop].

noncomputable def Zeta5Irrational.allocK {m : ℕ} (β : Fin (m + 1) → ℤ) (h : ℕ) (kf : ℤ) (c : Fin (m + 1)) : ℕ

The allocation.

Equations

• Zeta5Irrational.allocK β h kf c = if c = 0 then h - Zeta5Irrational.rowsK β kf else Zeta5Irrational.lrow kf (β c)

theorem Zeta5Irrational.sum_allocK {m : ℕ} (β : Fin (m + 1) → ℤ) (h : ℕ) (kf : ℤ) (hkf : rowsK β kf ≤ h) : ∑ c : Fin (m + 1), allocK β h kf c = h

theorem Zeta5Irrational.sum_deficit_le (D : ℚ) (L : ℕ) : ∑ i ∈ Finset.range L, max 0 (D - 2 * ↑i) ≤ max 0 D * (max 0 D / 2 + 1)

The zero-class deficit: ∑_{i<L} (D - 2i)⁺ ≤ D⁺ (D⁺/2 + 1).

theorem Zeta5Irrational.tmin_allocK_ge {m : ℕ} (hm1 : 1 ≤ m) (b : ℕ → ℚ) (β : Fin (m + 1) → ℤ) (hβ : ∀ (c : Fin (m + 1)), c ≠ 0 → b ↑c = ↑(β c) + 4) (h : ℕ) (kf : ℤ) : ↑kf / 2 ≤ tmin hm1 (allocK β h kf) b

theorem Zeta5Irrational.tmin_allocK_le {m : ℕ} (hm1 : 1 ≤ m) (b : ℕ → ℚ) (β : Fin (m + 1) → ℤ) (hβ : ∀ (c : Fin (m + 1)), c ≠ 0 → b ↑c = ↑(β c) + 4) (h : ℕ) (kf : ℤ) : tmin hm1 (allocK β h kf) b ≤ max (↑(β ⟨1, ⋯⟩)) (↑kf + 1) / 2

theorem Zeta5Irrational.sum_wcap_allocK {m : ℕ} (hm1 : 1 ≤ m) (b : ℕ → ℚ) (β : Fin (m + 1) → ℤ) (hβ : ∀ (c : Fin (m + 1)), c ≠ 0 → b ↑c = ↑(β c) + 4) (h : ℕ) (kf : ℤ) (hkf : rowsK β kf ≤ h) : PhiK β h kf - max 0 (↑kf / 2 - (b 0 - 4) / 2) * (max 0 (↑kf / 2 - (b 0 - 4) / 2) / 2 + 1) ≤ ∑ s : (a : Fin (m + 1)) × Fin (allocK β h kf a), wcap hm1 (allocK β h kf) b s

The weight sum of the allocation: ∑ wcap ≥ Φ(kf) - B₀.