RegularLocalizedPackets.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Localization of finite packet matrices

Cutting off a packet cuts off its scalar coefficient. The localized average of each packet matrix is consequently a product of the actual convolution generators, not an assumed measurable operator integral.

def OAI.KadisonKastler.regularSandwichLinear line 23

def OAI.KadisonKastler.regularLocalizationAverageLinear line 40

Source documentation

Linearity in the operator being localized and averaged.

def regularLocalizationAverageLinear
    (s : Set ℝ) (hs : MeasurableSet s) (hfinite : volume s ≠ ⊤) :
    (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) →ₗ[ℂ]
      (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :=
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert

theorem OAI.KadisonKastler.integrable_regularIndicatorPacket line 47
theorem OAI.KadisonKastler.regularIndicatorProjection_gaugedPacket line 59
theorem OAI.KadisonKastler.regularGaugedPacket_adjoint_indicator line 74
def OAI.KadisonKastler.regularPacketOperator line 91
Source documentation
A rank-one scalar packet matrix with an arbitrary bounded vector coefficient.
```
def regularPacketOperator
    (φ ψ : Lp ℂ 2 (volume : Measure ℝ)) (A : H →L[ℂ] H) :
    RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularLocalizationAverage_packetOperator line 96
theorem OAI.KadisonKastler.regularLocalizationAverage_packetOperator_mem line 118

theorem OAI.KadisonKastler.regularLocalizationAverage_compression_mem line 128

Source documentation

Every finite compression has its localized average in the candidate commutant.

theorem regularLocalizationAverage_compression_mem
    (P : VonNeumannAlgebra H)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ A ∈ P, Commute T (regularCoreEmbedding U hU A))
    (s : Set ℝ) (hs : MeasurableSet s) (hfinite : volume s ≠ ⊤)
    (d : Finset ℕ) :
    regularLocalizationAverage s hs hfinite
      (regularPacketProjection U hU d * T * regularPacketProjection U hU d) ∈
      regularCommutantAlgebra U P := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularCoreEmbedding, OAI.KadisonKastler.regularLocalizationAverage, OAI.KadisonKastler.regularPacketProjection, OAI.KadisonKastler.regularCommutantAlgebra

theorem OAI.KadisonKastler.regularLocalizationAverage_mem line 157

Source documentation

Bounded weak convergence removes the finite packet compression.

theorem regularLocalizationAverage_mem
    (P : VonNeumannAlgebra H)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ A ∈ P, Commute T (regularCoreEmbedding U hU A))
    (s : Set ℝ) (hs : MeasurableSet s) (hfinite : volume s ≠ ⊤) :
    regularLocalizationAverage s hs hfinite T ∈ regularCommutantAlgebra U P := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularCoreEmbedding, OAI.KadisonKastler.regularLocalizationAverage, OAI.KadisonKastler.regularCommutantAlgebra