HomogeneousPhysicalInjective.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Faithfulness of the physical homogeneous realization

The inverse Fourier realization is injective. The proof uses Fourier duality against Schwartz tests and the fundamental lemma for locally integrable functions.

theorem OAI.DefocusingNLS.integral_fourier_mul_schwartz line 19
theorem OAI.DefocusingNLS.ae_eq_zero_of_fourier_zero line 26
theorem OAI.DefocusingNLS.ae_eq_zero_of_inverseRadian_zero line 44
theorem OAI.DefocusingNLS.inverseRadianFourier_injective_ae line 55
Source documentation
Equality of inverse Fourier transforms determines integrable Fourier data.
```
theorem inverseRadianFourier_injective_ae {f g : E → ℂ}
    (hf : Integrable f) (hg : Integrable g)
    (h : inverseRadianFourier f = inverseRadianFourier g) : f =ᵐ[volume] g := by
…
```
Mentions: OAI.DefocusingNLS.inverseRadianFourier
theorem OAI.DefocusingNLS.homogeneousPhysicalCLM_injective line 73
Source documentation
Distinct Y vectors represent distinct continuous functions.
```
theorem homogeneousPhysicalCLM_injective (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) :
    Function.Injective (homogeneousPhysicalCLM a k ha ha1 hk) := by
…
```
Mentions: OAI.DefocusingNLS.homogeneousPhysicalCLM