OAI/Analysis/ModularTheory/LpGauge.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The measurable unitary gauge on the Hilbert space used for the modular crossed product. This constructs the actual change of representation, not a semifiniteness or nuclearity assumption.

  1. lemma OAI.BoundedRecovery.RealSpectralCalculus.continuous_unitary_action line 17
  2. lemma OAI.BoundedRecovery.RealSpectralCalculus.aestronglyMeasurable_unitary_gauge line 37
  3. lemma OAI.BoundedRecovery.RealSpectralCalculus.memLp_unitary_gauge line 45
  4. def OAI.BoundedRecovery.RealSpectralCalculus.lpGauge line 51
  5. lemma OAI.BoundedRecovery.RealSpectralCalculus.lpGauge_ae line 54
  6. lemma OAI.BoundedRecovery.RealSpectralCalculus.lpGauge_norm line 58
  7. lemma OAI.BoundedRecovery.RealSpectralCalculus.lpGauge_add line 64
  8. lemma OAI.BoundedRecovery.RealSpectralCalculus.lpGauge_smul line 72
  9. lemma OAI.BoundedRecovery.RealSpectralCalculus.lpGauge_comp line 79
  10. lemma OAI.BoundedRecovery.RealSpectralCalculus.lpGauge_zero line 86
  11. def OAI.BoundedRecovery.RealSpectralCalculus.lpGaugeEquiv line 92

    Source documentation

    A genuine Hilbert-space unitary, with inverse given by the opposite gauge.

    def lpGaugeEquiv (c : ℝ) : Lp H 2 μ ≃ₗᵢ[ℂ] Lp H 2 μ where
…
  12. lemma OAI.BoundedRecovery.RealSpectralCalculus.lpGaugeEquiv_apply line 101
  13. lemma OAI.BoundedRecovery.RealSpectralCalculus.lpGauge_conjugate_constant_ae line 106

    Source documentation

    Conjugating a constant operator gives the modularly twisted measurable operator field. The formula is an almost-everywhere equality on actual L².

    lemma lpGauge_conjugate_constant_ae (c : ℝ) (T : H →L[ℂ] H) (f : Lp H 2 μ) :
    D.lpGauge μ c (T.compLpL 2 μ (D.lpGauge μ (-c) f)) =ᵐ[μ]
      fun t => D.unitary (c * t) (T (D.unitary (-(c * t)) (f t))) := by
…