OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TorusClassContinuousOnEnergy.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VelocityDetection.TorusClass.continuousOn_energy line 11
  2. theorem OAI.VelocityDetection.TorusClass.energy_hasDerivAt line 16
  3. abbrev OAI.VelocityDetection.TorusClass.L2Space line 35
  4. theorem OAI.VelocityDetection.TorusClass.energy_eq_L2 line 37
  5. theorem OAI.VelocityDetection.TorusClass.periodic_eq_zero_of_ae line 49
  6. theorem OAI.VelocityDetection.TorusClass.eq_zero_of_energy_zero line 71
  7. theorem OAI.VelocityDetection.TorusClass.difference_zero line 86
  8. theorem OAI.VelocityDetection.TorusClass.lap_sub line 126
  9. theorem OAI.VelocityDetection.TorusClass.SliceH2.sub line 133
  10. theorem OAI.VelocityDetection.TorusClass.PressureH1.sub line 152
  11. theorem OAI.VelocityDetection.TorusClass.fderiv_eq_zero_of_D_eq_zero line 162
  12. theorem OAI.VelocityDetection.TorusClass.pressure_zero_of_gradient_zero line 174
  13. structure OAI.VelocityDetection.TorusClass.EnergyRegularOn line 184
  14. def OAI.VelocityDetection.TorusClass.solvesOn line 197
  15. theorem OAI.VelocityDetection.TorusClass.unique_velocity_and_pressure line 204
  16. def OAI.VelocityDetection.TorusClass.dt line 285

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

  17. structure OAI.VelocityDetection.TorusClass.ComparisonClass line 288

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

  18. theorem OAI.VelocityDetection.TorusClass.SliceH2.of_smooth_periodic line 309
  19. theorem OAI.VelocityDetection.TorusClass.PressureH1.of_smooth_periodic line 316
  20. theorem OAI.VelocityDetection.TorusClass.finite_cylinder_bound line 320
  21. theorem OAI.VelocityDetection.TorusClass.ComparisonClass.bounds line 340
  22. theorem OAI.VelocityDetection.TorusClass.ComparisonClass.energyRegularOn line 362
  23. theorem OAI.VelocityDetection.TorusClass.spatialD_eq line 370
  24. theorem OAI.VelocityDetection.TorusClass.second_spatialD_eq line 375
  25. theorem OAI.VelocityDetection.TorusClass.laplacian_eq line 383
  26. theorem OAI.VelocityDetection.TorusClass.ComparisonClass.solvesOn line 387
  27. theorem OAI.VelocityDetection.TorusClass.comparison_unique line 407