OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFourierL1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fourier L¹ control by the exact homogeneous norm

Cauchy--Schwarz with the integrable inverse weight gives an actual L¹ Fourier representative for every vector of Y, with no quotient by polynomials.

  1. theorem OAI.DefocusingNLS.integrable_and_integral_norm_of_memLp_homogeneous line 19