RegularPacketCompression.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Finite scalar-packet compressions

Scalar Hilbert coordinates give finite orthogonal projections on the regular Hilbert space. Their compressions converge boundedly in the weak operator topology and have the expected finite packet expansion.

def OAI.KadisonKastler.regularGaugedCoordinates line 27
Source documentation
Scalar coordinates after undoing the gauge in the packet inclusions.
```
def regularGaugedCoordinates : RegularCoreHilbert H ≃ₗᵢ[ℂ] CountableHilbertSum H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.CountableHilbertSum
theorem OAI.KadisonKastler.regularGaugedCoordinates_symm_single line 31
theorem OAI.KadisonKastler.regularGaugedCoordinates_apply line 42
def OAI.KadisonKastler.regularPacketProjection line 55
Source documentation
Projection onto finitely many whole vector-valued scalar packets.
```
def regularPacketProjection (s : Finset ℕ) :
    RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.canonical_partialDiagonal_apply line 60
theorem OAI.KadisonKastler.canonical_partialDiagonal_projection line 69
theorem OAI.KadisonKastler.regularPacketProjection_isStarProjection line 82
theorem OAI.KadisonKastler.norm_regularPacketProjection_le line 87
theorem OAI.KadisonKastler.regularPacketProjection_apply line 91
theorem OAI.KadisonKastler.regularPacketProjection_tendsto line 101
theorem OAI.KadisonKastler.regularPacketCompression_norm_le line 110

theorem OAI.KadisonKastler.regularPacketCompression_tendsto_weak line 122

Source documentation

The finite packet compressions converge weakly, with their original bound.

theorem regularPacketCompression_tendsto_weak
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (f g : RegularCoreHilbert H) :
    Tendsto (fun s : Finset ℕ => inner ℂ g
      ((regularPacketProjection U hU s * T * regularPacketProjection U hU s) f))
      atTop (𝓝 (inner ℂ g (T f))) := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularPacketProjection

theorem OAI.KadisonKastler.regularPacketCompression_apply line 143

Source documentation

A finite compression is the finite matrix of its packet coefficients.

theorem regularPacketCompression_apply
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (s : Finset ℕ) (f : RegularCoreHilbert H) :
    (regularPacketProjection U hU s * T * regularPacketProjection U hU s) f =
      ∑ i ∈ s, ∑ j ∈ s, regularGaugedPacket U hU (regularScalarBasis i)
        (regularPacketCoefficient U hU T (regularScalarBasis i) (regularScalarBasis j)
          ((regularGaugedPacket U hU (regularScalarBasis j)).adjoint f)) := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularPacketProjection, OAI.KadisonKastler.regularGaugedPacket, OAI.KadisonKastler.regularScalarBasis, OAI.KadisonKastler.regularPacketCoefficient