OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousYConvolution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Continuous convolution on the faithful homogeneous completion

  1. def OAI.DefocusingNLS.homogeneousConvolutionPartial line 13
  2. theorem OAI.DefocusingNLS.homogeneousConvolutionPartial_on_Schwartz line 20
  3. theorem OAI.DefocusingNLS.homogeneousConvolutionPartial_norm_le line 29
  4. theorem OAI.DefocusingNLS.homogeneousConvolutionPartial_add line 37
  5. theorem OAI.DefocusingNLS.homogeneousConvolutionPartial_smul line 54
  6. def OAI.DefocusingNLS.homogeneousConvolutionPartialLinear line 69
  7. def OAI.DefocusingNLS.homogeneousYConvolution line 77

    Source documentation

    The actual continuous-frequency convolution extends to every vector of Y.

    noncomputable def homogeneousYConvolution (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) :
    HomogeneousY a k →L[ℂ] HomogeneousY a k →L[ℂ] HomogeneousY a k :=
…

    Mentions: OAI.DefocusingNLS.HomogeneousY

  8. theorem OAI.DefocusingNLS.homogeneousYConvolution_on_Schwartz line 83
  9. theorem OAI.DefocusingNLS.homogeneousYConvolution_norm_le line 101