theorem inf_max_set_nonempty {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (x : Fin n → ℝ) : {z : EReal | ∃ (y : Fin n → ℝ), z = max (f1 (x - y)) (f2 y)}.Nonempty

The max-value set used in the infimum is nonempty.

theorem mem_add_of_fx_lt {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} {α : EReal} {x : Fin n → ℝ} (hx : sInf {z : EReal | ∃ (y : Fin n → ℝ), z = max (f1 (x - y)) (f2 y)} < α) : x ∈ Set.image2 (fun (a b : Fin n → ℝ) => a + b) {a : Fin n → ℝ | f1 a < α} {b : Fin n → ℝ | f2 b < α}

If the infimum is below α, then the point lies in the Minkowski sum of sublevel sets.

theorem fx_lt_of_mem_add {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} {α : EReal} {x : Fin n → ℝ} (hx : x ∈ Set.image2 (fun (a b : Fin n → ℝ) => a + b) {a : Fin n → ℝ | f1 a < α} {b : Fin n → ℝ | f2 b < α}) : sInf {z : EReal | ∃ (y : Fin n → ℝ), z = max (f1 (x - y)) (f2 y)} < α

If x is a sum of sublevel points, then the infimum is below α.

theorem sublevelSet_inf_iSup_eq_add {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} : have f := fun (x : Fin n → ℝ) => sInf {z : EReal | ∃ (y : Fin n → ℝ), z = max (f1 (x - y)) (f2 y)}; ∀ (α : EReal), {x : Fin n → ℝ | f x < α} = Set.image2 (fun (x y : Fin n → ℝ) => x + y) {x : Fin n → ℝ | f1 x < α} {y : Fin n → ℝ | f2 y < α}

Text 5.8.5: Let f1, f2 be proper convex functions on ℝ^n and define f x = inf_y max { f1 (x - y), f2 y }. Then, for any α, {x | f x < α} = {x | f1 x < α} + {x | f2 x < α} (set sum).