theorem convexFunctionOn_precomp_linearMap {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (g : (Fin m → ℝ) → EReal) : ConvexFunctionOn Set.univ g → ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => g (A x)

Precomposition with a linear map preserves convexity on Set.univ.

theorem convexFunctionOn_inf_fiber_linearMap {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (h : (Fin n → ℝ) → EReal) : ConvexFunctionOn Set.univ h → ConvexFunctionOn Set.univ fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x}

Infimum over affine fibers of a linear map preserves convexity on Set.univ.

theorem convexFunctionOn_linearMap_precomp_and_inf {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : (∀ (g : (Fin m → ℝ) → EReal), ConvexFunctionOn Set.univ g → ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => g (A x)) ∧ ∀ (h : (Fin n → ℝ) → EReal), ConvexFunctionOn Set.univ h → ConvexFunctionOn Set.univ fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x}

Theorem 5.7: Let A be a linear transformation from R^n to R^m. Then, for each convex function g on R^m, the function gA defined by (gA)(x) = g(Ax) is convex on R^n. For each convex function h on R^n, the function Ah defined by (Ah)(y) = inf { h(x) | A x = y } is convex on R^m.

noncomputable def imageUnderLinearMap {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (h : (Fin n → ℝ) → EReal) : (Fin m → ℝ) → EReal

Text 5.7.1: The function Ah in Theorem 5.7 is called the image of h under A.

Equations

• imageUnderLinearMap A h y = sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x}

def inverseImageUnderLinearMap {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (g : (Fin m → ℝ) → EReal) : (Fin n → ℝ) → EReal

Text 5.7.1: The function gA in Theorem 5.7 is called the inverse image of g under A.

Equations

• inverseImageUnderLinearMap A g x = g (A x)

def projectionLinearMap {n m : ℕ} (hmn : m ≤ n) : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ

The coordinate projection onto the first m components as a linear map.

Equations

• projectionLinearMap hmn = { toFun := fun (x : Fin n → ℝ) (i : Fin m) => x ⟨↑i, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem projectionLinearMap_eq_iff {n m : ℕ} (hmn : m ≤ n) (x : Fin n → ℝ) (y : Fin m → ℝ) : (projectionLinearMap hmn) x = y ↔ ∀ (i : Fin m), x ⟨↑i, ⋯⟩ = y i

Coordinate-wise characterization of the projection fiber equation.

theorem convexFunctionOn_projection_inf {n m : ℕ} (hmn : m ≤ n) {h : (Fin n → ℝ) → EReal} (hh : ConvexFunctionOn Set.univ h) : ConvexFunctionOn Set.univ fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), (∀ (i : Fin m), x ⟨↑i, ⋯⟩ = y i) ∧ z = h x}

Text 5.7.2: Let A be the projection x = (xi_1, ..., xi_m, xi_{m+1}, ..., xi_n) ↦ (xi_1, ..., xi_m). Then (Ah)(xi_1, ..., xi_m) = inf_{xi_{m+1}, ..., xi_n} h(xi_1, ..., xi_n). This is convex in y = (xi_1, ..., xi_m) when h is convex.

theorem exists_eq_of_linearEquiv_fiber {n m : ℕ} (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin m → ℝ) (h : (Fin n → ℝ) → EReal) (y : Fin m → ℝ) (z : EReal) : (∃ (x : Fin n → ℝ), A x = y ∧ z = h x) ↔ z = h (A.symm y)

For a linear equivalence, the fiber over y is a singleton.

theorem imageUnderLinearMap_eq_inverseImage_under_symm {n m : ℕ} (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin m → ℝ) {h : (Fin n → ℝ) → EReal} : imageUnderLinearMap (↑A) h = inverseImageUnderLinearMap (↑A.symm) h

Text 5.7.3: Let A be a linear transformation from R^n to R^m. When A is non-singular (so n = m and A^{-1} exists), for a convex function h on R^n, Ah = hA^{-1}.

noncomputable def partialInfimalConvolutionZ {m p : ℕ} (f g : (Fin m → ℝ) × (Fin p → ℝ) → EReal) : (Fin m → ℝ) × (Fin p → ℝ) → EReal

Text 5.7.4 (Partial infimal convolution): Let n = m + p and write x = (y, z) with y ∈ ℝ^m and z ∈ ℝ^p. For proper convex f, g : ℝ^m × ℝ^p → (-∞, +∞], the partial infimal convolution of f and g with respect to the z-variable is the function h(y, z) = inf_{u ∈ ℝ^p} { f(y, z - u) + g(y, u) }.

Equations

• partialInfimalConvolutionZ f g yz = sInf {r : EReal | ∃ (u : Fin p → ℝ), r = f (yz.1, yz.2 - u) + g (yz.1, u)}

theorem rightScalarMultiple_one_eq {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) (x : Fin n → ℝ) : rightScalarMultiple f 1 x = f x

Right scalar multiple at 1 returns the original function.

theorem exists_mu1_mu2_of_ge_sum {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) {x : Fin n → ℝ} {μ : EReal} (hle : f1 x + f2 x ≤ μ) : ∃ (μ1 : EReal) (μ2 : EReal), μ = μ1 + μ2 ∧ f1 x ≤ μ1 ∧ f2 x ≤ μ2

Split a lower bound on f1 x + f2 x into two pieces.

theorem mem_F_iff_ge_sum {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (μ1 : EReal) (μ2 : EReal), μ = μ1 + μ2 ∧ (lam, x, μ1) ∈ K1 ∧ (lam, x, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; ∀ {x : Fin n → ℝ} {μ : EReal}, (x, μ) ∈ F ↔ f1 x + f2 x ≤ μ

Membership in F is equivalent to the sum inequality.

theorem sInf_Ici_eq_self {a : EReal} : sInf {μ : EReal | a ≤ μ} = a

The infimum of the upper set {μ | a ≤ μ} is a.

theorem sum_properConvex_eq_inf_of_K {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (μ1 : EReal) (μ2 : EReal), μ = μ1 + μ2 ∧ (lam, x, μ1) ∈ K1 ∧ (lam, x, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; have f := fun (x : Fin n → ℝ) => sInf {μ : EReal | (x, μ) ∈ F}; f = fun (x : Fin n → ℝ) => f1 x + f2 x

Text 5.8.0.1: Let f1, f2 be proper convex functions on ℝ^n. Define K1 = { (λ, x, μ) | λ ≥ 0, μ ≥ (f1 λ)(x) } and K2 = { (λ, x, μ) | λ ≥ 0, μ ≥ (f2 λ)(x) }. Let K = { (λ, x, μ) | ∃ μ1 μ2, μ = μ1 + μ2, (λ, x, μ1) ∈ K1, (λ, x, μ2) ∈ K2 }, F = { (x, μ) | (1, x, μ) ∈ K }, and f x = inf { μ | (x, μ) ∈ F }. Then f = f1 + f2.

theorem mem_F_of_exact_sum {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (μ1 : EReal) (μ2 : EReal) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), μ = μ1 + μ2 ∧ x = x1 + x2 ∧ (lam, x1, μ1) ∈ K1 ∧ (lam, x2, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; ∀ {x x1 x2 : Fin n → ℝ} {μ : EReal}, x1 + x2 = x → μ = f1 x1 + f2 x2 → (x, μ) ∈ F

Exact sums lie in F.

theorem exists_sum_le_of_mem_F {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (μ1 : EReal) (μ2 : EReal) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), μ = μ1 + μ2 ∧ x = x1 + x2 ∧ (lam, x1, μ1) ∈ K1 ∧ (lam, x2, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; ∀ {x : Fin n → ℝ} {μ : EReal}, (x, μ) ∈ F → ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), x1 + x2 = x ∧ f1 x1 + f2 x2 ≤ μ

Membership in F yields a split with a lower bound on μ.

theorem sInf_F_eq_sInf_infimal_pointwise {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (μ1 : EReal) (μ2 : EReal) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), μ = μ1 + μ2 ∧ x = x1 + x2 ∧ (lam, x1, μ1) ∈ K1 ∧ (lam, x2, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; ∀ (x : Fin n → ℝ), sInf {μ : EReal | (x, μ) ∈ F} = sInf {z : EReal | ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), x1 + x2 = x ∧ z = f1 x1 + f2 x2}

The sInf defining F matches the infimal convolution set pointwise.

theorem infimalConvolution_eq_inf_of_K {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (μ1 : EReal) (μ2 : EReal) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), μ = μ1 + μ2 ∧ x = x1 + x2 ∧ (lam, x1, μ1) ∈ K1 ∧ (lam, x2, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; have f := fun (x : Fin n → ℝ) => sInf {μ : EReal | (x, μ) ∈ F}; f = infimalConvolution f1 f2

Text 5.8.0.2: Let f1, f2 be proper convex functions on ℝ^n. Define K1 = { (λ, x, μ) | λ ≥ 0, μ ≥ (f1 λ)(x) } and K2 = { (λ, x, μ) | λ ≥ 0, μ ≥ (f2 λ)(x) }. Let K = { (λ, x, μ) | ∃ μ1 μ2 x1 x2, μ = μ1 + μ2, x = x1 + x2, (λ, x1, μ1) ∈ K1, (λ, x2, μ2) ∈ K2 }, F = { (x, μ) | (1, x, μ) ∈ K }, and f x = inf { μ | (x, μ) ∈ F }. Then f = f1 □ f2.

theorem mem_F_iff_exists_pair {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (lam1 : ℝ) (lam2 : ℝ), 0 ≤ lam1 ∧ 0 ≤ lam2 ∧ ∃ (μ1 : EReal) (μ2 : EReal) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), lam = lam1 + lam2 ∧ μ = μ1 + μ2 ∧ x = x1 + x2 ∧ (lam1, x1, μ1) ∈ K1 ∧ (lam2, x2, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; ∀ {x : Fin n → ℝ} {μ : EReal}, (x, μ) ∈ F ↔ ∃ (lam1 : ℝ) (lam2 : ℝ), 0 ≤ lam1 ∧ 0 ≤ lam2 ∧ ∃ (μ1 : EReal) (μ2 : EReal) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), 1 = lam1 + lam2 ∧ μ = μ1 + μ2 ∧ x = x1 + x2 ∧ (0 ≤ lam1 ∧ rightScalarMultiple f1 lam1 x1 ≤ μ1) ∧ 0 ≤ lam2 ∧ rightScalarMultiple f2 lam2 x2 ≤ μ2

Unpack membership in F for the pairwise convex hull construction.

theorem exists_sum_le_of_mem_F_pair {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (lam1 : ℝ) (lam2 : ℝ), 0 ≤ lam1 ∧ 0 ≤ lam2 ∧ ∃ (μ1 : EReal) (μ2 : EReal) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), lam = lam1 + lam2 ∧ μ = μ1 + μ2 ∧ x = x1 + x2 ∧ (lam1, x1, μ1) ∈ K1 ∧ (lam2, x2, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; ∀ {x : Fin n → ℝ} {μ : EReal}, (x, μ) ∈ F → ∃ (lam1 : ℝ) (lam2 : ℝ), 0 ≤ lam1 ∧ 0 ≤ lam2 ∧ lam1 + lam2 = 1 ∧ ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), x1 + x2 = x ∧ rightScalarMultiple f1 lam1 x1 + rightScalarMultiple f2 lam2 x2 ≤ μ

Membership in F yields a weighted split with a lower bound on μ.

theorem mem_F_of_exact_sum_pair {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (lam1 : ℝ) (lam2 : ℝ), 0 ≤ lam1 ∧ 0 ≤ lam2 ∧ ∃ (μ1 : EReal) (μ2 : EReal) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), lam = lam1 + lam2 ∧ μ = μ1 + μ2 ∧ x = x1 + x2 ∧ (lam1, x1, μ1) ∈ K1 ∧ (lam2, x2, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; ∀ {x x1 x2 : Fin n → ℝ} {lam1 lam2 : ℝ}, 0 ≤ lam1 → 0 ≤ lam2 → lam1 + lam2 = 1 → x1 + x2 = x → (x, rightScalarMultiple f1 lam1 x1 + rightScalarMultiple f2 lam2 x2) ∈ F

Exact weighted sums belong to F.

theorem sInf_F_eq_sInf_rightScalarMultiple_pair {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (lam1 : ℝ) (lam2 : ℝ), 0 ≤ lam1 ∧ 0 ≤ lam2 ∧ ∃ (μ1 : EReal) (μ2 : EReal) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), lam = lam1 + lam2 ∧ μ = μ1 + μ2 ∧ x = x1 + x2 ∧ (lam1, x1, μ1) ∈ K1 ∧ (lam2, x2, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; ∀ (x : Fin n → ℝ), sInf {μ : EReal | (x, μ) ∈ F} = sInf {z : EReal | ∃ (lam1 : ℝ) (lam2 : ℝ), 0 ≤ lam1 ∧ 0 ≤ lam2 ∧ lam1 + lam2 = 1 ∧ ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), x1 + x2 = x ∧ z = rightScalarMultiple f1 lam1 x1 + rightScalarMultiple f2 lam2 x2}

The sInf defining F matches the pairwise rightScalarMultiple infimum.

theorem sInf_pair_eq_sInf_infimalConvolutionFamily {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (x : Fin n → ℝ) : sInf {z : EReal | ∃ (lam1 : ℝ) (lam2 : ℝ), 0 ≤ lam1 ∧ 0 ≤ lam2 ∧ lam1 + lam2 = 1 ∧ ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), x1 + x2 = x ∧ z = rightScalarMultiple f1 lam1 x1 + rightScalarMultiple f2 lam2 x2} = sInf {z : EReal | ∃ (lam : Fin 2 → ℝ), (∀ (i : Fin 2), 0 ≤ lam i) ∧ ∑ i : Fin 2, lam i = 1 ∧ z = infimalConvolutionFamily (fun (i : Fin 2) => rightScalarMultiple (if i = 0 then f1 else f2) (lam i)) x}

The pairwise rightScalarMultiple infimum matches the Fin 2 family form.

theorem convexHullFunctionPair_eq_inf_of_K {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; ∃ (lam1 : ℝ) (lam2 : ℝ), 0 ≤ lam1 ∧ 0 ≤ lam2 ∧ ∃ (μ1 : EReal) (μ2 : EReal) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), lam = lam1 + lam2 ∧ μ = μ1 + μ2 ∧ x = x1 + x2 ∧ (lam1, x1, μ1) ∈ K1 ∧ (lam2, x2, μ2) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; have f := fun (x : Fin n → ℝ) => sInf {μ : EReal | (x, μ) ∈ F}; f = convexHullFunctionFamily fun (i : Fin 2) => if i = 0 then f1 else f2

Text 5.8.0.3: Let f1, f2 be proper convex functions on ℝ^n. Define K1 = { (λ, x, μ) | λ ≥ 0, μ ≥ (f1 λ)(x) } and K2 = { (λ, x, μ) | λ ≥ 0, μ ≥ (f2 λ)(x) }. Let K = { (λ, x, μ) | ∃ λ1, λ2 ≥ 0, ∃ μ1, μ2, x1, x2, λ = λ1 + λ2, μ = μ1 + μ2, x = x1 + x2, (λ1, x1, μ1) ∈ K1, (λ2, x2, μ2) ∈ K2 }, F = { (x, μ) | (1, x, μ) ∈ K }, and f x = inf { μ | (x, μ) ∈ F }. Then f = conv{f1, f2}.

theorem mem_F_iff_ge_both {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; (lam, x, μ) ∈ K1 ∧ (lam, x, μ) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; ∀ {x : Fin n → ℝ} {μ : EReal}, (x, μ) ∈ F ↔ f1 x ≤ μ ∧ f2 x ≤ μ

Membership in F is equivalent to simultaneous lower bounds for f1 and f2.

theorem mem_F_iff_ge_max {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; (lam, x, μ) ∈ K1 ∧ (lam, x, μ) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; ∀ {x : Fin n → ℝ} {μ : EReal}, (x, μ) ∈ F ↔ max (f1 x) (f2 x) ≤ μ

Membership in F is equivalent to a max lower bound.

theorem sInf_ge_max_eq {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (x : Fin n → ℝ) : sInf {μ : EReal | max (f1 x) (f2 x) ≤ μ} = max (f1 x) (f2 x)

The infimum of the upper set for the max is the max.

theorem max_properConvex_eq_inf_of_K {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : have K1 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f1 lam x}; have K2 := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; 0 ≤ lam ∧ μ ≥ rightScalarMultiple f2 lam x}; have K := {p : ℝ × (Fin n → ℝ) × EReal | have lam := p.1; have x := p.2.1; have μ := p.2.2; (lam, x, μ) ∈ K1 ∧ (lam, x, μ) ∈ K2}; have F := {p : (Fin n → ℝ) × EReal | (1, p.1, p.2) ∈ K}; have f := fun (x : Fin n → ℝ) => sInf {μ : EReal | (x, μ) ∈ F}; f = fun (x : Fin n → ℝ) => max (f1 x) (f2 x)

Text 5.8.0.4: Let f1, f2 be proper convex functions on ℝ^n. Define K1 = { (λ, x, μ) | λ ≥ 0, μ ≥ (f1 λ)(x) } and K2 = { (λ, x, μ) | λ ≥ 0, μ ≥ (f2 λ)(x) }. Let K = { (λ, x, μ) | (λ, x, μ) ∈ K1, (λ, x, μ) ∈ K2 }, F = { (x, μ) | (1, x, μ) ∈ K }, and f x = inf { μ | (x, μ) ∈ F }. Then f = max{f1, f2}.

theorem sum_components_convex_combo {n m : ℕ} (x' y' : Fin m → Fin n → ℝ) (t : ℝ) : ∑ i : Fin m, ((1 - t) • x' i + t • y' i) = (1 - t) • ∑ i : Fin m, x' i + t • ∑ i : Fin m, y' i

Sum of pointwise convex combinations equals the convex combination of sums.

theorem iSup_lt_of_forall_lt_fin {m : ℕ} {a : Fin m → EReal} {r : EReal} (hm : 0 < m) (h : ∀ (i : Fin m), a i < r) : iSup a < r

On a nonempty finite index, iSup preserves strict upper bounds.