OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CylinderEnergy.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VelocityDetection.Cylinder.periodic_eq_zero_of_ae line 14
  2. theorem OAI.VelocityDetection.Cylinder.eq_zero_of_energy_zero line 39
  3. theorem OAI.VelocityDetection.Cylinder.energy_gronwall_zero line 54
  4. theorem OAI.VelocityDetection.Cylinder.difference_zero line 84
  5. theorem OAI.VelocityDetection.Cylinder.lap_sub line 125
  6. theorem OAI.VelocityDetection.Cylinder.SliceH2.sub line 132
  7. theorem OAI.VelocityDetection.Cylinder.PressureH1.sub line 151
  8. theorem OAI.VelocityDetection.Cylinder.measure_univ line 161
  9. theorem OAI.VelocityDetection.Cylinder.fderiv_eq_zero_of_D_eq_zero line 170
  10. theorem OAI.VelocityDetection.Cylinder.pressure_zero_of_gradient_zero line 183
  11. structure OAI.VelocityDetection.Cylinder.EnergyRegularOn line 197
  12. def OAI.VelocityDetection.Cylinder.solvesOn line 213
  13. theorem OAI.VelocityDetection.Cylinder.unique_velocity_and_pressure line 220
  14. def OAI.VelocityDetection.Cylinder.dt line 307

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

  15. theorem OAI.VelocityDetection.Cylinder.spaceOuterMeasureClass line 310

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

  16. def OAI.VelocityDetection.Cylinder.continuousL2On line 313

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

  17. def OAI.VelocityDetection.Cylinder.continuousH2On line 319

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

  18. def OAI.VelocityDetection.Cylinder.continuousH1On line 325

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

  19. def OAI.VelocityDetection.Cylinder.C1L2On line 329

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

  20. structure OAI.VelocityDetection.Cylinder.ComparisonClass line 340

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

  21. theorem OAI.VelocityDetection.Cylinder.ComparisonClass.energyRegularOn line 362
  22. def OAI.VelocityDetection.Cylinder.navierStokes line 370
  23. theorem OAI.VelocityDetection.Cylinder.comparison_unique line 377
  24. def OAI.VelocityDetection.Cylinder.join line 393

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

  25. def OAI.VelocityDetection.Cylinder.split line 397