HomogeneousRadialSmoothL2.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Smooth radial channels of homogeneous-space vectors

Exterior ODE regularity supplies smoothness. The completed Fourier norm then forces the classical top radial derivative to lie in L²(r¹¹dr), excluding the nonintegrable fast asymptotic coefficient.

theorem OAI.DefocusingNLS.hasDerivAt_iteratedDeriv_on_open line 18

theorem OAI.DefocusingNLS.homogeneousAngularProjection_iteratedDeriv_integrable line 29

Source documentation

Smoothness only on the exterior suffices for the exact weighted L² bound.

theorem homogeneousAngularProjection_iteratedDeriv_integrable
    (a : ℝ) (N : ℕ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ))
    (h : PhysicalUnitSphere → ℂ) (hh : MemLp h 2 physicalSphereMeasure)
    (u : HomogeneousY a N) (R : ℝ) (hR : 0 ≤ R)
    (hsmooth : ContDiffOn ℝ ∞ (homogeneousAngularProjection a N ha ha1 hk h u) (Ioi R)) :
    IntegrableOn (fun r : ℝ => r ^ (11 : ℕ) *
      ‖iteratedDeriv N (homogeneousAngularProjection a N ha ha1 hk h u) r‖ ^ 2) (Ioi R) := by
…

Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousAngularProjection

theorem OAI.DefocusingNLS.homogeneousAngularProjection_fast_coefficient_zero line 45

Source documentation

A fast-mode asymptotic at or above the radial L² threshold must have zero coefficient for a genuine homogeneous-space vector.

theorem homogeneousAngularProjection_fast_coefficient_zero
    (a : ℝ) (N : ℕ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ))
    (h : PhysicalUnitSphere → ℂ) (hh : MemLp h 2 physicalSphereMeasure)
    (u : HomogeneousY a N) (R : ℝ) (hR : 0 ≤ R)
    (hsmooth : ContDiffOn ℝ ∞ (homogeneousAngularProjection a N ha ha1 hk h u) (Ioi R))
    (β c : ℝ) (hβ : -6 ≤ β) (hc : 0 ≤ c)
    (hlim : Tendsto (fun r =>
      ‖iteratedDeriv N (homogeneousAngularProjection a N ha ha1 hk h u) r‖ / r ^ β)
      atTop (𝓝 c)) : c = 0 :=
…

Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousAngularProjection