OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/ClassicalMaximalFlow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The maximal Sobolev flow is a classical solution of the defocusing equation

  1. def OAI.DefocusingNLS.IsClassicalDefocusingFlow line 12

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

  2. theorem OAI.DefocusingNLS.maximalSobolev_classical line 21