OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousConvolutionWeights.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact homogeneous weights for continuous Fourier convolution

  1. def OAI.DefocusingNLS.homogeneousFourierMagnitude line 15
  2. theorem OAI.DefocusingNLS.homogeneousFourierMagnitude_nonneg line 18
  3. theorem OAI.DefocusingNLS.homogeneousFourierMagnitude_continuous line 22
  4. theorem OAI.DefocusingNLS.homogeneous_magnitude_le_bessel line 26
  5. theorem OAI.DefocusingNLS.homogeneousFourierMagnitude_integrable line 39
  6. theorem OAI.DefocusingNLS.homogeneousFourierMagnitude_bounded line 47
  7. theorem OAI.DefocusingNLS.homogeneousFourierMagnitude_sq_integrable line 53
  8. theorem OAI.DefocusingNLS.homogeneousFrequencyWeight_add_le line 70

    Source documentation

    A sum of frequencies costs only the fixed constant 2^s.

    theorem homogeneousFrequencyWeight_add_le (s : ℝ) (hs : 0 ≤ s) (ξ η : E) :
    ‖ξ + η‖ ^ s ≤ 2 ^ s * (‖ξ‖ ^ s + ‖η‖ ^ s) := by
…