def maxTypeObjective {ι : Type u_1} [Fintype ι] [Nonempty ι] {X : Type u_2} (fi : ι → X → ℝ) : X → ℝ

The pointwise maximum of a nonempty finite family of real-valued functions.

theorem maxTypeObjective_apply {ι : Type u_1} [Fintype ι] [Nonempty ι] {X : Type u_2} (fi : ι → X → ℝ) (x : X) : maxTypeObjective fi x = Finset.univ.sup' ⋯ fun (i : ι) => fi i x

Evaluating the max-type objective at x returns the finite maximum of the component values.

theorem maxTypeObjective_le_iff {ι : Type u_1} [Fintype ι] [Nonempty ι] {X : Type u_2} (fi : ι → X → ℝ) (x : X) (t : ℝ) : maxTypeObjective fi x ≤ t ↔ ∀ (i : ι), fi i x ≤ t

The finite maximum is bounded above by t at x exactly when every component is.

theorem maxTypeObjective_convexOn {ι : Type u_1} [Fintype ι] [Nonempty ι] {E : Type u} [AddCommMonoid E] [Module ℝ E] (s : Set E) (fi : ι → E → ℝ) (hfi : ∀ (i : ι), ConvexOn ℝ s (fi i)) : ConvexOn ℝ s (maxTypeObjective fi)

A nonempty finite maximum of convex functions is convex on the same set.

noncomputable def maxTypeAffineApproximation {ι : Type u_1} [Fintype ι] [Nonempty ι] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (fi : ι → E → ℝ) (xBar : E) : E → ℝ

Definition 2.39: the affine approximation of a finite max-type objective at xBar is the pointwise maximum of the canonical first-order Taylor models of its components at xBar.

theorem maxTypeAffineApproximation_apply_firstOrderTaylorModelAt {ι : Type u_1} [Fintype ι] [Nonempty ι] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (fi : ι → E → ℝ) (xBar x : E) : maxTypeAffineApproximation fi xBar x = Finset.univ.sup' ⋯ fun (i : ι) => firstOrderTaylorModelAt (fi i) xBar x

Evaluating the max-type affine approximation at x gives the finite maximum of the component first-order Taylor models at xBar.

theorem maxTypeAffineApproximation_apply {ι : Type u_1} [Fintype ι] [Nonempty ι] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (fi : ι → E → ℝ) (xBar x : E) : maxTypeAffineApproximation fi xBar x = Finset.univ.sup' ⋯ fun (i : ι) => fi i xBar + inner ℝ (gradient (fi i) xBar) (x - xBar)

theorem maxTypeAffineApproximation_convexOn {ι : Type u_1} [Fintype ι] [Nonempty ι] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (s : Set E) (hs : Convex ℝ s) (fi : ι → E → ℝ) (xBar : E) : ConvexOn ℝ s (maxTypeAffineApproximation fi xBar)

The affine max-type approximation is convex on every convex set.