Continuous derivative jets on a closed interval

On a nondegenerate closed time interval, derivatives at the endpoints are one-sided. An interior derivative with a continuous extension to the closed interval is the derivative within that interval, including at its endpoints. Applying this observation successively identifies every field of a continuous derivative jet with iteratedDerivWithin.

The jet criterion contDiffOn_Icc_iff_exists_continuous_jet characterizes finite-order smoothness on a closed interval using only continuous fields and ordinary interior derivatives. It allows time derivatives of functions on closed slabs to be specified by continuous extensions without choosing an extension of the function outside the slab. The codomain may itself be a space of continuous multilinear maps.

The endpoint argument uses Mathlib's hasFDerivWithinAt_closure_of_tendsto_fderiv; higher orders use iteratedDerivWithin_succ and the native criterion for ContDiffOn in terms of iterated derivatives. No completeness assumption on the codomain is needed.

ContDiffOn.isBounded_image_deriv bounds the derivative of a C¹ function on a closed interval: it agrees with the continuous within-interval derivative away from the two endpoints.

theorem TauCeti.hasDerivWithinAt_Icc_of_continuousOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {f g : ℝ → F} (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) (hg : ContinuousOn g (Set.Icc a b)) (hd : ∀ x ∈ Set.Ioo a b, HasDerivAt f (g x) x) {x : ℝ} (hx : x ∈ Set.Icc a b) : HasDerivWithinAt f (g x) (Set.Icc a b) x

A continuous extension of an interior derivative is the derivative within the closed interval, also at its two endpoints.

theorem TauCeti.eqOn_iteratedDerivWithin_Icc_of_continuous_jet {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {f : ℝ → F} (hab : a < b) {n : ℕ} {J : ℕ → ℝ → F} (hzero : Set.EqOn (J 0) f (Set.Icc a b)) (hc : ∀ j ≤ n, ContinuousOn (J j) (Set.Icc a b)) (hd : ∀ j < n, ∀ x ∈ Set.Ioo a b, HasDerivAt (J j) (J (j + 1) x) x) {j : ℕ} (hj : j ≤ n) : Set.EqOn (iteratedDerivWithin j f (Set.Icc a b)) (J j) (Set.Icc a b)

Every field in a finite continuous interior derivative jet is the corresponding iterated derivative within the closed interval. In particular its endpoint values are canonical.

theorem TauCeti.contDiffOn_Icc_of_continuous_jet {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {f : ℝ → F} (hab : a < b) {n : ℕ} {J : ℕ → ℝ → F} (hzero : Set.EqOn (J 0) f (Set.Icc a b)) (hc : ∀ j ≤ n, ContinuousOn (J j) (Set.Icc a b)) (hd : ∀ j < n, ∀ x ∈ Set.Ioo a b, HasDerivAt (J j) (J (j + 1) x) x) : ContDiffOn ℝ (↑n) f (Set.Icc a b)

A finite continuous derivative jet in the interior yields smoothness up to both endpoints. Only the jet values on the closed interval matter.

theorem TauCeti.contDiffOn_Icc_iff_exists_continuous_jet {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {f : ℝ → F} (hab : a < b) {n : ℕ} : ContDiffOn ℝ (↑n) f (Set.Icc a b) ↔ ∃ (J : ℕ → ℝ → F), Set.EqOn (J 0) f (Set.Icc a b) ∧ (∀ j ≤ n, ContinuousOn (J j) (Set.Icc a b)) ∧ ∀ j < n, ∀ x ∈ Set.Ioo a b, HasDerivAt (J j) (J (j + 1) x) x

Finite-order smoothness on a nondegenerate closed interval is equivalent to the existence of continuous derivative fields satisfying the ordinary derivative identities in the interior. There is no condition on the fields outside the interval or above the specified order.

theorem ContDiffOn.isBounded_image_deriv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n f (Set.Icc a b)) (hn : 1 ≤ n) : Bornology.IsBounded (deriv f '' Set.Icc a b)

The derivative of a function that is C¹ on a closed interval has bounded image on that interval. At the two endpoints deriv f may differ from the one-sided derivative, but these contribute only two values.