noncomputable def coordinatewiseMax {ι : Type u} (x : ι → ℝ) : ℝ

The max function on a finite coordinate space, specializing to x ↦ max_i x i on ℝ^n.

def activeCoordinateFace {ι : Type u} [Fintype ι] (x : ι → ℝ) : Set (ι → ℝ)

The face of the standard simplex supported on the active coordinates of x, namely the indices i with coordinatewiseMax x = x i.

@[simp]

theorem mem_activeCoordinateFace_iff {ι : Type u} [Fintype ι] {x l : ι → ℝ} : l ∈ activeCoordinateFace x ↔ l ∈ stdSimplex ℝ ι ∧ ∀ (i : ι), coordinatewiseMax x ≠ x i → l i = 0

Membership in activeCoordinateFace x means belonging to the standard simplex and being supported on the active coordinates of x.

theorem coordinatewiseMax_eq_sup' {ι : Type u} [Fintype ι] [Nonempty ι] (x : ι → ℝ) : coordinatewiseMax x = Finset.univ.sup' ⋯ x

On a nonempty finite coordinate space, coordinatewiseMax x is the ordinary finite maximum over Finset.univ.

theorem le_coordinatewiseMax {ι : Type u} [Nonempty ι] [Finite ι] (x : ι → ℝ) (i : ι) : x i ≤ coordinatewiseMax x

theorem coordinatewiseMax_add_const {ι : Type u} [Nonempty ι] [Finite ι] (x : ι → ℝ) (t : ℝ) : (coordinatewiseMax fun (i : ι) => x i + t) = coordinatewiseMax x + t

@[simp]

theorem activeCoordinateFace_const_eq_stdSimplex {ι : Type u} [Fintype ι] [Nonempty ι] (α : ℝ) : (activeCoordinateFace fun (x : ι) => α) = stdSimplex ℝ ι

For a constant coordinate vector, every coordinate is active, so the active face is the whole standard simplex.

theorem euclidean_subdifferentialAt_coordinatewiseMax_eq_activeCoordinateFace {ι : Type u} [Fintype ι] [Nonempty ι] (x : EuclideanSpace ℝ ι) : euclideanSubdifferentialAt (fun (y : EuclideanSpace ℝ ι) => coordinatewiseMax y.ofLp) x = WithLp.toLp 2 '' activeCoordinateFace x.ofLp

Proposition 3.23 [Subdifferential of the max function]: the Euclidean/vector-side subdifferential of the coordinatewise maximum on ℝ^n is exactly the face of the standard simplex supported on the active coordinates.

theorem mem_euclideanSubdifferentialAt_coordinatewiseMax_toLp_iff {ι : Type u} [Fintype ι] [Nonempty ι] {x : ι → ℝ} {z : EuclideanSpace ℝ ι} : z ∈ euclideanSubdifferentialAt (fun (y : EuclideanSpace ℝ ι) => coordinatewiseMax y.ofLp) (WithLp.toLp 2 x) ↔ z.ofLp ∈ activeCoordinateFace x

Membership form of Proposition 3.23 at a coordinate vector x : ι → ℝ. This is the source-facing statement: a Euclidean vector z is a subgradient of y ↦ max_i y i at x exactly when its coordinate vector lies in the active face of the simplex at x.

theorem subdifferentialAt_coordinatewiseMax_eq_image_activeCoordinateFace {ι : Type u} [Fintype ι] [Nonempty ι] (x : EuclideanSpace ℝ ι) : subdifferentialAt (fun (y : EuclideanSpace ℝ ι) => coordinatewiseMax y.ofLp) x = ⇑(InnerProductSpace.toDualMap ℝ (EuclideanSpace ℝ ι)) '' WithLp.toLp 2 '' activeCoordinateFace x.ofLp

Continuous-dual reformulation of Proposition 3.23 obtained by applying the canonical Riesz map to the vector-side active face.

theorem euclidean_subdifferentialAt_coordinatewiseMax_const_eq_stdSimplex {ι : Type u} [Fintype ι] [Nonempty ι] (α : ℝ) : euclideanSubdifferentialAt (fun (y : EuclideanSpace ℝ ι) => coordinatewiseMax y.ofLp) (WithLp.toLp 2 fun (x : ι) => α) = WithLp.toLp 2 '' stdSimplex ℝ ι

At a constant vector α e, every coordinate is active, so the vector-side subdifferential of the max function is the whole standard simplex.

theorem subdifferentialAt_coordinatewiseMax_const_eq_image_stdSimplex {ι : Type u} [Fintype ι] [Nonempty ι] (α : ℝ) : subdifferentialAt (fun (y : EuclideanSpace ℝ ι) => coordinatewiseMax y.ofLp) (WithLp.toLp 2 fun (x : ι) => α) = ⇑(InnerProductSpace.toDualMap ℝ (EuclideanSpace ℝ ι)) '' WithLp.toLp 2 '' stdSimplex ℝ ι

Continuous-dual reformulation of the constant-vector case of Proposition 3.23.