OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousYProduct.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The homogeneous algebra is the actual pointwise physical product

  1. theorem OAI.DefocusingNLS.radianFourierIntegral_schwartzConvolution line 14
  2. theorem OAI.DefocusingNLS.inverseRadianFourier_normalizedConvolution line 25
  3. def OAI.DefocusingNLS.homogeneousYProduct line 35
  4. theorem OAI.DefocusingNLS.homogeneousYProduct_on_Schwartz line 41
  5. theorem OAI.DefocusingNLS.homogeneousYProduct_physical line 53

    Source documentation

    Multiplication on Y agrees everywhere with multiplication of the represented functions.

    theorem homogeneousYProduct_physical (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (f g : HomogeneousY a k) (y : E) :
    homogeneousPhysicalCLM a k ha ha1 hk (homogeneousYProduct a k ha ha1 hk f g) y =
      homogeneousPhysicalCLM a k ha ha1 hk f y * homogeneousPhysicalCLM a k ha ha1 hk g y := by
…

    Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPhysicalCLM, OAI.DefocusingNLS.homogeneousYProduct