L2FiniteCopies.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Finite Hilbert sums commute with L²

The isometry is the actual finite assembly of coordinate sections. Its pointwise formula is retained for transporting operator matrix actions.

def OAI.KadisonSimilarity.finiteCopyIsometry line 22
Source documentation
Insert a vector into a finite Hilbert coordinate.
```
def finiteCopyIsometry {n : ℕ} (i : Fin n) : H →ₗᵢ[ℂ] HilbertCopies H n where
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.finiteCopyIsometry_apply line 27
def OAI.KadisonSimilarity.l2FiniteAssembly line 31
Source documentation
Assemble a finite tuple of L² sections into one tuple-valued section.
```
def l2FiniteAssembly (n : ℕ) :
    HilbertCopies (Lp H 2 μ) n →L[ℂ] Lp (HilbertCopies H n) 2 μ :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.l2FiniteAssembly_ae line 35
theorem OAI.KadisonSimilarity.l2FiniteAssembly_norm line 50
def OAI.KadisonSimilarity.finiteCopyProjection line 76
def OAI.KadisonSimilarity.l2FiniteCoordinates line 80
Source documentation
The inverse takes the actual pointwise coordinate projections.
```
def l2FiniteCoordinates (n : ℕ) :
    Lp (HilbertCopies H n) 2 μ →L[ℂ] HilbertCopies (Lp H 2 μ) n :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.l2FiniteCoordinates_apply line 85
theorem OAI.KadisonSimilarity.l2FiniteCoordinates_ae line 89
theorem OAI.KadisonSimilarity.l2FiniteAssembly_coordinates line 94
def OAI.KadisonSimilarity.l2FiniteCopiesEquiv line 103
Source documentation
The exact unitary identification of finite L² sums.
```
def l2FiniteCopiesEquiv (n : ℕ) :
    HilbertCopies (Lp H 2 μ) n ≃ₗᵢ[ℂ] Lp (HilbertCopies H n) 2 μ :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.l2FiniteCopiesEquiv_ae line 110