J_curv

formal source

 129The total curvature cost is then 8 × (λ²/4) = 2λ².
 130
 131This is the curvature functional J_curv(λ). -/
 132noncomputable def J_curv (lam : ℝ) : ℝ := 2 * lam^2
 133
 134/-- J_curv(0) = 0. -/
 135theorem J_curv_zero : J_curv 0 = 0 := by simp [J_curv]
 136
 137/-- J_curv is non-negative. -/
 138theorem J_curv_nonneg (lam : ℝ) : J_curv lam ≥ 0 := by
 139  unfold J_curv
 140  have h : lam^2 ≥ 0 := sq_nonneg lam
 141  linarith
 142
 143/-! ## Part 3: Curvature Extremum Condition -/
 144
 145/-- **THE EXTREMUM EQUATION**: J_bit = J_curv(λ).
 146
 147Solving for λ: J_bit = 2λ² ⟹ λ = √(J_bit/2). -/
 148noncomputable def lambda_rec_from_Jbit : ℝ := sqrt (J_bit_val / 2)
 149
 150/-- λ_rec_from_Jbit > 0 since J_bit > 0. -/
 151theorem lambda_rec_from_Jbit_pos : lambda_rec_from_Jbit > 0 := by
 152  unfold lambda_rec_from_Jbit
 153  exact sqrt_pos.mpr (div_pos J_bit_pos (by norm_num : (2 : ℝ) > 0))
 154
 155/-- At λ_rec_from_Jbit, the extremum condition holds. -/
 156theorem extremum_condition : J_curv lambda_rec_from_Jbit = J_bit_val := by
 157  unfold J_curv lambda_rec_from_Jbit
 158  have h : J_bit_val / 2 ≥ 0 := le_of_lt (div_pos J_bit_pos (by norm_num))
 159  rw [sq_sqrt h]
 160  ring
 161
 162/-- The extremum is unique: if J_curv(λ) = J_bit for λ > 0, then λ = λ_rec_from_Jbit. -/