RieszIntegrability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the two Riesz weights used in the cubic dispersion integral.

theorem OAI.CubicFirstMoment.schwartz_riesz_integrable line 15
Source documentation
The singularity is locally integrable in dimension two; away from zero the weight is bounded and Schwartz integrability suffices.
```
theorem schwartz_riesz_integrable (F : 𝓢(ℂ,ℂ)) {a : ℝ} (ha : 0 < a) (ha2 : a < 2) :
    Integrable (fun z : ℂ => ((‖z‖^(-a):ℝ):ℂ)*F z) := by
…
```