OrthogonalColumns.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite orthogonal word levels and their full-codomain errors.

def OAI.KadisonSimilarity.sumColumns line 17
Source documentation
Assemble maps from the individual coordinates of a finite Hilbert sum.
```
def sumColumns {N : ℕ} (U : Fin N → H →L[ℂ] K) : HilbertCopies H N →L[ℂ] K :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.sumColumns_apply line 20

theorem OAI.KadisonSimilarity.norm_sum_sq_of_pairwise_orthogonal line 25

Source documentation

Pythagoras for the finite family of orthogonal output vectors.

theorem norm_sum_sq_of_pairwise_orthogonal {N : ℕ} (v : Fin N → K)
    (horth : ∀ i j, i ≠ j → inner ℂ (v i) (v j) = 0) :
    ‖∑ i : Fin N, v i‖ ^ 2 = ∑ i : Fin N, ‖v i‖ ^ 2 := by
…

theorem OAI.KadisonSimilarity.norm_sumColumns_le line 36

Source documentation

Orthogonal output levels allow the same bound at every matrix size.

theorem norm_sumColumns_le {N : ℕ} (U : Fin N → H →L[ℂ] K) {c : ℝ}
    (hc : 0 ≤ c) (hU : ∀ i, ‖U i‖ ≤ c)
    (horth : ∀ i j, i ≠ j → ∀ x y, inner ℂ (U i x) (U j y) = 0) :
    ‖sumColumns U‖ ≤ c := by
…

Mentions: OAI.KadisonSimilarity.sumColumns

theorem OAI.KadisonSimilarity.sumColumns_adjoint_apply line 56
theorem OAI.KadisonSimilarity.sumColumns_compression line 79
Source documentation
The block entries of the compressed operator are its coordinatewise compressions along the word-level inclusions.
```
theorem sumColumns_compression {N : ℕ} (U : Fin N → H →L[ℂ] K) (T : K →L[ℂ] K) :
    (sumColumns U).adjoint.comp (T.comp (sumColumns U)) =
      matrixOperator (fun i j => (U i).adjoint.comp (T.comp (U j))) := by
…
```
Mentions: OAI.KadisonSimilarity.sumColumns, OAI.KadisonSimilarity.matrixOperator

theorem OAI.KadisonSimilarity.sumColumns_intertwining_error line 88

Source documentation

The full error of an assembled inclusion is the assembly of its level errors.

theorem sumColumns_intertwining_error {N : ℕ} (U : Fin N → H →L[ℂ] K)
    (G : K →L[ℂ] K) (B : H →L[ℂ] H) :
    G.comp (sumColumns U) - (sumColumns U).comp (amplify B N) =
      sumColumns (fun i => G.comp (U i) - (U i).comp B) := by
…

Mentions: OAI.KadisonSimilarity.sumColumns, OAI.KadisonSimilarity.amplify

theorem OAI.KadisonSimilarity.adjoint_amplify line 96
Source documentation
Adjoint and finite Hilbert amplification commute.
```
theorem adjoint_amplify (B : H →L[ℂ] H) (N : ℕ) :
    (amplify B N).adjoint = amplify B.adjoint N := by
…
```
Mentions: OAI.KadisonSimilarity.amplify

theorem OAI.KadisonSimilarity.norm_word_inclusion_error_le line 107

Source documentation

The propagation estimate on individual orthogonal word levels gives a full-codomain norm bound on their assembled inclusion.

theorem norm_word_inclusion_error_le {N : ℕ}
    (U : Fin N → H →L[ℂ] K) (L : Fin N → Submodule ℂ K)
    (hU : ∀ i x, U i x ∈ L i)
    (horth : ∀ i j, i ≠ j → ∀ x ∈ L i, ∀ y ∈ L j, inner ℂ x y = 0)
    (G : K →L[ℂ] K) (B : H →L[ℂ] H)
    (hG : ∀ i x, x ∈ L i → G x ∈ L i)
    {η : ℝ} (hη : 0 ≤ η)
    (herr : ∀ i, ‖G.comp (U i) - (U i).comp B‖ ≤ η) :
    ‖G.comp (sumColumns U) - (sumColumns U).comp (amplify B N)‖ ≤ η := by
…

Mentions: OAI.KadisonSimilarity.sumColumns, OAI.KadisonSimilarity.amplify