OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.Cylinder.Space line 14

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

  2. abbrev OAI.VelocityDetection.Cylinder.Vect line 16

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

  3. def OAI.VelocityDetection.Cylinder.measure line 18

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

  4. def OAI.VelocityDetection.Cylinder.periodic line 20

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

  5. def OAI.VelocityDetection.Cylinder.frame line 22

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

  6. def OAI.VelocityDetection.Cylinder.D line 24

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

  7. abbrev OAI.VelocityDetection.Cylinder.div line 26
  8. abbrev OAI.VelocityDetection.Cylinder.lap line 28
  9. theorem OAI.VelocityDetection.Cylinder.D_mul line 30
  10. theorem OAI.VelocityDetection.Cylinder.D_sub line 37
  11. theorem OAI.VelocityDetection.Cylinder.continuous_D line 42
  12. theorem OAI.VelocityDetection.Cylinder.contDiff_D line 45
  13. theorem OAI.VelocityDetection.Cylinder.differential_horizontal line 48
  14. theorem OAI.VelocityDetection.Cylinder.hasDerivAt_vertical line 63
  15. theorem OAI.VelocityDetection.Cylinder.integral_mul_D line 70
  16. theorem OAI.VelocityDetection.Cylinder.periodic_D line 112
  17. theorem OAI.VelocityDetection.Cylinder.periodic_sub line 128
  18. theorem OAI.VelocityDetection.Cylinder.periodic_mul line 131
  19. theorem OAI.VelocityDetection.Cylinder.integrable_mul_L2 line 134
  20. theorem OAI.VelocityDetection.Cylinder.integrable_sq_L2 line 138
  21. theorem OAI.VelocityDetection.Cylinder.integrable_bdd_mul line 142
  22. theorem OAI.VelocityDetection.Cylinder.integral_transport_energy line 147
  23. theorem OAI.VelocityDetection.Cylinder.integral_pressure_work line 190
  24. theorem OAI.VelocityDetection.Cylinder.integral_laplacian_energy line 211
  25. theorem OAI.VelocityDetection.Cylinder.stretching_bound line 228
  26. abbrev OAI.VelocityDetection.Cylinder.energy line 251
  27. abbrev OAI.VelocityDetection.Cylinder.work line 253
  28. structure OAI.VelocityDetection.Cylinder.SliceH2 line 255

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

  29. structure OAI.VelocityDetection.Cylinder.PressureH1 line 262

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

  30. theorem OAI.VelocityDetection.Cylinder.integrable_energy line 268
  31. theorem OAI.VelocityDetection.Cylinder.integrable_work line 272
  32. theorem OAI.VelocityDetection.Cylinder.energy_nonneg line 278
  33. theorem OAI.VelocityDetection.Cylinder.difference_energy_inequality line 281
  34. theorem OAI.VelocityDetection.Cylinder.twoAtLeastTwo line 372

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

  35. abbrev OAI.VelocityDetection.Cylinder.LpSpace line 374

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

  36. abbrev OAI.VelocityDetection.Cylinder.L2Space line 377

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

  37. theorem OAI.VelocityDetection.Cylinder.energy_eq_L2 line 381
  38. theorem OAI.VelocityDetection.Cylinder.work_eq_L2 line 393
  39. theorem OAI.VelocityDetection.Cylinder.energy_hasDerivWithinAt line 407
  40. theorem OAI.VelocityDetection.Cylinder.continuousOn_energy line 419