Refined kernel parameters satisfying the required exponent and Hessian bounds.

noncomputable def V7.Stage5AboveTwoLower.S5ARepair.repairTheta (p : ℝ) (d : ℕ) : ℝ

A parameter choice close enough to one to leave quantitative room for the finite-dimensional \ell_{r₀}-to-\ell_p conversion in the Hessian bound. The frozen carrier only existentially quantifies theta; this definition does not alter any statement.

Equations

• V7.Stage5AboveTwoLower.S5ARepair.repairTheta p d = 1 + (V7.Stage5AboveTwoLower.kernelR0 p d - 2) / (100 * V7.Stage5AboveTwoLower.kernelR0 p d)

theorem V7.Stage5AboveTwoLower.S5ARepair.one_lt_repairTheta {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : 1 < repairTheta p d

theorem V7.Stage5AboveTwoLower.S5ARepair.repairTheta_lt_101_div_100 {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : repairTheta p d < 101 / 100

theorem V7.Stage5AboveTwoLower.S5ARepair.two_mul_repairTheta_lt_kernelR0 {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : 2 * repairTheta p d < kernelR0 p d

theorem V7.Stage5AboveTwoLower.S5ARepair.repair_hessian_coefficient_lt_101_div_25_mul_r0 {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : 4 * repairTheta p d * (kernelR0 p d - 1) < 101 / 25 * kernelR0 p d

theorem V7.Stage5AboveTwoLower.S5ARepair.repair_parameter_package {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : kernelR0 p d = min p (3 * Real.log ↑d) ∧ 1 < repairTheta p d ∧ 2 * repairTheta p d < kernelR0 p d