OAI/Analysis/KadisonKastler/HardyKernelRow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.hardyKernelRow line 16
2. theorem OAI.KadisonKastler.hardyKernelRow_inclusion line 19
3. theorem OAI.KadisonKastler.hardyKernelRow_projection line 23
4. theorem OAI.KadisonKastler.regularCharacter_adjoint_neg line 39
5. theorem OAI.KadisonKastler.hardyKernelRow_forward line 51

   Source documentation

   Positive character shifts have the expected scalar action under evaluation.

   theorem hardyKernelRow_forward (z : ℂ) (hz : 0 < z.re) {b : ℝ} (hb : 0 ≤ b)
       (f : RegularCoreHilbert H) (hf : regularFrequencyProjection 0 f = f) :
       hardyKernelRow z hz ((regularCharacterUnitary (H := H) (2 * Real.pi * b) :
   …

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