theorem
closure_epigraph_eq_of_embedded_closure_eq
{n : ℕ}
{f g : (Fin n → ℝ) → EReal}
:
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 → closure (epigraph Set.univ f) = closure (epigraph Set.univ g)
Equality of embedded epigraph closures yields equality of epigraph closures.
theorem
convexFunctionClosure_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)
:
Corollary 7.3.4. If f and g are convex functions on ℝ^n such that
ri (dom f) = ri (dom g), and f and g agree on the latter set, then
cl f = cl g.
theorem
exists_riEpigraph_point_on_vertical_line
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
(hf : ProperConvexFunctionOn Set.univ f)
{x : EuclideanSpace ℝ (Fin n)}
(hx : x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f))
:
∃ (μ : ℝ),
(appendAffineEquiv n 1)
((EuclideanSpace.equiv (Fin n) ℝ).symm x.ofLp, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => μ) ∈ riEpigraph f
A point of ri (dom f) lifts to a point of ri (epi f) on the vertical line.
theorem
embedded_epigraph_section_mem_iff
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
(x : Fin n → ℝ)
:
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 Cy := fun (y : EuclideanSpace ℝ (Fin n)) => {z : EuclideanSpace ℝ (Fin 1) | (appendAffineEquiv n 1) (y, z) ∈ C};
have coords1 := EuclideanSpace.equiv (Fin 1) ℝ;
have first1 := fun (z : EuclideanSpace ℝ (Fin 1)) => coords1 z 0;
∀ (z : EuclideanSpace ℝ (Fin 1)), z ∈ Cy y ↔ f x ≤ ↑(first1 z)
The vertical section of the embedded epigraph is the inequality in the last coordinate.
theorem
convexFunctionClosure_eq_on_ri
{n : ℕ}
{f : (Fin n → ℝ) → EReal}
(hf : ProperConvexFunctionOn Set.univ f)
(x : EuclideanSpace ℝ (Fin n))
:
x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f) →
convexFunctionClosure f x.ofLp = f x.ofLp
On the relative interior of the effective domain, cl f agrees with f.