HomogeneousRadialTestPairing.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Bounded radial test functionals on the actual homogeneous completion

Tensor-product tests turn the completed Cartesian derivatives into bounded functionals. Their exact radial integral formula is the bridge used when passing radial integration by parts through the Schwartz completion.

theorem OAI.DefocusingNLS.homogeneousPolarDerivative_Schwartz_ae line 18

Source documentation

On the dense Schwartz domain the polar completion agrees with the ordinary Cartesian derivative pulled back along the polar map.

theorem homogeneousPolarDerivative_Schwartz_ae (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ))
    (j : Fin N → Fin 12) (f : SchwartzMap (EuclideanSpace ℝ (Fin 12)) ℂ) :
    homogeneousPolarDerivative a N ha ha1 hk j
        (homogeneousSchwartzEmbedding a N ha ha1 hk f) =ᵐ[physicalPolarMeasure]
      fun p => homogeneousOrderedDerivative N j f (p.2.1 • p.1.1) := by
…

Mentions: OAI.DefocusingNLS.homogeneousPolarDerivative, OAI.DefocusingNLS.homogeneousSchwartzEmbedding, OAI.DefocusingNLS.physicalPolarMeasure, OAI.DefocusingNLS.homogeneousOrderedDerivative

theorem OAI.DefocusingNLS.memLp_polarProductTest line 33
Source documentation
Square-integrable radial and angular factors give a polar L² test.
```
theorem memLp_polarProductTest (h : PhysicalUnitSphere → ℂ)
    (ψ : PhysicalPositiveRadius → ℂ)
    (hh : MemLp h 2 physicalSphereMeasure) (hψ : MemLp ψ 2 physicalRadiusMeasure) :
    MemLp (fun p : PhysicalUnitSphere × PhysicalPositiveRadius =>
      h p.1 * star (ψ p.2)) 2 physicalPolarMeasure := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.physicalRadiusMeasure, OAI.DefocusingNLS.physicalPolarMeasure
def OAI.DefocusingNLS.polarProductTest line 44
theorem OAI.DefocusingNLS.integrable_polarTestPair line 50
theorem OAI.DefocusingNLS.inner_polarTest line 61

theorem OAI.DefocusingNLS.polarProductTest_pairing line 69

Source documentation

The test functional is exactly the radial integral of its angular projection.

theorem polarProductTest_pairing (h : PhysicalUnitSphere → ℂ)
    (ψ : PhysicalPositiveRadius → ℂ)
    (hh : MemLp h 2 physicalSphereMeasure) (hψ : MemLp ψ 2 physicalRadiusMeasure)
    (F : Lp ℂ 2 physicalPolarMeasure) :
    inner ℂ (polarProductTest h ψ hh hψ) F =
      ∫ r, ψ r * (∫ ω, inner ℂ (h ω) (F (ω, r)) ∂physicalSphereMeasure)
        ∂physicalRadiusMeasure := by
…

Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.physicalRadiusMeasure, OAI.DefocusingNLS.physicalPolarMeasure, OAI.DefocusingNLS.polarProductTest

def OAI.DefocusingNLS.homogeneousRadialTestComponent line 95
Source documentation
Each separated angular/radial test acts boundedly on an ordered derivative.
```
noncomputable def homogeneousRadialTestComponent (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ)) (j : Fin N → Fin 12)
    (h : PhysicalUnitSphere → ℂ) (ψ : PhysicalPositiveRadius → ℂ)
    (hh : MemLp h 2 physicalSphereMeasure) (hψ : MemLp ψ 2 physicalRadiusMeasure) :
    HomogeneousY a N →L[ℂ] ℂ :=
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.physicalRadiusMeasure, OAI.DefocusingNLS.HomogeneousY
def OAI.DefocusingNLS.homogeneousRadialTest line 105
Source documentation
The finite contracted test remains bounded on the full completion.
```
noncomputable def homogeneousRadialTest (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ))
    (h : PhysicalUnitSphere → ℂ) (ψ : PhysicalPositiveRadius → ℂ)
    (hh : MemLp h 2 physicalSphereMeasure) (hψ : MemLp ψ 2 physicalRadiusMeasure) :
    HomogeneousY a N →L[ℂ] ℂ :=
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.physicalRadiusMeasure, OAI.DefocusingNLS.HomogeneousY

theorem OAI.DefocusingNLS.homogeneousRadialTest_apply line 113

Source documentation

The bounded completion-level functional has the expected integral formula.

theorem homogeneousRadialTest_apply (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ))
    (h : PhysicalUnitSphere → ℂ) (ψ : PhysicalPositiveRadius → ℂ)
    (hh : MemLp h 2 physicalSphereMeasure) (hψ : MemLp ψ 2 physicalRadiusMeasure)
    (u : HomogeneousY a N) :
    homogeneousRadialTest a N ha ha1 hk h ψ hh hψ u =
      ∫ r, ψ r * homogeneousRadialAngularDerivative a N ha ha1 hk h u r
        ∂physicalRadiusMeasure := by
…

Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.physicalRadiusMeasure, OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousRadialTest, OAI.DefocusingNLS.homogeneousRadialAngularDerivative