OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialComplexBoundaryFormula.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The summed real boundary forms have the usual complex norm expression.

  1. theorem OAI.DefocusingNLS.radialComplexAngularBoundary_eq line 10