OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffForcingHistory.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Continuous histories for the actual approximate nonlinear solution

  1. def OAI.DefocusingNLS.sampledCutoffProfileHistory line 15
  2. theorem OAI.DefocusingNLS.continuous_sampledCutoffProfileHistory line 21
  3. theorem OAI.DefocusingNLS.sampledCutoffProfileHistory_of_mem line 28
  4. def OAI.DefocusingNLS.sampledCutoffNonlinearPath line 41
  5. def OAI.DefocusingNLS.sampledCutoffForcingPath line 52
  6. def OAI.DefocusingNLS.sampledCutoffForcingHistory line 62
  7. theorem OAI.DefocusingNLS.continuous_sampledCutoffForcingHistory line 71
  8. theorem OAI.DefocusingNLS.sampledCutoffForcingHistory_of_mem line 81
  9. theorem OAI.DefocusingNLS.sampledCutoffProfileHistory_coefficient line 98
  10. theorem OAI.DefocusingNLS.sampledCutoffResidualHistory_of_mem line 111