HomogeneousRadialL2.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Completed radial derivative contractions in the exact radial measure

def OAI.DefocusingNLS.radialTensorCoefficient line 11
theorem OAI.DefocusingNLS.continuous_radialTensorCoefficient line 14
theorem OAI.DefocusingNLS.radialTensorCoefficient_abs_le line 19
theorem OAI.DefocusingNLS.memLp_radialTensor_test line 31
Source documentation
Multiplying an angular test by a radial tensor coefficient preserves L².
```
theorem memLp_radialTensor_test (N : ℕ) (j : Fin N → Fin 12)
    (h : PhysicalUnitSphere → ℂ) (hh : MemLp h 2 physicalSphereMeasure) :
    MemLp (fun ω => (radialTensorCoefficient N j ω : ℂ) * h ω)
      2 physicalSphereMeasure := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.radialTensorCoefficient
theorem OAI.DefocusingNLS.radial_weighted_integrable_of_memLp line 44
Source documentation
Remove the polar density: this is exactly square integrability with respect to r^11 dr, on the positive real half-line.
```
theorem radial_weighted_integrable_of_memLp (f : ℝ → ℂ)
    (hf : MemLp (fun r : PhysicalPositiveRadius => f r) 2 physicalRadiusMeasure) :
    IntegrableOn (fun r : ℝ => r ^ (11 : ℕ) * ‖f r‖ ^ 2) (Ioi 0) := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalRadiusMeasure
def OAI.DefocusingNLS.homogeneousRadialAngularDerivative line 62
Source documentation
The contraction is formed after completing each Cartesian derivative. Its angular coefficients are r^11-weighted L² functions.
```
noncomputable def homogeneousRadialAngularDerivative (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ))
    (h : PhysicalUnitSphere → ℂ) (u : HomogeneousY a N)
    (r : PhysicalPositiveRadius) : ℂ :=
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.PhysicalPositiveRadius
theorem OAI.DefocusingNLS.homogeneousRadialAngularDerivative_memLp line 70