GaussianEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The all-dimensional Gaussian Fourier energy bound

theorem OAI.Falconer.gaussian_mass_bound_real line 13
theorem OAI.Falconer.gaussian_energy_bound line 24
theorem OAI.Falconer.fourier_gaussian_energy_bound line 42

theorem OAI.Falconer.fourier_ball_energy_bound line 68

Source documentation

A Gaussian majorant of the Fourier energy in a fixed multiple of the frequency ball.

theorem fourier_ball_energy_bound (μ : Measure (Space d)) [IsFiniteMeasure μ]
    {B K s C : ℝ} {k : ℕ} (hB : 0 < B) (hK : 0 ≤ K) (hsk : s ≤ k) (hC : 0 ≤ C)
    (hb : ∀ x : Space d, ∀ r : ℝ, 1/B ≤ r →
      μ (ball x r) ≤ ENNReal.ofReal (K*r^s)) :
    (∫ ξ in ball (0:Space d) (C*B), ‖PlanarFalconer.sourceFourier μ ξ‖^2) ≤
      Real.exp (Real.pi^2*C^2)*(B^2/Real.pi)^((d:ℝ)/2)*
        (μ.real univ*(K*(1/B)^s*gaussianBallConstant k)) := by
…

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