OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialWeightedTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The pressure-weighted transport identity, with all endpoint terms explicit.

  1. theorem OAI.DefocusingNLS.radialMatched_weighted_transport line 12
  2. theorem OAI.DefocusingNLS.radialMatched_pressure_transport_identity line 58