OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TorusClass.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.TorusClass.Space line 10

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:723 (same declaration text).

  2. abbrev OAI.VelocityDetection.TorusClass.Vect line 12
  3. def OAI.VelocityDetection.TorusClass.measure line 14

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:725 (same declaration text).

  4. theorem OAI.VelocityDetection.TorusClass.measure_univ line 16
  5. instance OAI.VelocityDetection.TorusClass.(instance at line 19) line 19
  6. def OAI.VelocityDetection.TorusClass.periodic line 21

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:727 (same declaration text).

  7. def OAI.VelocityDetection.TorusClass.frame line 23

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:729 (same declaration text).

  8. def OAI.VelocityDetection.TorusClass.D line 25

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:731 (same declaration text).

  9. abbrev OAI.VelocityDetection.TorusClass.div line 27
  10. abbrev OAI.VelocityDetection.TorusClass.lap line 29
  11. theorem OAI.VelocityDetection.TorusClass.D_mul line 31
  12. theorem OAI.VelocityDetection.TorusClass.D_sub line 38
  13. theorem OAI.VelocityDetection.TorusClass.continuous_D line 43
  14. theorem OAI.VelocityDetection.TorusClass.contDiff_D line 46
  15. theorem OAI.VelocityDetection.TorusClass.integrable_continuous line 49
  16. theorem OAI.VelocityDetection.TorusClass.memLp_continuous line 52
  17. theorem OAI.VelocityDetection.TorusClass.periodic_faces line 58
  18. theorem OAI.VelocityDetection.TorusClass.integral_D_eq_zero line 68
  19. theorem OAI.VelocityDetection.TorusClass.periodic_D line 103
  20. theorem OAI.VelocityDetection.TorusClass.periodic_sub line 115
  21. theorem OAI.VelocityDetection.TorusClass.periodic_mul line 118
  22. theorem OAI.VelocityDetection.TorusClass.integral_mul_D line 121
  23. theorem OAI.VelocityDetection.TorusClass.integrable_mul_L2 line 132
  24. theorem OAI.VelocityDetection.TorusClass.integrable_sq_L2 line 136
  25. theorem OAI.VelocityDetection.TorusClass.integrable_bdd_mul line 140
  26. theorem OAI.VelocityDetection.TorusClass.integral_transport_energy line 145
  27. theorem OAI.VelocityDetection.TorusClass.integral_pressure_work line 186
  28. theorem OAI.VelocityDetection.TorusClass.integral_laplacian_energy line 207
  29. theorem OAI.VelocityDetection.TorusClass.stretching_bound line 224
  30. abbrev OAI.VelocityDetection.TorusClass.energy line 247
  31. abbrev OAI.VelocityDetection.TorusClass.work line 249
  32. structure OAI.VelocityDetection.TorusClass.SliceH2 line 251
  33. structure OAI.VelocityDetection.TorusClass.PressureH1 line 258
  34. theorem OAI.VelocityDetection.TorusClass.integrable_energy line 264
  35. theorem OAI.VelocityDetection.TorusClass.integrable_work line 268
  36. theorem OAI.VelocityDetection.TorusClass.energy_nonneg line 274
  37. theorem OAI.VelocityDetection.TorusClass.difference_energy_inequality line 277
  38. theorem OAI.VelocityDetection.TorusClass.continuous_slice line 368
  39. theorem OAI.VelocityDetection.TorusClass.continuous_time line 375
  40. theorem OAI.VelocityDetection.TorusClass.integral_continuous line 381
  41. theorem OAI.VelocityDetection.TorusClass.integral_hasDerivAt line 395