HomogeneousAngularL2.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Angular projection preserves the radial L² condition

This applies to every square-integrable angular test, hence in particular to each normalized spherical harmonic. No angular eigenfunction equation is assumed or used by the measure-theoretic estimate.

theorem OAI.DefocusingNLS.norm_sq_toLp line 16

theorem OAI.DefocusingNLS.angular_integral_norm_sq_le line 27

Source documentation

Cauchy--Schwarz in the angular variable, with its exact L² constant.

theorem angular_integral_norm_sq_le {α : Type*} [MeasurableSpace α]
    (μ : Measure α) (h f : α → ℂ) (hh : MemLp h 2 μ) (hf : MemLp f 2 μ) :
    ‖∫ x, inner ℂ (h x) (f x) ∂μ‖ ^ 2 ≤
      (∫ x, ‖h x‖ ^ 2 ∂μ) * (∫ x, ‖f x‖ ^ 2 ∂μ) := by
…

theorem OAI.DefocusingNLS.memLp_angularProjection line 44
Source documentation
A fixed L² angular projection of an L² polar field is in L²(r^11 dr).
```
theorem memLp_angularProjection (h : PhysicalUnitSphere → ℂ)
    (hh : MemLp h 2 physicalSphereMeasure)
    (F : PhysicalUnitSphere × PhysicalPositiveRadius → ℂ)
    (hF : MemLp F 2 physicalPolarMeasure) :
    MemLp (fun r => ∫ ω, inner ℂ (h ω) (F (ω, r)) ∂physicalSphereMeasure)
      2 physicalRadiusMeasure := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalPolarMeasure, OAI.DefocusingNLS.physicalRadiusMeasure
theorem OAI.DefocusingNLS.homogeneousPolarDerivative_angular_memLp line 70
Source documentation
The angular component of each completed Cartesian top derivative satisfies exactly the radial weighted L² condition used in spectral exclusion.
```
theorem homogeneousPolarDerivative_angular_memLp (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ)) (j : Fin N → Fin 12)
    (h : PhysicalUnitSphere → ℂ) (hh : MemLp h 2 physicalSphereMeasure)
    (u : HomogeneousY a N) :
    MemLp (fun r => ∫ ω, inner ℂ (h ω)
      (homogeneousPolarDerivative a N ha ha1 hk j u (ω, r)) ∂physicalSphereMeasure)
      2 physicalRadiusMeasure :=
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPolarDerivative, OAI.DefocusingNLS.physicalRadiusMeasure