OAI/MeasureTheory/Falconer/Shells/HalfDimensionalShell.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Falconer.halfDimensionalShellConstant line 14
2. theorem OAI.Falconer.halfDimensionalShellConstant_nonneg line 19
3. theorem OAI.Falconer.damped_half_dimensional_shell line 26
4. theorem OAI.Falconer.half_dimensional_shell line 74

   Source documentation

   One frequency shell for a bounded original probability, with no lower-scale ball bounds.

   theorem half_dimensional_shell (μ : Measure (Space d)) [IsProbabilityMeasure μ]
       (ν : Measure (Sphere d)) [IsFiniteMeasure ν]
       {D B R K L : ℝ} (hD : 0 ≤ D) (hsupport : ∀ᵐ x ∂μ, ‖x‖ ≤ D)
       (hB : 1 ≤ B) (hBR : B ≤ R) (hK : 0 ≤ K) (hL : 1 ≤ L) (hmass : ν univ ≤ 1)
       (hμ : ∀ x : Space d, ∀ r : ℝ, 1/B ≤ r →
         μ (ball x r) ≤ ENNReal.ofReal (K*r^((d:ℝ)/2)))
       (hν : ∀ x : Space d, ∀ r : ℝ, 1/R ≤ r → r ≤ 1 →
         ν {w : Sphere d | dist (w:Space d) x < r} ≤ ENNReal.ofReal (L*r^((d:ℝ)/2))) :
       (∫⁻ v, ENNReal.ofReal (‖PlanarFalconer.sourceFourier μ v‖^2) ∂radialFrequencyMeasure ν B) ≤
         ENNReal.ofReal (halfDimensionalShellConstant d*
           (Real.exp ((Real.pi^2/2)*D^2))^2*K*L) := by
   …

   Mentions: OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.PlanarFalconer.sourceFourier, OAI.Falconer.radialFrequencyMeasure, OAI.Falconer.halfDimensionalShellConstant