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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Identification of the local implicit Picard family with an actual flow. The short-time uniqueness proof is a norm estimate in the compact path space.

  1. theorem OAI.ForcedComputation.Flow.postcompose_norm_sub_le line 17
  2. theorem OAI.ForcedComputation.Flow.picard_solution_unique line 26
  3. def OAI.ForcedComputation.Flow.orbitPath line 53
  4. theorem OAI.ForcedComputation.Flow.orbitPath_apply line 61
  5. theorem OAI.ForcedComputation.Flow.orbitPath_picard line 66
  6. theorem OAI.ForcedComputation.Flow.flow_contDiffAt_short line 97

    Source documentation

    Joint smoothness in short elapsed time and the initial point.

    theorem flow_contDiffAt_short (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) (τ : ℝ) (x : E)
    (hτ : |τ| * (L : ℝ) < 1) :
    ContDiffAt ℝ ∞ (fun p : ℝ × E => Ψ p.1 p.2) (τ, x) := by
…