RegularLocalizationReconstruction.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Reconstruction from localized Haar averages

Finite packet averages belong to the explicit commutant algebra. The normalized interval limit recovers every operator commuting with the regular core, and hence proves the published commutant formula.

theorem OAI.KadisonKastler.complex_normalization_identity line 19
theorem OAI.KadisonKastler.regularNormalizedIntervalAverage_tendsto_supported line 31
theorem OAI.KadisonKastler.regularIndicatorProjection_larger line 70
theorem OAI.KadisonKastler.regularNormalizedIntervalAverage_tendsto_weak line 82
Source documentation
Normalized interval localization converges weakly on all regular vectors.
```
theorem regularNormalizedIntervalAverage_tendsto_weak
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ r : ℝ, Commute T (regularRightTranslation (H := H) (Multiplicative.ofAdd r) :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularRightTranslation

theorem OAI.KadisonKastler.regularLocalizationReconstruction_mem line 109

Source documentation

The explicit convolution algebra contains every core-commuting operator.

theorem regularLocalizationReconstruction_mem
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H))
    (hU : ∀ ξ, Continuous (fun t : ℝ => (U (Multiplicative.ofAdd t) : H →L[ℂ] H) ξ))
    (P : VonNeumannAlgebra H)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hπ : ∀ a ∈ P, Commute T (regularCoreEmbedding U hU a))
    (hρ : ∀ r : ℝ, Commute T (regularRightTranslation (H := H) (Multiplicative.ofAdd r) :
…

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

theorem OAI.KadisonKastler.publishedRegularCommutant line 132
Source documentation
The regular commutant identity follows from packet localization.
```
theorem publishedRegularCommutant : PublishedRegularCommutant.{u} := by
…
```