OAI/Analysis/KadisonKastler/PoissonKernelContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Quantitative translation continuity of the Poisson kernel

  1. theorem OAI.KadisonKastler.realPoissonKernel_eq_cauchyPDFReal line 13
  2. theorem OAI.KadisonKastler.realPoissonKernel_nonneg line 21
  3. theorem OAI.KadisonKastler.integrable_realPoissonKernel line 26
  4. theorem OAI.KadisonKastler.integral_realPoissonKernel line 33
  5. theorem OAI.KadisonKastler.abs_realPoissonKernel_sub_le line 45

    Source documentation

    A pointwise integrable bound for changing the center while keeping positive height fixed.

    theorem abs_realPoissonKernel_sub_le (t u s : ℝ) {r : ℝ} (hr : 0 < r) :
    |realPoissonKernel t r s - realPoissonKernel u r s| ≤
      (|t - u| / r) * (realPoissonKernel t r s + realPoissonKernel u r s) := by
…

    Mentions: OAI.KadisonKastler.realPoissonKernel