OAI/MathematicalPhysics/RapidForcing/NSUniqueness.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.L2ContinuousOn.memLp line 12
  2. lemma OAI.RapidForcing.spatialMulti_zero line 18
  3. lemma OAI.RapidForcing.spatialMulti_single line 21
  4. lemma OAI.RapidForcing.order_single line 26
  5. lemma OAI.RapidForcing.EnergyRegularity.memLp_velocity line 29
  6. lemma OAI.RapidForcing.EnergyRegularity.memLp_pressure line 34
  7. lemma OAI.RapidForcing.EnergyRegularity.memLp_velocityD line 39
  8. lemma OAI.RapidForcing.EnergyRegularity.memLp_velocityDD line 47
  9. lemma OAI.RapidForcing.EnergyRegularity.memLp_pressureD line 55
  10. lemma OAI.RapidForcing.timeD_sub line 63
  11. lemma OAI.RapidForcing.spaceD_sub_twice line 68
  12. lemma OAI.RapidForcing.advection_difference line 76
  13. lemma OAI.RapidForcing.navierStokes_difference_energy line 85
  14. lemma OAI.RapidForcing.energy_zero line 146
  15. theorem OAI.RapidForcing.energy_velocity_unique line 176
  16. lemma OAI.RapidForcing.volume_space_univ line 233
  17. lemma OAI.RapidForcing.gradient_apply line 239
  18. theorem OAI.RapidForcing.energy_pressure_unique line 243
  19. theorem OAI.RapidForcing.energy_solution_unique line 283
  20. theorem OAI.RapidForcing.addressed_uniqueEnergySolution line 293