6.24. QuantumBlockEncoding/RectangularGivens.lean🔗

19 explicit public declarations, in source order.

Definition6.24.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sweep”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.24.1●1 definition

defdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

def QuantumBlockEncoding.RectangularGivens.sweep {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (k remaining : ℕ) :
  k + remaining ≤ M → Matrix (Fin N) (Fin M) ℝ

def QuantumBlockEncoding.RectangularGivens.sweep
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (k remaining : ℕ) :
  k + remaining ≤ M →
    Matrix (Fin N) (Fin M) ℝ

Definition6.24.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sweep steps”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.24.2●1 definition

defdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

def QuantumBlockEncoding.RectangularGivens.sweepSteps {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (k remaining : ℕ) :
  k + remaining ≤ M → List (QuantumBlockEncoding.AdjacentGivens.Step N)

def QuantumBlockEncoding.RectangularGivens.sweepSteps
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (k remaining : ℕ) :
  k + remaining ≤ M →
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N)

Theorem6.24.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sweep steps action”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.3●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.sweepSteps_action {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (k remaining : ℕ)
  (columns : k + remaining ≤ M) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.RectangularGivens.sweepSteps A k remaining
        columns)
      A =
    QuantumBlockEncoding.RectangularGivens.sweep A k remaining columns

theorem QuantumBlockEncoding.RectangularGivens.sweepSteps_action
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (k remaining : ℕ)
  (columns : k + remaining ≤ M) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.RectangularGivens.sweepSteps
        A k remaining columns)
      A =
    QuantumBlockEncoding.RectangularGivens.sweep
      A k remaining columns

Definition6.24.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “upper prefix”. Previously eliminated columns vanish strictly below their diagonal.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. Previously eliminated columns vanish strictly below their diagonal.

Declaration kind. def.

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

Lean code for Definition6.24.4●1 definition

defdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

def QuantumBlockEncoding.RectangularGivens.UpperPrefix {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (k : ℕ) : Prop

def QuantumBlockEncoding.RectangularGivens.UpperPrefix
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (k : ℕ) : Prop

Previously eliminated columns vanish strictly below their diagonal.

Theorem6.24.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep upper prefix”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.5●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.columnSweep_upperPrefix {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (col : Fin M) (h : ↑col < N)
  (fixedPrefix :
    QuantumBlockEncoding.RectangularGivens.UpperPrefix A ↑col) :
  QuantumBlockEncoding.RectangularGivens.UpperPrefix
    (QuantumBlockEncoding.AdjacentGivens.columnSweep A col (↑col)
      (N - 1 - ↑col) ⋯)
    (↑col + 1)

theorem QuantumBlockEncoding.RectangularGivens.columnSweep_upperPrefix
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (col : Fin M) (h : ↑col < N)
  (fixedPrefix :
    QuantumBlockEncoding.RectangularGivens.UpperPrefix
      A ↑col) :
  QuantumBlockEncoding.RectangularGivens.UpperPrefix
    (QuantumBlockEncoding.AdjacentGivens.columnSweep
      A col (↑col) (N - 1 - ↑col) ⋯)
    (↑col + 1)

Theorem6.24.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sweep upper prefix”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.6●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.sweep_upperPrefix {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (k remaining : ℕ)
  (columns : k + remaining ≤ M)
  (fixedPrefix :
    QuantumBlockEncoding.RectangularGivens.UpperPrefix A k) :
  QuantumBlockEncoding.RectangularGivens.UpperPrefix
    (QuantumBlockEncoding.RectangularGivens.sweep A k remaining columns)
    (k + remaining)

theorem QuantumBlockEncoding.RectangularGivens.sweep_upperPrefix
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (k remaining : ℕ)
  (columns : k + remaining ≤ M)
  (fixedPrefix :
    QuantumBlockEncoding.RectangularGivens.UpperPrefix
      A k) :
  QuantumBlockEncoding.RectangularGivens.UpperPrefix
    (QuantumBlockEncoding.RectangularGivens.sweep
      A k remaining columns)
    (k + remaining)

Theorem6.24.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sweep steps length le”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.7●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.sweepSteps_length_le {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (k remaining : ℕ)
  (columns : k + remaining ≤ M) :
  (QuantumBlockEncoding.RectangularGivens.sweepSteps A k remaining
        columns).length ≤
    N * remaining

theorem QuantumBlockEncoding.RectangularGivens.sweepSteps_length_le
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (k remaining : ℕ)
  (columns : k + remaining ≤ M) :
  (QuantumBlockEncoding.RectangularGivens.sweepSteps
        A k remaining columns).length ≤
    N * remaining

Theorem6.24.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “steps matrix orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.8●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.stepsMatrix_orthogonal {N : ℕ}
  (steps : List (QuantumBlockEncoding.AdjacentGivens.Step N)) :
  (QuantumBlockEncoding.AdjacentGivens.stepsMatrix steps).transpose *
      QuantumBlockEncoding.AdjacentGivens.stepsMatrix steps =
    1

theorem QuantumBlockEncoding.RectangularGivens.stepsMatrix_orthogonal
  {N : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N)) :
  (QuantumBlockEncoding.AdjacentGivens.stepsMatrix
          steps).transpose *
      QuantumBlockEncoding.AdjacentGivens.stepsMatrix
        steps =
    1

Theorem6.24.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “steps matrix det”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.9●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.stepsMatrix_det {N : ℕ}
  (steps : List (QuantumBlockEncoding.AdjacentGivens.Step N)) :
  (QuantumBlockEncoding.AdjacentGivens.stepsMatrix steps).det = 1

theorem QuantumBlockEncoding.RectangularGivens.stepsMatrix_det
  {N : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N)) :
  (QuantumBlockEncoding.AdjacentGivens.stepsMatrix
        steps).det =
    1

Definition6.24.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “decompose”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.24.10●1 definition

defdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

def QuantumBlockEncoding.RectangularGivens.decompose {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  List (QuantumBlockEncoding.AdjacentGivens.Step N)

def QuantumBlockEncoding.RectangularGivens.decompose
  {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  List
    (QuantumBlockEncoding.AdjacentGivens.Step
      N)

Definition6.24.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “reduced”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.24.11●1 definition

defdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

def QuantumBlockEncoding.RectangularGivens.reduced {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) : Matrix (Fin N) (Fin M) ℝ

def QuantumBlockEncoding.RectangularGivens.reduced
  {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  Matrix (Fin N) (Fin M) ℝ

Definition6.24.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “transform”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.24.12●1 definition

defdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

def QuantumBlockEncoding.RectangularGivens.transform {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) : Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.RectangularGivens.transform
  {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  Matrix (Fin N) (Fin N) ℝ

Theorem6.24.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “decompose action”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.13●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.decompose_action {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.RectangularGivens.decompose A) A =
    QuantumBlockEncoding.RectangularGivens.reduced A

theorem QuantumBlockEncoding.RectangularGivens.decompose_action
  {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.RectangularGivens.decompose
        A)
      A =
    QuantumBlockEncoding.RectangularGivens.reduced
      A

Theorem6.24.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “transform mul”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.14●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.transform_mul {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  QuantumBlockEncoding.RectangularGivens.transform A * A =
    QuantumBlockEncoding.RectangularGivens.reduced A

theorem QuantumBlockEncoding.RectangularGivens.transform_mul
  {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  QuantumBlockEncoding.RectangularGivens.transform
        A *
      A =
    QuantumBlockEncoding.RectangularGivens.reduced
      A

Theorem6.24.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reduced zero below”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.15●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.reduced_zero_below {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (row : Fin N) (col : Fin M)
  (below : ↑col < ↑row) :
  QuantumBlockEncoding.RectangularGivens.reduced A row col = 0

theorem QuantumBlockEncoding.RectangularGivens.reduced_zero_below
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (row : Fin N) (col : Fin M)
  (below : ↑col < ↑row) :
  QuantumBlockEncoding.RectangularGivens.reduced
      A row col =
    0

Theorem6.24.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “decompose length le”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.16●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.decompose_length_le {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  (QuantumBlockEncoding.RectangularGivens.decompose A).length ≤ N * M

theorem QuantumBlockEncoding.RectangularGivens.decompose_length_le
  {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  (QuantumBlockEncoding.RectangularGivens.decompose
        A).length ≤
    N * M

Theorem6.24.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “transform orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.17●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.transform_orthogonal {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  (QuantumBlockEncoding.RectangularGivens.transform A).transpose *
      QuantumBlockEncoding.RectangularGivens.transform A =
    1

theorem QuantumBlockEncoding.RectangularGivens.transform_orthogonal
  {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  (QuantumBlockEncoding.RectangularGivens.transform
          A).transpose *
      QuantumBlockEncoding.RectangularGivens.transform
        A =
    1

Theorem6.24.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “transform det”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.18●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.transform_det {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  (QuantumBlockEncoding.RectangularGivens.transform A).det = 1

theorem QuantumBlockEncoding.RectangularGivens.transform_det
  {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  (QuantumBlockEncoding.RectangularGivens.transform
        A).det =
    1

Theorem6.24.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exact recovery”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.24.19●1 theorem

theoremdefined in QuantumBlockEncoding/RectangularGivens.lean

complete

theorem QuantumBlockEncoding.RectangularGivens.exact_recovery {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  (QuantumBlockEncoding.RectangularGivens.transform A).transpose *
      QuantumBlockEncoding.RectangularGivens.reduced A =
    A

theorem QuantumBlockEncoding.RectangularGivens.exact_recovery
  {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) :
  (QuantumBlockEncoding.RectangularGivens.transform
          A).transpose *
      QuantumBlockEncoding.RectangularGivens.reduced
        A =
    A