Global solutions of continuous linear ODEs with coefficients bounded on each compact time interval.

def AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowClamp (s : ℝ) (n : ℕ) (t : ℝ) : ℝ

Clamp time to the radius-n window around a specified starting time.

Equations

• AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowClamp s n t = max (s - ↑n) (min (s + ↑n) t)

theorem AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowClamp_mem (s : ℝ) (n : ℕ) (t : ℝ) : linearWindowClamp s n t ∈ Set.Icc (s - ↑n) (s + ↑n)

theorem AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowClamp_eq_of_mem (s : ℝ) (n : ℕ) {t : ℝ} (ht : t ∈ Set.Icc (s - ↑n) (s + ↑n)) : linearWindowClamp s n t = t

theorem AVenhance.Infra.Flow.LinearGlobalExistence.exists_linearOperator_norm_bound_on_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (a d : ℝ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ Set.Icc a d, ‖A t‖ ≤ M

A continuous operator-valued function is bounded on every compact time interval.

def AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : ℝ → E →L[ℝ] E) (s : ℝ) (n : ℕ) : ℝ → E → E

Linear vector field with time clamped to a finite window.

Equations

• AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowField A s n t z = (A (AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowClamp s n t)) z

theorem AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowField_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (s : ℝ) (n : ℕ) : Continuous fun (p : ℝ × E) => linearWindowField A s n p.1 p.2

theorem AVenhance.Infra.Flow.LinearGlobalExistence.exists_linearWindowLip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (s : ℝ) (n : ℕ) : ∃ (K : NNReal), ∀ (t : ℝ), LipschitzWith K (linearWindowField A s n t)

theorem AVenhance.Infra.Flow.LinearGlobalExistence.exists_linearWindowFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (s : ℝ) (n : ℕ) : ∃ (Y : ℝ → E → ℝ → E), IsFlowOn (linearWindowField A s n) Y

noncomputable def AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (s : ℝ) (n : ℕ) : ℝ → E → ℝ → E

Chosen flow of the finite-window linear vector field.

Equations

• AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowFlow A hA s n = Classical.choose ⋯

theorem AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowFlow_isFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (s : ℝ) (n : ℕ) : IsFlowOn (linearWindowField A s n) (linearWindowFlow A hA s n)

theorem AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowFlow_spec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (s : ℝ) (n : ℕ) : (∀ (x : E), linearWindowFlow A hA s n s x s = x) ∧ (∀ (x : E), ContinuousOn (fun (t : ℝ) => linearWindowFlow A hA s n t x s) (Set.Icc (s - ↑n) (s + ↑n))) ∧ ∀ (x : E), ∀ t ∈ Set.Ioo (s - ↑n) (s + ↑n), HasDerivAt (fun (r : ℝ) => linearWindowFlow A hA s n r x s) ((A t) (linearWindowFlow A hA s n t x s)) t

theorem AVenhance.Infra.Flow.LinearGlobalExistence.linearWindowFlow_eqOn_overlap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (s : ℝ) (n m : ℕ) (hn : 0 < n) (hm : 0 < m) (x : E) : Set.EqOn (fun (t : ℝ) => linearWindowFlow A hA s n t x s) (fun (t : ℝ) => linearWindowFlow A hA s m t x s) (Set.Icc (s - ↑(min n m)) (s + ↑(min n m)))

noncomputable def AVenhance.Infra.Flow.LinearGlobalExistence.linearRadiusIndex (s t : ℝ) : ℕ

Least natural radius strictly greater than the elapsed time for a linear flow.

Equations

• AVenhance.Infra.Flow.LinearGlobalExistence.linearRadiusIndex s t = Nat.find ⋯

theorem AVenhance.Infra.Flow.LinearGlobalExistence.linearRadiusIndex_spec (s t : ℝ) : |t - s| < ↑(linearRadiusIndex s t)

noncomputable def AVenhance.Infra.Flow.LinearGlobalExistence.globalLinearFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) : ℝ → E → ℝ → E

Global linear flow obtained by patching compatible finite-window flows.

Equations

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

theorem AVenhance.Infra.Flow.LinearGlobalExistence.globalLinearFlow_initial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (s : ℝ) (x : E) : globalLinearFlow A hA s x s = x

theorem AVenhance.Infra.Flow.LinearGlobalExistence.globalLinearFlow_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (s : ℝ) (x : E) (t : ℝ) : HasDerivAt (fun (r : ℝ) => globalLinearFlow A hA r x s) ((A t) (globalLinearFlow A hA t x s)) t

theorem AVenhance.Infra.Flow.existsUnique_linearFlowOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) : ∃! V : ℝ → E → ℝ → E, IsFlowOn (fun (t : ℝ) (z : E) => (A t) z) V

A continuous time-dependent linear system has a unique global flow; no uniform-in-time bound on its operator coefficients is required.