Exact Euclidean estimate-sequence weights

This module records the source recurrence A₀ = 0, aₖ₊₁ = euclideanWeight Aₖ, and Aₖ₊₁ = Aₖ + aₖ₊₁. In particular, the quadratic identity defining the weight gives the exact alternative form Aₖ₊₁ = aₖ₊₁².

noncomputable def O3.euclideanA : ℕ → ℝ

The cumulative weights in the Euclidean estimate sequence.

Equations

• O3.euclideanA 0 = 0
• O3.euclideanA k.succ = O3.euclideanA k + O3.euclideanWeight (O3.euclideanA k)

@[simp]

theorem O3.euclideanA_zero : euclideanA 0 = 0

@[simp]

theorem O3.euclideanA_succ (k : ℕ) : euclideanA (k + 1) = euclideanA k + euclideanWeight (euclideanA k)

theorem O3.euclideanA_nonneg (k : ℕ) : 0 ≤ euclideanA k

theorem O3.euclideanA_increment_pos (k : ℕ) : 0 < euclideanWeight (euclideanA k)

Every recursive increment is strictly positive.

theorem O3.euclideanA_increment (k : ℕ) : euclideanA (k + 1) - euclideanA k = euclideanWeight (euclideanA k)

Exact defining increment of the cumulative weight.

theorem O3.euclideanWeight_sq_eq_next (k : ℕ) : euclideanWeight (euclideanA k) ^ 2 = euclideanA (k + 1)

The source quadratic relation aₖ₊₁²=Aₖ₊₁.

theorem O3.euclideanA_pos_of_one_le {k : ℕ} (hk : 1 ≤ k) : 0 < euclideanA k

theorem O3.euclideanWeight_ge_half_succ {k : ℕ} (hA : (↑k + 1) ^ 2 / 4 ≤ euclideanA k) : (↑k + 2) / 2 ≤ euclideanWeight (euclideanA k)

A convenient lower bound on the next weight implied by a quadratic lower bound on the current cumulative weight.

theorem O3.euclideanA_quadratic_lower {m : ℕ} (hm : 1 ≤ m) : (↑m + 1) ^ 2 / 4 ≤ euclideanA m

Exact source denominator growth: for every nonzero horizon, Aₘ ≥ (m+1)²/4.