HomogeneousRadialSchwartz.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

This is the dense-domain identity for the completed radial derivative.

theorem OAI.DefocusingNLS.schwartz_radial_iteratedDeriv line 20
Source documentation
The ordinary radial derivative is the contraction of the Cartesian jet against the unit vector, with no lower-order correction terms.
```
theorem schwartz_radial_iteratedDeriv (N : ℕ) (f : 𝓢(E, ℂ))
    (ω : PhysicalUnitSphere) (r : ℝ) :
    iteratedDeriv N (fun t : ℝ => f (t • ω.1)) r =
      ∑ j : Fin N → Fin 12,
        (radialTensorCoefficient N j ω : ℂ) *
          homogeneousOrderedDerivative N j f (r • ω.1) := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalUnitSphere, OAI.DefocusingNLS.radialTensorCoefficient, OAI.DefocusingNLS.homogeneousOrderedDerivative