OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSchwartzConvolution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.homogeneousSchwartzConvolution line 15
2. theorem OAI.DefocusingNLS.positive_integrand_integrable line 18
3. theorem OAI.DefocusingNLS.homogeneousSchwartzConvolution_weighted_pointwise line 27
4. theorem OAI.DefocusingNLS.homogeneousSchwartzConvolution_energy_le line 78

   Source documentation

   The homogeneous energy is controlled by the L¹ norms and matching energies.

   theorem homogeneousSchwartzConvolution_energy_le (s : ℝ) (hs : 0 ≤ s)
       (ψ φ : 𝓢(E, ℂ)) :
       homogeneousFrequencyEnergy s (homogeneousSchwartzConvolution ψ φ) ≤
         2 * (2 ^ s) ^ 2 * ((∫ ξ, ‖φ ξ‖) ^ 2 * homogeneousFrequencyEnergy s ψ +
           (∫ ξ, ‖ψ ξ‖) ^ 2 * homogeneousFrequencyEnergy s φ) := by
   …

   Mentions: OAI.DefocusingNLS.homogeneousFrequencyEnergy, OAI.DefocusingNLS.homogeneousSchwartzConvolution