HomogeneousPolarTesting.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Integrable polar tests of the faithful physical realization

The radial variable here is ordinary Lebesgue measure on the real line. This lets a compactly supported radial test absorb the polar Jacobian before integration by parts. The test is a bounded functional on physical C0.

def OAI.DefocusingNLS.physicalLinePolarMeasure line 19
theorem OAI.DefocusingNLS.physicalCZero_norm_le line 22
theorem OAI.DefocusingNLS.integrable_linePolarTest line 26
def OAI.DefocusingNLS.physicalPolarTest line 39
Source documentation
An L¹ polar test is continuous on the actual physical C0 realization.
```
noncomputable def physicalPolarTest (K : PhysicalUnitSphere × ℝ → ℂ)
    (hK : Integrable K physicalLinePolarMeasure) : C₀(E, ℂ) →L[ℂ] ℂ := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalLinePolarMeasure
theorem OAI.DefocusingNLS.physicalPolarTest_apply line 68
theorem OAI.DefocusingNLS.integrable_linePolarProduct line 74
Source documentation
Product tests are integrable without regularity of the angular factor.
```
theorem integrable_linePolarProduct (h : PhysicalUnitSphere → ℂ) (φ : ℝ → ℂ)
    (hh : Integrable h physicalSphereMeasure) (hφ : Integrable φ) :
    Integrable (fun p : PhysicalUnitSphere × ℝ => star (h p.1) * φ p.2)
      physicalLinePolarMeasure := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.physicalLinePolarMeasure

theorem OAI.DefocusingNLS.physicalPolarTest_product line 86

Source documentation

The product-test functional equals its iterated angular/radial formula.

theorem physicalPolarTest_product (h : PhysicalUnitSphere → ℂ) (φ : ℝ → ℂ)
    (hh : Integrable h physicalSphereMeasure) (hφ : Integrable φ)
    (f : C₀(E, ℂ)) :
    physicalPolarTest (fun p => star (h p.1) * φ p.2)
        (integrable_linePolarProduct h φ hh hφ) f =
      ∫ ω, star (h ω) * (∫ r, φ r * f (r • ω.1)) ∂physicalSphereMeasure := by
…

Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.physicalSphereMeasure, OAI.DefocusingNLS.physicalPolarTest, OAI.DefocusingNLS.integrable_linePolarProduct