OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/BalancedEuclidean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The compact Euclidean solution uses the prescribed coordinate residual. The coordinate change commutes with all spatial derivatives and with the right time derivative on the nonnegative time axis.

  1. theorem OAI.ForcedComputation.CompactEuclidean.velocity_residual line 16
  2. theorem OAI.ForcedComputation.CompactEuclidean.compact_prescribed_solution line 39