OAI/Analysis/LipschitzHilbert/Fourier/FourierAveragingTail.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative tails of the averaging kernel

The Fourier-square kernel has a finite second moment, proved directly from its Schwartz seminorms. This gives the polynomial tail estimate used in the near-uniform interval convolution, with a constant from a fixed kernel.

  1. theorem OAI.LipschitzHilbert.fourierSquare_second_moment_integrable line 20
  2. theorem OAI.LipschitzHilbert.fourierAveraging_second_moment_integrable line 34
  3. theorem OAI.LipschitzHilbert.fourierAveraging_second_moment_nonneg line 47
  4. theorem OAI.LipschitzHilbert.probability_central_mass_of_second_moment line 52

    Source documentation

    The tail outside a central interval is controlled by the second moment.

    theorem probability_central_mass_of_second_moment (μ : Measure ℝ)
    [IsProbabilityMeasure μ] (hint : Integrable (fun t : ℝ => t ^ 2) μ)
    {R : ℝ} (hR : 0 < R) :
    1 - (∫ t : ℝ, t ^ 2 ∂μ) / R ^ 2 ≤ μ.real (Set.Icc (-R) R) := by
…
  5. theorem OAI.LipschitzHilbert.fourierGap_map_dilation line 82

    Source documentation

    Dilation changes the Fourier gap by the reciprocal physical scale.

    theorem fourierGap_map_dilation (μ : Measure ℝ) [IsFiniteMeasure μ]
    {gap scale : ℝ} (hscale : 0 < scale) (hgap : PhaseCombinatorics.FourierGap μ gap) :
    PhaseCombinatorics.FourierGap (μ.map (fun t => scale * t)) (gap / scale) := by
…

    Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.FourierGap

  6. theorem OAI.LipschitzHilbert.second_moment_map_dilation line 101