OAI/MathematicalPhysics/DefocusingNLS/Profile/RadianFourierSeries.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The physical localized Fourier series

Absolute summability gives the actual continuous periodic function on Euclidean space. Its localized Fourier transform is the limit of the exact finite-cutoff formula; domination is supplied by the integrable Schwartz cutoff.

  1. def OAI.DefocusingNLS.spatialFourierCharacter line 21
  2. theorem OAI.DefocusingNLS.spatialFourierCharacter_norm line 24
  3. theorem OAI.DefocusingNLS.continuous_spatialFourierCharacter line 27
  4. def OAI.DefocusingNLS.spatialFourierSeries line 30
  5. theorem OAI.DefocusingNLS.summable_spatialFourierSeries line 33
  6. theorem OAI.DefocusingNLS.continuous_spatialFourierSeries line 39
  7. theorem OAI.DefocusingNLS.spatialFourierSeries_norm_le line 48
  8. def OAI.DefocusingNLS.localizedFourierSeries line 56
  9. theorem OAI.DefocusingNLS.continuous_localizedFourierSeries line 60
  10. theorem OAI.DefocusingNLS.integrable_localizedFourierSeries line 66
  11. theorem OAI.DefocusingNLS.hasSum_localizedFourierSeries_transform line 74

    Source documentation

    The infinite physical Fourier transform is the limit of the finite cutoff transforms.

    theorem hasSum_localizedFourierSeries_transform (L : ℝ) (hL : 0 < L)
    (Ο‡ : 𝓒(E, β„‚)) (v : frequencyLattice β†’ β„‚)
    (hv : Summable (fun n => β€–v nβ€–)) (ΞΎ : E) :
    HasSum (fun n => (L ^ (12 : β„•) : ℝ) β€’
      (v n * radianFourierKernel Ο‡ (L β€’ ΞΎ - n)))
      (radianFourierIntegral (localizedFourierSeries L Ο‡ v) ΞΎ) := by
…

    Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.radianFourierKernel, OAI.DefocusingNLS.radianFourierIntegral, OAI.DefocusingNLS.localizedFourierSeries

  12. theorem OAI.DefocusingNLS.tendsto_localizedFourierPolynomial_transform line 114