theorem exists_fiber_lt_of_sInf_lt {n : ℕ} {F : Set ((Fin n → ℝ) × ℝ)} {x : Fin n → ℝ} {α : ℝ} (h : sInf {μ : ℝ | (x, μ) ∈ F} < α) (hne : {μ : ℝ | (x, μ) ∈ F}.Nonempty) : ∃ (μ : ℝ), (x, μ) ∈ F ∧ μ < α

From a strict upper bound on the infimum of a fiber, pick a point below it.

theorem convexOn_inf_section_of_convex_of_nonempty_bddBelow {n : ℕ} {F : Set ((Fin n → ℝ) × ℝ)} (hF : Convex ℝ F) (hne : ∀ (x : Fin n → ℝ), {μ : ℝ | (x, μ) ∈ F}.Nonempty) (hbdd : ∀ (x : Fin n → ℝ), BddBelow {μ : ℝ | (x, μ) ∈ F}) : ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => sInf {μ : ℝ | (x, μ) ∈ F}

If every fiber is nonempty and bounded below, the inf-section is convex.

theorem exists_fiber_lt_of_sInf_lt_ereal {n : ℕ} {F : Set ((Fin n → ℝ) × ℝ)} {x : Fin n → ℝ} {α : ℝ} (h : sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ F}) < ↑α) : ∃ (μ : ℝ), (x, μ) ∈ F ∧ ↑μ < ↑α

From a strict upper bound on the EReal-infimum of a fiber, pick a real point below it.

theorem convex_combo_mem_F {n : ℕ} {F : Set ((Fin n → ℝ) × ℝ)} (hF : Convex ℝ F) {x y : Fin n → ℝ} {μ ν a b : ℝ} (hx : (x, μ) ∈ F) (hy : (y, ν) ∈ F) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : (a • x + b • y, a * μ + b * ν) ∈ F

Convexity of F gives closure under convex combinations.

theorem strict_ineq_inf_section_ereal {n : ℕ} {F : Set ((Fin n → ℝ) × ℝ)} (hF : Convex ℝ F) {x y : Fin n → ℝ} {α β t : ℝ} (hfx : sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ F}) < ↑α) (hfy : sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (y, μ) ∈ F}) < ↑β) (ht0 : 0 < t) (ht1 : t < 1) : sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | ((1 - t) • x + t • y, μ) ∈ F}) < ↑(1 - t) * ↑α + ↑t * ↑β

Strict inequality for the inf-section in the EReal setting.

theorem convexOn_inf_section_of_convex {n : ℕ} {F : Set ((Fin n → ℝ) × ℝ)} (hF : Convex ℝ F) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ F})

Theorem 5.3: Let F be a convex set in R^{n+1}, and define f x = inf { μ | (x, μ) ∈ F }, interpreted in EReal so empty fibers give +∞. Then f is convex on R^n.

theorem convexFunctionOn_inf_sum_of_proper {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => sInf {z : EReal | ∃ (x' : Fin m → Fin n → ℝ), ∑ i : Fin m, x' i = x ∧ z = ∑ i : Fin m, f i (x' i)}

Theorem 5.4: Let f_1, ..., f_m be proper convex functions on R^n, and define f x = inf { f_1 x_1 + ... + f_m x_m | x_i ∈ R^n, x_1 + ... + x_m = x }. Then f is a convex function on R^n.

noncomputable def infimalConvolution {n : ℕ} (f g : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Text 5.4.0 (Infimal convolution of two functions): Let f, g : R^n -> R union {+infty} be proper convex functions. Their infimal convolution f square g is the function (f square g)(x) = inf { f x1 + g x2 | x1, x2 in R^n, x1 + x2 = x }, equivalently (f square g)(x) = inf_{y in R^n} { f y + g (x - y) }.

Equations

• infimalConvolution f g x = sInf {z : EReal | ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), x1 + x2 = x ∧ z = f x1 + g x2}

noncomputable def infimalConvolutionFamily {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Text 5.4.1: Let f_1, ..., f_m be proper convex functions on R^n, and let f x = inf { f_1 x_1 + ... + f_m x_m | x_i ∈ R^n, x_1 + ... + x_m = x }. The function f is denoted by f_1 square f_2 square ... square f_m; the operation square is called infimal convolution.

Equations

• infimalConvolutionFamily f x = sInf {z : EReal | ∃ (x' : Fin m → Fin n → ℝ), ∑ i : Fin m, x' i = x ∧ z = ∑ i : Fin m, f i (x' i)}

theorem infimalConvolution_eq_infimalConvolutionFamily_two {n : ℕ} (f g : (Fin n → ℝ) → EReal) : infimalConvolution f g = infimalConvolutionFamily fun (i : Fin 2) => if i = 0 then f else g

The two-function infimal convolution matches the family version on Fin 2.

theorem indicatorFunction_singleton_simp {n : ℕ} (a x : Fin n → ℝ) : indicatorFunction {a} x = if x = a then 0 else ⊤

The indicator of a singleton is 0 at the point and ⊤ elsewhere.

theorem infimalConvolution_indicator_singleton_le {n : ℕ} (f : (Fin n → ℝ) → EReal) (a x : Fin n → ℝ) : infimalConvolution f (indicatorFunction {a}) x ≤ f (x - a)

The infimal convolution is bounded above by the translate f (x - a).

theorem infimalConvolution_indicator_singleton_ge {n : ℕ} (f : (Fin n → ℝ) → EReal) (a : Fin n → ℝ) (hf : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (x : Fin n → ℝ) : f (x - a) ≤ infimalConvolution f (indicatorFunction {a}) x

The translate f (x - a) is a lower bound when f never takes the value ⊥.

theorem infimalConvolution_indicator_singleton {n : ℕ} (f : (Fin n → ℝ) → EReal) (a : Fin n → ℝ) (hf : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : infimalConvolution f (indicatorFunction {a}) = fun (x : Fin n → ℝ) => f (x - a)

Text 5.4.1.1: If g = δ(· | a) for a point a ∈ R^n (where δ(x | a) = +infty for x ≠ a and δ(a | a) = 0), then (f square g)(x) = f (x - a).

theorem infimalConvolution_eq_sInf_param {n : ℕ} (f g : (Fin n → ℝ) → EReal) (x : Fin n → ℝ) : infimalConvolution f g x = sInf {r : EReal | ∃ (z : Fin n → ℝ), r = g z + f (x - z)}

Reparametrize the defining set in infimalConvolution.

theorem infimalConvolution_reflection_indicator_inner {n : ℕ} (f : (Fin n → ℝ) → EReal) (x z : Fin n → ℝ) (hf : ∀ (y : Fin n → ℝ), f y ≠ ⊥) : infimalConvolution (fun (y : Fin n → ℝ) => f (-y)) (indicatorFunction {x}) z = f (x - z)

The singleton indicator collapses the reflected infimal convolution.

theorem infimalConvolution_reflection_indicator_finalize {n : ℕ} (f g : (Fin n → ℝ) → EReal) (hf : ∀ (y : Fin n → ℝ), f y ≠ ⊥) (x : Fin n → ℝ) : sInf {r : EReal | ∃ (z : Fin n → ℝ), r = g z + infimalConvolution (fun (y : Fin n → ℝ) => f (-y)) (indicatorFunction {x}) z} = sInf {r : EReal | ∃ (z : Fin n → ℝ), r = g z + f (x - z)}

Replace the inner infimal convolution using the singleton indicator formula.

theorem infimalConvolution_reflection_indicator {n : ℕ} (f g : (Fin n → ℝ) → EReal) (hf : ∀ (y : Fin n → ℝ), f y ≠ ⊥) (x : Fin n → ℝ) : infimalConvolution f g x = sInf {r : EReal | ∃ (z : Fin n → ℝ), r = g z + infimalConvolution (fun (y : Fin n → ℝ) => f (-y)) (indicatorFunction {x}) z}

Text 5.4.1.2: Let f, g : ℝ^n → ℝ ∪ {+∞} and define the reflection h(y) = f(-y). Then for every x ∈ ℝ^n, (f □ g)(x) = inf_{z ∈ ℝ^n} { g(z) + (h □ δ(· | x))(z) }.

theorem effectiveDomain_infimalConvolution_subset_sum {n : ℕ} (f g : (Fin n → ℝ) → EReal) (hf : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (hg : ∀ (x : Fin n → ℝ), g x ≠ ⊥) (x : Fin n → ℝ) : x ∈ effectiveDomain Set.univ (infimalConvolution f g) → x ∈ Set.image2 (fun (x y : Fin n → ℝ) => x + y) (effectiveDomain Set.univ f) (effectiveDomain Set.univ g)

Points in the effective domain of the infimal convolution decompose into points in each effective domain, assuming no ⊥ values.

theorem effectiveDomain_sum_subset_infimalConvolution {n : ℕ} (f g : (Fin n → ℝ) → EReal) (x : Fin n → ℝ) : x ∈ Set.image2 (fun (x y : Fin n → ℝ) => x + y) (effectiveDomain Set.univ f) (effectiveDomain Set.univ g) → x ∈ effectiveDomain Set.univ (infimalConvolution f g)

Any sum of points from the effective domains lies in the effective domain of f □ g.

theorem effectiveDomain_infimalConvolution_eq_sum {n : ℕ} (f g : (Fin n → ℝ) → EReal) (hf : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (hg : ∀ (x : Fin n → ℝ), g x ≠ ⊥) : effectiveDomain Set.univ (infimalConvolution f g) = Set.image2 (fun (x y : Fin n → ℝ) => x + y) (effectiveDomain Set.univ f) (effectiveDomain Set.univ g)

Text 5.4.1.3: The effective domain of f □ g is the sum of dom f and dom g.

theorem indicator_add_norm_eq_if {n : ℕ} {C : Set (Fin n → ℝ)} (x z : Fin n → ℝ) : indicatorFunction C z + ↑‖x - z‖ = if z ∈ C then ↑‖x - z‖ else ⊤

Adding the indicator yields the norm on C and ⊤ outside.

theorem infimalConvolution_norm_indicator_eq_sInf_range {n : ℕ} {C : Set (Fin n → ℝ)} (x : Fin n → ℝ) : infimalConvolution (fun (y : Fin n → ℝ) => ↑‖y‖) (indicatorFunction C) x = sInf (Set.range fun (z : ↑C) => ↑‖x - ↑z‖)

Rewriting the infimal convolution with an indicator as an infimum over C.

theorem sInf_range_norm_eq_infDist {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (x : Fin n → ℝ) : sInf (Set.range fun (z : ↑C) => ↑‖x - ↑z‖) = ↑(Metric.infDist x C)

The infimum of norms over a nonempty set gives the distance.

theorem infimalConvolution_norm_indicator_eq_infDist {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (x : Fin n → ℝ) : infimalConvolution (fun (y : Fin n → ℝ) => ↑‖y‖) (indicatorFunction C) x = ↑(Metric.infDist x C)

Text 5.4.1.4: Taking f to be the Euclidean norm and g to be the indicator function of a convex set C, we get (f □ g)(x) = d(x, C), where d(x, C) denotes the distance between x and C.

theorem properConvexFunctionOn_norm {n : ℕ} : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑‖x‖

The Euclidean norm is a proper convex function on Set.univ.

theorem properConvexFunctionOn_indicator_of_convex_of_nonempty {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (hCne : C.Nonempty) : ProperConvexFunctionOn Set.univ (indicatorFunction C)

The indicator of a nonempty convex set is a proper convex function.

theorem convexFunctionOn_infimalConvolution_of_proper {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) (hg : ProperConvexFunctionOn Set.univ g) : ConvexFunctionOn Set.univ (infimalConvolution f g)

The infimal convolution of two proper convex functions is convex.

theorem convexOn_infDist_of_convex {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) : ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => Metric.infDist x C

Text 5.4.1.5: For a convex set C, let d(x, C) denote the distance between x and C. Then the function d(·, C) is convex on ℝ^n.