RealNestMultiplier.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Real character averaging of a bounded multiplier

The real group is made discrete only for its invariant mean. Its unitary representation is the actual character multiplication on L²(real,H).

theorem OAI.KadisonKastler.regularFieldOperator_commutes_character line 22

theorem OAI.KadisonKastler.exists_real_nest_multiplier line 49

Source documentation

All mean and character-representation data are constructed here. The only approximation hypotheses are the actual nest defect and the published nest and diagonal decomposition theorems.

theorem exists_real_nest_multiplier
    [TopologicalSpace.SeparableSpace H]
    (hNest : PublishedRealNestDistance.{u})
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (P : ℝ → RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hP : ∀ a, IsStarProjection (P a))
    (hmono : ∀ a b, a ≤ b → P a * P b = P a)
    (hperm : ∀ a b : ℝ, ∃ c, P a = unitaryConj (regularCharacterUnitary b) (P c))
    (F : ℝ → H →L[ℂ] H) (hF : ∀ x, AEStronglyMeasurable (fun t => F t x) volume)
    {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ᵐ t, ‖F t‖ ≤ C)
    {δ : ℝ} (hδ : 0 < δ)
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCharacterUnitary