theorem domf_subset_domcl_of_closure_le {n : ℕ} (f : (Fin n → ℝ) → EReal) : (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f ⊆ (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (convexFunctionClosure f)

The effective domain of f is contained in the effective domain of its closure.

theorem domcl_subset_closure_domf {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (convexFunctionClosure f) ⊆ closure ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f)

The effective domain of the closure lies in the closure of the effective domain.

theorem domcl_subset_domf_union_rbd {n : ℕ} {domf domcl : Set (EuclideanSpace ℝ (Fin n))} (hsubset : domcl ⊆ closure domf) : domcl ⊆ domf ∪ euclideanRelativeBoundary n domf

If domcl lies in closure domf, then it lies in domf or its relative boundary.

theorem closure_domcl_eq_domf {n : ℕ} {domf domcl : Set (EuclideanSpace ℝ (Fin n))} (hdomf : domf ⊆ domcl) (hdomcl : domcl ⊆ closure domf) : closure domcl = closure domf

Equal closures for domf and domcl follow from the two inclusions.

theorem ri_domcl_eq_domf {n : ℕ} {domf domcl : Set (EuclideanSpace ℝ (Fin n))} (hconvf : Convex ℝ domf) (hconvcl : Convex ℝ domcl) (hcl : closure domcl = closure domf) : euclideanRelativeInterior n domcl = euclideanRelativeInterior n domf

Relative interiors coincide under closure equality for convex sets.

theorem convexFunctionClosure_effectiveDomain_subset_relativeBoundary_and_same_closure_ri_dim {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : have domf := (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f; have domcl := (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (convexFunctionClosure f); domf ⊆ domcl ∧ domcl ⊆ domf ∪ euclideanRelativeBoundary n domf ∧ closure domcl = closure domf ∧ euclideanRelativeInterior n domcl = euclideanRelativeInterior n domf ∧ Module.finrank ℝ ↥(affineSpan ℝ domcl).direction = Module.finrank ℝ ↥(affineSpan ℝ domf).direction

Corollary 7.4.1. If f is a proper convex function, then dom (cl f) differs from dom f at most by including some additional relative boundary points of dom f. In particular, dom (cl f) and dom f have the same closure and relative interior, as well as the same dimension.

theorem ri_eq_and_boundary_empty_of_isAffineSet {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hC : IsAffineSet n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) '' C)) : euclideanRelativeInterior n C = C ∧ euclideanRelativeBoundary n C = ∅

Affine sets have full relative interior and empty relative boundary.

theorem domcl_eq_domf_of_affine_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) (haff : IsAffineSet n (effectiveDomain Set.univ f)) : have domf := (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f; have domcl := (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (convexFunctionClosure f); domcl = domf

For affine effective domain, the effective domain of the closure coincides.

theorem convexFunctionClosure_eq_of_affine_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) (haff : IsAffineSet n (effectiveDomain Set.univ f)) : convexFunctionClosure f = f

For affine effective domain, the closure agrees with the function everywhere.

theorem properConvexFunction_closed_of_affine_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) (haff : IsAffineSet n (effectiveDomain Set.univ f)) : ClosedConvexFunction f

Corollary 7.4.2. If f is a proper convex function such that dom f is an affine set (which holds in particular if f is finite throughout ℝ^n), then f is closed.

theorem lowerSemicontinuousAt_of_le_of_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f g : α → β} {x : α} (hg : LowerSemicontinuousAt g x) (hle : g ≤ f) (hxeq : g x = f x) : LowerSemicontinuousAt f x

A lower semicontinuous minorant that agrees at a point transfers lsc.

theorem convexFunction_lowerSemicontinuousAt_on_ri_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) (x : EuclideanSpace ℝ (Fin n)) : x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f) → LowerSemicontinuousAt f x.ofLp

theorem properConvexFunctionOn_ne_top_on_ri_effectiveDomain {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) → f x.ofLp ≠ ⊥ ∧ f x.ofLp ≠ ⊤

Proper convex functions are finite on the relative interior of their effective domain.

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

The toReal of a proper convex function is convex on its effective domain.

theorem continuousOn_ereal_of_toReal {α : Type u_1} [TopologicalSpace α] {f : α → EReal} {s : Set α} (hcont : ContinuousOn (fun (x : α) => (f x).toReal) s) (hfinite : ∀ x ∈ s, f x ≠ ⊥ ∧ f x ≠ ⊤) : ContinuousOn f s

Lift continuity of toReal ∘ f to continuity of f on finite-valued sets.

theorem convexOn_continuousOn_ri_of_affineSpan_eq_univ {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {g : EuclideanSpace ℝ (Fin n) → ℝ} (hg : ConvexOn ℝ C g) (hspan : ↑(affineSpan ℝ C) = Set.univ) : ContinuousOn g (euclideanRelativeInterior n C)

In full dimension, relative interior equals interior, giving continuity for convex maps.

theorem continuousOn_ri_of_affineEquiv {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {g : EuclideanSpace ℝ (Fin n) → ℝ} (e : EuclideanSpace ℝ (Fin n) ≃ᵃ[ℝ] EuclideanSpace ℝ (Fin n)) (hcont : ContinuousOn (fun (x : EuclideanSpace ℝ (Fin n)) => g (e.symm x)) (euclideanRelativeInterior n (⇑e '' C))) : ContinuousOn g (euclideanRelativeInterior n C)

Affine equivalences transport continuity on relative interiors.

def coordinateSubmodule (n m : ℕ) : Submodule ℝ (EuclideanSpace ℝ (Fin n))

The coordinate subspace as a submodule.

Equations

• coordinateSubmodule n m = { carrier := coordinateSubspace n m, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def coordinateSubspace_affineEquiv {n m : ℕ} (hmn : m ≤ n) : EuclideanSpace ℝ (Fin m) ≃ᵃ[ℝ] ↥(coordinateSubmodule n m)

Coordinate-subspace affine equivalence using extend-by-zero and restriction.

Equations

• One or more equations did not get rendered due to their size.

theorem affineSpan_preimage_eq_univ {n m : ℕ} (hmn : m ≤ n) {C : Set (EuclideanSpace ℝ (Fin n))} (hspan : ↑(affineSpan ℝ C) = coordinateSubspace n m) : ↑(affineSpan ℝ (⇑(coordinateSubspace_affineEquiv hmn).symm '' (Subtype.val ⁻¹' C))) = Set.univ

Pulling back a full-dimensional set from the coordinate subspace gives full affine span.

theorem image_preimage_eq_of_rightInverse {α : Type u_1} {β : Type u_2} {A : α → β} {g : β → α} {s : Set β} (hright : ∀ y ∈ s, A (g y) = y) : A '' (A ⁻¹' s) = s

If A has a right inverse on s, then A '' (A ⁻¹' s) = s.

theorem affineMap_apply_eq_linear {n m : ℕ} (A : EuclideanSpace ℝ (Fin m) →ᵃ[ℝ] EuclideanSpace ℝ (Fin n)) (hA0 : A 0 = 0) (x : EuclideanSpace ℝ (Fin m)) : A x = A.linear x

For linear affine maps, the value equals the linear part.

theorem ri_image_linearMap_eq {n m : ℕ} {D : Set (EuclideanSpace ℝ (Fin m))} (hconvD : Convex ℝ D) (A : EuclideanSpace ℝ (Fin m) →ᵃ[ℝ] EuclideanSpace ℝ (Fin n)) (hA0 : A 0 = 0) : euclideanRelativeInterior n (⇑A '' D) = ⇑A '' euclideanRelativeInterior m D

The relative interior of a linear affine image is the image of the relative interior.

theorem A_image_eq_C' {n m : ℕ} {C' : Set (EuclideanSpace ℝ (Fin n))} (e : EuclideanSpace ℝ (Fin m) ≃ᵃ[ℝ] ↥(coordinateSubmodule n m)) (A : EuclideanSpace ℝ (Fin m) →ᵃ[ℝ] EuclideanSpace ℝ (Fin n)) (hA : A = (coordinateSubmodule n m).subtype.toAffineMap.comp ↑e) (hC' : C' ⊆ coordinateSubspace n m) : ⇑A '' (⇑A ⁻¹' C') = C'

The coordinate-subspace embedding is surjective onto subsets of the subspace.

theorem continuousOn_of_leftInverse_on_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {A : α → β} {g : β → α} {f : β → γ} {s : Set α} {t : Set β} (hcont : ContinuousOn (fun (x : α) => f (A x)) s) (hleft : Function.LeftInverse g A) (ht : t = A '' s) (hg : Continuous g) : ContinuousOn f t

Transfer continuity along a left inverse on an image.

theorem convexOn_continuousOn_ri_via_coordinateSubspace {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {g : EuclideanSpace ℝ (Fin n) → ℝ} (hg : ConvexOn ℝ C g) : ContinuousOn g (euclideanRelativeInterior n C)

Reduce continuity on relative interior via an affine coordinate subspace model.