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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The spatial-clock part of the eventually stationary construction. The clock needs unit speed only along the selected planar trajectory.

  1. def OAI.ForcedComputation.spatialSuspension line 14
  2. theorem OAI.ForcedComputation.spatialSuspension_smooth line 17
  3. theorem OAI.ForcedComputation.spatialSuspension_periodic line 33
  4. def OAI.ForcedComputation.suspensionPath line 47
  5. theorem OAI.ForcedComputation.suspensionPath_hasDerivAt line 49
  6. theorem OAI.ForcedComputation.spatialSuspension_tracks line 69
  7. theorem OAI.ForcedComputation.spatialSuspension_observation line 92
  8. theorem OAI.ForcedComputation.spatialSuspension_tracks_interval line 112

    Source documentation

    An individual finite processor segment can be lifted without making any claim about the planar trajectory after that segment.

    theorem spatialSuspension_tracks_interval {V : ℝ → Plane → Plane} {g : Plane → ℝ}
    {ψ : ℝ → Plane} {Φ : ℝ → Space → Space} {K : ℝ≥0} {a b : ℝ} (x : Space)
    (hc : ContinuousOn (suspensionPath ψ) (Icc a b))
    (hp : suspensionPath ψ a = Φ a x)
    (hψ : ∀ s ∈ Ico a b, HasDerivAt ψ (V s (ψ s)) s)
    (hg : ∀ s ∈ Ico a b, g (ψ s) = 1)
    (hK : LipschitzWith K (spatialSuspension V g))
    (hΦ : IsMaterialFlow 1 (fun y => spatialSuspension V g y.2) Φ) :
    EqOn (fun s => Φ s x) (suspensionPath ψ) (Icc a b) := by
…

    Mentions: OAI.ForcedComputation.suspensionPath, OAI.ForcedComputation.spatialSuspension