OAI/MeasureTheory/Falconer/Slicing/GaussianDamping.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Damping a finite source measure and recovering its Fourier transform

  1. def OAI.Falconer.gaussianDampedMeasure line 12
  2. theorem OAI.Falconer.gaussianDampedMeasure_le line 15
  3. instance OAI.Falconer.gaussianDampedMeasure_finite line 26
  4. theorem OAI.Falconer.sourceFourier_gaussianDampedMeasure line 30
  5. theorem OAI.Falconer.gaussian_convolution_damped line 41

    Source documentation

    Exact convolution formula, before the Cauchy--Schwarz bound.

    theorem gaussian_convolution_damped (β : Measure (Space d)) [IsFiniteMeasure β]
    (v : Space d) :
    (∫ u : Space d, (Real.exp (-2*‖u-v‖^2):ℂ)*PlanarFalconer.sourceFourier β u) =
      (((Real.pi/2:ℝ)^((d:ℝ)/2):ℝ):ℂ)*
        PlanarFalconer.sourceFourier (gaussianDampedMeasure β) v := by
…

    Mentions: OAI.Falconer.Space, OAI.PlanarFalconer.sourceFourier, OAI.Falconer.gaussianDampedMeasure