HomogeneousCZero.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual continuous functions represented by the homogeneous space

Every Y vector has an integrable Fourier representative. Its inverse Fourier integral is continuous, vanishes at infinity, and obeys a uniform norm bound.

def OAI.DefocusingNLS.inverseRadianFourier line 21
theorem OAI.DefocusingNLS.continuous_inverseRadianFourier line 24
theorem OAI.DefocusingNLS.zero_at_infty_inverseRadianFourier line 28
theorem OAI.DefocusingNLS.inverseRadianFourier_norm_le line 47
theorem OAI.DefocusingNLS.inverseRadianFourier_kernel line 59
Source documentation
The inverse Fourier normalization recovers every Schwartz function exactly.
```
theorem inverseRadianFourier_kernel (χ : 𝓢(E, ℂ)) (y : E) :
    inverseRadianFourier (radianFourierKernel χ) y = χ y := by
…
```
Mentions: OAI.DefocusingNLS.inverseRadianFourier, OAI.DefocusingNLS.radianFourierKernel
def OAI.DefocusingNLS.homogeneousPhysicalFunction line 77
theorem OAI.DefocusingNLS.homogeneousPhysicalFunction_apply line 84

theorem OAI.DefocusingNLS.homogeneousPhysicalFunction_norm_le line 89

Source documentation

Whole-space point observation has one finite constant determined by the exact weight.

theorem homogeneousPhysicalFunction_norm_le (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (f : HomogeneousY a k) :
    ‖homogeneousPhysicalFunction a k ha ha1 hk f‖ ≤
      (((2 * Real.pi) ^ (12 : ℕ))⁻¹ *
        Real.sqrt (∫ ξ, (homogeneousFourierWeight a k ξ)⁻¹)) * ‖f‖ := by
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPhysicalFunction, OAI.DefocusingNLS.homogeneousFourierWeight