Time regularity of a solution of an evolution equation in a tower of Banach spaces

prop:lps-smoothing: if a curve solves u' = N(u) in integral form in every space of a tower X_m, with N smooth from X_{m+2} to X_m, then the curve is C^∞ on the closed interval in every X_m, with one-sided derivatives at the endpoints.

theorem ESS.lps_hasDerivWithinAt_Icc_of_integral_banach {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a < b) {f g : ℝ → E} (hg : ContinuousOn g (Set.Icc a b)) (hid : ∀ s ∈ Set.Icc a b, ∀ t ∈ Set.Icc a b, s ≤ t → f t - f s = ∫ (τ : ℝ) in s..t, g τ) (t : ℝ) : t ∈ Set.Icc a b → HasDerivWithinAt f (g t) (Set.Icc a b) t

A curve in a Banach space that is a primitive of a function continuous on [a,b] on all subintervals is differentiable within [a,b] with that derivative.

theorem ESS.lps_ode_tower_contDiffOn {a b : ℝ} (hab : a < b) {X : ℕ → Type u_1} [(m : ℕ) → NormedAddCommGroup (X m)] [(m : ℕ) → NormedSpace ℝ (X m)] [∀ (m : ℕ), CompleteSpace (X m)] (N : (m : ℕ) → X (m + 2) → X m) (hN : ∀ (m : ℕ), ContDiff ℝ (↑⊤) (N m)) (u : (m : ℕ) → ℝ → X m) (hcont : ∀ (m : ℕ), ContinuousOn (u m) (Set.Icc a b)) (hint : ∀ (m : ℕ), ∀ s ∈ Set.Icc a b, ∀ t ∈ Set.Icc a b, s ≤ t → u m t - u m s = ∫ (τ : ℝ) in s..t, N m (u (m + 2) τ)) (n m : ℕ) : ContDiffOn ℝ (↑n) (u m) (Set.Icc a b)

Tower of Banach spaces: a curve solving the evolution equation in integral form in every space is C^n on the closed interval in every space, for every finite n (prop:lps-smoothing).