Continuous linear dependence on initial data for finite-window linear ODEs.

theorem AVenhance.Infra.Flow.linearFlow_continuousLinearMap_on_window {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : ℝ → E →L[ℝ] E) {V : ℝ → E → ℝ → E} (hV : IsFlowOn (fun (r : ℝ) (z : E) => (A r) z) V) {a d s t M : ℝ} (hs : s ∈ Set.Ioo a d) (ht : t ∈ Set.Icc a d) (hM0 : 0 ≤ M) (hM : ∀ r ∈ Set.Icc a d, ‖A r‖ ≤ M) : ∃ (J : E →L[ℝ] E), ∀ (v : E), J v = V t v s

A global flow of a linear system is a continuous linear map in its initial state at each fixed pair of times. The operator norm is controlled by the finite-window Grönwall estimate.