def IsVerticalHalfSpace (n : ℕ) (H : Set ((Fin n → ℝ) × ℝ)) : Prop

Defn 12.1: A closed half-space in ℝ^(n+1) (written with coordinates (x, μ) where x ∈ ℝ^n and μ ∈ ℝ) is classified into three types by its defining inequality:

1. (Vertical) a set {(x, μ) | ⟪x, b⟫ ≤ β} with b ≠ 0;
2. (Upper) a set {(x, μ) | μ ≥ ⟪x, b⟫ - β} (the epigraph of an affine function);
3. (Lower) a set {(x, μ) | μ ≤ ⟪x, b⟫ - β}.

Equations

• IsVerticalHalfSpace n H = ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ H = {p : (Fin n → ℝ) × ℝ | p.1 ⬝ᵥ b ≤ β}

def IsUpperHalfSpace (n : ℕ) (H : Set ((Fin n → ℝ) × ℝ)) : Prop

Defn 12.1 (Upper): H ⊆ ℝ^n × ℝ has the form {(x, μ) | μ ≥ ⟪x, b⟫ - β}.

Equations

• IsUpperHalfSpace n H = ∃ (b : Fin n → ℝ) (β : ℝ), H = {p : (Fin n → ℝ) × ℝ | p.2 ≥ p.1 ⬝ᵥ b - β}

def IsLowerHalfSpace (n : ℕ) (H : Set ((Fin n → ℝ) × ℝ)) : Prop

Defn 12.1 (Lower): H ⊆ ℝ^n × ℝ has the form {(x, μ) | μ ≤ ⟪x, b⟫ - β}.

Equations

• IsLowerHalfSpace n H = ∃ (b : Fin n → ℝ) (β : ℝ), H = {p : (Fin n → ℝ) × ℝ | p.2 ≤ p.1 ⬝ᵥ b - β}

theorem dotProduct_self_ne_zero {n : ℕ} (b : Fin n → ℝ) (hb : b ≠ 0) : b ⬝ᵥ b ≠ 0

If b ≠ 0, then b ⬝ᵥ b ≠ 0.

theorem exists_dotProduct_le {n : ℕ} (b : Fin n → ℝ) (hb : b ≠ 0) (β : ℝ) : ∃ (x : Fin n → ℝ), x ⬝ᵥ b ≤ β

For a nonzero vector b, there exists an x with x ⬝ᵥ b ≤ β.

theorem closedHalfSpace_isVertical_of_repr_t_eq_zero {n : ℕ} {H : Set ((Fin n → ℝ) × ℝ)} {b : Fin n → ℝ} {t β : ℝ} (hnonzero : b ≠ 0 ∨ t ≠ 0) (ht : t = 0) (hrepr : H = {p : (Fin n → ℝ) × ℝ | p.1 ⬝ᵥ b + p.2 * t ≤ β}) : IsVerticalHalfSpace n H

If H has a representation with t = 0, then it is a vertical half-space.

theorem closedHalfSpace_isUpper_of_repr_t_neg {n : ℕ} {H : Set ((Fin n → ℝ) × ℝ)} {b : Fin n → ℝ} {t β : ℝ} (ht : t < 0) (hrepr : H = {p : (Fin n → ℝ) × ℝ | p.1 ⬝ᵥ b + p.2 * t ≤ β}) : IsUpperHalfSpace n H

If H = {p | p.1 ⬝ᵥ b + p.2 * t ≤ β} with t < 0, then H is an upper half-space.

theorem closedHalfSpace_isLower_of_repr_t_pos {n : ℕ} {H : Set ((Fin n → ℝ) × ℝ)} {b : Fin n → ℝ} {t β : ℝ} (ht : 0 < t) (hrepr : H = {p : (Fin n → ℝ) × ℝ | p.1 ⬝ᵥ b + p.2 * t ≤ β}) : IsLowerHalfSpace n H

If H = {p | p.1 ⬝ᵥ b + p.2 * t ≤ β} with 0 < t, then H is a lower half-space.

theorem halfSpaceTypes_pairwise_disjoint {n : ℕ} {H : Set ((Fin n → ℝ) × ℝ)} : ¬(IsVerticalHalfSpace n H ∧ IsUpperHalfSpace n H) ∧ ¬(IsVerticalHalfSpace n H ∧ IsLowerHalfSpace n H) ∧ ¬(IsUpperHalfSpace n H ∧ IsLowerHalfSpace n H)

The three half-space types (vertical, upper, lower) are pairwise incompatible.

theorem closedHalfSpace_trichotomy (n : ℕ) (H : Set ((Fin n → ℝ) × ℝ)) (hH : ∃ (b : Fin n → ℝ) (t : ℝ) (β : ℝ), (b ≠ 0 ∨ t ≠ 0) ∧ H = {p : (Fin n → ℝ) × ℝ | p.1 ⬝ᵥ b + p.2 * t ≤ β}) : (IsVerticalHalfSpace n H ∨ IsUpperHalfSpace n H ∨ IsLowerHalfSpace n H) ∧ ¬(IsVerticalHalfSpace n H ∧ IsUpperHalfSpace n H) ∧ ¬(IsVerticalHalfSpace n H ∧ IsLowerHalfSpace n H) ∧ ¬(IsUpperHalfSpace n H ∧ IsLowerHalfSpace n H)

Text 12.0.1: Every closed half-space in ℝ^(n+1) belongs to exactly one of the following categories: vertical, upper, or lower.

theorem strongDual_apply_prod {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (l : StrongDual ℝ (E × ℝ)) (x : E) (μ : ℝ) : l (x, μ) = l (x, 0) + μ * l (0, 1)

A continuous linear functional on E × ℝ evaluates as l (x, μ) = l (x, 0) + μ * l (0, 1).

theorem epigraph_closed_convex_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_closed : LowerSemicontinuous f) : have C := {p : E × ℝ | f p.1 ≤ p.2}; Convex ℝ C ∧ IsClosed C

The epigraph {(x, μ) | f x ≤ μ} of a convex lower-semicontinuous function is closed and convex.

theorem exists_affineMap_strictly_above_below_point {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_closed : LowerSemicontinuous f) (x0 : E) (μ0 : ℝ) : μ0 < f x0 → ∃ (h : E →ᵃ[ℝ] ℝ), (∀ (y : E), h y ≤ f y) ∧ μ0 < h x0

Any point strictly below the epigraph can be strictly separated by an affine minorant.

theorem closedConvex_eq_sSup_affineMap_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (hf_convex : ConvexOn ℝ Set.univ f) (hf_closed : LowerSemicontinuous f) (x : E) : f x = sSup ((fun (h : E →ᵃ[ℝ] ℝ) => h x) '' {h : E →ᵃ[ℝ] ℝ | ∀ (y : E), h y ≤ f y})

Theorem 12.1. A closed convex function f is the pointwise supremum of the collection of all affine maps h such that h ≤ f.

noncomputable def clConv (n : ℕ) (f : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

clConv n f is a Lean stand-in for the book's cl (conv f) for an extended-real-valued function f : ℝ^n → [-∞, ∞]. It is defined pointwise as the supremum of all affine functions majorized by f.

Equations

• clConv n f x = sSup ((fun (h : (Fin n → ℝ) →ᵃ[ℝ] ℝ) => ↑(h x)) '' {h : (Fin n → ℝ) →ᵃ[ℝ] ℝ | ∀ (y : Fin n → ℝ), ↑(h y) ≤ f y})

theorem clConv_eq_sSup_affineMap_le (n : ℕ) (f : (Fin n → ℝ) → EReal) (x : Fin n → ℝ) : clConv n f x = sSup ((fun (h : (Fin n → ℝ) →ᵃ[ℝ] ℝ) => ↑(h x)) '' {h : (Fin n → ℝ) →ᵃ[ℝ] ℝ | ∀ (y : Fin n → ℝ), ↑(h y) ≤ f y})

Corollary 12.1.1. If f : ℝ^n → [-∞, ∞] is any function, then cl (conv f) (here represented by clConv n f) is the pointwise supremum of the collection of all affine functions on ℝ^n majorized by f.

theorem properConvexFunctionOn_exists_finite_point {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : ∃ (x0 : Fin n → ℝ) (r0 : ℝ), f x0 = ↑r0

A proper convex function on ℝ^n has a point where it takes a finite real value.

theorem convexOn_toReal_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : ConvexOn ℝ (effectiveDomain Set.univ f) fun (x : Fin n → ℝ) => (f x).toReal

The Real-valued function x ↦ (f x).toReal is convex on the effective domain of a proper convex function f.

theorem point_below_not_mem_closure_epigraph_of_mem_intrinsicInterior {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) {x0 : Fin n → ℝ} {r0 : ℝ} (hx0 : x0 ∈ intrinsicInterior ℝ (effectiveDomain Set.univ f)) (hr0 : f x0 = ↑r0) : (x0, r0 - 1) ∉ closure (epigraph Set.univ f)

If x0 lies in the intrinsic interior of the effective domain of a proper convex function, then the point (x0, f x0 - 1) lies outside the closure of the epigraph.

theorem linearMap_exists_dotProduct_representation {n : ℕ} (φ : (Fin n → ℝ) →ₗ[ℝ] ℝ) : ∃ (b : Fin n → ℝ), ∀ (x : Fin n → ℝ), φ x = x ⬝ᵥ b

A linear functional on ℝ^n can be represented as a dot product with a coefficient vector.

theorem properConvexFunctionOn_exists_linear_lowerBound {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : ∃ (b : Fin n → ℝ) (β : ℝ), ∀ (x : Fin n → ℝ), f x ≥ ↑(x ⬝ᵥ b - β)

Corollary 12.1.2. Given any proper convex function f on ℝ^n, there exist b : ℝ^n and β : ℝ such that f x ≥ ⟪x, b⟫ - β for every x.

theorem le_indicatorFunction_iff_forall_mem_le_zero {n : ℕ} {C : Set (Fin n → ℝ)} {g : (Fin n → ℝ) → ℝ} : (fun (x : Fin n → ℝ) => ↑(g x)) ≤ indicatorFunction C ↔ ∀ x ∈ C, g x ≤ 0

A real-valued function g (coerced to EReal) is pointwise below indicatorFunction C iff g x ≤ 0 for every x ∈ C.

theorem forall_mem_sub_le_zero_iff_subset_halfspace {n : ℕ} {C : Set (Fin n → ℝ)} (b : Fin n → ℝ) (β : ℝ) : (∀ x ∈ C, x ⬝ᵥ b - β ≤ 0) ↔ C ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ β}

The inequality x ⬝ᵥ b - β ≤ 0 on C is equivalent to the half-space containment C ⊆ {x | x ⬝ᵥ b ≤ β}.

theorem affine_le_indicatorFunction_iff_subset_halfspace {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (b : Fin n → ℝ) (β : ℝ) : (fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b - β)) ≤ indicatorFunction C ↔ C ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ β}

Text 12.1.1: If f is the indicator function of a convex set C and h x = ⟪x, b⟫ - β, then h ≤ f if and only if h x ≤ 0 for every x ∈ C, i.e. if and only if C ⊆ {x | ⟪x, b⟫ ≤ β}.

theorem affine_majorized_iff_forall_dotSub_le_mu {n : ℕ} (f : (Fin n → ℝ) → ℝ) (xStar : Fin n → ℝ) (muStar : ℝ) : (∀ (x : Fin n → ℝ), x ⬝ᵥ xStar - muStar ≤ f x) ↔ ∀ (x : Fin n → ℝ), x ⬝ᵥ xStar - f x ≤ muStar

Rearranging x ⬝ᵥ xStar - muStar ≤ f x yields x ⬝ᵥ xStar - f x ≤ muStar.

theorem bddAbove_range_of_forall_le {α : Type u_1} {β : Type u_2} [Preorder β] (g : α → β) (a : β) (h : ∀ (x : α), g x ≤ a) : BddAbove (Set.range g)

A pointwise upper bound yields BddAbove for the range.

theorem affine_majorized_iff_mu_ge_sSup (n : ℕ) (f : (Fin n → ℝ) → ℝ) (xStar : Fin n → ℝ) (muStar : ℝ) : (∀ (x : Fin n → ℝ), x ⬝ᵥ xStar - muStar ≤ f x) ↔ BddAbove (Set.range fun (x : Fin n → ℝ) => x ⬝ᵥ xStar - f x) ∧ muStar ≥ sSup (Set.range fun (x : Fin n → ℝ) => x ⬝ᵥ xStar - f x)

Text 12.1.2: Let f be a function on ℝ^n (contextually: closed convex), and let h x = ⟪x, x*⟫ - μ* be an affine function. Then h is majorized by f (i.e. h x ≤ f x for every x) if and only if μ* ≥ sup {⟪x, x*⟫ - f x | x ∈ ℝ^n}.