OAI/MathematicalPhysics/AlternatingFlow/Analytic.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AlternatingNS.Analytic.spatial_fderiv_smooth line 10
  2. lemma OAI.AlternatingNS.Analytic.dx_smooth line 15
  3. def OAI.AlternatingNS.Analytic.fullDt line 20
  4. lemma OAI.AlternatingNS.Analytic.fullDt_smooth line 23
  5. lemma OAI.AlternatingNS.Analytic.dt_eq_full line 29
  6. lemma OAI.AlternatingNS.Analytic.smooth_classical line 37
  7. lemma OAI.AlternatingNS.Analytic.residual_navierStokes line 55
  8. lemma OAI.AlternatingNS.Analytic.advection_smooth line 65
  9. lemma OAI.AlternatingNS.Analytic.laplacian_smooth line 69
  10. lemma OAI.AlternatingNS.Analytic.residual_smooth line 76
  11. lemma OAI.AlternatingNS.Analytic.dx_supported line 86
  12. lemma OAI.AlternatingNS.Analytic.outside_dt line 93
  13. lemma OAI.AlternatingNS.Analytic.residual_supported line 101
  14. lemma OAI.AlternatingNS.Analytic.finite_bound line 114
  15. lemma OAI.AlternatingNS.Analytic.finite_lipschitz line 126
  16. lemma OAI.AlternatingNS.Analytic.trajectory_unique line 144
  17. lemma OAI.AlternatingNS.Analytic.finite_trajectory line 158
  18. lemma OAI.AlternatingNS.Analytic.finite_trajectory_unique line 174
  19. lemma OAI.AlternatingNS.Analytic.global_trajectory line 192
  20. theorem OAI.AlternatingNS.Analytic.global_material_flow line 224
  21. def OAI.AlternatingNS.Construction.force line 239
  22. theorem OAI.AlternatingNS.Construction.smooth_forced_simulation line 242
  23. def OAI.AlternatingNS.Analytic.zeroExtend line 274
  24. lemma OAI.AlternatingNS.Analytic.zeroExtend_memLp line 279
  25. def OAI.AlternatingNS.Analytic.compactToL2 line 297
  26. lemma OAI.AlternatingNS.Analytic.compactToL2_coe line 333
  27. def OAI.AlternatingNS.Analytic.onCompact line 337
  28. lemma OAI.AlternatingNS.Analytic.onCompact_continuous line 342
  29. lemma OAI.AlternatingNS.Analytic.compactToL2_onCompact line 347
  30. lemma OAI.AlternatingNS.Analytic.onCompact_hasDerivAt line 360
  31. lemma OAI.AlternatingNS.Analytic.iterate_dx_smooth line 386
  32. lemma OAI.AlternatingNS.Analytic.spatial_smooth line 394
  33. lemma OAI.AlternatingNS.Analytic.iterate_dx_supported line 398
  34. lemma OAI.AlternatingNS.Analytic.spatial_supported line 407
  35. lemma OAI.AlternatingNS.Analytic.fullDt_supported line 413
  36. lemma OAI.AlternatingNS.Analytic.smooth_continuousInH line 423
  37. lemma OAI.AlternatingNS.Analytic.smooth_C1InL2 line 434
  38. theorem OAI.AlternatingNS.Analytic.smooth_energyClass line 453
  39. theorem OAI.AlternatingNS.Construction.velocity_energyClass line 474