Absorb the degree-dependent projection box factor into a constant depending only on ambient dimension, retaining the exact exponent 1/d and d³ factor.

def CCDN.projectionLogConstant (n : ℕ) : ℝ

The constant c = 2 * n ^ 2 + 3 * n, for which log (projectionBoxFactor n d) ≤ c * d.

Equations

• CCDN.projectionLogConstant n = 2 * ↑n ^ 2 + 3 * ↑n

theorem CCDN.projectionLogConstant_nonneg (n : ℕ) : 0 ≤ projectionLogConstant n

The projection log constant is nonnegative.

theorem CCDN.projectionBoxFactor_log_le (n : ℕ) {d : ℕ} (hd : 0 < d) : Real.log (projectionBoxFactor n d) ≤ projectionLogConstant n * ↑d

For d > 0, the logarithm of the projection box factor is at most projectionLogConstant n * d.

theorem CCDN.projection_curveBound_scale (n : ℕ) {d : ℕ} (hd : 0 < d) {B : ℝ} (hB : 1 ≤ B) : curveBound d (projectionBoxFactor n d * B) ≤ Real.exp (projectionLogConstant n) * (projectionLogConstant n + 1) * curveBound d B

Scaling the radius by the projection box factor multiplies the curve bound by at most a constant depending only on n: with c = projectionLogConstant n, for d > 0 and B ≥ 1, curveBound d (projectionBoxFactor n d * B) ≤ exp c * (c + 1) * curveBound d B.