OAI/Analysis/KadisonKastler/HardyKernelVectors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Reproducing-kernel vectors and their character tests

  1. theorem OAI.KadisonKastler.regularFrequencyProjection_zero_tensor line 17
  2. theorem OAI.KadisonKastler.regularCharacter_tensor line 31
  3. theorem OAI.KadisonKastler.hardyKernelInclusion_positive line 45
  4. theorem OAI.KadisonKastler.hardyUnitKernel_backward_shift line 52
  5. theorem OAI.KadisonKastler.hardyKernelInclusion_backward_shift line 63
  6. theorem OAI.KadisonKastler.hardyKernelInclusion_adjoint_self line 78
  7. theorem OAI.KadisonKastler.hardyUnitKernel_ne_zero_ae line 89
  8. theorem OAI.KadisonKastler.hardyKernelInclusion_ext line 100

    Source documentation

    Character-kernel vectors determine continuous operators on the regular space.

    theorem hardyKernelInclusion_ext (z : ℂ) (hz : 0 < z.re)
    {A B : RegularCoreHilbert H →L[ℂ] H}
    (he : ∀ s : ℝ, ∀ x : H,
      A ((regularCharacterUnitary (H := H) (2 * Real.pi * s) :
…

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