theorem dualNormDef_unitSphere_bddAbove_section02 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Module.Dual ℝ E) : BddAbove {r : ℝ | ∃ (x : E), ‖x‖ = 1 ∧ r = DualPairing s x}

Unit-sphere values of a dual functional are bounded above (local version).

theorem dualPairing_le_dualNormDef_mul_norm_section02 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Module.Dual ℝ E) (x : E) : DualPairing s x ≤ DualNormDef s * ‖x‖

Dual pairing is bounded by the dual norm times the primal norm (local version).

theorem strongConvexOn_lower_quadratic_of_isMinOn {E2 : Type u_1} [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (f : E2 → ℝ) (m : ℝ) (u0 : E2) (hconv : StrongConvexOn Q2 m f) (hu0mem : u0 ∈ Q2) (hu0 : IsMinOn f Q2 u0) (u : E2) : u ∈ Q2 → f u0 + m / 2 * ‖u - u0‖ ^ 2 ≤ f u

Quadratic growth at a minimizer of a strongly convex function.

theorem smoothedMaximizer_isMinOn {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (phihat d2 : E2 → ℝ) (μ : ℝ) (x : E1) (u : E2) (hU : IsSmoothedMaximizer Q2 A phihat d2 μ x u) : IsMinOn (fun (v : E2) => phihat v + μ * d2 v - (A x) v) Q2 u

Smoothed maximizers minimize the negated objective.