OAI/Analysis/ModularTheory/LpRepresentation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The pointwise operator representation, and its modular gauge conjugate, on the Hilbert space of square-integrable vector-valued functions. This supplies the coefficient representation for the continuous core.

  1. lemma OAI.WeakPureInfiniteness.pointwiseLp_star line 18
  2. def OAI.WeakPureInfiniteness.pointwiseLpRepresentation line 29
  3. def OAI.WeakPureInfiniteness.modularLpRepresentation line 67

    Source documentation

    The actual modularly twisted coefficient representation.

    def modularLpRepresentation (D : BoundedRecovery.RealSpectralCalculus H) :
    (H →L[ℂ] H) →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ) :=
…

    Mentions: OAI.BoundedRecovery.RealSpectralCalculus

  4. lemma OAI.WeakPureInfiniteness.modularLpRepresentation_ae line 72