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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A terminating evaluator for the initialized force and every mixed derivative. A single coarse time approximation chooses a valid local formula. The overlap is supplied by the fixed zero collars, including at times zero and one.

  1. theorem OAI.ForcedComputation.force_germ_of_germ line 15
  2. theorem OAI.ForcedComputation.mixedForce_eq_of_germ line 21
  3. def OAI.ForcedComputation.evaluateInitializedForce line 29

    Source documentation

    The two finite shear expressions are evaluated by their existing certified algorithms; the extra time test only selects between overlapping exact germs.

    def evaluateInitializedForce (loader body : Input)
    (hloader : ValidInput loader) (hbody : ValidInput body)
    (α : List (Fin 4)) (a : ℕ → ℚ) (b : ℕ → RationalSpaceTime)
    (ε : ℚ) (hε : 0 < ε) : RationalVector :=
…
  4. theorem OAI.ForcedComputation.evaluateInitializedForce_spec line 38