Documentation

LeanPool.NavierStokesAndEuler.Euler.BoundedFlowContinuity

The actual bounded Lipschitz flow is jointly continuous in both times and the initial point. Reversing its two time arguments gives its genuine continuous inverse, so each fixed-time map is a homeomorphism.

source
theorem EulerBoundedLipschitzFlow.Data.flow_distance {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s t s₀ t₀ : ℝ) (x x₀ : E) :
dist (V.flow s t x) (V.flow s₀ t₀ x₀) ≤ (dist x x₀ + ↑V.speedBound * |s - s₀|) * Real.exp (↑V.lipschitzConstant * |t - s|) + ↑V.speedBound * |t - t₀|
source
theorem EulerBoundedLipschitzFlow.Data.flow_joint_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) :
Continuous fun (p : ℝ × ℝ × E) => V.flow p.1 p.2.1 p.2.2
source
noncomputable def EulerBoundedLipschitzFlow.Data.flowHomeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s t : ℝ) :
E ≃ₜ E

Flow homeomorph, bundling toFun, invFun, left_inv, right_inv and the required compatibility proofs.

Equations
  • V.flowHomeomorph s t = { toFun := V.flow s t, invFun := V.flow t s, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
    source
    noncomputable def EulerBoundedLipschitzFlow.Data.forward {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (t : ℝ) (x : E) :
    E

    Forward, given by V.flow 0 t x.

    Equations
    Instances For
      source
      noncomputable def EulerBoundedLipschitzFlow.Data.backward {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (t : ℝ) (x : E) :
      E

      Backward, given by V.flow t 0 x.

      Equations
      Instances For
        source
        @[simp]
        theorem EulerBoundedLipschitzFlow.Data.backward_forward {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (t : ℝ) (x : E) :
        V.backward t (V.forward t x) = x
        source
        @[simp]
        theorem EulerBoundedLipschitzFlow.Data.forward_backward {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (t : ℝ) (x : E) :
        V.forward t (V.backward t x) = x
        source
        @[simp]
        theorem EulerBoundedLipschitzFlow.Data.forward_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (x : E) :
        V.forward 0 x = x
        source
        @[simp]
        theorem EulerBoundedLipschitzFlow.Data.backward_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (x : E) :
        V.backward 0 x = x
        source
        theorem EulerBoundedLipschitzFlow.Data.forward_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (t : ℝ) (x : E) :
        HasDerivAt (fun (s : ℝ) => V.forward s x) (V.velocity t (V.forward t x)) t
        source
        theorem EulerBoundedLipschitzFlow.Data.forward_joint_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) :
        Continuous (Function.uncurry V.forward)
        source
        theorem EulerBoundedLipschitzFlow.Data.backward_joint_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) :
        Continuous (Function.uncurry V.backward)
        source
        theorem EulerBoundedLipschitzFlow.Data.forward_displacement {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (t : ℝ) (x : E) :
        dist (V.forward t x) x ≤ ↑V.speedBound * |t|