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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for a smooth startup and its stationary tail

All mixed derivatives are controlled by one compact transition cylinder and the periodic stationary tail. The argument works with actual germs of the fields, so it also controls derivatives across the ends of the transition.

  1. theorem OAI.ForcedComputation.mixedDerivative_eventuallyEq line 20
  2. theorem OAI.ForcedComputation.mixedDerivative_zero line 28
  3. theorem OAI.ForcedComputation.boundedMixed_of_stationary_tail line 38

    Source documentation

    A smooth periodic field which is zero before zero and stationary after one has globally bounded derivatives of every mixed order.

    theorem boundedMixed_of_stationary_tail {L : ℝ} (hL : 0 < L)
    {F G : Velocity} (hF : ContDiff ℝ ∞ F) (hG : ContDiff ℝ ∞ G)
    (hpF : SpatiallyPeriodic L F) (hpG : SpatiallyPeriodic L G)
    (htG : TimePeriodic G)
    (hleft : ∀ t, t < 0 → ∀ x, F (t, x) = 0)
    (hright : ∀ t, 1 < t → ∀ x, F (t, x) = G (t, x)) :
    BoundedMixedDerivatives F := by
…
  4. theorem OAI.ForcedComputation.residual_spatially_periodic line 69
  5. theorem OAI.ForcedComputation.startup_bounds line 85