noncomputable def quadraticInterpolationExerciseObjective (t : ℝ) : ℝ

The objective function t ↦ 1 - t * exp (-(t ^ 2)) from the quadratic interpolation exercise.

theorem quadraticInterpolationExerciseObjective_isMinOn_unitInterval : IsMinOn quadraticInterpolationExerciseObjective (Set.Icc 0 1) (√2 / 2)

Chapter02 Exercise 2.4. The function quadraticInterpolationExerciseObjective attains its minimum on Set.Icc (0 : ℝ) 1 at Real.sqrt 2 / 2.