OAI/MeasureTheory/Falconer/Fourier/AllDimensionalSpatialFourierIntegration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Falconer.spatialPairPhase line 12
2. theorem OAI.Falconer.spatialPairPhase_continuous line 15
3. theorem OAI.Falconer.spatialPairPhase_norm line 20
4. theorem OAI.Falconer.spatialFourier_joint_integrable line 24
5. theorem OAI.Falconer.spatialFourier_integral_swap line 42
6. theorem OAI.Falconer.spatialInverseDistance_integral_separation line 66

   Source documentation

   The spatial factor needed after a stationary inverse term, separated into bounded multipliers of the two original endpoints.

   theorem spatialInverseDistance_integral_separation
       (δ L : ℝ) (hδ : 0 < δ) (hL : 0 < L) (j : ℕ) {s : ℝ} (hs : 0 < s)
       (μ : Measure (Space d × Space d)) [IsFiniteMeasure μ]
       (hsep : ∀ᵐ z ∂μ, δ ≤ dist z.1 z.2 / s ∧ dist z.1 z.2 / s ≤ L)
       (A : Space d × Space d → ℂ) (hA : Measurable A) {C : ℝ}
       (hb : ∀ z, ‖A z‖ ≤ C) :
       (∫ z, (↑((dist z.1 z.2 / s)^j)⁻¹ : ℂ) * A z ∂μ) =
         ∫ ξ, spatialFourierCoeff (d := d) δ L hδ hL j ξ *
   …

   Mentions: OAI.Falconer.Space, OAI.Falconer.spatialFourierCoeff