An explicit extension converts one-sided derivatives on a nondegenerate closed time interval into ordinary derivatives there. It uses affine tails whose slopes are the actual endpoint derivatives.

noncomputable def EulerClosedIntervalDerivativeExtension.affineExtension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (g₀ gT : E) (T t : ℝ) : E

Affine extension, with branches according to t < 0.

Equations

• EulerClosedIntervalDerivativeExtension.affineExtension f g₀ gT T t = if t < 0 then f 0 + t • g₀ else if T < t then f T + (t - T) • gT else f t

theorem EulerClosedIntervalDerivativeExtension.affineExtension_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {g₀ gT : E} {T t : ℝ} (ht : t ∈ Set.Icc 0 T) : affineExtension f g₀ gT T t = f t

theorem EulerClosedIntervalDerivativeExtension.affineExtension_eq_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {g₀ gT : E} {T t : ℝ} (hT : 0 ≤ T) (ht : t ≤ 0) : affineExtension f g₀ gT T t = f 0 + t • g₀

theorem EulerClosedIntervalDerivativeExtension.affineExtension_eq_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {g₀ gT : E} {T t : ℝ} (hT : 0 ≤ T) (ht : T ≤ t) : affineExtension f g₀ gT T t = f T + (t - T) • gT

theorem EulerClosedIntervalDerivativeExtension.affineExtension_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {T t : ℝ} (hT : 0 < T) (ht : t ∈ Set.Icc 0 T) (hf : HasDerivWithinAt f (g t) (Set.Icc 0 T) t) : HasDerivAt (affineExtension f (g 0) (g T) T) (g t) t

No continuity of the derivative is needed: the matching endpoint slopes and the one-sided derivative suffice.

theorem EulerClosedIntervalDerivativeExtension.exists_extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {T : ℝ} (hT : 0 < T) (hf : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt f (g t) (Set.Icc 0 T) t) : ∃ (F : ℝ → E), Set.EqOn F f (Set.Icc 0 T) ∧ ∀ t ∈ Set.Icc 0 T, HasDerivAt F (g t) t