OAI/MeasureTheory/Falconer/Radial/RadialLocalization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Radial localization for the actual shell measure

The normalized radial shell integral is exactly the Fourier transform of its fixed Schwartz cutoff. This identifies the oscillatory kernel in the longitudinal discarded terms and gives arbitrary power decay, including after integration against finite spatial and angular laws.

  1. theorem OAI.Falconer.radial_shell_oscillator_fourier line 19
  2. theorem OAI.Falconer.radial_shell_arbitrary_decay line 44
  3. theorem OAI.Falconer.radial_discarded_term_bound_uniform line 64

    Source documentation

    Integrating a discarded term loses only its amplitude bound and the finite mass of the remaining variables. The phase gap is required only where the amplitude is nonzero.

    theorem radial_discarded_term_bound_uniform {X : Type*} [MeasurableSpace X]
    (Ο† : 𝓒(ℝ, β„‚)) (Ξ¨ : ℝ β†’ ℝ)
    (hΟ† : βˆ€ u, Ο† u = (Ξ¨ u : β„‚)) (hΞ¨ : Measurable Ξ¨)
    (hpos : βˆ€ u, 0 ≀ Ξ¨ u) (hzero : βˆ€ u ≀ 0, Ξ¨ u = 0)
    {Ξ± : ℝ} (hΞ± : 0 < Ξ±) (T : ℝ) :
    βˆƒ C : ℝ, 0 < C ∧ βˆ€ (ΞΌ : Measure X) [IsFiniteMeasure ΞΌ], βˆ€ R : ℝ, 1 ≀ R β†’ βˆ€ v : ℝ,
      βˆ€ (A : X β†’ β„‚) (s : X β†’ ℝ) (B : ℝ), 0 ≀ B β†’
      (βˆ€ x, β€–A xβ€– ≀ B) β†’
      (βˆ€ x, A x β‰  0 β†’ 2*Real.pi*R^Ξ± ≀ (2 : ℝ)^v*|s x|) β†’
      β€–βˆ« x, ∫ r, A x * Complex.exp (Complex.I * (r*s x : ℝ))
        βˆ‚PlanarFalconer.sourceAngularShellMeasure v Ξ¨ βˆ‚ΞΌβ€– ≀
        (B*C*ΞΌ.real Set.univ)*R^(-T) := by
…

    Mentions: OAI.PlanarFalconer.sourceAngularShellMeasure

  4. theorem OAI.Falconer.radial_discarded_term_bound line 92