QuantumBlockEncoding/StoredThinLQ.lean

This record groups the data and proof fields needed for “factors”. A proposition-valued field is a requirement until a constructor supplies it.

structure Factors (m n k : ℕ) where
  R : StoredMatrix m k
  Q : StoredMatrix k n

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “entry”.

def entry {N M : ℕ} (A : StoredMatrix N M) (i : Fin N) (j : Fin M) : Run ℝ := do
  let row ← read A i
  read row j

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “entry value”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem entry_value {N M : ℕ} (A : StoredMatrix N M) (i : Fin N) (j : Fin M) :
    (entry A i j).value = denote A i j := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “entry cost”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem entry_cost {N M : ℕ} (A : StoredMatrix N M) (i : Fin N) (j : Fin M)
    (op : Op) : (entry A i j).cost op = 2 * tick .read op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “transpose”.

def transpose {m n : ℕ} (A : StoredMatrix m n) : Run (StoredMatrix n m) :=
  materialize (fun i j => entry A j i)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “transpose value”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem transpose_value {m n : ℕ} (A : StoredMatrix m n) :
    denote (transpose A).value = (denote A).transpose := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “extraction budget”.

def extractionBudget (N M : ℕ) : Cost := fun op =>
  2 * N * M * tick .read op + (N * M + N) * (2 * tick .read op + 2 * tick .write op)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “transpose cost”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem transpose_cost {m n : ℕ} (A : StoredMatrix m n) (op : Op) :
    (transpose A).cost op = extractionBudget n m op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “extract r”.

def extractR {m n : ℕ} (h : m ≤ n) (C : StoredMatrix n m) : Run (StoredMatrix m m) :=
  materialize (fun i j => entry C (Fin.castLE h j) i)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “extract q”.

def extractQ {m n : ℕ} (h : m ≤ n) (E : StoredMatrix n n) : Run (StoredMatrix m n) :=
  materialize (fun i j => entry E (Fin.castLE h i) j)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “extract r value”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem extractR_value {m n : ℕ} (h : m ≤ n) (C : StoredMatrix n m) :
    denote (extractR h C).value = fun i j => denote C (Fin.castLE h j) i := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “extract q value”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem extractQ_value {m n : ℕ} (h : m ≤ n) (E : StoredMatrix n n) :
    denote (extractQ h E).value = fun i j => denote E (Fin.castLE h i) j := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “extract r cost”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem extractR_cost {m n : ℕ} (h : m ≤ n) (C : StoredMatrix n m) (op : Op) :
    (extractR h C).cost op = extractionBudget m m op := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “extract q cost”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem extractQ_cost {m n : ℕ} (h : m ≤ n) (E : StoredMatrix n n) (op : Op) :
    (extractQ h E).cost op = extractionBudget m n op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “wide”.

noncomputable def wide {m n : ℕ} (h : m ≤ n) (A : StoredMatrix m n) :
    Run (Factors m n m) := do
  let At ← transpose A
  let result ← StoredRectangularGivens.compile At
  let R ← extractR h result.reduced
  let Q ← extractQ h result.transform
  pure ⟨R, Q⟩

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “wide r”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem wide_R {m n : ℕ} (h : m ≤ n) (A : StoredMatrix m n) :
    denote (wide h A).value.R = ConstructiveThinLQ.wideR h (denote A) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “wide q”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem wide_Q {m n : ℕ} (h : m ≤ n) (A : StoredMatrix m n) :
    denote (wide h A).value.Q = ConstructiveThinLQ.wideQ h (denote A) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “wide correct”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem wide_correct {m n : ℕ} (h : m ≤ n) (A : StoredMatrix m n) :
    denote A = denote (wide h A).value.R * denote (wide h A).value.Q ∧
      denote (wide h A).value.Q * (denote (wide h A).value.Q).transpose = 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “wide budget”.

def wideBudget (m n : ℕ) : Cost :=
  extractionBudget n m + StoredRectangularGivens.polynomialBudget n m +
    extractionBudget m m + extractionBudget m n

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “wide cost le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem wide_cost_le {m n : ℕ} (h : m ≤ n) (A : StoredMatrix m n) (op : Op) :
    (wide h A).cost op ≤ wideBudget m n op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “compile body”.

noncomputable def compileBody {m n : ℕ} (A : StoredMatrix m n) :
    Run (Factors m n (min m n)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “compile”. The all-shape dispatcher additionally charges its dimension comparison.

noncomputable def compile {m n : ℕ} (A : StoredMatrix m n) :
    Run (Factors m n (min m n)) :=
  let result := compileBody A
  ⟨result.value, tick .compare + result.cost⟩

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile r”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compile_R {m n : ℕ} (A : StoredMatrix m n) :
    denote (compile A).value.R = (ConstructiveThinLQ.factor (denote A)).R := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile q”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compile_Q {m n : ℕ} (A : StoredMatrix m n) :
    denote (compile A).value.Q = (ConstructiveThinLQ.factor (denote A)).Q := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile correct”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compile_correct {m n : ℕ} (A : StoredMatrix m n) :
    denote A = denote (compile A).value.R * denote (compile A).value.Q ∧
      denote (compile A).value.Q * (denote (compile A).value.Q).transpose = 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “compile budget”.

def compileBudget (m n : ℕ) : Cost := tick .compare +
  if m ≤ n then wideBudget m n else StoredRectangularGivens.identityBudget n

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile cost le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compile_cost_le {m n : ℕ} (A : StoredMatrix m n) (op : Op) :
    (compile A).cost op ≤ compileBudget m n op := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Uniform cubic polynomial, including transpose/extraction and dispatch.

theorem compile_total_cost_le {m n : ℕ} (A : StoredMatrix m n) :
    StoredRectangularGivens.total (compile A).cost ≤
      n * m * (22 * m + 30 * n + 41) + 5 * n * n + 6 * m * m +
        8 * n + 9 * m + 2 := by

commit-pinned source · Verso Blueprint panel