HomogeneousAngularProjection.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Classical angular projections of the actual physical realization

Only square integrability of the angular test is needed. Harmonicity and the angular eigenvalue are deliberately absent from this calculus lemma.

theorem OAI.DefocusingNLS.integrable_sphere_pairing line 20
theorem OAI.DefocusingNLS.continuous_sphere_pairing line 34
theorem OAI.DefocusingNLS.hasDerivAt_sphere_pairing line 59
def OAI.DefocusingNLS.homogeneousAngularProjection line 87

theorem OAI.DefocusingNLS.hasDerivAt_homogeneousAngularProjection line 94

Source documentation

The first derivative of the angular component is the angular component of the directional radial derivative.

theorem hasDerivAt_homogeneousAngularProjection (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
    (h : PhysicalUnitSphere → ℂ) (hh : MemLp h 2 physicalSphereMeasure)
    (u : HomogeneousY a k) (r : ℝ) :
    HasDerivAt (homogeneousAngularProjection a k ha ha1 hk h u)
      (∫ ω, inner ℂ (h ω)
        (fderiv ℝ (homogeneousPhysicalCLM a k ha ha1 hk u) (r • ω.1) ω.1)
        ∂physicalSphereMeasure) r := by
…

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

theorem OAI.DefocusingNLS.contDiff_homogeneousAngularProjection line 118
Source documentation
Every angular coefficient of an actual Y vector is C² in the radius. No spherical harmonic equation is needed for this regularity.
```
theorem contDiff_homogeneousAngularProjection (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
    (h : PhysicalUnitSphere → ℂ) (hh : MemLp h 2 physicalSphereMeasure)
    (u : HomogeneousY a k) :
    ContDiff ℝ 2 (homogeneousAngularProjection a k ha ha1 hk h u) := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousAngularProjection