HomogeneousRadialWeakTesting.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact radial weak derivatives of the completed homogeneous space

The identity is proved on Schwartz functions by radial integration by parts, then extended through the faithful Y completion using two bounded functionals. No classical high derivative of the completed vector is assumed.

theorem OAI.DefocusingNLS.radial_tensor_inner line 22

theorem OAI.DefocusingNLS.homogeneousRadialTest_Schwartz line 32

Source documentation

Dense-domain version of the exact transposed radial identity.

theorem homogeneousRadialTest_Schwartz (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ))
    (h : PhysicalUnitSphere → ℂ) (hh : MemLp h 2 physicalSphereMeasure)
    (ψ : 𝓢(ℝ, ℂ)) (hψ : ∀ r, r ≤ 0 → ψ r = 0) (f : 𝓢(E, ℂ)) :
    homogeneousRadialTest a N ha ha1 hk h (fun r => ψ r) hh (memLp_radialSchwartz ψ)
        (homogeneousSchwartzEmbedding a N ha ha1 hk f) =
      (-1 : ℂ) ^ N * physicalPolarTest
        (fun p => star (h p.1) * radialTransposedTest N ψ p.2)
        (integrable_linePolarProduct h (radialTransposedTest N ψ)
          (hh.integrable (by norm_num)) (radialTransposedTest N ψ).integrable)
        (homogeneousPhysicalCLM a N ha ha1 hk
          (homogeneousSchwartzEmbedding a N ha ha1 hk f)) := by
…

Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.homogeneousRadialTest, OAI.DefocusingNLS.memLp_radialSchwartz, OAI.DefocusingNLS.homogeneousSchwartzEmbedding, OAI.DefocusingNLS.physicalPolarTest, OAI.DefocusingNLS.radialTransposedTest, OAI.DefocusingNLS.integrable_linePolarProduct, OAI.DefocusingNLS.homogeneousPhysicalCLM

theorem OAI.DefocusingNLS.homogeneousRadial_weak_testing line 132

Source documentation

Exact weak radial differentiation for every vector in the completion.

theorem homogeneousRadial_weak_testing (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ))
    (h : PhysicalUnitSphere → ℂ) (hh : MemLp h 2 physicalSphereMeasure)
    (ψ : 𝓢(ℝ, ℂ)) (hψ : ∀ r, r ≤ 0 → ψ r = 0) (u : HomogeneousY a N) :
    homogeneousRadialTest a N ha ha1 hk h (fun r => ψ r) hh (memLp_radialSchwartz ψ) u =
      (-1 : ℂ) ^ N * physicalPolarTest
        (fun p => star (h p.1) * radialTransposedTest N ψ p.2)
        (integrable_linePolarProduct h (radialTransposedTest N ψ)
          (hh.integrable (by norm_num)) (radialTransposedTest N ψ).integrable)
        (homogeneousPhysicalCLM a N ha ha1 hk u) := by
…

Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousRadialTest, OAI.DefocusingNLS.memLp_radialSchwartz, OAI.DefocusingNLS.physicalPolarTest, OAI.DefocusingNLS.radialTransposedTest, OAI.DefocusingNLS.integrable_linePolarProduct, OAI.DefocusingNLS.homogeneousPhysicalCLM

theorem OAI.DefocusingNLS.homogeneousAngularProjection_weak_derivative line 157

Source documentation

Integral form: the contracted L² derivative is the distributional Nth radial derivative of the actual angular projection.

theorem homogeneousAngularProjection_weak_derivative (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ))
    (h : PhysicalUnitSphere → ℂ) (hh : MemLp h 2 physicalSphereMeasure)
    (ψ : 𝓢(ℝ, ℂ)) (hψ : ∀ r, r ≤ 0 → ψ r = 0) (u : HomogeneousY a N) :
    (∫ r, ψ r * homogeneousRadialAngularDerivative a N ha ha1 hk h u r
      ∂physicalRadiusMeasure) =
      (-1 : ℂ) ^ N * ∫ r : ℝ, radialTransposedTest N ψ r *
        homogeneousAngularProjection a N ha ha1 hk h u r := by
…

Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousRadialAngularDerivative, OAI.DefocusingNLS.physicalRadiusMeasure, OAI.DefocusingNLS.radialTransposedTest, OAI.DefocusingNLS.homogeneousAngularProjection