OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/ScalarBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Constant and affine barriers give the quantitative scalar estimates used during injection and stirring.

  1. theorem OAI.ForcedComputation.VelocityDetector.scalarGenerator_const line 13
  2. theorem OAI.ForcedComputation.VelocityDetector.affine_solution line 18
  3. theorem OAI.ForcedComputation.VelocityDetector.TorusScalarSolution.upper_bound line 28
  4. theorem OAI.ForcedComputation.VelocityDetector.TorusScalarSolution.absolute_bound line 35
  5. theorem OAI.ForcedComputation.VelocityDetector.TorusScalarSolution.stability line 54

    Source documentation

    A residual bound gives a pointwise error bound, including an initial error.

    theorem TorusScalarSolution.stability {T ν : ℝ} {a : ℝ → Plane → Plane}
    {h k w v : ℝ → Plane → ℝ} {w₀ v₀ : Plane → ℝ}
    (hw : TorusScalarSolution T ν a h w w₀)
    (hv : TorusScalarSolution T ν a k v v₀) (hT : 0 ≤ T) (hν : 0 ≤ ν)
    {E D : ℝ} (hres : ∀ t ∈ Icc 0 T, ∀ x, |h t x - k t x| ≤ D)
    (hinit : ∀ x, |w₀ x - v₀ x| ≤ E) :
    ∀ t ∈ Icc 0 T, ∀ x, |w t x - v t x| ≤ E + D * t :=
…

    Mentions: OAI.ForcedComputation.VelocityDetector.TorusScalarSolution