CauchyCharacter.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The characteristic function of the Cauchy density

The frequency is expressed in radians, matching the characters used by the modular comparison. Fourier inversion accounts for the 2*pi change from mathlib's Fourier convention.

theorem OAI.KadisonKastler.laplaceKernel_rescale line 19

theorem OAI.KadisonKastler.integral_cauchyPDFReal_character_zero line 30

Source documentation

The centered Cauchy characteristic function in the radian convention.

theorem integral_cauchyPDFReal_character_zero {γ : NNReal} (hγ : 0 < γ) (s : ℝ) :
    (∫ x : ℝ, (cauchyPDFReal 0 γ x : ℂ) * (Circle.exp (s * x) : ℂ)) =
      (Real.exp (-(γ : ℝ) * |s|) : ℂ) := by
…

theorem OAI.KadisonKastler.integral_cauchyPDFReal_character line 48

Source documentation

Translation of the density gives the phase factor for an arbitrary center.

theorem integral_cauchyPDFReal_character {γ : NNReal} (hγ : 0 < γ) (t s : ℝ) :
    (∫ x : ℝ, (cauchyPDFReal t γ x : ℂ) * (Circle.exp (s * x) : ℂ)) =
      (Real.exp (-(γ : ℝ) * |s|) : ℂ) * (Circle.exp (s * t) : ℂ) := by
…