HomogeneousRadialCompletion.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Local integrability of the completed radial derivative

The extension by zero is only a measurable representative. On positive radii its weighted square integral is exactly the polar L² integral.

def OAI.DefocusingNLS.positiveRadiusExtension line 16
theorem OAI.DefocusingNLS.positiveRadiusExtension_coe line 19
theorem OAI.DefocusingNLS.positiveRadiusExtension_aestronglyMeasurable line 27
theorem OAI.DefocusingNLS.positiveRadiusExtension_weighted_square line 42
theorem OAI.DefocusingNLS.positiveRadiusExtension_weighted_locallyIntegrable line 51
Source documentation
The Jacobian times the completed radial derivative is locally integrable on the entire positive half-line.
```
theorem positiveRadiusExtension_weighted_locallyIntegrable
    (g : PhysicalPositiveRadius → ℂ) (hg : MemLp g 2 physicalRadiusMeasure) :
    LocallyIntegrableOn (fun r : ℝ => (r : ℂ) ^ (11 : ℕ) * positiveRadiusExtension g r)
      (Ioi 0) := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalRadiusMeasure, OAI.DefocusingNLS.positiveRadiusExtension
theorem OAI.DefocusingNLS.positiveRadiusExtension_weighted_square_tail line 83
Source documentation
Once a classical representative agrees almost everywhere on a tail, it inherits the exact radial weighted L² condition.
```
theorem positiveRadiusExtension_weighted_square_tail
    (g : PhysicalPositiveRadius → ℂ) (hg : MemLp g 2 physicalRadiusMeasure)
    (R : ℝ) (hR : 0 ≤ R) (F : ℝ → ℂ)
    (heq : ∀ᵐ r ∂volume, r ∈ Ioi R → positiveRadiusExtension g r = F r) :
    IntegrableOn (fun r : ℝ => r ^ (11 : ℕ) * ‖F r‖ ^ 2) (Ioi R) := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalRadiusMeasure, OAI.DefocusingNLS.positiveRadiusExtension