OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedFluxLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The transport coefficient converges by its mass-average identity, including the origin; no derivative convergence across the pressure layer is used.

  1. theorem OAI.DefocusingNLS.radialMatchedWeightedFlux_average_nonneg line 16
  2. theorem OAI.DefocusingNLS.radialUniform_const_mul line 32
  3. theorem OAI.DefocusingNLS.radialMatchedWeightedFlux_uniform_limit line 52