← Mathematical handbook

def Verification.rankUpdateSlots (n : ℕ) : ℕ

Four explicit sparse update slots per observation.

Equations

• Verification.rankUpdateSlots n = Fintype.card (Fin n × Fin 2 × Fin 2)

def Verification.matrixProductSlots (K : ℕ) : ℕ

Number of scalar products in one dense K-by-K matrix multiplication.

Equations

• Verification.matrixProductSlots K = Fintype.card (Fin K × Fin K × Fin K)

theorem Verification.rankUpdateSlots_eq (n : ℕ) : rankUpdateSlots n = 4 * n

theorem Verification.matrixProductSlots_eq (K : ℕ) : matrixProductSlots K = K ^ 3

def Verification.checkerboardEstimatorWork {α : Type u_1} {β : Type u_2} (leX : α → α → Bool) (leY : β → β → Bool) (xs : List α) (ys : List β) (K : ℕ) : ℕ

Unit-cost work for two rank sorts, four sparse updates per sample, and three dense matrix products, initialization and traces. The factor 32 covers scalar arithmetic and indexing in each slot of the explicit finite formulas.

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.checkerboardEstimatorWork_bound {α : Type u_1} {β : Type u_2} (leX : α → α → Bool) (leY : β → β → Bool) (xs : List α) (ys : List β) (hxy : ys.length = xs.length) (K : ℕ) (hK : 0 < K) (hKn : K ^ 3 ≤ xs.length) : checkerboardEstimatorWork leX leY xs ys K ≤ 6 * xs.length * Nat.clog 2 xs.length + 320 * xs.length

theorem Verification.nat_clog_two_le_log (n : ℕ) (hn : 2 ≤ n) : ↑(Nat.clog 2 n) ≤ 2 / Real.log 2 * Real.log ↑n

theorem Verification.checkerboardEstimatorWork_isBigO {α : Type u_1} {β : Type u_2} (leX : α → α → Bool) (leY : β → β → Bool) (xs : ℕ → List α) (ys : ℕ → List β) (hx : ∀ (n : ℕ), (xs n).length = n + 1) (hy : ∀ (n : ℕ), (ys n).length = n + 1) (κ : ℝ) (hκ : 0 ≤ κ) (hκ' : κ ≤ 1 / 3) : (fun (n : ℕ) => ↑(checkerboardEstimatorWork leX leY (xs n) (ys n) (powerGridIndex κ n + 1))) =O[Filter.atTop] fun (n : ℕ) => (↑n + 1) * Real.log (↑n + 1)

The prescribed sparse/matrix work schedule is O(N log N) for the source's power grid, with the standard unit-cost arithmetic and array-update convention.