Global existence for continuous, uniformly globally Lipschitz ODE fields.

def AVenhance.Infra.Flow.GlobalExistence.clampPoint (a b : ℝ) (hab : a ≤ b) (t : ℝ) : ↑(Set.Icc a b)

Clamp a real parameter to a nonempty closed interval.

Equations

• AVenhance.Infra.Flow.GlobalExistence.clampPoint a b hab t = ⟨max a (min b t), ⋯⟩

def AVenhance.Infra.Flow.GlobalExistence.extendCurve {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (u : C(↑(Set.Icc a b), E)) : ℝ → E

Extend an interval-valued continuous curve constantly past its endpoints.

Equations

• AVenhance.Infra.Flow.GlobalExistence.extendCurve hab u t = u (AVenhance.Infra.Flow.GlobalExistence.clampPoint a b hab t)

theorem AVenhance.Infra.Flow.GlobalExistence.continuous_extendCurve {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (u : C(↑(Set.Icc a b), E)) : Continuous (extendCurve hab u)

theorem AVenhance.Infra.Flow.GlobalExistence.extendCurve_eq_of_mem {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (u : C(↑(Set.Icc a b), E)) {t : ℝ} (ht : t ∈ Set.Icc a b) : extendCurve hab u t = u ⟨t, ht⟩

def AVenhance.Infra.Flow.GlobalExistence.curveRhs {E : Type u_1} [NormedAddCommGroup E] (b : ℝ → E → E) {a d : ℝ} (had : a ≤ d) (u : C(↑(Set.Icc a d), E)) (t : ℝ) : E

Evaluate the vector field along the clamped extension of a curve.

Equations

• AVenhance.Infra.Flow.GlobalExistence.curveRhs b had u t = b t (AVenhance.Infra.Flow.GlobalExistence.extendCurve had u t)

theorem AVenhance.Infra.Flow.GlobalExistence.continuous_curveRhs {E : Type u_1} [NormedAddCommGroup E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {a d : ℝ} (had : a ≤ d) (u : C(↑(Set.Icc a d), E)) : Continuous (curveRhs b had u)

noncomputable def AVenhance.Infra.Flow.GlobalExistence.volterra {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {a d : ℝ} (had : a ≤ d) (s : ℝ) (x : E) : C(↑(Set.Icc a d), E) → C(↑(Set.Icc a d), E)

Volterra integral operator for the initial-value problem on a compact interval.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Flow.GlobalExistence.volterra_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {a d : ℝ} (had : a ≤ d) (s : ℝ) (x : E) (u : C(↑(Set.Icc a d), E)) (t : ↑(Set.Icc a d)) : (volterra b hb had s x u) t = x + ∫ (r : ℝ) in s..↑t, curveRhs b had u r

theorem AVenhance.Infra.Flow.GlobalExistence.dist_volterra_rhs_le {E : Type u_1} [NormedAddCommGroup E] (b : ℝ → E → E) {a d : ℝ} (had : a ≤ d) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) (u v : C(↑(Set.Icc a d), E)) (t : ↑(Set.Icc a d)) : dist (curveRhs b had u ↑t) (curveRhs b had v ↑t) ≤ ↑K * dist (u t) (v t)

theorem AVenhance.Infra.Flow.GlobalExistence.dist_iterate_volterra_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {a d : ℝ} (had : a ≤ d) {s : ℝ} (hs : s ∈ Set.Icc a d) (x : E) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) (u v : C(↑(Set.Icc a d), E)) (n : ℕ) (t : ↑(Set.Icc a d)) : dist (((volterra b hb had s x)^[n] u) t) (((volterra b hb had s x)^[n] v) t) ≤ (↑K * |↑t - s|) ^ n / ↑n.factorial * dist u v

theorem AVenhance.Infra.Flow.GlobalExistence.dist_iterate_volterra_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {a d : ℝ} (had : a ≤ d) {s : ℝ} (hs : s ∈ Set.Icc a d) (x : E) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) (u v : C(↑(Set.Icc a d), E)) (n : ℕ) : dist ((volterra b hb had s x)^[n] u) ((volterra b hb had s x)^[n] v) ≤ (↑K * max (d - s) (s - a)) ^ n / ↑n.factorial * dist u v

theorem AVenhance.Infra.Flow.GlobalExistence.exists_contracting_volterra_iterate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {a d : ℝ} (had : a ≤ d) {s : ℝ} (hs : s ∈ Set.Icc a d) (x : E) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) : ∃ (n : ℕ) (Q : NNReal), ContractingWith Q (volterra b hb had s x)^[n]

theorem AVenhance.Infra.Flow.GlobalExistence.exists_finite_integralCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) (s : ℝ) (x : E) (n : ℕ) : ∃ (γ : ℝ → E), Continuous γ ∧ γ s = x ∧ ∀ t ∈ Set.Ioo (s - ↑n) (s + ↑n), HasDerivAt γ (b t (γ t)) t

noncomputable def AVenhance.Infra.Flow.GlobalExistence.finiteCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) (s : ℝ) (x : E) (n : ℕ) : ℝ → E

Integral curve constructed on a finite time window about the starting time.

Equations

• AVenhance.Infra.Flow.GlobalExistence.finiteCurve b hb hLip s x n = Classical.choose ⋯

theorem AVenhance.Infra.Flow.GlobalExistence.finiteCurve_spec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) (s : ℝ) (x : E) (n : ℕ) : Continuous (finiteCurve b hb hLip s x n) ∧ finiteCurve b hb hLip s x n s = x ∧ ∀ t ∈ Set.Ioo (s - ↑n) (s + ↑n), HasDerivAt (finiteCurve b hb hLip s x n) (b t (finiteCurve b hb hLip s x n t)) t

theorem AVenhance.Infra.Flow.GlobalExistence.finiteCurves_eqOn_overlap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) (s : ℝ) (x : E) (n m : ℕ) (hn : 0 < n) (hm : 0 < m) : Set.EqOn (finiteCurve b hb hLip s x n) (finiteCurve b hb hLip s x m) (Set.Icc (s - ↑(min n m)) (s + ↑(min n m)))

noncomputable def AVenhance.Infra.Flow.GlobalExistence.radiusIndex (s t : ℝ) : ℕ

Least natural radius strictly greater than the elapsed time.

Equations

• AVenhance.Infra.Flow.GlobalExistence.radiusIndex s t = Nat.find ⋯

theorem AVenhance.Infra.Flow.GlobalExistence.abs_lt_radiusIndex (s t : ℝ) : |t - s| < ↑(radiusIndex s t)

theorem AVenhance.Infra.Flow.GlobalExistence.radiusIndex_pos (s t : ℝ) : 0 < radiusIndex s t

noncomputable def AVenhance.Infra.Flow.GlobalExistence.globalIntegralCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) (s : ℝ) (x : E) : ℝ → E

Global integral curve obtained from compatible finite-window constructions.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Flow.GlobalExistence.globalIntegralCurve_initial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) (s : ℝ) (x : E) : globalIntegralCurve b hb hLip s x s = x

theorem AVenhance.Infra.Flow.GlobalExistence.globalIntegralCurve_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (b t)) (s : ℝ) (x : E) (t : ℝ) : HasDerivAt (globalIntegralCurve b hb hLip s x) (b t (globalIntegralCurve b hb hLip s x t)) t

theorem AVenhance.Infra.Flow.existsUnique_flowOn_uniform {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (b : ℝ → E → E) (hb : Continuous fun (p : ℝ × E) => b p.1 p.2) (hLip : ∃ (K : NNReal), ∀ (t : ℝ), LipschitzWith K (b t)) : ∃! Y : ℝ → E → ℝ → E, IsFlowOn b Y

Every continuous uniformly globally Lipschitz vector field on a complete normed state space has a unique characterized global flow.

theorem AVenhance.Infra.Flow.existsUnique_flow (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb : Continuous fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (hL : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) : ∃! X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2, IsFlow b X

Every continuous vector field with a uniform global spatial Lipschitz bound has a unique global flow.