Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.Arithmetic.Exponent

Division-free arithmetic programs over a field and their operation counts.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.AdmissibleExponent.mono {F : Type u_1} [Field F] {τ σ : ℝ} (hτ : AdmissibleExponent F τ) (hτσ : τ ≤ σ) :

AdmissibleExponent F σ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.omega_two_le {F : Type u_1} [Field F] :

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.omega_nonneg {F : Type u_1} [Field F] :

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.omega_le_three {F : Type u_1} [Field F] :

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.omega_admissibleExponent {F : Type u_1} [Field F] :

AdmissibleExponent F (omega F)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_iff_omega_le {F : Type u_1} [Field F] {τ : ℝ} :

AdmissibleExponent F τ ↔ omega F ≤ τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RectangularAdmissibleExponent.mono {F : Type u_1} [Field F] {k τ σ : ℝ} (hτ : RectangularAdmissibleExponent F k τ) (hτσ : τ ≤ σ) :

RectangularAdmissibleExponent F k σ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_uniform_costs {F : Type u_1} [Field F] {k τ C : ℝ} (hC : 0 < C) (hbound : ∀ (n : ℕ), 1 ≤ n → ∃ (P : MatrixAlgorithm F n (innerSize n k) n), P.Correct ∧ ↑P.cost ≤ C * ↑n ^ τ) :

RectangularAdmissibleExponent F k τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_naive {F : Type u_1} [Field F] (k : ℝ) :

RectangularAdmissibleExponent F k (2 + max k 0)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_nonempty {F : Type u_1} [Field F] (k : ℝ) :

{τ : ℝ | RectangularAdmissibleExponent F k τ}.Nonempty

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_two_le {F : Type u_1} [Field F] (k : ℝ) :

2 ≤ rectangularOmega F k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_admissibleExponent {F : Type u_1} [Field F] (k : ℝ) :

RectangularAdmissibleExponent F k (rectangularOmega F k)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_iff_omega_le {F : Type u_1} [Field F] {k τ : ℝ} :

RectangularAdmissibleExponent F k τ ↔ rectangularOmega F k ≤ τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_mono {F : Type u_1} [Field F] {k l : ℝ} (hkl : k ≤ l) :

rectangularOmega F k ≤ rectangularOmega F l

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_zero {F : Type u_1} [Field F] :

rectangularOmega F 0 = 2

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.complexAlpha_set_nonempty :

{k : ℝ | k ∈ Set.Icc 0 1 ∧ rectangularOmega ℂ k = 2}.Nonempty

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.complexAlpha_set_bddAbove :

BddAbove {k : ℝ | k ∈ Set.Icc 0 1 ∧ rectangularOmega ℂ k = 2}

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.le_complexAlpha {k : ℝ} (hk : k ∈ Set.Icc 0 1) (hω : rectangularOmega ℂ k = 2) :

k ≤ complexAlpha

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.complexAlpha_le_one :

complexAlpha ≤ 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.complexAlpha_nonneg :

0 ≤ complexAlpha