QuadraticIntegral.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual sphere integral in fixed quadratic coordinates

The only measure input is the already recorded gnomonic surface formula. The quadratic coordinate Jacobian is proved locally. Its product with the gnomonic density is exactly the manuscript's (1-‖u‖²/4)^((n-2)/2).

theorem OAI.Falconer.quadratic_gnomonic_density line 17
theorem OAI.Falconer.quadratic_jacobian_density line 39

theorem OAI.Falconer.quadratic_sphere_integral line 52

Source documentation

A function supported in this fixed north-pole chart has exactly the quadratic-coordinate integral, including its surface Jacobian.

theorem quadratic_sphere_integral (hpublished : PublishedGnomonicSurface)
    (m : ℕ) (f : Sphere (m+3) → ℂ) (hf : Measurable f)
    (hs : ∀ w, w ∉ northHemisphere (m+2) → f w = 0)
    (hchart : ∀ x : Space (m+2),
      x ∉ quadraticToGnomonic '' Metric.ball (0 : Space (m+2)) 1 →
        f (gnomonicChart x) = 0) :
    (∫ w, f w ∂sphereMeasure (m+3)) =
      ∫ u in Metric.ball (0 : Space (m+2)) 1,
        (Real.sqrt (1-‖u‖^2/4))^m • f (gnomonicChart (quadraticToGnomonic u)) := by
…

Mentions: OAI.Falconer.PublishedGnomonicSurface, OAI.Falconer.Sphere, OAI.Falconer.northHemisphere, OAI.Falconer.Space, OAI.Falconer.quadraticToGnomonic, OAI.Falconer.gnomonicChart, OAI.Falconer.sphereMeasure

theorem OAI.Falconer.quadratic_sphere_oscillatory_integral line 81

Source documentation

The north-pole phase is exactly a constant phase times the negative quadratic phase. This is the local integral to which quadratic stationary phase will be applied.

theorem quadratic_sphere_oscillatory_integral (hpublished : PublishedGnomonicSurface)
    (m : ℕ) (Λ : ℝ) (b : Sphere (m+3) → ℂ) (hb : Measurable b)
    (hs : ∀ w, w ∉ northHemisphere (m+2) → b w = 0)
    (hchart : ∀ x : Space (m+2),
      x ∉ quadraticToGnomonic '' Metric.ball (0 : Space (m+2)) 1 →
        b (gnomonicChart x) = 0) :
    (∫ w : Sphere (m+3),
      Complex.exp (Complex.I*(Λ : ℂ)*
        (inner ℝ (w : Space (m+3)) (coordinateJoin (0 : Space (m+2)) 1) : ℂ)) * b w
      ∂sphereMeasure (m+3)) =
    Complex.exp (Complex.I*(Λ : ℂ)) *
      ∫ u in Metric.ball (0 : Space (m+2)) 1,
…