OAI/Analysis/KadisonKastler/PoissonCharacter.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual Poisson averages of scalar characters

  1. theorem OAI.KadisonKastler.integral_realPoissonKernel_character line 14
  2. def OAI.KadisonKastler.poissonCharacterField line 24

    Source documentation

    Scalar characters, regarded as a concrete field of operators.

    def poissonCharacterField (s t : ℝ) : H →L[ℂ] H := (Circle.exp (s * t) : ℂ) • 1
…
  3. theorem OAI.KadisonKastler.poissonCharacterField_measurable line 27
  4. theorem OAI.KadisonKastler.norm_poissonCharacterField_le line 34
  5. theorem OAI.KadisonKastler.measurablePoissonAverage_character line 40

    Source documentation

    The explicit Cauchy character formula for the vector-defined Poisson average, with the same field and integral used by analytic smoothing.

    theorem measurablePoissonAverage_character (s t : ℝ) {r : ℝ} (hr : 0 < r) :
    measurablePoissonAverage (poissonCharacterField (H := H) s)
…

    Mentions: OAI.KadisonKastler.measurablePoissonAverage, OAI.KadisonKastler.poissonCharacterField