Explicit exponents and dimension-dependent Hessian constants for the smoothing kernel.

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

The kernel coordinate exponent, capped by three times the logarithm of the dimension.

Equations

• V7.Stage5AboveTwoLower.kernelR0 p d = min p (3 * Real.log ↑d)

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

The kernel power parameter chosen strictly between one and half the coordinate exponent.

Equations

• V7.Stage5AboveTwoLower.kernelTheta p d = 1 + (V7.Stage5AboveTwoLower.kernelR0 p d - 2) / (4 * V7.Stage5AboveTwoLower.kernelR0 p d)

theorem V7.Stage5AboveTwoLower.two_lt_three_mul_log_nat {d : ℕ} (hd : 2 ≤ d) : 2 < 3 * Real.log ↑d

theorem V7.Stage5AboveTwoLower.two_lt_kernelR0 {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : 2 < kernelR0 p d

theorem V7.Stage5AboveTwoLower.one_lt_kernelTheta {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : 1 < kernelTheta p d

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

theorem V7.Stage5AboveTwoLower.kernelTheta_lt_five_four {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : kernelTheta p d < 5 / 4

theorem V7.Stage5AboveTwoLower.kernel_hessian_coefficient_lt_five_mul_r0 {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : 4 * kernelTheta p d * (kernelR0 p d - 1) < 5 * kernelR0 p d

theorem V7.Stage5AboveTwoLower.kernel_hessian_coefficient_explicit_bound {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : 4 * kernelTheta p d * (kernelR0 p d - 1) ≤ if p ≤ 3 * Real.log ↑d then 5 * p else 15 * Real.exp (2 / 3) * Real.log ↑d

theorem V7.Stage5AboveTwoLower.kernel_hessian_coefficient_universal_bound {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : 4 * kernelTheta p d * (kernelR0 p d - 1) ≤ 15 * min p (Real.log ↑d)

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