HomogeneousPolarL2.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The exact twelve-dimensional polar L² realization

The surface measure is the Haar-induced (unnormalized) sphere measure, and its radial partner is r^11 dr. This transfers the already constructed physical derivatives, without making an additional regularity assumption.

abbrev OAI.DefocusingNLS.PhysicalUnitSphere line 17
abbrev OAI.DefocusingNLS.PhysicalPositiveRadius line 18
def OAI.DefocusingNLS.physicalSphereMeasure line 20
def OAI.DefocusingNLS.physicalRadiusMeasure line 23
instance OAI.DefocusingNLS.(instance at line 26) line 26
instance OAI.DefocusingNLS.(instance at line 30) line 30
def OAI.DefocusingNLS.physicalPolarMeasure line 34
def OAI.DefocusingNLS.physicalPolarPoint line 37
theorem OAI.DefocusingNLS.measurePreserving_physicalPolarPoint line 41
Source documentation
Polar coordinates preserve precisely the Cartesian volume measure.
```
theorem measurePreserving_physicalPolarPoint :
    MeasurePreserving physicalPolarPoint physicalPolarMeasure volume := by
…
```
Mentions: OAI.DefocusingNLS.physicalPolarPoint, OAI.DefocusingNLS.physicalPolarMeasure
def OAI.DefocusingNLS.physicalPolarL2 line 59
Source documentation
The pullback is a genuine L² isometry, including for nonsmooth completed data.
```
noncomputable def physicalPolarL2 :
    Lp ℂ 2 (volume : Measure (EuclideanSpace ℝ (Fin 12))) →ₗᵢ[ℂ]
      Lp ℂ 2 physicalPolarMeasure :=
…
```
Mentions: OAI.DefocusingNLS.physicalPolarMeasure
theorem OAI.DefocusingNLS.physicalPolarL2_ae line 64
def OAI.DefocusingNLS.homogeneousPolarDerivative line 70
Source documentation
Every Cartesian derivative from the homogeneous completion has an exact sphere/radius L² representative with the same norm.
```
noncomputable def homogeneousPolarDerivative (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ)) (j : Fin N → Fin 12) :
    HomogeneousY a N →L[ℂ] Lp ℂ 2 physicalPolarMeasure :=
…
```
Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.physicalPolarMeasure
theorem OAI.DefocusingNLS.homogeneousPolarDerivative_norm_le line 76