OAI/MathematicalPhysics/DefocusingNLS/Certificates/PolynomialProjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.weightedPolynomialIntegrand line 11
2. def OAI.DefocusingNLS.weightedPolynomialIntegral line 14
3. def OAI.DefocusingNLS.weightedPolynomialFunctional line 17
4. theorem OAI.DefocusingNLS.weightedPolynomialFunctional_apply line 32
5. theorem OAI.DefocusingNLS.hasDerivAt_weightedPolynomialIntegrand line 36
6. theorem OAI.DefocusingNLS.weightedPolynomialIntegral_derivative line 49
7. theorem OAI.DefocusingNLS.weightedPolynomialIntegral_laguerre_operator line 74

   Source documentation

   Symmetry of the Laguerre differential operator against a smooth function.

   theorem weightedPolynomialIntegral_laguerre_operator (f f' f'' : ℝ → ℂ) (p : ℂ[X])
       (hd : ∀ t ∈ Ioi (0 : ℝ), HasDerivAt f (f' t) t)
       (hd' : ∀ t ∈ Ioi (0 : ℝ), HasDerivAt f' (f'' t) t)
       (hc : ContinuousWithinAt f (Ici 0) 0)
       (hc' : ContinuousWithinAt f' (Ici 0) 0)
       (hi : ∀ p, IntegrableOn (weightedPolynomialIntegrand f p) (Ioi 0))
       (hi' : ∀ p, IntegrableOn (weightedPolynomialIntegrand f' p) (Ioi 0))
       (hi'' : ∀ p, IntegrableOn (weightedPolynomialIntegrand f'' p) (Ioi 0)) :
       weightedPolynomialIntegral f'' (X * p) +
         weightedPolynomialIntegral f' ((1 - X) * p) =
         weightedPolynomialIntegral f (laguerreOperator p) := by
   …

   Mentions: OAI.DefocusingNLS.weightedPolynomialIntegrand, OAI.DefocusingNLS.weightedPolynomialIntegral, OAI.DefocusingNLS.laguerreOperator