HomogeneousRadialComplexTesting.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Complex radial integration by parts on the Schwartz core

theorem OAI.DefocusingNLS.schwartz_radial_integral_mul_by_parts line 15

Source documentation

The complex bilinear form of radial integration by parts.

theorem schwartz_radial_integral_mul_by_parts (N : ℕ) (ψ : 𝓢(ℝ, ℂ))
    (f : 𝓢(E, ℂ)) (ω : PhysicalUnitSphere) :
    (∫ r : ℝ, ψ r *
      (∑ j : Fin N → Fin 12, (radialTensorCoefficient N j ω : ℂ) *
        homogeneousOrderedDerivative N j f (r • ω.1))) =
      (-1 : ℂ) ^ N * ∫ r : ℝ,
        ((∂^{fun _ : Fin N => (1 : ℝ)} ψ) r) * f (r • ω.1) := by
…

Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.radialTensorCoefficient, OAI.DefocusingNLS.homogeneousOrderedDerivative