RegularCommutantPackets.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Gauged wave-packet coefficients

Compression between two scalar wave packets turns commutation with the regular copy of P into membership in P'. Translation commutation then gives the exact covariance of these coefficients. These are the operator-valued coefficients used in the regular commutant argument.

def OAI.KadisonKastler.regularGaugedPacket line 26
Source documentation
A scalar wave packet in the regular representation, with its gauge removed.
```
def regularGaugedPacket (φ : Lp ℂ 2 (volume : Measure ℝ)) :
    H →L[ℂ] RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularGaugedPacket_apply_ae line 31
theorem OAI.KadisonKastler.norm_regularGaugedPacket_apply line 38
theorem OAI.KadisonKastler.norm_regularGaugedPacket_le line 45
theorem OAI.KadisonKastler.regularGaugedPacket_intertwines line 52
Source documentation
The packet inclusion intertwines the original and regular actions.
```
theorem regularGaugedPacket_intertwines
    (φ : Lp ℂ 2 (volume : Measure ℝ)) (A : H →L[ℂ] H) :
    (regularCoreEmbedding U hU A).comp (regularGaugedPacket U hU φ) =
      (regularGaugedPacket U hU φ).comp A := by
…
```
Mentions: OAI.KadisonKastler.regularCoreEmbedding, OAI.KadisonKastler.regularGaugedPacket

theorem OAI.KadisonKastler.regularGaugedPacket_adjoint_intertwines line 72

Source documentation

The adjoint packet intertwines in the reverse direction.

theorem regularGaugedPacket_adjoint_intertwines
    (φ : Lp ℂ 2 (volume : Measure ℝ)) (A : H →L[ℂ] H) :
    (regularGaugedPacket U hU φ).adjoint.comp (regularCoreEmbedding U hU A) =
      A.comp (regularGaugedPacket U hU φ).adjoint := by
…

Mentions: OAI.KadisonKastler.regularGaugedPacket, OAI.KadisonKastler.regularCoreEmbedding

def OAI.KadisonKastler.regularPacketCoefficient line 85
Source documentation
An operator coefficient between two wave packets.
```
def regularPacketCoefficient
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (φ ψ : Lp ℂ 2 (volume : Measure ℝ)) : H →L[ℂ] H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.inner_regularPacketCoefficient line 90

theorem OAI.KadisonKastler.regularPacketCoefficient_mem_commutant line 101

Source documentation

Core commutation forces every packet coefficient into the original commutant.

theorem regularPacketCoefficient_mem_commutant (P : VonNeumannAlgebra H)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ A ∈ P, Commute T (regularCoreEmbedding U hU A))
    (φ ψ : Lp ℂ 2 (volume : Measure ℝ)) :
    regularPacketCoefficient U hU T φ ψ ∈ P.commutant := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularCoreEmbedding, OAI.KadisonKastler.regularPacketCoefficient

theorem OAI.KadisonKastler.regularTranslation_gaugedPacket line 129
Source documentation
Translation shifts a scalar packet and acts on its vector by U_s*.
```
theorem regularTranslation_gaugedPacket
    (s : Multiplicative ℝ) (φ : Lp ℂ 2 (volume : Measure ℝ)) :
    (regularRightTranslation (H := H) s :
…
```
Mentions: OAI.KadisonKastler.regularRightTranslation