OAI/MathematicalPhysics/DefocusingNLS/Linear/FourierAbsolute.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Absolute Fourier coefficients and the quantitative ℓ¹ embedding

  1. def OAI.DefocusingNLS.fourierAbsolute line 12

    Source documentation

    Replace each ℓ² coordinate by its nonnegative norm, embedded in ℂ.

    noncomputable def fourierAbsolute (f : FourierL2) : FourierL2 :=
…

    Mentions: OAI.DefocusingNLS.FourierL2

  2. theorem OAI.DefocusingNLS.fourierAbsolute_apply line 15
  3. theorem OAI.DefocusingNLS.fourierAbsolute_norm line 18
  4. lemma OAI.DefocusingNLS.sobolevFourierCoefficient_absolute line 23
  5. theorem OAI.DefocusingNLS.tsum_norm_sobolevFourierCoefficient_le line 33

    Source documentation

    The Sobolev-to-ℓ¹ estimate has the same constant as point evaluation.

    theorem tsum_norm_sobolevFourierCoefficient_le (k : ℝ) (hk : 6 < k) (f : FourierL2) :
    (∑' n, ‖sobolevFourierCoefficient k f n‖) ≤
      ‖sobolevObservationVector k hk‖ * ‖f‖ := by
…

    Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevFourierCoefficient, OAI.DefocusingNLS.sobolevObservationVector