`BookProof.Howland.hasDerivAt_autonomize` (f : ℝ → E → E) (x : ℝ → E) (t : ℝ) (hx : HasDerivAt x (f t (x t)) t) : HasDerivAt (fun s : ℝ => ((s, x s) : ℝ × E)) (autonomize f (t, x t

Proved

BookProof.Howland.hasDerivAt_autonomize

by leonardopedro · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterHowlandAutonomization.

BookProof.Howland.hasDerivAt_autonomize (f : ℝ → E → E) (x : ℝ → E) (t : ℝ) (hx : HasDerivAt x (f t (x t)) t) : HasDerivAt (fun s : ℝ => ((s, x s) : ℝ × E)) (autonomize f (t, x t)) t

Formalization note: Lean 4 identifier BookProof.Howland.hasDerivAt_autonomize.

Preamble

-- Generated from ChapterHowlandAutonomization.lean — theorem BookProof.Howland.hasDerivAt_autonomize
import Mathlib
import Definitions.Def_ChapterHowlandAutonomization
open BookProof.Howland



open MeasureTheory

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

Formal statement

theorem BookProof.Howland.hasDerivAt_autonomize (f : ℝ → E → E) (x : ℝ → E) (t : ℝ)
    (hx : HasDerivAt x (f t (x t)) t) :
    HasDerivAt (fun s : ℝ => ((s, x s) : ℝ × E)) (autonomize f (t, x t)) t := by sorry

View graph