Convex Analysis (Rockafellar, 1970) -- Chapter 02 -- Section 06 -- Part 6
noncomputable sectionopen scoped Pointwisesection Chap02section Section06
Corollary 6.8.1: Let C be a non-empty convex set in R^n, and let K be the convex
cone in R^{n+1} generated by {(1, x) | x ∈ C}. Then ri K consists of the pairs
such that and .
theorem euclideanRelativeInterior_convexConeGenerated_eq (n : Nat)
(C : Set (EuclideanSpace Real (Fin n))) (hC : Convex Real C) (hCne : C.Nonempty) :
let coords : EuclideanSpace Real (Fin (1 + n)) → (Fin (1 + n) → Real) :=
EuclideanSpace.equiv (𝕜 := Real) (ι := Fin (1 + n))
let first : EuclideanSpace Real (Fin (1 + n)) → Real := fun v => coords v 0
let tail : EuclideanSpace Real (Fin (1 + n)) → EuclideanSpace Real (Fin n) :=
fun v =>
(EuclideanSpace.equiv (𝕜 := Real) (ι := Fin n)).symm
(fun i => coords v (Fin.natAdd 1 i))
let S : Set (EuclideanSpace Real (Fin (1 + n))) := {v | first v = 1 ∧ tail v ∈ C}
let K : Set (EuclideanSpace Real (Fin (1 + n))) :=
(ConvexCone.hull Real S : Set (EuclideanSpace Real (Fin (1 + n))))
euclideanRelativeInterior (1 + n) K =
{v | 0 < first v ∧ tail v ∈ (first v) • euclideanRelativeInterior n C} := by
classical
let coords : EuclideanSpace Real (Fin (1 + n)) → (Fin (1 + n) → Real) :=
EuclideanSpace.equiv (𝕜 := Real) (ι := Fin (1 + n))
let first : EuclideanSpace Real (Fin (1 + n)) → Real := fun v => coords v 0
let tail : EuclideanSpace Real (Fin (1 + n)) → EuclideanSpace Real (Fin n) :=
fun v =>
(EuclideanSpace.equiv (𝕜 := Real) (ι := Fin n)).symm
(fun i => coords v (Fin.natAdd 1 i))
let S : Set (EuclideanSpace Real (Fin (1 + n))) := {v | first v = 1 ∧ tail v ∈ C}
let K : Set (EuclideanSpace Real (Fin (1 + n))) :=
(ConvexCone.hull Real S : Set (EuclideanSpace Real (Fin (1 + n))))
let first1 : EuclideanSpace Real (Fin 1) → Real :=
fun y => (EuclideanSpace.equiv (𝕜 := Real) (ι := Fin 1) y) 0
let append :
EuclideanSpace Real (Fin 1) → EuclideanSpace Real (Fin n) →
EuclideanSpace Real (Fin (1 + n)) :=
fun y z =>
(EuclideanSpace.equiv (𝕜 := Real) (ι := Fin (1 + n))).symm
((Fin.appendIsometry 1 n)
((EuclideanSpace.equiv (𝕜 := Real) (ι := Fin 1)) y,
(EuclideanSpace.equiv (𝕜 := Real) (ι := Fin n)) z))
let Cy : EuclideanSpace Real (Fin 1) → Set (EuclideanSpace Real (Fin n)) :=
fun y => {z | append y z ∈ K}
let D : Set (EuclideanSpace Real (Fin 1)) := {y | (Cy y).Nonempty}
have hmain :
euclideanRelativeInterior (1 + n) K =
{v | 0 < first v ∧ tail v ∈ (first v) • euclideanRelativeInterior n C} := by
have hKconv : Convex Real K := by
simpa [K] using (ConvexCone.convex (C := ConvexCone.hull Real S))
have hmem :
∀ v, v ∈ K ↔ 0 < first v ∧ tail v ∈ (first v) • C := by
simpa [coords, first, tail, S, K] using
(mem_K_iff_first_tail (n := n) (C := C) hC)
have happend_first_tail :
∀ y z, first (append y z) = first1 y ∧ tail (append y z) = z := by
intro y z
simpa [coords, first, tail, append, first1] using
(first_tail_append (n := n) (y := y) (z := z))
have hCy :
∀ y, Cy y = {z | 0 < first1 y ∧ z ∈ first1 y • C} := by
intro y
ext z
constructor
· intro hz
have hz' :
0 < first (append y z) ∧ tail (append y z) ∈ (first (append y z)) • C :=
(hmem (append y z)).1 hz
rcases happend_first_tail y z with ⟨hfirst, htail⟩
refine ⟨?_, ?_⟩
· simpa [hfirst] using hz'.1
· simpa [hfirst, htail] using hz'.2
· intro hz
rcases happend_first_tail y z with ⟨hfirst, htail⟩
have hz' :
0 < first (append y z) ∧ tail (append y z) ∈ (first (append y z)) • C := by
refine ⟨?_, ?_⟩
· simpa [hfirst] using hz.1
· simpa [hfirst, htail] using hz.2
exact (hmem (append y z)).2 hz'
have hD : D = {y | 0 < first1 y} := by
ext y; constructor
· intro hy
rcases hy with ⟨z, hz⟩
have hz' : z ∈ {z | 0 < first1 y ∧ z ∈ first1 y • C} := by
simpa [hCy y] using hz
exact hz'.1
· intro hy
rcases hCne with ⟨x, hxC⟩
have hz : first1 y • x ∈ {z | 0 < first1 y ∧ z ∈ first1 y • C} := by
refine ⟨hy, ?_⟩
exact ⟨x, hxC, rfl⟩
have hz' : first1 y • x ∈ Cy y := by
simpa [hCy y] using hz
exact ⟨first1 y • x, hz'⟩
have hD_open : IsOpen D := by
have hcont : Continuous first1 := by
simpa [first1] using
(continuous_apply 0).comp
(EuclideanSpace.equiv (𝕜 := Real) (ι := Fin 1)).continuous
simpa [hD, Set.preimage, Set.mem_setOf_eq] using (isOpen_Ioi.preimage hcont)
have hD_nonempty : D.Nonempty := by
let y0 : EuclideanSpace Real (Fin 1) :=
(EuclideanSpace.equiv (𝕜 := Real) (ι := Fin 1)).symm (fun _ => 1)
refine ⟨y0, ?_⟩
have : 0 < first1 y0 := by
simp [first1, y0]
simpa [hD] using this
have hD_span : (affineSpan Real D : Set (EuclideanSpace Real (Fin 1))) = Set.univ := by
have hspan := IsOpen.affineSpan_eq_top hD_open hD_nonempty
ext x
simp [hspan]
have hriD : euclideanRelativeInterior 1 D = D := by
calc
euclideanRelativeInterior 1 D = interior D :=
euclideanRelativeInterior_eq_interior_of_affineSpan_eq_univ 1 D hD_span
_ = D := hD_open.interior_eq
have hriCy :
∀ y, 0 < first1 y →
euclideanRelativeInterior n (Cy y) = first1 y • euclideanRelativeInterior n C := by
intro y hy
have hCy_eq : Cy y = first1 y • C := by
ext z
simp [hCy y, hy]
simpa [hCy_eq] using (euclideanRelativeInterior_smul n C hC (first1 y))
have hsection :
∀ y z,
append y z ∈ euclideanRelativeInterior (1 + n) K ↔
y ∈ euclideanRelativeInterior 1 D ∧ z ∈ euclideanRelativeInterior n (Cy y) := by
intro y z
simpa [append, Cy, D] using
(euclideanRelativeInterior_mem_iff_relativeInterior_section (m := 1) (p := n) (C := K)
hKconv y z)
ext v; constructor
· intro hv
let yz := (appendAffineEquiv 1 n).symm v
let y := yz.1
let z := yz.2
have hv_append : append y z = v := by
have h1 : append y z = appendAffineEquiv 1 n (y, z) := by
simp [append, appendAffineEquiv_apply]
have h2 : appendAffineEquiv 1 n (y, z) = v := by
simp [y, z, yz]
exact h1.trans h2
have hfirst_tail : first v = first1 y ∧ tail v = z := by
simpa [hv_append] using (happend_first_tail y z)
have hv' : append y z ∈ euclideanRelativeInterior (1 + n) K := by
simpa [hv_append] using hv
rcases (hsection y z).1 hv' with ⟨hyD, hzCy⟩
have hyD' : y ∈ D := by
simpa [hriD] using hyD
have hypos : 0 < first1 y := by
have : y ∈ {y | 0 < first1 y} := by
simpa [hD] using hyD'
simpa using this
have hzCy' : z ∈ first1 y • euclideanRelativeInterior n C := by
have hri := hriCy y hypos
simpa [hri] using hzCy
have hpos : 0 < first v := by
simpa [hfirst_tail.1] using hypos
have htail : tail v ∈ first v • euclideanRelativeInterior n C := by
simpa [hfirst_tail.1, hfirst_tail.2] using hzCy'
exact ⟨hpos, htail⟩
· rintro ⟨hpos, htail⟩
let yz := (appendAffineEquiv 1 n).symm v
let y := yz.1
let z := yz.2
have hv_append : append y z = v := by
have h1 : append y z = appendAffineEquiv 1 n (y, z) := by
simp [append, appendAffineEquiv_apply]
have h2 : appendAffineEquiv 1 n (y, z) = v := by
simp [y, z, yz]
exact h1.trans h2
have hfirst_tail : first v = first1 y ∧ tail v = z := by
simpa [hv_append] using (happend_first_tail y z)
have hypos : 0 < first1 y := by
simpa [hfirst_tail.1] using hpos
have hyD : y ∈ euclideanRelativeInterior 1 D := by
have : y ∈ D := by
have : y ∈ {y | 0 < first1 y} := by
simpa using hypos
simpa [hD] using this
simpa [hriD] using this
have hzCy : z ∈ euclideanRelativeInterior n (Cy y) := by
have hz' : z ∈ first1 y • euclideanRelativeInterior n C := by
simpa [hfirst_tail.1, hfirst_tail.2] using htail
have hri := hriCy y hypos
simpa [hri] using hz'
have hv' : append y z ∈ euclideanRelativeInterior (1 + n) K := by
exact (hsection y z).2 ⟨hyD, hzCy⟩
simpa [hv_append] using hv'
simpa [coords, first, tail, S, K] using hmainend Section06end Chap02