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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Global smooth dependence for a finite-dimensional autonomous flow. The proof iterates the short-time implicit-function construction.

  1. theorem OAI.ForcedComputation.Flow.flow_add line 18
  2. def OAI.ForcedComputation.Flow.flowSteps line 34
  3. theorem OAI.ForcedComputation.Flow.flowSteps_eq line 39
  4. theorem OAI.ForcedComputation.Flow.flowSteps_contDiffAt line 52
  5. theorem OAI.ForcedComputation.Flow.flow_contDiff line 67

    Source documentation

    An actual global flow of a smooth globally Lipschitz finite-dimensional field is jointly smooth in elapsed time and the initial point.

    theorem flow_contDiff (Z : C(E, E))
    (hZ : ContDiff ℝ ∞ (Z : E → E)) {L : ℝ≥0} (hL : LipschitzWith L Z)
    {Ψ : ℝ → E → E}
    (hΨ : ∀ t x, HasDerivAt (fun s => Ψ s x) (Z (Ψ t x)) t)
    (hzero : ∀ x, Ψ 0 x = x) :
    ContDiff ℝ ∞ (fun p : ℝ × E => Ψ p.1 p.2) := by
…