OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/PhysicalCutoffBlowup.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The physical open-family orbits have the asserted finite-time singularity

  1. def OAI.DefocusingNLS.HasFiniteTimeSelfSimilarBlowup line 14

    Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:249 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.HasFiniteTimeSelfSimilarBlowup@path.

  2. theorem OAI.DefocusingNLS.HasPhysicalCutoffOrbit.blowup line 28