BoundedMatrixOperator.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.FiniteFactor.SourceFiberHilbert line 11
def OAI.FiniteFactor.fiberFiniteEmbedding line 14
Source documentation
Canonical inclusion of finite coordinate vectors in l2(Z).
```
def fiberFiniteEmbedding : (ℤ →₀ ℂ) →ₗ[ℂ] SourceFiberHilbert :=
…
```
Mentions: OAI.FiniteFactor.SourceFiberHilbert
theorem OAI.FiniteFactor.fiberFiniteEmbedding_single line 17
theorem OAI.FiniteFactor.fiberFiniteEmbedding_sum line 21
theorem OAI.FiniteFactor.fiberFiniteEmbedding_norm_sq line 25
theorem OAI.FiniteFactor.fiberFiniteEmbedding_dense line 30
def OAI.FiniteFactor.fiberMatrixLinear line 40
Source documentation
The algebraic action of a matrix on finite vectors.
```
def fiberMatrixLinear (m : ℤ → ℤ → ℂ) : (ℤ →₀ ℂ) →ₗ[ℂ] (ℤ → ℂ) :=
…
```
theorem OAI.FiniteFactor.fiberMatrixLinear_apply line 43

theorem OAI.FiniteFactor.fiberOperator_ext line 49

Source documentation

Every bounded operator is determined by its coordinate matrix.

theorem fiberOperator_ext {A B : SourceFiberHilbert →L[ℂ] SourceFiberHilbert}
    (h : ∀ k n : ℤ, (A (lp.single 2 n (1 : ℂ))) k = (B (lp.single 2 n (1 : ℂ))) k) : A = B := by
…

Mentions: OAI.FiniteFactor.SourceFiberHilbert

theorem OAI.FiniteFactor.fiberOperator_hasSum line 64
theorem OAI.FiniteFactor.fiberOperator_action line 74
theorem OAI.FiniteFactor.fiberMatrixLinear_mem line 88
def OAI.FiniteFactor.fiberMatrixFinite line 94
Source documentation
The finite matrix action takes values in actual l2, by the finite-sum bound.
```
def fiberMatrixFinite : (ℤ →₀ ℂ) →ₗ[ℂ] SourceFiberHilbert where
…
```
Mentions: OAI.FiniteFactor.SourceFiberHilbert
theorem OAI.FiniteFactor.fiberMatrixFinite_norm_le line 99
def OAI.FiniteFactor.boundedMatrixOperator line 115
Source documentation
Extension of the bounded finite matrix action to every l2 vector.
```
def boundedMatrixOperator : SourceFiberHilbert →L[ℂ] SourceFiberHilbert :=
…
```
Mentions: OAI.FiniteFactor.SourceFiberHilbert
theorem OAI.FiniteFactor.boundedMatrixOperator_norm line 118
theorem OAI.FiniteFactor.boundedMatrixOperator_entry line 122