OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarAnisotropic.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Anisotropic four-shear routes. Horizontal compression of the recorder must persist throughout the scaling stage, so the parking columns remain disjoint even when there are many instructions. All four coefficients are rational functions of the input data.

  1. def OAI.ForcedComputation.PlanarHamiltonian.diagonalScale line 17
  2. def OAI.ForcedComputation.PlanarHamiltonian.diagonalLinear line 19
  3. theorem OAI.ForcedComputation.PlanarHamiltonian.diagonalScale_hasDerivAt line 28
  4. def OAI.ForcedComputation.PlanarHamiltonian.anisotropicPotential line 39
  5. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicPotential_smooth line 45
  6. theorem OAI.ForcedComputation.PlanarHamiltonian.field_anisotropicPotential line 50
  7. def OAI.ForcedComputation.PlanarHamiltonian.normalizedOffset line 82
  8. def OAI.ForcedComputation.PlanarHamiltonian.anisotropicRoute line 85
  9. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicRoute_smooth line 88
  10. def OAI.ForcedComputation.PlanarHamiltonian.anisotropicVelocity line 95
  11. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicVelocity_smooth line 100
  12. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicVelocity_compactSupport line 109
  13. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicVelocity_integral_eq_zero line 121
  14. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicVelocity_scale line 145
  15. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicVelocity_plateau line 159
  16. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicRoute_hasDerivAt line 168
  17. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicRoute_initial line 180
  18. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicRoute_final line 190
  19. theorem OAI.ForcedComputation.PlanarHamiltonian.anisotropicRoute_bound line 198