OAI/Analysis/KadisonKastler/HardyUnitKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Unit Hardy kernels and their Poisson compression

  1. def OAI.KadisonKastler.hardyUnitKernel line 15
  2. theorem OAI.KadisonKastler.hardyUnitKernel_norm line 18
  3. theorem OAI.KadisonKastler.hardyUnitKernel_density line 26
  4. theorem OAI.KadisonKastler.hardyUnitKernel_positive line 36
  5. def OAI.KadisonKastler.hardyKernelInclusion line 43

    Source documentation

    The isometric copy of the coefficient Hilbert space carried by a unit kernel.

    def hardyKernelInclusion (z : ℂ) (hz : 0 < z.re) : H →ₗᵢ[ℂ] RegularCoreHilbert H where
…

    Mentions: OAI.KadisonKastler.RegularCoreHilbert

  6. def OAI.KadisonKastler.hardyKernelCompression line 48
  7. theorem OAI.KadisonKastler.hardyKernelCompression_eq_poisson line 54

    Source documentation

    Compressing a represented multiplication field gives its Poisson average.

    theorem hardyKernelCompression_eq_poisson {z : ℂ} (hz : 0 < z.re)
    (F : ℝ → H →L[ℂ] H)
    (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) volume)
    (C : ℝ) (hC : ∀ᵐ s, ‖F s‖ ≤ C)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : RepresentsOperatorField volume F T) :
    hardyKernelCompression z hz T = measurablePoissonAverage F hF C hC
      (z.im / (2 * Real.pi)) (z.re / (2 * Real.pi)) (div_pos hz (by positivity)) := by
…

    Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.hardyKernelCompression, OAI.KadisonKastler.measurablePoissonAverage