Grönwall bounds for global linear flows with coefficients bounded only on the finite time window under consideration.

theorem AVenhance.Infra.Flow.LinearWindowBounds.linearFlow_norm_bound_forward {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A : ℝ → E →L[ℝ] E} {V : ℝ → E → ℝ → E} (hV : IsFlowOn (fun (t : ℝ) (z : E) => (A t) z) V) {a d s t M : ℝ} (has : a ≤ s) (hst : s ≤ t) (htd : t ≤ d) (hM : ∀ r ∈ Set.Icc a d, ‖A r‖ ≤ M) (v : E) : ‖V t v s‖ ≤ Real.exp (M * (t - s)) * ‖v‖

theorem AVenhance.Infra.Flow.linearFlow_norm_bound_on_window {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A : ℝ → E →L[ℝ] E} {V : ℝ → E → ℝ → E} (hV : IsFlowOn (fun (t : ℝ) (z : E) => (A t) z) V) {a d s M : ℝ} (hs : s ∈ Set.Icc a d) (hM : ∀ r ∈ Set.Icc a d, ‖A r‖ ≤ M) (v : E) (t : ℝ) : t ∈ Set.Icc a d → ‖V t v s‖ ≤ Real.exp (M * |t - s|) * ‖v‖

A linear solution grows at most exponentially on a compact window, in either target-time orientation. The coefficient needs a bound only on that window.