Intrinsic interior points of compact and convex sets

Follow the ray from a point p of a compact set C through another point x of C. The last point of C on this ray lies in the intrinsic frontier of C (IsCompact.exists_lineMap_mem_intrinsicFrontier): beyond it the ray leaves C, so it cannot be an intrinsic interior point. No convexity is needed.

A nonempty convex subset of t whose intrinsic interior misses that of t, such as a convex piece of the intrinsic frontier of t, has strictly smaller dimension (TauCeti.finrank_vectorSpan_lt_of_disjoint_intrinsicInterior): equal dimensions would force equal affine spans, and the intrinsic interior is monotone on sets with a common affine span (TauCeti.intrinsicInterior_mono_of_affineSpan_eq). Consequently, in a family of convex cells with pairwise disjoint intrinsic interiors whose intrinsic frontiers are covered by a set S and the smaller cells, every point of a cell lies in S or in the intrinsic interior of a cell contained in it (TauCeti.mem_intrinsicInterior_or_of_mem), and the intrinsic interior of a cell avoiding S meets no other cell of smaller or equal dimension (TauCeti.eq_or_finrank_lt_of_mem_intrinsicInterior).

If s has the same affine span as t and contains the part of t in an open set U, then the intrinsic interior points of t in U are intrinsic interior points of s (TauCeti.intrinsicInterior_inter_subset_of_affineSpan_eq). From an intrinsic interior point, every small move along the affine span stays in the set (TauCeti.eventually_add_smul_mem_of_mem_intrinsicInterior). Consequently an affine function which is nonnegative on a set and vanishes at one of its intrinsic interior points vanishes on the whole set (TauCeti.eq_zero_of_nonneg_of_mem_intrinsicInterior). In particular, an inequality a ≤ b between affine functions on s, which persists on the convex hull of s (TauCeti.le_of_forall_le_of_mem_convexHull), is strict on the intrinsic interior of that hull unless a = b on all of it (TauCeti.eq_of_le_of_mem_intrinsicInterior). The intrinsic frontier of a closed set consists of its points outside its intrinsic interior (IsClosed.sdiff_intrinsicInterior). These are the tools for computing intrinsic interiors and frontiers of concrete cells, such as the bands of TauCeti/Analysis/Convex/RegionBetween.lean, and the cells of a hyperplane arrangement.

Read in the ambient space, x is an intrinsic interior point of s when it lies in the affine span of s and the points of that span near x lie in s (TauCeti.mem_intrinsicInterior_iff_eventually). A subset u of a convex set s which meets the intrinsic interior of s has its intrinsic interior inside that of s (TauCeti.intrinsicInterior_mono_of_inter_intrinsicInterior_nonempty). Consequently, if the intrinsic interiors of two convex sets meet, the intrinsic interior of their intersection is the intersection of their intrinsic interiors (TauCeti.intrinsicInterior_inter; Rockafellar, Convex Analysis, Theorem 6.5). This computes the intrinsic interiors of the cells σ ∩ τ cut out by two triangulations.

A closed bounded convex set C of a real normed space, with a point c of its intrinsic interior, is homeomorphic to the closed unit ball of the direction V of its affine span (TauCeti.convexClosedBallHomeomorph). Translating by -c turns C into a closed bounded convex neighbourhood S of 0 in V, and Mathlib's gaugeRescaleHomeomorph rescales each ray of V through the origin to carry the closed unit ball onto S. Explicitly, the homeomorphism sends v to c + (‖v‖ / gauge (-c +ᵥ C) v) • v (TauCeti.coe_convexClosedBallHomeomorph_apply); for a unit vector u of V the number (gauge (-c +ᵥ C) u)⁻¹ is the length of the segment from c in direction u inside C. No finite-dimensionality is needed. This identifies every nonempty compact convex set of a finite-dimensional space with a disk, which is how Brouwer's fixed-point theorem passes from the disk to compact convex sets.

theorem IsCompact.exists_lineMap_mem_intrinsicFrontier {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] {C : Set E} {p x : E} (hC : IsCompact C) (hp : p ∈ C) (hx : x ∈ C) (hxp : x ≠ p) : ∃ (T : ℝ), 1 ≤ T ∧ (AffineMap.lineMap p x) T ∈ intrinsicFrontier ℝ C

On the ray from a point p of a compact set C through another point x of C, some point at parameter T ≥ 1 lies in the intrinsic frontier of C.

@[simp]

theorem TauCeti.intrinsicInterior_univ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] : intrinsicInterior 𝕜 Set.univ = Set.univ

The intrinsic interior of the whole space is the whole space.

theorem TauCeti.intrinsicInterior_mono_of_affineSpan_eq {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s t : Set P} (hst : s ⊆ t) (h : affineSpan 𝕜 s = affineSpan 𝕜 t) : intrinsicInterior 𝕜 s ⊆ intrinsicInterior 𝕜 t

The intrinsic interior is monotone on sets with a common affine span.

theorem TauCeti.intrinsicInterior_inter_subset_of_affineSpan_eq {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s t U : Set P} (hU : IsOpen U) (htU : t ∩ U ⊆ s) (h : affineSpan 𝕜 s = affineSpan 𝕜 t) : intrinsicInterior 𝕜 t ∩ U ⊆ intrinsicInterior 𝕜 s

If s has the same affine span as t and contains the part t ∩ U of t in an open set U, then the intrinsic interior points of t in U are intrinsic interior points of s.

theorem IsClosed.sdiff_intrinsicInterior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} (hs : IsClosed s) : s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s

The intrinsic frontier of a closed set consists of its points outside its intrinsic interior.

theorem TauCeti.mem_intrinsicInterior_iff_eventually {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} {x : P} : x ∈ intrinsicInterior 𝕜 s ↔ x ∈ affineSpan 𝕜 s ∧ ∀ᶠ (y : P) in nhds x, y ∈ affineSpan 𝕜 s → y ∈ s

Membership in the intrinsic interior, read in the ambient space: x is an intrinsic interior point of s when it lies in the affine span of s and every point of that span close to x lies in s.

theorem TauCeti.intrinsicInterior_inter_intrinsicInterior_subset {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s t : Set P} : intrinsicInterior 𝕜 s ∩ intrinsicInterior 𝕜 t ⊆ intrinsicInterior 𝕜 (s ∩ t)

A point in the intrinsic interiors of two sets is in the intrinsic interior of their intersection.

theorem TauCeti.intrinsicFrontier_subset_iUnion_of_exists_mem_intrinsicInterior {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {ι : Type u_4} {Q : ι → Set P} (i : ι) (hQc : IsClosed (Q i)) (h : ∀ x ∈ Q i, ∃ (j : ι), x ∈ intrinsicInterior 𝕜 (Q j) ∧ Q j ⊆ Q i) : intrinsicFrontier 𝕜 (Q i) ⊆ ⋃ (j : ι), ⋃ (_ : j ≠ i ∧ Q j ⊆ Q i), Q j

The intrinsic frontier of a closed cell is covered by the other cells contained in it, when every point of the cell lies in the intrinsic interior of a cell contained in it.

theorem TauCeti.inter_subset_intrinsicFrontier_of_disjoint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C S : Set E} (hint : Disjoint (intrinsicInterior ℝ C) S) : C ∩ S ⊆ intrinsicFrontier ℝ C

A point of C lying in a set S which the intrinsic interior of C avoids lies in the intrinsic frontier of C.

theorem TauCeti.finrank_vectorSpan_lt_of_disjoint_intrinsicInterior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s t : Set E} (hs : Convex ℝ s) (hsne : s.Nonempty) (hst : s ⊆ t) (hd : Disjoint (intrinsicInterior ℝ s) (intrinsicInterior ℝ t)) : Module.finrank ℝ ↥(vectorSpan ℝ s) < Module.finrank ℝ ↥(vectorSpan ℝ t)

A nonempty convex subset s of t whose intrinsic interior is disjoint from that of t (for instance a nonempty convex subset of the intrinsic frontier of t) has strictly smaller dimension than t.

theorem TauCeti.mem_intrinsicInterior_or_of_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} {P : ι → Set E} {S : Set E} (hPv : ∀ (i : ι), Convex ℝ (P i)) (hri : Pairwise fun (i j : ι) => Disjoint (intrinsicInterior ℝ (P i)) (intrinsicInterior ℝ (P j))) (hfr : ∀ (i : ι), intrinsicFrontier ℝ (P i) ⊆ S ∪ ⋃ (j : ι), ⋃ (_ : j ≠ i ∧ P j ⊆ P i), P j) {i : ι} {x : E} (hx : x ∈ P i) : x ∈ intrinsicInterior ℝ (P i) ∨ x ∈ S ∨ ∃ (k : ι), Module.finrank ℝ ↥(vectorSpan ℝ (P k)) < Module.finrank ℝ ↥(vectorSpan ℝ (P i)) ∧ P k ⊆ P i ∧ x ∈ intrinsicInterior ℝ (P k)

A point of a cell lies in its intrinsic interior, in S, or in the intrinsic interior of a smaller-dimensional cell contained in it, when the frontier of every cell is covered by S and the other cells contained in it.

theorem TauCeti.eq_or_finrank_lt_of_mem_intrinsicInterior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} {P : ι → Set E} {S : Set E} (hPv : ∀ (i : ι), Convex ℝ (P i)) (hri : Pairwise fun (i j : ι) => Disjoint (intrinsicInterior ℝ (P i)) (intrinsicInterior ℝ (P j))) (hfr : ∀ (i : ι), intrinsicFrontier ℝ (P i) ⊆ S ∪ ⋃ (j : ι), ⋃ (_ : j ≠ i ∧ P j ⊆ P i), P j) (hS : ∀ (i : ι), Disjoint (intrinsicInterior ℝ (P i)) S) {i j : ι} {x : E} (hxi : x ∈ intrinsicInterior ℝ (P i)) (hxj : x ∈ P j) : i = j ∨ Module.finrank ℝ ↥(vectorSpan ℝ (P i)) < Module.finrank ℝ ↥(vectorSpan ℝ (P j))

Under the hypotheses of TauCeti.mem_intrinsicInterior_or_of_mem, if the intrinsic interiors of the cells avoid S, the intrinsic interior of a cell meets no other cell of smaller or equal dimension.

theorem TauCeti.le_of_forall_le_of_mem_convexHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] {a b : E →ᵃ[ℝ] ℝ} {s : Set E} (h : ∀ x ∈ s, a x ≤ b x) {x : E} (hx : x ∈ (convexHull ℝ) s) : a x ≤ b x

An inequality between two affine functions on a set persists on its convex hull.

A closed bounded convex set as a ball around an intrinsic interior point

theorem TauCeti.setOf_add_mem_eq_preimage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (C : Set E) (c : E) : {v : ↥(affineSpan ℝ C).direction | c + ↑v ∈ C} = ⇑(affineSpan ℝ C).direction.subtype ⁻¹' (-c +ᵥ C)

The displacements from c inside C, read in the direction of the affine span of C, are the preimage of the translate -c +ᵥ C.

theorem TauCeti.gauge_setOf_add_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (v : ↥(affineSpan ℝ C).direction) : gauge {w : ↥(affineSpan ℝ C).direction | c + ↑w ∈ C} v = gauge (-c +ᵥ C) ↑v

The gauge of the displacement set agrees with the gauge of the translated set in the ambient space.

theorem TauCeti.convex_setOf_add_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hconv : Convex ℝ C) : Convex ℝ {v : ↥(affineSpan ℝ C).direction | c + ↑v ∈ C}

For convex C and any c, the displacements v in the direction of affineSpan ℝ C with c + v ∈ C form a convex set.

theorem TauCeti.isClosed_setOf_add_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hcl : IsClosed C) : IsClosed {v : ↥(affineSpan ℝ C).direction | c + ↑v ∈ C}

Displacements from a point into a closed set form a closed set in its affine direction.

theorem TauCeti.isVonNBounded_setOf_add_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hb : Bornology.IsBounded C) : Bornology.IsVonNBounded ℝ {v : ↥(affineSpan ℝ C).direction | c + ↑v ∈ C}

Displacements into a bounded set are von Neumann bounded in its affine direction.

theorem TauCeti.add_mem_intrinsicFrontier_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (v : ↥(affineSpan ℝ C).direction) : c + ↑v ∈ intrinsicFrontier ℝ C ↔ v ∈ frontier {w : ↥(affineSpan ℝ C).direction | c + ↑w ∈ C}

c + v lies in the intrinsic frontier of C iff v lies in the frontier, within the direction of the affine span of C, of the displacement set {w | c + w ∈ C}.

theorem TauCeti.setOf_add_mem_mem_nhds_of_mem_intrinsicInterior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hc : c ∈ intrinsicInterior ℝ C) : {v : ↥(affineSpan ℝ C).direction | c + ↑v ∈ C} ∈ nhds 0

For a point c of the intrinsic interior of C, the displacements v in the direction of the affine span of C with c + v ∈ C form a neighbourhood of 0.

theorem TauCeti.gauge_setOf_add_mem_pos_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hb : Bornology.IsBounded C) (hc : c ∈ intrinsicInterior ℝ C) (v : ↥(affineSpan ℝ C).direction) : 0 < gauge {w : ↥(affineSpan ℝ C).direction | c + ↑w ∈ C} v ↔ v ≠ 0

The gauge of the translated set in its affine direction is positive exactly away from zero, for a bounded set with an intrinsic interior center.

theorem TauCeti.eventually_add_smul_mem_of_mem_intrinsicInterior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hc : c ∈ intrinsicInterior ℝ C) {v : E} (hv : v ∈ (affineSpan ℝ C).direction) : ∀ᶠ (ε : ℝ) in nhds 0, c + ε • v ∈ C

From a point c of the intrinsic interior of C, every sufficiently small move ε • v along a direction v of the affine span of C stays in C.

theorem TauCeti.eq_zero_of_nonneg_of_mem_intrinsicInterior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} {g : E →ᵃ[ℝ] ℝ} (hg : ∀ y ∈ C, 0 ≤ g y) (hc : c ∈ intrinsicInterior ℝ C) (hgc : g c = 0) {y : E} (hy : y ∈ C) : g y = 0

An affine function which is nonnegative on a set C and vanishes at an intrinsic interior point c of C vanishes on all of C.

theorem TauCeti.eq_of_le_of_mem_intrinsicInterior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : E →ᵃ[ℝ] ℝ} {s : Set E} (h : ∀ x ∈ s, a x ≤ b x) {x y : E} (hx : x ∈ intrinsicInterior ℝ ((convexHull ℝ) s)) (hxe : a x = b x) (hy : y ∈ (convexHull ℝ) s) : a y = b y

If a ≤ b on s for two affine functions, with equality at an intrinsic interior point of the convex hull of s, then a = b on the whole convex hull.

theorem TauCeti.intrinsicInterior_mono_of_inter_intrinsicInterior_nonempty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s u : Set E} (hs : Convex ℝ s) (hus : u ⊆ s) (h : (u ∩ intrinsicInterior ℝ s).Nonempty) : intrinsicInterior ℝ u ⊆ intrinsicInterior ℝ s

A subset u of a convex set s meeting the intrinsic interior of s has its intrinsic interior inside that of s.

theorem TauCeti.intrinsicInterior_inter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s t : Set E} (hs : Convex ℝ s) (ht : Convex ℝ t) (h : (intrinsicInterior ℝ s ∩ intrinsicInterior ℝ t).Nonempty) : intrinsicInterior ℝ (s ∩ t) = intrinsicInterior ℝ s ∩ intrinsicInterior ℝ t

The intrinsic interior of an intersection (Rockafellar, Theorem 6.5). If the intrinsic interiors of two convex sets meet, the intrinsic interior of their intersection is the intersection of their intrinsic interiors.

noncomputable def TauCeti.convexClosedBallHomeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hconv : Convex ℝ C) (hcl : IsClosed C) (hb : Bornology.IsBounded C) (hc : c ∈ intrinsicInterior ℝ C) : ↑(Metric.closedBall 0 1) ≃ₜ ↑C

A closed bounded convex set is a ball around each intrinsic interior point. For a closed bounded convex set C of a real normed space and a point c of its intrinsic interior, the closed unit ball of the direction of the affine span of C is homeomorphic to C. The homeomorphism sends 0 to c and v to c + (‖v‖ / gauge (-c +ᵥ C) v) • v (TauCeti.coe_convexClosedBallHomeomorph_apply): it rescales the ray through v by Mathlib's gaugeRescaleHomeomorph, then translates by c.

theorem TauCeti.coe_convexClosedBallHomeomorph_apply_eq_gaugeRescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hconv : Convex ℝ C) (hcl : IsClosed C) (hb : Bornology.IsBounded C) (hc : c ∈ intrinsicInterior ℝ C) (v : ↑(Metric.closedBall 0 1)) : ↑((convexClosedBallHomeomorph hconv hcl hb hc) v) = c + ↑(gaugeRescale (Metric.closedBall 0 1) {w : ↥(affineSpan ℝ C).direction | c + ↑w ∈ C} ↑v)

The convex-ball homeomorphism is gauge rescaling followed by translation by c.

theorem TauCeti.coe_convexClosedBallHomeomorph_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hconv : Convex ℝ C) (hcl : IsClosed C) (hb : Bornology.IsBounded C) (hc : c ∈ intrinsicInterior ℝ C) (v : ↑(Metric.closedBall 0 1)) : ↑((convexClosedBallHomeomorph hconv hcl hb hc) v) = c + (‖↑↑v‖ / gauge (-c +ᵥ C) ↑↑v) • ↑↑v

TauCeti.convexClosedBallHomeomorph in explicit coordinates: v is sent to c + (‖v‖ / gauge (-c +ᵥ C) v) • v.

@[simp]

theorem TauCeti.coe_convexClosedBallHomeomorph_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hconv : Convex ℝ C) (hcl : IsClosed C) (hb : Bornology.IsBounded C) (hc : c ∈ intrinsicInterior ℝ C) : ↑((convexClosedBallHomeomorph hconv hcl hb hc) ⟨0, ⋯⟩) = c

TauCeti.convexClosedBallHomeomorph sends the centre of the ball to c.

theorem TauCeti.coe_convexClosedBallHomeomorph_symm_apply_eq_gaugeRescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hconv : Convex ℝ C) (hcl : IsClosed C) (hb : Bornology.IsBounded C) (hc : c ∈ intrinsicInterior ℝ C) (x : ↑C) : ↑↑((convexClosedBallHomeomorph hconv hcl hb hc).symm x) = ↑(gaugeRescale {w : ↥(affineSpan ℝ C).direction | c + ↑w ∈ C} (Metric.closedBall 0 1) ⟨↑x - c, ⋯⟩)

The inverse convex-ball homeomorphism translates by -c, then rescales by the gauge.

theorem TauCeti.coe_convexClosedBallHomeomorph_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hconv : Convex ℝ C) (hcl : IsClosed C) (hb : Bornology.IsBounded C) (hc : c ∈ intrinsicInterior ℝ C) (x : ↑C) : ↑↑((convexClosedBallHomeomorph hconv hcl hb hc).symm x) = (gauge (-c +ᵥ C) (↑x - c) / ‖↑x - c‖) • (↑x - c)

The inverse of TauCeti.convexClosedBallHomeomorph in explicit coordinates: x is sent to (gauge (-c +ᵥ C) (x - c) / ‖x - c‖) • (x - c).

theorem TauCeti.coe_convexClosedBallHomeomorph_mem_intrinsicFrontier_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {c : E} (hconv : Convex ℝ C) (hcl : IsClosed C) (hb : Bornology.IsBounded C) (hc : c ∈ intrinsicInterior ℝ C) (v : ↑(Metric.closedBall 0 1)) : ↑((convexClosedBallHomeomorph hconv hcl hb hc) v) ∈ intrinsicFrontier ℝ C ↔ ‖↑v‖ = 1

The unit sphere corresponds exactly to the intrinsic frontier under the convex-ball homeomorphism. No full-dimensionality assumption is needed. Use this as an explicit rewrite; the native simp normal form expands membership in the intrinsic frontier.