HomogeneousRadialIdentification.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Identification of the classical exterior radial derivative

Local smooth jets are identified with the completed radial L² derivative by test functions. No smoothness through the origin or interface is required.

theorem OAI.DefocusingNLS.compact_test_integrable line 19

theorem OAI.DefocusingNLS.positiveRadiusExtension_eq_of_local_testing line 30

Source documentation

Local test equality suffices to identify a classical representative of the completed radial function on an exterior interval.

theorem positiveRadiusExtension_eq_of_local_testing
    (g : PhysicalPositiveRadius → ℂ) (hg : MemLp g 2 physicalRadiusMeasure)
    (R : ℝ) (hR : 0 ≤ R) (F : ℝ → ℂ) (hF : ContinuousOn F (Ioi R))
    (htest : ∀ ψ : 𝓢(ℝ, ℂ), HasCompactSupport ψ → tsupport ψ ⊆ Ioi R →
      (∫ r, ψ r * ((r : ℂ) ^ (11 : ℕ) * positiveRadiusExtension g r)) =
        ∫ r, ψ r * ((r : ℂ) ^ (11 : ℕ) * F r)) :
    ∀ᵐ r ∂volume, r ∈ Ioi R → positiveRadiusExtension g r = F r := by
…

Mentions: OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalRadiusMeasure, OAI.DefocusingNLS.positiveRadiusExtension

theorem OAI.DefocusingNLS.radialTransposedTest_eq line 73

theorem OAI.DefocusingNLS.homogeneousRadialAngularDerivative_eq_classical line 80

Source documentation

The classical Nth radial jet on a smooth exterior interval agrees almost everywhere with the exact contraction of the completed Cartesian derivatives.

theorem homogeneousRadialAngularDerivative_eq_classical
    (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) (F : ℕ → ℝ → ℂ)
    (hF : ∀ j r, r ∈ Ioi R → HasDerivAt (F j) (F (j + 1) r) r)
    (hF0 : F 0 = homogeneousAngularProjection a N ha ha1 hk h u) :
    ∀ᵐ r ∂volume, r ∈ Ioi R →
      positiveRadiusExtension (homogeneousRadialAngularDerivative a N ha ha1 hk h u) r =
        F N r := by
…

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

theorem OAI.DefocusingNLS.homogeneousRadial_classical_weighted_square line 128

Source documentation

The classical exterior Nth radial derivative has the weighted L² integrability required to exclude a nonzero fast outgoing component.

theorem homogeneousRadial_classical_weighted_square
    (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) (F : ℕ → ℝ → ℂ)
    (hF : ∀ j r, r ∈ Ioi R → HasDerivAt (F j) (F (j + 1) r) r)
    (hF0 : F 0 = homogeneousAngularProjection a N ha ha1 hk h u) :
    IntegrableOn (fun r : ℝ => r ^ (11 : ℕ) * ‖F N r‖ ^ 2) (Ioi R) :=
…

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