ASPBE Lean Blueprint

6.48. QuantumBlockEncoding/ThinLQ.lean🔗

3 explicit public declarations, in source order.

Theorem6.48.1
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sum prefix of zero”; the hypotheses and conclusion in the code panel fix its exact scope. Restrict a finite sum to a prefix when all remaining summands vanish.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Restrict a finite sum to a prefix when all remaining summands vanish.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ThinLQ.lean:18. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.48.1●1 theorem
  • theoremdefined in QuantumBlockEncoding/ThinLQ.lean
    complete
    theorem QuantumBlockEncoding.ThinLQ.sum_prefix_of_zero.{u_1} {m n : ℕ}
  {M : Type u_1} [AddCommMonoid M] (hmn : m ≤ n) (f : Fin n → M)
  (hf : ∀ (j : Fin n), m ≤ ↑j → f j = 0) :
  ∑ i, f (Fin.castLE hmn i) = ∑ j, f j
    theorem QuantumBlockEncoding.ThinLQ.sum_prefix_of_zero.{u_1}
  {m n : ℕ} {M : Type u_1}
  [AddCommMonoid M] (hmn : m ≤ n)
  (f : Fin n → M)
  (hf : ∀ (j : Fin n), m ≤ ↑j → f j = 0) :
  ∑ i, f (Fin.castLE hmn i) = ∑ j, f j
    Restrict a finite sum to a prefix when all remaining summands vanish.
Theorem6.48.2
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists factor of le”; the hypotheses and conclusion in the code panel fix its exact scope. A wide real matrix has an exact factorization with orthonormal rows.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. A wide real matrix has an exact factorization with orthonormal rows. No linear-independence or nonzero-row assumption is required.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ThinLQ.lean:38. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.48.2●1 theorem
  • theoremdefined in QuantumBlockEncoding/ThinLQ.lean
    complete
    theorem QuantumBlockEncoding.ThinLQ.exists_factor_of_le {m n : ℕ} (hmn : m ≤ n)
  (A : Matrix (Fin m) (Fin n) ℝ) :
  ∃ R Q, A = R * Q ∧ Q * Q.transpose = 1
    theorem QuantumBlockEncoding.ThinLQ.exists_factor_of_le
  {m n : ℕ} (hmn : m ≤ n)
  (A : Matrix (Fin m) (Fin n) ℝ) :
  ∃ R Q, A = R * Q ∧ Q * Q.transpose = 1
    A wide real matrix has an exact factorization with orthonormal rows.
No linear-independence or nonzero-row assumption is required.
Theorem6.48.3
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists thin lq”; the hypotheses and conclusion in the code panel fix its exact scope. Every finite real matrix admits a thin factorization with exactly 'min m n' orthonormal rows.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Every finite real matrix admits a thin factorization with exactly 'min m n' orthonormal rows. This includes rank-deficient and empty matrices.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ThinLQ.lean:81. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.48.3●1 theorem
  • theoremdefined in QuantumBlockEncoding/ThinLQ.lean
    complete
    theorem QuantumBlockEncoding.ThinLQ.exists_thin_lq {m n : ℕ}
  (A : Matrix (Fin m) (Fin n) ℝ) :
  ∃ R Q, A = R * Q ∧ Q * Q.transpose = 1
    theorem QuantumBlockEncoding.ThinLQ.exists_thin_lq
  {m n : ℕ}
  (A : Matrix (Fin m) (Fin n) ℝ) :
  ∃ R Q, A = R * Q ∧ Q * Q.transpose = 1
    Every finite real matrix admits a thin factorization with exactly
`min m n` orthonormal rows. This includes rank-deficient and empty matrices.