mathlib3 documentation

analysis.convex.intrinsic

Intrinsic frontier and interior #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the intrinsic frontier, interior and closure of a set in a normed additive torsor. These are also known as relative frontier, interior, closure.

The intrinsic frontier/interior/closure of a set s is the frontier/interior/closure of s considered as a set in its affine span.

The intrinsic interior is in general greater than the topological interior, the intrinsic frontier in general less than the topological frontier, and the intrinsic closure in cases of interest the same as the topological closure.

Definitions #

intrinsic_interior: Intrinsic interior
intrinsic_frontier: Intrinsic frontier
intrinsic_closure: Intrinsic closure

Results #

The main results are:

affine_isometry.image_intrinsic_interior/affine_isometry.image_intrinsic_frontier/ affine_isometry.image_intrinsic_closure: Intrinsic interiors/frontiers/closures commute with taking the image under an affine isometry.
set.nonempty.intrinsic_interior: The intrinsic interior of a nonempty convex set is nonempty.

References #

Chapter 8 of Barry Simon, Convexity
Chapter 1 of [Rolf Schneider, Convex Bodies: The Brunn-Minkowski theory][schneider2013].

TODO #

is_closed s → is_extreme 𝕜 s (intrinsic_frontier 𝕜 s)
x ∈ s → y ∈ intrinsic_interior 𝕜 s → open_segment 𝕜 x y ⊆ intrinsic_interior 𝕜 s

def intrinsic_interior (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (s : set P) :

The intrinsic interior of a set is its interior considered as a set in its affine span.

Equations

intrinsic_interior 𝕜 s = coe '' interior (coe ⁻¹' s)

def intrinsic_frontier (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (s : set P) :

The intrinsic frontier of a set is its frontier considered as a set in its affine span.

Equations

intrinsic_frontier 𝕜 s = coe '' frontier (coe ⁻¹' s)

def intrinsic_closure (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (s : set P) :

The intrinsic closure of a set is its closure considered as a set in its affine span.

Equations

intrinsic_closure 𝕜 s = coe '' closure (coe ⁻¹' s)

@[simp]

theorem mem_intrinsic_interior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} {x : P} :

x ∈ intrinsic_interior 𝕜 s ↔ ∃ (y : ↥(affine_span 𝕜 s)), y ∈ interior (coe ⁻¹' s) ∧ ↑y = x

@[simp]

theorem mem_intrinsic_frontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} {x : P} :

x ∈ intrinsic_frontier 𝕜 s ↔ ∃ (y : ↥(affine_span 𝕜 s)), y ∈ frontier (coe ⁻¹' s) ∧ ↑y = x

@[simp]

theorem mem_intrinsic_closure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} {x : P} :

x ∈ intrinsic_closure 𝕜 s ↔ ∃ (y : ↥(affine_span 𝕜 s)), y ∈ closure (coe ⁻¹' s) ∧ ↑y = x

theorem intrinsic_interior_subset {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} :

intrinsic_interior 𝕜 s ⊆ s

theorem intrinsic_frontier_subset {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} (hs : is_closed s) :

intrinsic_frontier 𝕜 s ⊆ s

theorem intrinsic_frontier_subset_intrinsic_closure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} :

intrinsic_frontier 𝕜 s ⊆ intrinsic_closure 𝕜 s

theorem subset_intrinsic_closure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} :

s ⊆ intrinsic_closure 𝕜 s

@[simp]

theorem intrinsic_interior_empty {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] :

intrinsic_interior 𝕜 ∅ = ∅

@[simp]

theorem intrinsic_frontier_empty {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] :

intrinsic_frontier 𝕜 ∅ = ∅

@[simp]

theorem intrinsic_closure_empty {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] :

intrinsic_closure 𝕜 ∅ = ∅

@[simp]

theorem intrinsic_closure_nonempty {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} :

(intrinsic_closure 𝕜 s).nonempty ↔ s.nonempty

@[protected]

theorem set.nonempty.intrinsic_closure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} :

s.nonempty → (intrinsic_closure 𝕜 s).nonempty

Alias of the reverse direction of intrinsic_closure_nonempty.

theorem set.nonempty.of_intrinsic_closure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} :

(intrinsic_closure 𝕜 s).nonempty → s.nonempty

Alias of the forward direction of intrinsic_closure_nonempty.

@[simp]

theorem intrinsic_interior_singleton {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (x : P) :

intrinsic_interior 𝕜 {x} = {x}

@[simp]

theorem intrinsic_frontier_singleton {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (x : P) :

intrinsic_frontier 𝕜 {x} = ∅

@[simp]

theorem intrinsic_closure_singleton {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (x : P) :

intrinsic_closure 𝕜 {x} = {x}

Note that neither intrinsic_interior nor intrinsic_frontier is monotone.

theorem intrinsic_closure_mono {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s t : set P} (h : s ⊆ t) :

intrinsic_closure 𝕜 s ⊆ intrinsic_closure 𝕜 t

theorem interior_subset_intrinsic_interior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} :

interior s ⊆ intrinsic_interior 𝕜 s

theorem intrinsic_closure_subset_closure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} :

intrinsic_closure 𝕜 s ⊆ closure s

theorem intrinsic_frontier_subset_frontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} :

intrinsic_frontier 𝕜 s ⊆ frontier s

theorem intrinsic_closure_subset_affine_span {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} :

intrinsic_closure 𝕜 s ⊆ ↑(affine_span 𝕜 s)

@[simp]

theorem intrinsic_closure_diff_intrinsic_frontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (s : set P) :

intrinsic_closure 𝕜 s \ intrinsic_frontier 𝕜 s = intrinsic_interior 𝕜 s

@[simp]

theorem intrinsic_closure_diff_intrinsic_interior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (s : set P) :

intrinsic_closure 𝕜 s \ intrinsic_interior 𝕜 s = intrinsic_frontier 𝕜 s

@[simp]

theorem intrinsic_interior_union_intrinsic_frontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (s : set P) :

intrinsic_interior 𝕜 s ∪ intrinsic_frontier 𝕜 s = intrinsic_closure 𝕜 s

@[simp]

theorem intrinsic_frontier_union_intrinsic_interior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (s : set P) :

intrinsic_frontier 𝕜 s ∪ intrinsic_interior 𝕜 s = intrinsic_closure 𝕜 s

theorem is_closed_intrinsic_closure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} (hs : is_closed ↑(affine_span 𝕜 s)) :

is_closed (intrinsic_closure 𝕜 s)

theorem is_closed_intrinsic_frontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} (hs : is_closed ↑(affine_span 𝕜 s)) :

is_closed (intrinsic_frontier 𝕜 s)

@[simp]

theorem affine_span_intrinsic_closure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (s : set P) :

affine_span 𝕜 (intrinsic_closure 𝕜 s) = affine_span 𝕜 s

@[protected]

theorem is_closed.intrinsic_closure {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] {s : set P} (hs : is_closed (coe ⁻¹' s)) :

intrinsic_closure 𝕜 s = s

@[simp]

theorem intrinsic_closure_idem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [ring 𝕜] [add_comm_group V] [module 𝕜 V] [topological_space P] [add_torsor V P] (s : set P) :

intrinsic_closure 𝕜 (intrinsic_closure 𝕜 s) = intrinsic_closure 𝕜 s

@[simp]

theorem affine_isometry.image_intrinsic_interior {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [normed_field 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group W] [normed_space 𝕜 V] [normed_space 𝕜 W] [metric_space P] [pseudo_metric_space Q] [normed_add_torsor V P] [normed_add_torsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : set P) :

intrinsic_interior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsic_interior 𝕜 s

@[simp]

theorem affine_isometry.image_intrinsic_frontier {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [normed_field 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group W] [normed_space 𝕜 V] [normed_space 𝕜 W] [metric_space P] [pseudo_metric_space Q] [normed_add_torsor V P] [normed_add_torsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : set P) :

intrinsic_frontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsic_frontier 𝕜 s

@[simp]

theorem affine_isometry.image_intrinsic_closure {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [normed_field 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group W] [normed_space 𝕜 V] [normed_space 𝕜 W] [metric_space P] [pseudo_metric_space Q] [normed_add_torsor V P] [normed_add_torsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : set P) :

intrinsic_closure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsic_closure 𝕜 s

@[simp]

theorem intrinsic_closure_eq_closure (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [nontrivially_normed_field 𝕜] [complete_space 𝕜] [normed_add_comm_group V] [normed_space 𝕜 V] [finite_dimensional 𝕜 V] [metric_space P] [normed_add_torsor V P] (s : set P) :

intrinsic_closure 𝕜 s = closure s

@[simp]

theorem closure_diff_intrinsic_interior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [nontrivially_normed_field 𝕜] [complete_space 𝕜] [normed_add_comm_group V] [normed_space 𝕜 V] [finite_dimensional 𝕜 V] [metric_space P] [normed_add_torsor V P] (s : set P) :

closure s \ intrinsic_interior 𝕜 s = intrinsic_frontier 𝕜 s

@[simp]

theorem closure_diff_intrinsic_frontier {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [nontrivially_normed_field 𝕜] [complete_space 𝕜] [normed_add_comm_group V] [normed_space 𝕜 V] [finite_dimensional 𝕜 V] [metric_space P] [normed_add_torsor V P] (s : set P) :

closure s \ intrinsic_frontier 𝕜 s = intrinsic_interior 𝕜 s

@[protected]

theorem set.nonempty.intrinsic_interior {V : Type u_2} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V] {s : set V} (hscv : convex ℝ s) (hsne : s.nonempty) :

(intrinsic_interior ℝ s).nonempty

The intrinsic interior of a nonempty convex set is nonempty.

theorem intrinsic_interior_nonempty {V : Type u_2} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V] {s : set V} (hs : convex ℝ s) :

(intrinsic_interior ℝ s).nonempty ↔ s.nonempty