OAI/Analysis/KadisonKastler/HardyReproducingKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The concrete Hardy reproducing vectors

The inverse Fourier transform of a one-sided exponential belongs to the positive-frequency space. Its normalization is computed, not assumed.

  1. def OAI.KadisonKastler.hardyFrequencyKernel line 20
  2. def OAI.KadisonKastler.hardyReproducingKernel line 23
  3. theorem OAI.KadisonKastler.hardyFrequencyKernel_norm_sq line 26
  4. theorem OAI.KadisonKastler.hardyReproducingKernel_norm_sq line 52
  5. theorem OAI.KadisonKastler.hardyReproducingKernel_positive line 57