OAI/MathematicalPhysics/DefocusingNLS/Certificates/LaguerreProjection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Differentiation in Laguerre coefficients

Integration by parts gives the triangular derivative rule directly. No interchange of an infinite Laguerre expansion and differentiation is needed.

  1. def OAI.DefocusingNLS.laguerreValue line 17
  2. def OAI.DefocusingNLS.laguerreIntegrand line 20
  3. def OAI.DefocusingNLS.laguerreCoefficientIntegral line 23
  4. theorem OAI.DefocusingNLS.hasDerivAt_laguerreValue line 26
  5. theorem OAI.DefocusingNLS.hasDerivAt_laguerreIntegrand line 33
  6. theorem OAI.DefocusingNLS.laguerreCoefficientIntegral_derivative line 47

    Source documentation

    A weighted derivative coefficient is a finite partial sum minus the boundary value. Both endpoint limits follow from the integrability hypotheses.

    theorem laguerreCoefficientIntegral_derivative (f f' : ℝ → ℂ) (n : ℕ)
    (hf : ∀ t ∈ Ioi (0 : ℝ), HasDerivAt f (f' t) t)
    (hc : ContinuousWithinAt f (Ici 0) 0)
    (hi : ∀ j, IntegrableOn (laguerreIntegrand f j) (Ioi 0))
    (hi' : IntegrableOn (laguerreIntegrand f' n) (Ioi 0)) :
    laguerreCoefficientIntegral f' n =
      -f 0 + ∑ j ∈ Finset.range (n + 1), laguerreCoefficientIntegral f j := by
…

    Mentions: OAI.DefocusingNLS.laguerreIntegrand, OAI.DefocusingNLS.laguerreCoefficientIntegral