HomogeneousRadialTesting.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Integration by parts along each radial line

This is the dense-domain testing identity for the completed contraction. Tests supported in the positive half-line can later be multiplied by r^11 before this identity is applied.

theorem OAI.DefocusingNLS.scalar_schwartz_iterated_ibp line 20
def OAI.DefocusingNLS.schwartzRadialRestriction line 44
Source documentation
Restrict a Schwartz function to a radial line through a unit vector.
```
noncomputable def schwartzRadialRestriction (ω : PhysicalUnitSphere) :
    𝓢(E, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere
theorem OAI.DefocusingNLS.schwartzRadialRestriction_apply line 51

theorem OAI.DefocusingNLS.schwartz_radial_integral_by_parts line 56

Source documentation

The contracted top Cartesian derivative has the expected scalar integration-by-parts formula on every fixed radial line.

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

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