← Mathematical handbook

noncomputable def Verification.powerGridIndex (κ : ℝ) (n : ℕ) : ℕ

Zero-based grid dimension: actual order is floor((n+1)^κ).

Equations

• Verification.powerGridIndex κ n = ⌊(↑n + 1) ^ κ⌋₊ - 1

theorem Verification.powerGridIndex_succ (κ : ℝ) (hκ : 0 ≤ κ) (n : ℕ) : powerGridIndex κ n + 1 = ⌊(↑n + 1) ^ κ⌋₊

theorem Verification.powerGridIndex_tendsto (κ : ℝ) (hκ : 0 < κ) : Filter.Tendsto (powerGridIndex κ) Filter.atTop Filter.atTop

theorem Verification.powerGridIndex_bound (κ : ℝ) (hκ : 0 ≤ κ) (hκ' : κ ≤ 1 / 3) (n : ℕ) : ↑(powerGridIndex κ n) + 1 ≤ (↑n + 2) ^ (1 / 3)

theorem Verification.powerGridIndex_rate_tendsto (κ : ℝ) (hκ : 0 ≤ κ) (hκ' : κ ≤ 1 / 3) : Filter.Tendsto (fun (n : ℕ) => (↑(powerGridIndex κ n) + 1) * (3 * empiricalCDFRadius n + 8 / (↑n + 1))) Filter.atTop (nhds 0)

theorem Verification.powerGridIndex_cube_le (κ : ℝ) (hκ : 0 ≤ κ) (hκ' : κ ≤ 1 / 3) (n : ℕ) : (powerGridIndex κ n + 1) ^ 3 ≤ n + 1

The cubic matrix-arithmetic term is bounded by the sample size.