def levelParameterObjective (α : ℝ) : ℝ

Definition 3.71: the level-parameter objective is the chapter's scalar iteration-cap factor α ↦ α (1 - α)^2 (2 - α), equivalently (1 - α)^2 (1 - (1 - α)^2), on [0, 1].

noncomputable def optimalLevelParameter : ℝ

The optimal level parameter α* = 1 / (2 + √2).

theorem one_sub_optimalLevelParameter_eq : 1 - optimalLevelParameter = √2 / 2

The displayed optimizer satisfies the exact bridge identity 1 - α* = √2 / 2.

theorem levelParameterObjective_eq_quarter_sub_sq (α : ℝ) : levelParameterObjective α = 1 / 4 - ((1 - α) ^ 2 - 1 / 2) ^ 2

Completing the square rewrites the level-parameter objective in the canonical form used to prove its maximum.

theorem levelParameterObjective_pos {α : ℝ} (hα : α ∈ Set.Ioo 0 1) : 0 < levelParameterObjective α

On the admissible interval (0, 1), the level-parameter objective is strictly positive.

theorem optimalLevelParameterObjective_eq_quarter : levelParameterObjective optimalLevelParameter = 1 / 4

Evaluating the level-parameter objective at the displayed optimizer gives the extremal value 1 / 4.

theorem optimalLevelParameter_mem_Ioo : optimalLevelParameter ∈ Set.Ioo 0 1

The displayed optimizer lies in the admissible interval (0, 1).

theorem optimalLevelParameter_mem_Icc : optimalLevelParameter ∈ Set.Icc 0 1

The displayed optimizer lies in the feasible interval [0, 1].

theorem optimalLevelParameter_isMaxOn : IsMaxOn levelParameterObjective (Set.Icc 0 1) optimalLevelParameter

The displayed optimizer maximizes the level-parameter objective on [0, 1].