OAI/Analysis/KadisonKastler/PositiveFrequencyAlgebra.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.positiveFrequencyAlgebra line 17

   Source documentation

   Decomposable operators preserving the actual positive-frequency cut. Commutation with characters is included so the published causal multiplier theorem applies after Fourier conjugation.

   def positiveFrequencyAlgebra : Subalgebra ℂ
       (RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) where
   …

   Mentions: OAI.KadisonKastler.RegularCoreHilbert

2. theorem OAI.KadisonKastler.regularFieldOperator_mem_positiveFrequencyAlgebra line 58

   Source documentation

   A nest-preserving represented field is an element of the concrete positive-frequency multiplier algebra.

   theorem regularFieldOperator_mem_positiveFrequencyAlgebra
       (F : ℝ → H →L[ℂ] H)
       (hF : ∀ x, MeasureTheory.AEStronglyMeasurable (fun t => F t x) MeasureTheory.volume)
       (C : ℝ) (hC : ∀ᵐ t ∂MeasureTheory.volume, ‖F t‖ ≤ C)
       (hpres : PreservesProjectionNest regularFrequencyNest
         (regularFieldOperator MeasureTheory.volume F hF C hC)) :
       regularFieldOperator MeasureTheory.volume F hF C hC ∈
         positiveFrequencyAlgebra (H := H) := by
   …

   Mentions: OAI.KadisonKastler.PreservesProjectionNest, OAI.KadisonKastler.regularFrequencyNest, OAI.KadisonKastler.regularFieldOperator, OAI.KadisonKastler.positiveFrequencyAlgebra