theorem maxTypeObjective_lower_tangent_quadratic_of_components {ι : Type u_1} [Fintype ι] [Nonempty ι] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (fi : ι → E → ℝ) (μ : ℝ) (hstrong : ∀ (i : ι), StrongConvexOn Set.univ μ (fi i)) (hcontDiff : ∀ (i : ι), ContDiff ℝ 1 (fi i)) (x xBar : E) : maxTypeObjective fi x ≥ maxTypeAffineApproximation fi xBar x + μ / 2 * ‖x - xBar‖ ^ 2

If each component is μ-strongly convex on the whole space and C¹, then the finite max-type objective satisfies the corresponding quadratic lower tangent bound relative to maxTypeAffineApproximation fi xBar.

theorem maxTypeObjective_upper_tangent_quadratic_of_components {ι : Type u_1} [Fintype ι] [Nonempty ι] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (fi : ι → E → ℝ) (L : NNReal) (hcontDiff : ∀ (i : ι), ContDiff ℝ 1 (fi i)) (hgrad_lipschitz : ∀ (i : ι), LipschitzWith L (gradient (fi i))) (x xBar : E) : maxTypeObjective fi x ≤ maxTypeAffineApproximation fi xBar x + ↑L / 2 * ‖x - xBar‖ ^ 2

If each component is C¹ and has L-Lipschitz gradient, then the finite max-type objective satisfies the corresponding quadratic upper tangent bound relative to maxTypeAffineApproximation fi xBar.

theorem maxTypeObjective_quadratic_bounds_of_components_mem {ι : Type u_1} [Fintype ι] [Nonempty ι] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (fi : ι → E → ℝ) (μ L : ℝ) (hfi : ∀ (i : ι), fi i ∈ setOf (IsStrongConvexSmoothObjective μ L)) (x xBar : E) : maxTypeObjective fi x ≥ maxTypeAffineApproximation fi xBar x + μ / 2 * ‖x - xBar‖ ^ 2 ∧ maxTypeObjective fi x ≤ maxTypeAffineApproximation fi xBar x + L / 2 * ‖x - xBar‖ ^ 2

Lemma 2.18 in the chapter notation surface: if each component of a finite max-type objective lies in 𝓢[μ, L]¹¹, then the max-type function satisfies the corresponding lower and upper quadratic bounds relative to its canonical affine approximation maxTypeAffineApproximation fi xBar.