Convex Analysis (Rockafellar, 1970) -- Chapter 01 -- Section 02 -- Part 2

open scoped BigOperatorsopen scoped Pointwisesection Chap01section Section02

Positive scaling sends the nonnegative ray into itself.

lemma smul_rayNonneg_subset (n : Nat) (S : Set (Fin n → Real)) {t : Real} (ht : 0 < t) : t • rayNonneg n S ⊆ rayNonneg n S := by intro y hy rcases hy with ⟨y', hy', rfl⟩ rcases hy' with ⟨x, hxS, r, hr, rfl⟩ refine ⟨x, hxS, t * r, ?_, by simp [smul_smul]⟩ exact mul_nonneg (le_of_lt ht) hr

The convex hull of the ray is closed under positive scaling.

lemma convexHull_rayNonneg_smul_closed (n : Nat) (S : Set (Fin n → Real)) : ∀ x ∈ convexHull Real (rayNonneg n S), ∀ t : Real, 0 < t → t • x ∈ convexHull Real (rayNonneg n S) := by intro x hx t ht have hsubset : t • rayNonneg n S ⊆ rayNonneg n S := smul_rayNonneg_subset n S ht have hx' : t • x ∈ t • convexHull Real (rayNonneg n S) := ⟨x, hx, rfl⟩ have hx'' : t • x ∈ convexHull Real (t • rayNonneg n S) := by have : t • convexHull Real (rayNonneg n S) = convexHull Real (t • rayNonneg n S) := by simpa using (convexHull_smul (𝕜:=Real) (a:=t) (s:=rayNonneg n S)).symm simpa [this] using hx' have hsubsetHull : convexHull Real (t • rayNonneg n S) ⊆ convexHull Real (rayNonneg n S) := convexHull_min (hsubset.trans (subset_convexHull (𝕜:=Real) (s:=rayNonneg n S))) (convex_convexHull Real (rayNonneg n S)) exact hsubsetHull hx''

The convex hull of the ray is closed under addition.

lemma convexHull_rayNonneg_add_closed (n : Nat) (S : Set (Fin n → Real)) : ∀ x ∈ convexHull Real (rayNonneg n S), ∀ y ∈ convexHull Real (rayNonneg n S), x + y ∈ convexHull Real (rayNonneg n S) := by intro x hx y hy have hmid : midpoint Real x y ∈ convexHull Real (rayNonneg n S) := Convex.midpoint_mem (convex_convexHull Real (rayNonneg n S)) hx hy have htwo : (2 : Real) • midpoint Real x y ∈ convexHull Real (rayNonneg n S) := convexHull_rayNonneg_smul_closed n S _ hmid 2 (by norm_num) have hsum : x + y = (2 : Real) • midpoint Real x y := by calc x + y = midpoint Real x y + midpoint Real x y := by simp _ = (2 : Real) • midpoint Real x y := by simpa using (two_smul Real (midpoint Real x y)).symm simpa [hsum] using htwo

Corollary 2.6.11. For any nonempty subset failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `S`S ⊆ Real^Unknown identifier `n`n, the convex cone generated by Unknown identifier `S`S satisfies Unknown identifier `cone`sorry = sorry : Propcone S = Unknown identifier `conv`conv (ray S).

theorem convexConeGenerated_eq_convexHull_ray (n : Nat) (S : Set (Fin n → Real)) (hS : S.Nonempty) : convexConeGenerated n S = convexHull Real {y : Fin n → Real | ∃ x ∈ S, ∃ t : Real, 0 ≤ t ∧ y = t • x} := by change convexConeGenerated n S = convexHull Real (rayNonneg n S) refine subset_antisymm ?_ ?_ · let K : ConvexCone Real (Fin n → Real) := { carrier := convexHull Real (rayNonneg n S) smul_mem' := by intro c hc x hx exact convexHull_rayNonneg_smul_closed n S x hx c hc add_mem' := by intro x hx y hy exact convexHull_rayNonneg_add_closed n S x hx y hy } have hSsub : S ⊆ (K : Set (Fin n → Real)) := by intro x hx have hxray : x ∈ rayNonneg n S := by refine ⟨x, hx, 1, by norm_num, by simp⟩ exact (subset_convexHull (𝕜:=Real) (s:=rayNonneg n S)) hxray have hHullSub : (ConvexCone.hull Real S : Set (Fin n → Real)) ⊆ K := by intro x hx exact (ConvexCone.hull_min (s:=S) (C:=K) hSsub) hx rcases hS with ⟨x0, hx0⟩ have h0ray : (0 : Fin n → Real) ∈ rayNonneg n S := by refine ⟨x0, hx0, 0, le_rfl, ?_⟩ simp have h0conv : (0 : Fin n → Real) ∈ convexHull Real (rayNonneg n S) := (subset_convexHull (𝕜:=Real) (s:=rayNonneg n S)) h0ray intro y hy have hy' : y = 0 ∨ y ∈ (ConvexCone.hull Real S : Set (Fin n → Real)) := by simpa [convexConeGenerated] using hy cases hy' with | inl hy0 => subst hy0 simpa using h0conv | inr hyHull => exact hHullSub hyHull · have hconv : Convex Real (convexConeGenerated n S) := convexConeGenerated_convex n S have hsubset : rayNonneg n S ⊆ convexConeGenerated n S := rayNonneg_subset_convexConeGenerated n S exact convexHull_min hsubset hconv

Theorem 2.7. Let Unknown identifier `K`K be a convex cone containing 0 : ℕ0. Then the smallest subspace containing Unknown identifier `K`K is the set of differences , which coincides with Unknown identifier `aff`aff K, and the largest subspace contained in Unknown identifier `K`K is failed to synthesize Inter ℤ Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.-sorry ∩ sorry : ℤ(-Unknown identifier `K`K) ∩ Unknown identifier `K`K.

theorem convexCone_smallest_largest_subspace (n : Nat) (K : Set (Fin n → Real)) (hK : IsConvexCone n K) (h0 : (0 : Fin n → Real) ∈ K) : (Submodule.span Real K : Set (Fin n → Real)) = {z : Fin n → Real | ∃ x ∈ K, ∃ y ∈ K, z = x - y} ∧ (Submodule.span Real K : Set (Fin n → Real)) = (affineSpan Real K : Set (Fin n → Real)) ∧ (∃ S : Submodule Real (Fin n → Real), (S : Set (Fin n → Real)) ⊆ K ∧ (∀ T : Submodule Real (Fin n → Real), (T : Set (Fin n → Real)) ⊆ K → T ≤ S) ∧ (S : Set (Fin n → Real)) = {x : Fin n → Real | x ∈ K ∧ -x ∈ K}) := by have hadd : ∀ x ∈ K, ∀ y ∈ K, x + y ∈ K := isConvexCone_add_closed n K hK have hsmul_nonneg : ∀ x ∈ K, ∀ t : Real, 0 ≤ t → t • x ∈ K := by intro x hx t ht by_cases ht0 : t = 0 · subst ht0 simpa using h0 · have htpos : 0 < t := lt_of_le_of_ne ht (Ne.symm ht0) exact hK.1 x hx t htpos have hspan_eq : (Submodule.span Real K : Set (Fin n → Real)) = {z : Fin n → Real | ∃ x ∈ K, ∃ y ∈ K, z = x - y} := by refine subset_antisymm ?_ ?_ · intro z hz refine Submodule.span_induction (p:=fun z _ => ∃ x ∈ K, ∃ y ∈ K, z = x - y) ?_ ?_ ?_ ?_ hz · intro x hx exact ⟨x, hx, 0, h0, by simp⟩ · exact ⟨0, h0, 0, h0, by simp⟩ · intro x y hx hy hxrep hyrep rcases hxrep with ⟨x1, hx1, x2, hx2, rfl⟩ rcases hyrep with ⟨y1, hy1, y2, hy2, rfl⟩ refine ⟨x1 + y1, hadd _ hx1 _ hy1, x2 + y2, hadd _ hx2 _ hy2, ?_⟩ simp [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] · intro a x hx hxrep rcases hxrep with ⟨x1, hx1, x2, hx2, rfl⟩ by_cases ha : 0 ≤ a · refine ⟨a • x1, hsmul_nonneg _ hx1 _ ha, a • x2, hsmul_nonneg _ hx2 _ ha, ?_⟩ simp [smul_sub] · have ha' : 0 ≤ -a := by linarith refine ⟨(-a) • x2, hsmul_nonneg _ hx2 _ ha', (-a) • x1, hsmul_nonneg _ hx1 _ ha', ?_⟩ calc a • (x1 - x2) = a • x1 - a • x2 := by simp [smul_sub] _ = (-a) • x2 - (-a) • x1 := by simp [sub_eq_add_neg, add_comm, neg_smul] · intro z hz rcases hz with ⟨x, hx, y, hy, rfl⟩ exact Submodule.sub_mem _ (Submodule.subset_span hx) (Submodule.subset_span hy) have hspan_affine : (Submodule.span Real K : Set (Fin n → Real)) = (affineSpan Real K : Set (Fin n → Real)) := by simpa [Set.insert_eq_of_mem h0] using (affineSpan_insert_zero (k:=Real) (s:=K)).symm let S : Submodule Real (Fin n → Real) := { carrier := {x : Fin n → Real | x ∈ K ∧ -x ∈ K} zero_mem' := by refine ⟨h0, ?_⟩ simpa using h0 add_mem' := by intro x y hx hy rcases hx with ⟨hxK, hxneg⟩ rcases hy with ⟨hyK, hyneg⟩ refine ⟨hadd _ hxK _ hyK, ?_⟩ simpa [neg_add] using hadd (-y) hyneg (-x) hxneg smul_mem' := by intro a x hx rcases hx with ⟨hxK, hxneg⟩ by_cases ha : 0 ≤ a · have h1 : a • x ∈ K := hsmul_nonneg x hxK a ha have h2 : a • (-x) ∈ K := hsmul_nonneg (-x) hxneg a ha refine ⟨h1, ?_⟩ simpa [smul_neg] using h2 · have ha' : 0 ≤ -a := by linarith have h1 : (-a) • (-x) ∈ K := hsmul_nonneg (-x) hxneg (-a) ha' have h2 : (-a) • x ∈ K := hsmul_nonneg x hxK (-a) ha' refine ⟨?_, ?_⟩ · simpa [smul_neg, neg_smul] using h1 · simpa [neg_smul] using h2 } have hSsubset : (S : Set (Fin n → Real)) ⊆ K := by intro x hx exact hx.1 have hSmax : ∀ T : Submodule Real (Fin n → Real), (T : Set (Fin n → Real)) ⊆ K → T ≤ S := by intro T hT x hx refine ⟨hT hx, ?_⟩ exact hT (by simpa using T.neg_mem hx) refine ⟨hspan_eq, hspan_affine, ?_⟩ refine ⟨S, hSsubset, hSmax, rfl⟩

Definition 2.7.10. A vector is normal to a convex set Unknown identifier `C`C at a point Unknown identifier `a`sorry ∈ sorry : Propa ∈ Unknown identifier `C`C if for every Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `C`C; the set of all vectors normal to Unknown identifier `C`C at Unknown identifier `a`a is called the normal cone to Unknown identifier `C`C at Unknown identifier `a`a.

def IsNormalToConvexSet (n : Nat) (C : Set (Fin n → Real)) (a xstar : Fin n → Real) : Prop := a ∈ C ∧ ∀ x ∈ C, (x - a) ⬝ᵥ xstar ≤ 0

Definition 2.7.10. The normal cone to Unknown identifier `C`C at Unknown identifier `a`a is the set of all vectors normal to Unknown identifier `C`C at Unknown identifier `a`a.

def normalConeAt (n : Nat) (C : Set (Fin n → Real)) (a : Fin n → Real) : Set (Fin n → Real) := {xstar : Fin n → Real | IsNormalToConvexSet n C a xstar}

Definition 2.7.11. The barrier cone of a convex set Unknown identifier `C`C is the set of all vectors such that there exists failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `β`β ∈ ℝ with for every Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `C`C.

def barrierCone (n : Nat) (C : Set (Fin n → Real)) : Set (Fin n → Real) := {xstar : Fin n → Real | ∃ β : Real, ∀ x ∈ C, x ⬝ᵥ xstar ≤ β}

The barrier cone is closed under positive scalar multiplication.

lemma barrierCone_smul_mem (n : Nat) (C : Set (Fin n → Real)) {xstar : Fin n → Real} (hx : xstar ∈ barrierCone n C) {t : Real} (ht : 0 < t) : t • xstar ∈ barrierCone n C := by rcases hx with ⟨β, hxβ⟩ refine ⟨t * β, ?_⟩ intro x hxC have hle : x ⬝ᵥ xstar ≤ β := hxβ x hxC have hmul : t * (x ⬝ᵥ xstar) ≤ t * β := by exact mul_le_mul_of_nonneg_left hle (le_of_lt ht) simpa [dotProduct_smul, mul_assoc, mul_left_comm, mul_comm] using hmul

The barrier cone is closed under addition.

lemma barrierCone_add_mem (n : Nat) (C : Set (Fin n → Real)) {xstar1 : Fin n → Real} (hx1 : xstar1 ∈ barrierCone n C) {xstar2 : Fin n → Real} (hx2 : xstar2 ∈ barrierCone n C) : xstar1 + xstar2 ∈ barrierCone n C := by rcases hx1 with ⟨β1, hx1β⟩ rcases hx2 with ⟨β2, hx2β⟩ refine ⟨β1 + β2, ?_⟩ intro x hxC have h1 : x ⬝ᵥ xstar1 ≤ β1 := hx1β x hxC have h2 : x ⬝ᵥ xstar2 ≤ β2 := hx2β x hxC have hsum : x ⬝ᵥ xstar1 + x ⬝ᵥ xstar2 ≤ β1 + β2 := add_le_add h1 h2 simpa [dotProduct_add] using hsum

The normal cone at Unknown identifier `a`a is closed under addition.

lemma normalConeAt_add_mem (n : Nat) (C : Set (Fin n → Real)) (a : Fin n → Real) {xstar1 : Fin n → Real} (hx1 : xstar1 ∈ normalConeAt n C a) {xstar2 : Fin n → Real} (hx2 : xstar2 ∈ normalConeAt n C a) : xstar1 + xstar2 ∈ normalConeAt n C a := by rcases hx1 with ⟨ha1, hx1⟩ rcases hx2 with ⟨_, hx2⟩ refine ⟨ha1, ?_⟩ intro x hxC have h1 : (x - a) ⬝ᵥ xstar1 ≤ 0 := hx1 x hxC have h2 : (x - a) ⬝ᵥ xstar2 ≤ 0 := hx2 x hxC have hsum : (x - a) ⬝ᵥ xstar1 + (x - a) ⬝ᵥ xstar2 ≤ 0 := add_nonpos h1 h2 simpa [dotProduct_add] using hsum

The normal cone at Unknown identifier `a`a is closed under positive scalar multiplication.

lemma normalConeAt_smul_mem (n : Nat) (C : Set (Fin n → Real)) (a : Fin n → Real) {xstar : Fin n → Real} (hx : xstar ∈ normalConeAt n C a) {t : Real} (ht : 0 < t) : t • xstar ∈ normalConeAt n C a := by rcases hx with ⟨ha, hx⟩ refine ⟨ha, ?_⟩ intro x hxC have h : (x - a) ⬝ᵥ xstar ≤ 0 := hx x hxC have hsmul : t • ((x - a) ⬝ᵥ xstar) ≤ 0 := smul_nonpos_of_nonneg_of_nonpos (le_of_lt ht) h simpa [dotProduct_smul] using hsmul

Proposition 2.7.12. For a convex set failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `C`C ⊆ ℝ^Unknown identifier `n`n and a point Unknown identifier `a`sorry ∈ sorry : Propa ∈ Unknown identifier `C`C, the normal cone to Unknown identifier `C`C at Unknown identifier `a`a is a convex cone.

theorem normalConeAt_isConvexCone (n : Nat) (C : Set (Fin n → Real)) (a : Fin n → Real) (_hC : Convex Real C) (_ha : a ∈ C) : IsConvexCone n (normalConeAt n C a) := by refine (isConvexCone_iff_add_closed_and_pos_smul_closed n (normalConeAt n C a)).2 ?_ refine ⟨?_, ?_⟩ · intro x hx y hy exact normalConeAt_add_mem n C a hx hy · intro x hx t ht exact normalConeAt_smul_mem n C a hx ht

Proposition 2.7.13. For a convex set failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `C`C ⊆ ℝ^Unknown identifier `n`n, the barrier cone of Unknown identifier `C`C is a convex cone.

theorem barrierCone_isConvexCone (n : Nat) (C : Set (Fin n → Real)) (_hC : Convex Real C) : IsConvexCone n (barrierCone n C) := by refine (isConvexCone_iff_add_closed_and_pos_smul_closed n (barrierCone n C)).2 ?_ refine ⟨?_, ?_⟩ · intro x hx y hy exact barrierCone_add_mem n C hx hy · intro x hx t ht exact barrierCone_smul_mem n C hx ht

The dot-product half-space is convex.

lemma convex_closedHalfSpaceLE_dotProduct (n : Nat) (b : Fin n → Real) (β : Real) : Convex Real (closedHalfSpaceLE n b β) := by simpa [closedHalfSpaceLE] using (convex_dotProduct_le n b β)

The dot-product half-space is convex.

lemma convex_closedHalfSpaceGE_dotProduct (n : Nat) (b : Fin n → Real) (β : Real) : Convex Real (closedHalfSpaceGE n b β) := by simpa [closedHalfSpaceGE] using (convex_halfSpace_ge (f := fun x : Fin n → Real => x ⬝ᵥ b) (h := isLinearMap_dotProduct_left n b) β)

The strict dot-product half-spaces ( and ) are convex.

lemma convex_openHalfSpaces_dotProduct (n : Nat) (b : Fin n → Real) (β : Real) : Convex Real (openHalfSpaceLT n b β) ∧ Convex Real (openHalfSpaceGT n b β) := by constructor · simpa [openHalfSpaceLT] using (convex_halfSpace_lt (f := fun x : Fin n → Real => x ⬝ᵥ b) (h := isLinearMap_dotProduct_left n b) β) · simpa [openHalfSpaceGT] using (convex_halfSpace_gt (f := fun x : Fin n → Real => x ⬝ᵥ b) (h := isLinearMap_dotProduct_left n b) β)

Corollary 2.0.4. For non-zero failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `b`b ∈ Real^Unknown identifier `n`n and failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `β`β ∈ Real, each of the four half-spaces , , , is a convex subset of ℝ ^ sorry : TypeReal^Unknown identifier `n`n.

theorem convex_halfSpaces_dotProduct (n : Nat) (b : Fin n → Real) (hb : b ≠ 0) (β : Real) : Convex Real (closedHalfSpaceLE n b β) ∧ Convex Real (closedHalfSpaceGE n b β) ∧ Convex Real (openHalfSpaceLT n b β) ∧ Convex Real (openHalfSpaceGT n b β) := by have hb' : b ≠ 0 := hb clear hb' refine ⟨convex_closedHalfSpaceLE_dotProduct n b β, ?_⟩ refine ⟨convex_closedHalfSpaceGE_dotProduct n b β, ?_⟩ exact convex_openHalfSpaces_dotProduct n b β

Proposition 2.0.5. Every affine subset of ℝ ^ sorry : Typeℝ^Unknown identifier `n`n (including ∅ : ?m.1∅ and ℝ ^ sorry : Typeℝ^Unknown identifier `n`n itself) is convex.

theorem isAffineSet_imp_convex (n : Nat) (M : Set (Fin n → Real)) (hM : IsAffineSet n M) : Convex Real M := by rcases (isAffineSet_iff_affineSubspace n M).1 hM with ⟨s, rfl⟩ simpa using (s.convex : Convex Real (s : Set (Fin n → Real)))

A nonzero vector has positive dot product with itself.

lemma dotProduct_self_pos_of_ne_zero {n : Nat} {b : Fin n → Real} (hb : b ≠ 0) : 0 < b ⬝ᵥ b := by have hb' : (0 < b ⬝ᵥ b ↔ b ≠ 0) := by simpa using (Matrix.dotProduct_self_star_pos_iff (v := b)) exact hb'.2 hb

For nonzero Unknown identifier `b`b, there is a vector with prescribed dot product with Unknown identifier `b`b.

lemma exists_dotProduct_eq_of_ne_zero (n : Nat) (b : Fin n → Real) (β : Real) (hb : b ≠ 0) : ∃ x0 : Fin n → Real, x0 ⬝ᵥ b = β := by have hbpos : 0 < b ⬝ᵥ b := dotProduct_self_pos_of_ne_zero (b := b) hb have hbne : b ⬝ᵥ b ≠ 0 := ne_of_gt hbpos refine ⟨(β / (b ⬝ᵥ b)) • b, ?_⟩ simp [div_eq_mul_inv, hbne]

Dot products with Unknown identifier `b`b after shifting by in the left argument.

lemma dotProduct_shift_by_b (n : Nat) (b x : Fin n → Real) : (x + b) ⬝ᵥ b = x ⬝ᵥ b + b ⬝ᵥ b ∧ (x - b) ⬝ᵥ b = x ⬝ᵥ b - b ⬝ᵥ b := by constructor <;> simp

Proposition 2.0.6. For any non-zero failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `b`b ∈ Real^Unknown identifier `n`n and any failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `β`β ∈ Real, each of the four half-spaces , , , is non-empty.

theorem halfSpaces_dotProduct_nonempty (n : Nat) (b : Fin n → Real) (hb : b ≠ 0) (β : Real) : (closedHalfSpaceLE n b β).Nonempty ∧ (closedHalfSpaceGE n b β).Nonempty ∧ (openHalfSpaceLT n b β).Nonempty ∧ (openHalfSpaceGT n b β).Nonempty := by have hbpos : 0 < b ⬝ᵥ b := dotProduct_self_pos_of_ne_zero (b := b) hb obtain ⟨x0, hx0⟩ := exists_dotProduct_eq_of_ne_zero n b β hb refine ⟨?_, ?_⟩ · refine ⟨x0, ?_⟩ simp [closedHalfSpaceLE, hx0] refine ⟨?_, ?_⟩ · refine ⟨x0, ?_⟩ simp [closedHalfSpaceGE, hx0] refine ⟨?_, ?_⟩ · refine ⟨x0 - b, ?_⟩ have hminus : (x0 - b) ⬝ᵥ b = x0 ⬝ᵥ b - b ⬝ᵥ b := (dotProduct_shift_by_b n b x0).2 have : β - b ⬝ᵥ b < β := sub_lt_self β hbpos simpa [openHalfSpaceLT, hminus, hx0] using this · refine ⟨x0 + b, ?_⟩ have hplus : (x0 + b) ⬝ᵥ b = x0 ⬝ᵥ b + b ⬝ᵥ b := (dotProduct_shift_by_b n b x0).1 have : β < β + b ⬝ᵥ b := lt_add_of_pos_right β hbpos simpa [openHalfSpaceGT, hplus, hx0] using this

A comparison symbol for linear inequalities/equations.

inductive LinearComparison : Type | le | ge | lt | gt | eq

Interpret as a subset of ℝ ^ sorry : TypeReal^Unknown identifier `n`n.

def linearComparisonSet (n : Nat) (b : Fin n → Real) (β : Real) : LinearComparison → Set (Fin n → Real) | .le => closedHalfSpaceLE n b β | .ge => closedHalfSpaceGE n b β | .lt => openHalfSpaceLT n b β | .gt => openHalfSpaceGT n b β | .eq => {x : Fin n → Real | x ⬝ᵥ b = β}

The hyperplane is convex, as an intersection of the two closed half-spaces and .

lemma convex_dotProduct_eq (n : Nat) (b : Fin n → Real) (β : Real) : Convex Real {x : Fin n → Real | x ⬝ᵥ b = β} := by have hset : ({x : Fin n → Real | x ⬝ᵥ b = β} : Set (Fin n → Real)) = closedHalfSpaceLE n b β ∩ closedHalfSpaceGE n b β := by ext x constructor · intro hx have hx' : x ⬝ᵥ b = β := by simpa using hx refine ⟨?_, ?_⟩ · simp [closedHalfSpaceLE, hx'] · simp [closedHalfSpaceGE, hx'] · rintro ⟨hxle, hxge⟩ show x ⬝ᵥ b = β exact le_antisymm hxle hxge simpa [hset] using (convex_closedHalfSpaceLE_dotProduct n b β).inter (convex_closedHalfSpaceGE_dotProduct n b β)

Each of the five comparison relations (, , , , ) defines a convex subset of ℝ ^ sorry : TypeReal^Unknown identifier `n`n via linearComparisonSet (n : ℕ) (b : Fin n → ℝ) (β : ℝ) : LinearComparison → Set (Fin n → ℝ)linearComparisonSet.

lemma convex_linearComparisonSet (n : Nat) (b : Fin n → Real) (β : Real) (r : LinearComparison) : Convex Real (linearComparisonSet n b β r) := by cases r with | le => simpa [linearComparisonSet] using (convex_closedHalfSpaceLE_dotProduct n b β) | ge => simpa [linearComparisonSet] using (convex_closedHalfSpaceGE_dotProduct n b β) | lt => simpa [linearComparisonSet] using (convex_openHalfSpaces_dotProduct n b β).1 | gt => simpa [linearComparisonSet] using (convex_openHalfSpaces_dotProduct n b β).2 | eq => simpa [linearComparisonSet] using (convex_dotProduct_eq n b β)

The solution set of a family of linear comparisons is the intersection of the individual constraint sets.

lemma solutionSet_linearComparison_eq_iInter {ι : Sort*} (n : Nat) (b : ι → Fin n → Real) (β : ι → Real) (rel : ι → LinearComparison) : {x : Fin n → Real | ∀ i, x ∈ linearComparisonSet n (b i) (β i) (rel i)} = ⋂ i, linearComparisonSet n (b i) (β i) (rel i) := by ext x simp

Corollary 2.1.2. Given any system of simultaneous linear inequalities and equations in Unknown identifier `n`n variables, obtained by combining relations of the form , , , , and (with failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `b`b i ∈ Real^Unknown identifier `n`n and failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `β`β i ∈ Real), the set of all solutions failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `C`C ⊆ Real^Unknown identifier `n`n is convex.

theorem convex_solutionSet_linearComparison {ι : Sort*} (n : Nat) (b : ι → Fin n → Real) (β : ι → Real) (rel : ι → LinearComparison) : Convex Real {x : Fin n → Real | ∀ i, x ∈ linearComparisonSet n (b i) (β i) (rel i)} := by have hC : ∀ i, Convex Real (linearComparisonSet n (b i) (β i) (rel i)) := fun i => convex_linearComparisonSet n (b i) (β i) (rel i) simpa [solutionSet_linearComparison_eq_iInter (n := n) (b := b) (β := β) (rel := rel)] using (convex_iInter_family (n := n) (C := fun i => linearComparisonSet n (b i) (β i) (rel i)) hC)

If Unknown identifier `D`D lies in an affine subspace Unknown identifier `A`A, then the dimension of Unknown identifier `D`D is at most the finrank of Unknown identifier `A.direction`A.direction.

lemma convexSetDim_le_finrank_direction_of_subset_affineSubspace {n : Nat} {D : Set (Fin n → Real)} {A : AffineSubspace Real (Fin n → Real)} (hDA : D ⊆ (A : Set (Fin n → Real))) : convexSetDim n D ≤ Module.finrank Real A.direction := by have hspan : affineSpan Real D ≤ A := affineSpan_le_of_subset_coe (k := Real) hDA have hdir : (affineSpan Real D).direction ≤ A.direction := AffineSubspace.direction_le hspan simpa [convexSetDim] using (Submodule.finrank_mono hdir)

If Unknown identifier `D`D contains a 2 : ℕ2-simplex, then the dimension of Unknown identifier `D`D is at least 2 : ℕ2.

lemma two_le_convexSetDim_of_exists_simplex_two {n : Nat} {D : Set (Fin n → Real)} (hsimplex : ∃ P, P ⊆ D ∧ IsSimplex n 2 P) : 2 ≤ convexSetDim n D := by rcases hsimplex with ⟨P, hPD, hP⟩ simpa using (simplex_dim_le_convexSetDim n D 2 P hPD hP)

Proposition 2.4.11. Every convex disk in ℝ ^ sorry : Typeℝ^Unknown identifier `n`n has dimension 2 : ℕ2, independently of the ambient dimension Unknown identifier `n`n.

theorem convexDisk_convexSetDim_eq_two (n : Nat) (D : Set (Fin n → Real)) (hconv : Convex Real D) (hsub : ∃ A : AffineSubspace Real (Fin n → Real), D ⊆ (A : Set (Fin n → Real)) ∧ Module.finrank Real A.direction = 2) (hsimplex : ∃ P, P ⊆ D ∧ IsSimplex n 2 P) : convexSetDim n D = 2 := by have _hconv : Convex Real D := hconv rcases hsub with ⟨A, hDA, hArank⟩ have hle : convexSetDim n D ≤ 2 := by simpa [hArank] using (convexSetDim_le_finrank_direction_of_subset_affineSubspace (n := n) (D := D) (A := A) hDA) have hge : 2 ≤ convexSetDim n D := two_le_convexSetDim_of_exists_simplex_two (n := n) (D := D) hsimplex exact Nat.le_antisymm hle hge

Rewrite as .

lemma setOf_forall_dotProduct_ge_zero_eq_setOf_forall_dotProduct_le_zero_neg {ι : Sort*} (n : Nat) (b : ι → Fin n → Real) : {x : Fin n → Real | ∀ i, 0 ≤ x ⬝ᵥ b i} = {x : Fin n → Real | ∀ i, x ⬝ᵥ (-b i) ≤ 0} := by ext x constructor · intro hx i have : -(x ⬝ᵥ b i) ≤ (0 : Real) := (neg_nonpos).2 (hx i) simpa [dotProduct_neg] using this · intro hx i have : -(x ⬝ᵥ b i) ≤ (0 : Real) := by simpa [dotProduct_neg] using hx i exact (neg_nonpos).1 this

Corollary 2.5.2. Let failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `b`b i ∈ Real^Unknown identifier `n`n for Unknown identifier `i`sorry ∈ sorry : Propi ∈ Unknown identifier `I`I, where Unknown identifier `I`I is an arbitrary index set. Then is a convex cone.

theorem convexCone_of_dotProduct_ge_zero {ι : Sort*} (n : Nat) (b : ι → Fin n → Real) : IsConvexCone n {x : Fin n → Real | ∀ i, 0 ≤ x ⬝ᵥ b i} := by simpa [setOf_forall_dotProduct_ge_zero_eq_setOf_forall_dotProduct_le_zero_neg (n := n) (b := b)] using (convexCone_of_dotProduct_le_zero (n := n) (b := fun i => -b i))

Pointwise add-closure for {x | ∀ (i : ?m.22 x), 0 < x ⬝ᵥ sorry} : Set (?m.11 → ℕ){x | ∀ i, 0 < x ⬝ᵥ Unknown identifier `b`b i}.

lemma add_mem_setOf_forall_dotProduct_pos {ι : Sort*} {n : Nat} {b : ι → Fin n → Real} {x y : Fin n → Real} : (∀ i, 0 < x ⬝ᵥ b i) → (∀ i, 0 < y ⬝ᵥ b i) → (∀ i, 0 < (x + y) ⬝ᵥ b i) := by intro hx hy i have hpos : 0 < x ⬝ᵥ b i + y ⬝ᵥ b i := add_pos (hx i) (hy i) simpa [add_dotProduct] using hpos

Pointwise positive-scalar closure for {x | ∀ (i : ?m.22 x), 0 < x ⬝ᵥ sorry} : Set (?m.11 → ℕ){x | ∀ i, 0 < x ⬝ᵥ Unknown identifier `b`b i}.

lemma smul_mem_setOf_forall_dotProduct_pos {ι : Sort*} {n : Nat} {b : ι → Fin n → Real} {x : Fin n → Real} {t : Real} : (∀ i, 0 < x ⬝ᵥ b i) → 0 < t → (∀ i, 0 < (t • x) ⬝ᵥ b i) := by intro hx ht i have hpos : 0 < t * (x ⬝ᵥ b i) := mul_pos ht (hx i) simpa [smul_dotProduct] using hpos

Corollary 2.5.3. Let failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `b`b i ∈ Real^Unknown identifier `n`n for Unknown identifier `i`sorry ∈ sorry : Propi ∈ Unknown identifier `I`I, where Unknown identifier `I`I is an arbitrary index set. Then is a convex cone.

theorem convexCone_of_dotProduct_pos {ι : Sort*} (n : Nat) (b : ι → Fin n → Real) : IsConvexCone n {x : Fin n → Real | ∀ i, 0 < x ⬝ᵥ b i} := by refine (isConvexCone_iff_add_closed_and_pos_smul_closed n {x : Fin n → Real | ∀ i, 0 < x ⬝ᵥ b i}).2 ?_ refine ⟨?_, ?_⟩ · intro x hx y hy exact add_mem_setOf_forall_dotProduct_pos (x := x) (y := y) hx hy · intro x hx t ht exact smul_mem_setOf_forall_dotProduct_pos (x := x) (t := t) hx ht

Rewrite as .

lemma setOf_forall_dotProduct_lt_zero_eq_setOf_forall_dotProduct_pos_neg {ι : Sort*} (n : Nat) (b : ι → Fin n → Real) : {x : Fin n → Real | ∀ i, x ⬝ᵥ b i < 0} = {x : Fin n → Real | ∀ i, 0 < x ⬝ᵥ (-b i)} := by ext x constructor · intro hx i have : 0 < -(x ⬝ᵥ b i) := (neg_pos).2 (hx i) simpa [dotProduct_neg] using this · intro hx i have : 0 < -(x ⬝ᵥ b i) := by simpa [dotProduct_neg] using hx i exact (neg_pos).1 this

Corollary 2.5.4. Let failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `b`b i ∈ Real^Unknown identifier `n`n for Unknown identifier `i`sorry ∈ sorry : Propi ∈ Unknown identifier `I`I, where Unknown identifier `I`I is an arbitrary index set. Then is a convex cone.

theorem convexCone_of_dotProduct_lt_zero {ι : Sort*} (n : Nat) (b : ι → Fin n → Real) : IsConvexCone n {x : Fin n → Real | ∀ i, x ⬝ᵥ b i < 0} := by simpa [setOf_forall_dotProduct_lt_zero_eq_setOf_forall_dotProduct_pos_neg (n := n) (b := b)] using (convexCone_of_dotProduct_pos (ι := ι) (n := n) (b := fun i => -b i))

Pointwise add-closure for {x | ∀ (i : ?m.19 x), x ⬝ᵥ sorry = 0} : Set (?m.9 → ℕ){x | ∀ i, x ⬝ᵥ Unknown identifier `b`b i = 0}.

lemma add_mem_setOf_forall_dotProduct_eq_zero {ι : Sort*} {n : Nat} {b : ι → Fin n → Real} {x y : Fin n → Real} : (∀ i, x ⬝ᵥ b i = 0) → (∀ i, y ⬝ᵥ b i = 0) → (∀ i, (x + y) ⬝ᵥ b i = 0) := by intro hx hy i simp [add_dotProduct, hx i, hy i]

Pointwise scalar closure for {x | ∀ (i : ?m.19 x), x ⬝ᵥ sorry = 0} : Set (?m.9 → ℕ){x | ∀ i, x ⬝ᵥ Unknown identifier `b`b i = 0}.

lemma smul_mem_setOf_forall_dotProduct_eq_zero {ι : Sort*} {n : Nat} {b : ι → Fin n → Real} {x : Fin n → Real} {t : Real} : (∀ i, x ⬝ᵥ b i = 0) → (∀ i, (t • x) ⬝ᵥ b i = 0) := by intro hx i simp [smul_dotProduct, hx i]

Corollary 2.5.5. Let failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `b`b i ∈ Real^Unknown identifier `n`n for Unknown identifier `i`sorry ∈ sorry : Propi ∈ Unknown identifier `I`I, where Unknown identifier `I`I is an arbitrary index set. Then is a convex cone.

theorem convexCone_of_dotProduct_eq_zero {ι : Sort*} (n : Nat) (b : ι → Fin n → Real) : IsConvexCone n {x : Fin n → Real | ∀ i, x ⬝ᵥ b i = 0} := by refine (isConvexCone_iff_add_closed_and_pos_smul_closed n {x : Fin n → Real | ∀ i, x ⬝ᵥ b i = 0}).2 ?_ refine ⟨?_, ?_⟩ · intro x hx y hy exact add_mem_setOf_forall_dotProduct_eq_zero (x := x) (y := y) hx hy · intro x hx t ht exact smul_mem_setOf_forall_dotProduct_eq_zero (x := x) (t := t) hx

Each homogeneous linear comparison set is a convex cone.

lemma convexCone_linearComparisonSet_zero (n : Nat) (b : Fin n → Real) (r : LinearComparison) : IsConvexCone n (linearComparisonSet n b (0 : Real) r) := by cases r with | le => simpa [linearComparisonSet, closedHalfSpaceLE] using (IsConvexCone_dotProduct_le_zero n b) | ge => have hset : (linearComparisonSet n b (0 : Real) LinearComparison.ge) = {x : Fin n → Real | x ⬝ᵥ (-b) ≤ 0} := by ext x constructor · intro hx have : 0 ≤ x ⬝ᵥ b := by simpa [linearComparisonSet, closedHalfSpaceGE] using hx have : -(x ⬝ᵥ b) ≤ 0 := (neg_nonpos).2 this simpa [dotProduct_neg] using this · intro hx have : -(x ⬝ᵥ b) ≤ 0 := by simpa [dotProduct_neg] using hx have : 0 ≤ x ⬝ᵥ b := (neg_nonpos).1 this simpa [linearComparisonSet, closedHalfSpaceGE] using this simpa [hset] using (IsConvexCone_dotProduct_le_zero n (-b)) | lt => have hset : (linearComparisonSet n b (0 : Real) LinearComparison.lt) = {x : Fin n → Real | 0 < x ⬝ᵥ (-b)} := by ext x constructor · intro hx have : x ⬝ᵥ b < 0 := by simpa [linearComparisonSet, openHalfSpaceLT] using hx have : 0 < -(x ⬝ᵥ b) := (neg_pos).2 this simpa [dotProduct_neg] using this · intro hx have : 0 < -(x ⬝ᵥ b) := by simpa [dotProduct_neg] using hx have : x ⬝ᵥ b < 0 := (neg_pos).1 this simpa [linearComparisonSet, openHalfSpaceLT] using this -- Reuse Corollary 2.5.3 on `-b` and the set equality above. have : IsConvexCone n {x : Fin n → Real | 0 < x ⬝ᵥ (-b)} := by simpa using (convexCone_of_dotProduct_pos (ι := PUnit.{0}) (n := n) (b := fun _ => -b)) simpa [hset] using this | gt => -- Directly show closure under addition and positive scaling. refine (isConvexCone_iff_add_closed_and_pos_smul_closed n (linearComparisonSet n b (0 : Real) LinearComparison.gt)).2 ?_ refine ⟨?_, ?_⟩ · intro x hx y hy have hx' : 0 < x ⬝ᵥ b := by simpa [linearComparisonSet, openHalfSpaceGT] using hx have hy' : 0 < y ⬝ᵥ b := by simpa [linearComparisonSet, openHalfSpaceGT] using hy have hpos : 0 < x ⬝ᵥ b + y ⬝ᵥ b := add_pos hx' hy' have : 0 < (x + y) ⬝ᵥ b := by simpa [add_dotProduct] using hpos simpa [linearComparisonSet, openHalfSpaceGT] using this · intro x hx t ht have hx' : 0 < x ⬝ᵥ b := by simpa [linearComparisonSet, openHalfSpaceGT] using hx have hpos : 0 < t * (x ⬝ᵥ b) := mul_pos ht hx' have : 0 < (t • x) ⬝ᵥ b := by simpa [smul_dotProduct] using hpos simpa [linearComparisonSet, openHalfSpaceGT] using this | eq => refine (isConvexCone_iff_add_closed_and_pos_smul_closed n (linearComparisonSet n b (0 : Real) LinearComparison.eq)).2 ?_ refine ⟨?_, ?_⟩ · intro x hx y hy have hx' : x ⬝ᵥ b = 0 := by simpa [linearComparisonSet] using hx have hy' : y ⬝ᵥ b = 0 := by simpa [linearComparisonSet] using hy have : (x + y) ⬝ᵥ b = 0 := by simp [add_dotProduct, hx', hy'] simpa [linearComparisonSet] using this · intro x hx t _ht have hx' : x ⬝ᵥ b = 0 := by simpa [linearComparisonSet] using hx have : (t • x) ⬝ᵥ b = 0 := by simp [smul_dotProduct, hx'] simpa [linearComparisonSet] using this

Corollary 2.5.6. Let failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `b`b i ∈ Real^Unknown identifier `n`n for Unknown identifier `i`sorry ∈ sorry : Propi ∈ Unknown identifier `I`I, where Unknown identifier `I`I is an arbitrary index set, and consider a system of homogeneous linear relations of the form , , , , and for various indices Unknown identifier `i`sorry ∈ sorry : Propi ∈ Unknown identifier `I`I. Then the set Unknown identifier `K`K of all solutions failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `x`x ∈ Real^Unknown identifier `n`n is a convex cone.

theorem convexCone_solutionSet_homogeneous_linearComparison {ι : Sort*} (n : Nat) (b : ι → Fin n → Real) (rel : ι → LinearComparison) : IsConvexCone n {x : Fin n → Real | ∀ i, x ∈ linearComparisonSet n (b i) (0 : Real) (rel i)} := by have hK : ∀ i, IsConvexCone n (linearComparisonSet n (b i) (0 : Real) (rel i)) := fun i => convexCone_linearComparisonSet_zero n (b i) (rel i) simpa [solutionSet_linearComparison_eq_iInter (n := n) (b := b) (β := fun _ => (0 : Real)) (rel := rel)] using (convexCone_iInter_family (n := n) (K := fun i => linearComparisonSet n (b i) (0 : Real) (rel i)) hK)

A submodule (linear subspace) is closed under addition.

lemma submodule_add_closed (n : Nat) (S : Submodule Real (Fin n → Real)) : ∀ x ∈ (S : Set (Fin n → Real)), ∀ y ∈ (S : Set (Fin n → Real)), x + y ∈ (S : Set (Fin n → Real)) := by intro x hx y hy exact S.add_mem hx hy

A submodule (linear subspace) is closed under positive scalar multiplication.

lemma submodule_pos_smul_closed (n : Nat) (S : Submodule Real (Fin n → Real)) : ∀ x ∈ (S : Set (Fin n → Real)), ∀ t : Real, 0 < t → t • x ∈ (S : Set (Fin n → Real)) := by intro x hx t _ht exact S.smul_mem t hx

Proposition 2.5.14. Every linear subspace of ℝ ^ sorry : TypeReal^Unknown identifier `n`n is a convex cone.

theorem submodule_isConvexCone (n : Nat) (S : Submodule Real (Fin n → Real)) : IsConvexCone n (S : Set (Fin n → Real)) := by refine (isConvexCone_iff_add_closed_and_pos_smul_closed n (S : Set (Fin n → Real))).2 ?_ exact ⟨submodule_add_closed n S, submodule_pos_smul_closed n S⟩

The nonnegative orthant is closed under addition.

lemma nonNegativeOrthant_add_mem (n : Nat) : ∀ x ∈ nonNegativeOrthant n, ∀ y ∈ nonNegativeOrthant n, x + y ∈ nonNegativeOrthant n := by intro x hx y hy simp [nonNegativeOrthant] at hx hy ⊢ intro i exact add_nonneg (hx i) (hy i)

The nonnegative orthant is closed under positive scalar multiplication.

lemma nonNegativeOrthant_pos_smul_mem (n : Nat) : ∀ x ∈ nonNegativeOrthant n, ∀ t : Real, 0 < t → t • x ∈ nonNegativeOrthant n := by intro x hx t ht simp [nonNegativeOrthant] at hx ⊢ intro i have : 0 ≤ t * x i := mul_nonneg (le_of_lt ht) (hx i) simpa [smul_eq_mul] using this

The positive orthant is closed under addition.

lemma positiveOrthant_add_mem (n : Nat) : ∀ x ∈ positiveOrthant n, ∀ y ∈ positiveOrthant n, x + y ∈ positiveOrthant n := by intro x hx y hy simp [positiveOrthant] at hx hy ⊢ intro i exact add_pos (hx i) (hy i)

The positive orthant is closed under positive scalar multiplication.

lemma positiveOrthant_pos_smul_mem (n : Nat) : ∀ x ∈ positiveOrthant n, ∀ t : Real, 0 < t → t • x ∈ positiveOrthant n := by intro x hx t ht simp [positiveOrthant] at hx ⊢ intro i have : 0 < t * x i := mul_pos ht (hx i) simpa [smul_eq_mul] using this

Proposition 2.5.15. The non-negative orthant and the positive orthant of ℝ ^ sorry : TypeReal^Unknown identifier `n`n are convex cones.

theorem orthants_isConvexCone (n : Nat) : IsConvexCone n (nonNegativeOrthant n) ∧ IsConvexCone n (positiveOrthant n) := by refine ⟨?_, ?_⟩ · refine (isConvexCone_iff_add_closed_and_pos_smul_closed n (nonNegativeOrthant n)).2 ?_ exact ⟨nonNegativeOrthant_add_mem n, nonNegativeOrthant_pos_smul_mem n⟩ · refine (isConvexCone_iff_add_closed_and_pos_smul_closed n (positiveOrthant n)).2 ?_ exact ⟨positiveOrthant_add_mem n, positiveOrthant_pos_smul_mem n⟩

Proposition 2.5.16. The open and closed half-spaces corresponding to a hyperplane through the origin are convex cones. Concretely, for , the hyperplane has associated closed half-spaces , and open half-spaces , .

theorem halfSpaces_through_origin_isConvexCone (n : Nat) (b : Fin n → Real) : IsConvexCone n (closedHalfSpaceLE n b (0 : Real)) ∧ IsConvexCone n (closedHalfSpaceGE n b (0 : Real)) ∧ IsConvexCone n (openHalfSpaceLT n b (0 : Real)) ∧ IsConvexCone n (openHalfSpaceGT n b (0 : Real)) := by refine ⟨?_, ?_⟩ · simpa [closedHalfSpaceLE] using (convexCone_of_dotProduct_le_zero (ι := Unit) (n := n) (b := fun _ : Unit => b)) refine ⟨?_, ?_⟩ · simpa [closedHalfSpaceGE, ge_iff_le] using (convexCone_of_dotProduct_ge_zero (ι := Unit) (n := n) (b := fun _ : Unit => b)) refine ⟨?_, ?_⟩ · simpa [openHalfSpaceLT] using (convexCone_of_dotProduct_lt_zero (ι := Unit) (n := n) (b := fun _ : Unit => b)) · simpa [openHalfSpaceGT, gt_iff_lt] using (convexCone_of_dotProduct_pos (ι := Unit) (n := n) (b := fun _ : Unit => b))

Reading off the 0 : ℕ0-th coordinate of a Fin.cons.{u} {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin (n + 1)) : α iFin.cons equality gives the normalization .

lemma convexConeSection_sum_weights_eq_one_of_cons_eq {n m : Nat} {y : Fin n → Real} {x : Fin (m + 1) → Fin n → Real} {w : Fin (m + 1) → Real} (h : (Fin.cons (n := n) (α := fun _ : Fin (n + 1) => Real) (1 : Real) y) = ∑ i : Fin (m + 1), w i • (Fin.cons (n := n) (α := fun _ : Fin (n + 1) => Real) (1 : Real) (x i))) : (∑ i : Fin (m + 1), w i) = 1 := by have h0 := congrArg (fun f : Fin (n + 1) → Real => f 0) h have : (1 : Real) = ∑ i : Fin (m + 1), w i := by simpa [Finset.sum_apply, smul_eq_mul, mul_assoc] using h0 simpa using this.symm

Reading off the tail coordinates of a Fin.cons.{u} {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin (n + 1)) : α iFin.cons equality gives the corresponding weighted-sum identity in Fin sorry → ℝ : TypeFin Unknown identifier `n`n → ℝ.

lemma convexConeSection_tail_eq_sum_smul_of_cons_eq {n m : Nat} {y : Fin n → Real} {x : Fin (m + 1) → Fin n → Real} {w : Fin (m + 1) → Real} (h : (Fin.cons (n := n) (α := fun _ : Fin (n + 1) => Real) (1 : Real) y) = ∑ i : Fin (m + 1), w i • (Fin.cons (n := n) (α := fun _ : Fin (n + 1) => Real) (1 : Real) (x i))) : y = ∑ i : Fin (m + 1), w i • x i := by funext j have hj := congrArg (fun f : Fin (n + 1) → Real => f (Fin.succ j)) h simpa [Finset.sum_apply, smul_eq_mul, mul_assoc] using hj

Proposition 2.6.12. Every convex set failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `C`C ⊆ ℝ^Unknown identifier `n`n can be realized as a cross-section of a convex cone in a higher-dimensional space: there exists a convex cone failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `K`K ⊆ ℝ^{Unknown identifier `n`n+1} such that Unknown identifier `C`sorry = {x | sorry ∧ (1, x) ∈ sorry} : PropC = failed to synthesize Membership ?m.2 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.{x ∈ ℝ^Unknown identifier `n`n | (1, x) ∈ Unknown identifier `K`K}.

theorem exists_convexCone_section_eq (n : Nat) (C : Set (Fin n → Real)) (hC : Convex Real C) : ∃ K : Set (Fin (n + 1) → Real), IsConvexCone (n + 1) K ∧ C = {x : Fin n → Real | Fin.cons (n := n) (1 : Real) x ∈ K} := by classical let S : Set (Fin (n + 1) → Real) := {z : Fin (n + 1) → Real | ∃ x ∈ C, z = Fin.cons (n := n) (1 : Real) x} let K : Set (Fin (n + 1) → Real) := {y : Fin (n + 1) → Real | ∃ m : Nat, ∃ x : Fin (m + 1) → Fin (n + 1) → Real, ∃ w : Fin (m + 1) → Real, (∀ i, x i ∈ S) ∧ (∀ i, 0 < w i) ∧ y = ∑ i, w i • x i} have hKdata : IsConvexCone (n + 1) K ∧ S ⊆ K ∧ ∀ K' : Set (Fin (n + 1) → Real), IsConvexCone (n + 1) K' → S ⊆ K' → K ⊆ K' := by simpa [K, S] using (positiveLinearCombinationCone_isSmallest (n := n + 1) S) refine ⟨K, hKdata.1, ?_⟩ ext y constructor · intro hyC have hyS : Fin.cons (n := n) (α := fun _ : Fin (n + 1) => Real) (1 : Real) y ∈ S := ⟨y, hyC, rfl⟩ exact hKdata.2.1 hyS · intro hyK have hyK' : ∃ m : Nat, ∃ x : Fin (m + 1) → Fin (n + 1) → Real, ∃ w : Fin (m + 1) → Real, (∀ i, x i ∈ S) ∧ (∀ i, 0 < w i) ∧ Fin.cons (n := n) (α := fun _ : Fin (n + 1) => Real) (1 : Real) y = ∑ i, w i • x i := by simpa [K] using hyK rcases hyK' with ⟨m, x, w, hxS, hwpos, hsum⟩ have hxrepr : ∀ i : Fin (m + 1), ∃ xi : Fin n → Real, xi ∈ C ∧ x i = Fin.cons (n := n) (α := fun _ : Fin (n + 1) => Real) (1 : Real) xi := by intro i rcases hxS i with ⟨xi, hxiC, hxi⟩ exact ⟨xi, hxiC, hxi⟩ choose xC hxC hxEq using hxrepr have hsum' : Fin.cons (n := n) (α := fun _ : Fin (n + 1) => Real) (1 : Real) y = ∑ i : Fin (m + 1), w i • (Fin.cons (n := n) (α := fun _ : Fin (n + 1) => Real) (1 : Real) (xC i)) := by simpa [hxEq] using hsum have hwsum : (∑ i : Fin (m + 1), w i) = 1 := convexConeSection_sum_weights_eq_one_of_cons_eq (n := n) (m := m) (y := y) (x := xC) (w := w) hsum' have hy_eq : y = ∑ i : Fin (m + 1), w i • xC i := convexConeSection_tail_eq_sum_smul_of_cons_eq (n := n) (m := m) (y := y) (x := xC) (w := w) hsum' have hy_mem : (∑ i : Fin (m + 1), w i • xC i) ∈ C := by refine hC.sum_mem ?_ ?_ ?_ · intro i hi exact le_of_lt (hwpos i) · simpa using hwsum · intro i hi exact hxC i simpa [hy_eq] using hy_mem
end Section02end Chap01