RegularPacketCoefficients.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Covariance and faithfulness of regular packet coefficients

Gauged scalar packets span the whole regular Hilbert space. Consequently their operator coefficients are faithful, and simultaneous translation of the two scalar packets is conjugation of the coefficient by the original unitary group.

theorem OAI.KadisonKastler.regularGaugedPacket_translate line 26
Source documentation
Rewriting the packet translation identity in the forward vector direction.
```
theorem regularGaugedPacket_translate
    (s : Multiplicative ℝ) (φ : Lp ℂ 2 (volume : Measure ℝ)) (ξ : H) :
    regularGaugedPacket U hU (regularTranslateApply s.toAdd φ) ξ =
      (regularRightTranslation (H := H) s :
…
```
Mentions: OAI.KadisonKastler.regularGaugedPacket, OAI.KadisonKastler.regularTranslateApply, OAI.KadisonKastler.regularRightTranslation
theorem OAI.KadisonKastler.regularPacketCoefficient_translate line 43
Source documentation
Translation-invariant operators have covariant original-space coefficients.
```
theorem regularPacketCoefficient_translate
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (s : Multiplicative ℝ)
    (hT : Commute T (regularRightTranslation (H := H) s :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularRightTranslation

theorem OAI.KadisonKastler.regularGaugedPacket_ext line 76

Source documentation

A bounded map is determined by its values on all gauged scalar packets.

theorem regularGaugedPacket_ext
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
    {A B : RegularCoreHilbert H →L[ℂ] F}
    (h : ∀ φ ξ, A (regularGaugedPacket U hU φ ξ) =
      B (regularGaugedPacket U hU φ ξ)) : A = B := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularGaugedPacket

theorem OAI.KadisonKastler.regularPacketCoefficient_faithful line 116
Source documentation
Equality of every packet coefficient implies equality of the operators.
```
theorem regularPacketCoefficient_faithful
    {T S : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (h : ∀ φ ψ, regularPacketCoefficient U hU T φ ψ =
      regularPacketCoefficient U hU S φ ψ) : T = S := by
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularPacketCoefficient