ProjectionBlocks.lean`

46 declarations, 0 contain sorry, 0 declared as axioms

Matrix blocks of a finite orthogonal projection family

The Hilbert--Schmidt quantity below is the explicit sum of squared entry norms rather than an ambient matrix norm instance.

structure OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily line 26
Source documentation
A finite orthogonal decomposition of the identity by Hermitian projections.
```
structure OrthogonalProjectionFamily (P : κ → Matrix ι ι ℂ) : Prop where
…
```
theorem OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily.conjTranspose_eq line 38
theorem OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily.mul_eq_ite line 41
theorem OAI.LeanBlast.GotsmanLinial.sum_projection_blocks line 52
theorem OAI.LeanBlast.GotsmanLinial.projection_block_ext line 57
def OAI.LeanBlast.GotsmanLinial.matrixGrading line 63
Source documentation
The real-valued spectral multiplier defined by the projection family.
```
def matrixGrading (P : κ → Matrix ι ι ℂ) (weight : κ → ℝ) : Matrix ι ι ℂ :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.projection_mul_matrixGrading line 66
theorem OAI.LeanBlast.GotsmanLinial.matrixGrading_mul_projection line 72
theorem OAI.LeanBlast.GotsmanLinial.projection_commutator line 78
theorem OAI.LeanBlast.GotsmanLinial.projection_anticommutator line 94
theorem OAI.LeanBlast.GotsmanLinial.trace_projection_sandwich line 111
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_projection_mul line 115
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_mul_projection line 125
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_left_projection_decomposition line 133
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_right_projection_decomposition line 140
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_block_parseval line 146
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_matrixGrading line 154
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_matrixGrading_trace line 168
theorem OAI.LeanBlast.GotsmanLinial.sum_hsNormSq_blocks_column line 176
theorem OAI.LeanBlast.GotsmanLinial.sum_hsNormSq_blocks_row line 185
theorem OAI.LeanBlast.GotsmanLinial.sum_hsNormSq_blocks_column_trace line 191
theorem OAI.LeanBlast.GotsmanLinial.sum_hsNormSq_blocks_row_trace line 197
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_commutator line 203
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_anticommutator line 210
def OAI.LeanBlast.GotsmanLinial.degreeGrading line 218
Source documentation
The degree grading associated to projections indexed from zero to n.
```
def degreeGrading {n : ℕ} (P : Fin (n + 1) → Matrix ι ι ℂ) : Matrix ι ι ℂ :=
…
```
def OAI.LeanBlast.GotsmanLinial.centeredGrading line 222
Source documentation
The degree grading centered at n / 2.
```
def centeredGrading {n : ℕ} (P : Fin (n + 1) → Matrix ι ι ℂ) : Matrix ι ι ℂ :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_centeredGrading line 225
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_centeredGrading_trace line 231
theorem OAI.LeanBlast.GotsmanLinial.centeredGrading_eq line 237
theorem OAI.LeanBlast.GotsmanLinial.projection_centered_anticommutator line 244
theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_centered_anticommutator line 253
def OAI.LeanBlast.GotsmanLinial.operatorMatrixEquiv line 271
Source documentation
Matrix representation of a continuous operator in an orthonormal basis, bundled with its algebraic compatibility.
```
def operatorMatrixEquiv (b : OrthonormalBasis ι ℂ E) :
    (E →L[ℂ] E) ≃ₐ[ℂ] Matrix ι ι ℂ :=
…
```
def OAI.LeanBlast.GotsmanLinial.operatorMatrix line 278
Source documentation
Matrix entries for the counting orthonormal basis or any chosen orthonormal basis.
```
def operatorMatrix (b : OrthonormalBasis ι ℂ E) (T : E →L[ℂ] E) : Matrix ι ι ℂ :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_eq_toMatrix line 281
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_apply line 284
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_injective line 288
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_zero line 292
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_one line 296
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_add line 300
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_sub line 305
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_mul line 310
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_smul line 315
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_sum line 320
theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_isSelfAdjoint line 324

theorem OAI.LeanBlast.GotsmanLinial.orthogonalProjectionFamily_operatorMatrix line 332

Source documentation

Transfer an actually constructed orthogonal family of Hilbert-space projections to the matrix interface used by the block estimates.

theorem orthogonalProjectionFamily_operatorMatrix (b : OrthonormalBasis ι ℂ E)
    (T : κ → E →L[ℂ] E)
    (hself : ∀ k, IsSelfAdjoint (T k))
    (hidem : ∀ k, T k * T k = T k)
    (horth : ∀ r s, r ≠ s → T r * T s = 0)
    (hsum : ∑ k, T k = 1) :
    OrthogonalProjectionFamily (fun k => operatorMatrix b (T k)) where
…

Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.operatorMatrix

theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_toEuclideanCLM line 349
Source documentation
The standard-basis matrix representation is inverse to the standard Euclidean continuous linear operator associated to a matrix.
```
theorem operatorMatrix_toEuclideanCLM (A : Matrix ι ι ℂ) :
    operatorMatrix (EuclideanSpace.basisFun ι ℂ)
      (Matrix.toEuclideanCLM (n := ι) (𝕜 := ℂ) A) = A :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.operatorMatrix