OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableFrameContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Strong continuity of projected blocks and local nonlinear sources

  1. theorem OAI.DefocusingNLS.continuous_stableProjection_apply line 13
  2. theorem OAI.DefocusingNLS.continuous_stableProjectedBlock_apply line 20
  3. theorem OAI.DefocusingNLS.continuous_stableMixedBlock_apply line 33
  4. theorem OAI.DefocusingNLS.continuous_stableFrameAssembly_apply line 45
  5. theorem OAI.DefocusingNLS.continuous_stableFrame_sources_local line 50