OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousRadialLaplacianGreen.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.compactScalarTest_integrable line 14
2. theorem OAI.DefocusingNLS.compactScalarTest_first_green line 19
3. theorem OAI.DefocusingNLS.deriv_radialWeighted_firstTest line 34
4. theorem OAI.DefocusingNLS.radial_divergence_green line 51

   Source documentation

   The radial divergence operator is symmetric against a compact smooth test. The function being tested only needs two continuous derivatives.

   theorem radial_divergence_green (φ : 𝓢(ℝ, ℂ)) (hc : HasCompactSupport φ)
       (A : ℝ → ℂ) (hA : ContDiff ℝ 2 A) :
       (∫ r : ℝ, ((r : ℂ) ^ 11 * deriv (deriv φ) r +
         11 * (r : ℂ) ^ 10 * deriv φ r) * A r) =
       ∫ r : ℝ, φ r * ((r : ℂ) ^ 11 * deriv (deriv A) r +
         11 * (r : ℂ) ^ 10 * deriv A r) := by
   …

5. theorem OAI.DefocusingNLS.radial_laplacian_green line 100