OAI/MathematicalPhysics/AlternatingFlow/EnergyUniqueness.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AlternatingNS.Analytic.spatial_zero line 11
  2. lemma OAI.AlternatingNS.Analytic.spatial_single line 14
  3. lemma OAI.AlternatingNS.Analytic.h_memLp line 19
  4. lemma OAI.AlternatingNS.Analytic.h_dx_memLp line 26
  5. lemma OAI.AlternatingNS.Analytic.h_dxx_memLp line 33
  6. lemma OAI.AlternatingNS.Analytic.L2_inner_integrable line 40
  7. lemma OAI.AlternatingNS.Analytic.L2_bounded_smul line 47
  8. lemma OAI.AlternatingNS.Analytic.L2_coord line 57
  9. lemma OAI.AlternatingNS.Analytic.d_coord line 61
  10. lemma OAI.AlternatingNS.Analytic.sum_basis line 69
  11. lemma OAI.AlternatingNS.Analytic.directional_sum line 73
  12. lemma OAI.AlternatingNS.Analytic.L2_directional line 78
  13. lemma OAI.AlternatingNS.Analytic.diffusion_identity line 90
  14. lemma OAI.AlternatingNS.Analytic.norm_sq_d line 105
  15. lemma OAI.AlternatingNS.Analytic.bounded_L2_sq line 111
  16. lemma OAI.AlternatingNS.Analytic.pressure_identity line 118
  17. lemma OAI.AlternatingNS.Analytic.transport_identity line 148
  18. lemma OAI.AlternatingNS.Analytic.spatial_energy_inequality line 204
  19. lemma OAI.AlternatingNS.Analytic.d_sub line 274
  20. lemma OAI.AlternatingNS.Analytic.grad_zero line 280
  21. lemma OAI.AlternatingNS.Analytic.navierStokes_energy_inequality line 284
  22. lemma OAI.AlternatingNS.Analytic.l2_inner_representatives line 335
  23. lemma OAI.AlternatingNS.Analytic.l2_norm_sq_representative line 343
  24. theorem OAI.AlternatingNS.Analytic.energy_velocity_unique line 349
  25. lemma OAI.AlternatingNS.Analytic.pressure_zero_of_gradient_zero line 411
  26. theorem OAI.AlternatingNS.Analytic.energy_unique line 427
  27. theorem OAI.AlternatingNS.Construction.velocity_unique line 463