theorem
riEpigraph_D_eq_effectiveDomain
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
:
have C :=
⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) =>
((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f);
have Cy := fun (y : EuclideanSpace ℝ (Fin n)) => {z : EuclideanSpace ℝ (Fin 1) | (appendAffineEquiv n 1) (y, z) ∈ C};
have D := {y : EuclideanSpace ℝ (Fin n) | (Cy y).Nonempty};
D = (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f
The base of nonempty vertical sections equals the effective domain.
theorem
riEpigraph_section_ri_iff
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
(x : Fin n → ℝ)
(μ : ℝ)
(hfx : f x < ⊤)
:
have C :=
⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) =>
((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f);
have y := (EuclideanSpace.equiv (Fin n) ℝ).symm x;
have z := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => μ;
have Cy := fun (y : EuclideanSpace ℝ (Fin n)) => {z : EuclideanSpace ℝ (Fin 1) | (appendAffineEquiv n 1) (y, z) ∈ C};
z ∈ euclideanRelativeInterior 1 (Cy y) ↔ f x < ↑μ
Relative interior of a vertical section is the strict inequality when f x < ⊤.
theorem
riEpigraph_mem_iff
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
(hf : ConvexFunction f)
(x : Fin n → ℝ)
(μ : ℝ)
:
(appendAffineEquiv n 1)
((EuclideanSpace.equiv (Fin n) ℝ).symm x, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => μ) ∈ riEpigraph f ↔ (EuclideanSpace.equiv (Fin n) ℝ).symm x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f) ∧ f x < ↑μ ∧ ↑μ < ⊤
Lemma 7.3. For any convex function f, ri (epi f) consists of the pairs (x, μ)
such that x ∈ ri (dom f) and f x < μ < ∞.
The embedded epigraph used in riEpigraph is convex.
theorem
isOpen_openHalfspace_lastCoord
{n : ℕ}
{α : ℝ}
:
IsOpen {p : EuclideanSpace ℝ (Fin (n + 1)) | (EuclideanSpace.equiv (Fin 1) ℝ) ((appendAffineEquiv n 1).symm p).2 0 < α}
The open half-space defined by the last coordinate is open.
theorem
exists_point_openHalfspace_inter_embedded_epigraph
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
{α : ℝ}
(hα : ∃ (x : Fin n → ℝ), f x < ↑α)
:
have C :=
⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) =>
((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f);
have U :=
{p : EuclideanSpace ℝ (Fin (n + 1)) | (EuclideanSpace.equiv (Fin 1) ℝ) ((appendAffineEquiv n 1).symm p).2 0 < α};
(U ∩ C).Nonempty
Build a point of the embedded epigraph lying strictly below height α.
theorem
exists_lt_on_ri_effectiveDomain_of_convexFunction
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
(hf : ConvexFunction f)
{α : ℝ}
(hα : ∃ (x : Fin n → ℝ), f x < ↑α)
:
∃ x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f),
f x.ofLp < ↑α
Corollary 7.3.1: Let α be a real number, and let f be a convex function such that,
for some x, f x < α. Then there exists x ∈ ri (dom f) with f x < α.
theorem
exists_lt_on_ri_of_convexFunction_convexSet
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
(hf : ConvexFunction f)
{C : Set (EuclideanSpace ℝ (Fin n))}
(hC : Convex ℝ C)
(hri : euclideanRelativeInterior n C ⊆ (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f)
{α : ℝ}
(hα : ∃ x ∈ closure C, f x.ofLp < ↑α)
:
∃ x ∈ euclideanRelativeInterior n C, f x.ofLp < ↑α
Corollary 7.3.2. Let f be a convex function, and let C be a convex set such that
ri C ⊆ dom f. Let α ∈ ℝ be such that f x < α for some x ∈ cl C. Then f x < α
for some x ∈ ri C.
theorem
ri_subset_effectiveDomain_of_finite_on_C
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
{C : Set (EuclideanSpace ℝ (Fin n))}
(hfinite : ∀ x ∈ C, f x.ofLp ≠ ⊤ ∧ f x.ofLp ≠ ⊥)
:
euclideanRelativeInterior n C ⊆ (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f
If f is finite on C, then ri C lies in the effective domain of f.
theorem
convexFunction_ge_on_closure_of_convexSet
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
(hf : ConvexFunction f)
{C : Set (EuclideanSpace ℝ (Fin n))}
(hC : Convex ℝ C)
(hfinite : ∀ x ∈ C, f x.ofLp ≠ ⊤ ∧ f x.ofLp ≠ ⊥)
{α : ℝ}
(hα : ∀ x ∈ C, f x.ofLp ≥ ↑α)
(x : EuclideanSpace ℝ (Fin n))
:
Corollary 7.3.3. Let f be a convex function on ℝ^n, and let C be a convex set on
which f is finite. If f x ≥ α for every x ∈ C, then also f x ≥ α for every
x ∈ cl C.
theorem
exists_bot_on_ri_effectiveDomain_of_exists_bot
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
(hf : ConvexFunction f)
(hbot : ∃ (x : Fin n → ℝ), f x = ⊥)
:
∃ y ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f),
f y.ofLp = ⊥
If a convex function has a bottom value, then it attains ⊥ on ri (dom f).
theorem
riEpigraph_eq_of_agree_on_ri_effectiveDomain
{n : ℕ}
{f g : (Fin n → ℝ) → EReal}
(hf : ConvexFunction f)
(hg : ConvexFunction g)
(hri :
euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f) = euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ g))
(hagree :
∀ x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f),
f x.ofLp = g x.ofLp)
:
Agreement on ri (dom f) yields equality of ri (epi f).
theorem
closure_embedded_epigraph_eq_of_riEpigraph_eq
{n : ℕ}
{f g : (Fin n → ℝ) → EReal}
(hf : ConvexFunction f)
(hg : ConvexFunction g)
(hri_epi : riEpigraph f = riEpigraph g)
:
have C_f :=
⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) =>
((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f);
have C_g :=
⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) =>
((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ g);
closure C_f = closure C_g
Relative interior equality gives closure equality for embedded epigraphs.