Ample subsets of real vector spaces

In this file we study ample sets in real vector spaces. A set is ample if all its connected component have full convex hull. Ample sets are an important ingredient for defining ample differential relations.

Main results

• ampleSet_empty and ampleSet_univ: the empty set and univ are ample
• AmpleSet.union: the union of two ample sets is ample
• AmpleSet.{pre}image: being ample is invariant under continuous affine equivalences; AmpleSet.{pre}image_iff are "iff" versions of these
• AmpleSet.vadd: in particular, ample-ness is invariant under affine translations

TODO

AmpleSet.of_one_lt_codim: a linear subspace of codimension at least two has an ample complement. This is the crucial geometric ingredient which allows to apply convex integration to the theory of immersions in positive codimension.

Implementation notes

A priori, the definition of ample subset asks for a vector space structure and a topology on the ambient type without any link between those structures. In practice, we care most about using these for finite dimensional vector spaces with their natural topology.

All vector spaces in the file are real vector spaces. While the definition generalises to other connected fields, that is not useful in practice.

Tags

ample set

Definition and invariance

def AmpleSet {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (s : Set F) : Prop

A subset of a topological real vector space is ample if the convex hull of each of its connected components is the full space.

Equations

• AmpleSet s = ∀ x ∈ s, (convexHull ℝ) (connectedComponentIn s x) = Set.univ

@[simp]

theorem ampleSet_univ {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] : AmpleSet Set.univ

A whole vector space is ample.

@[simp]

theorem ampleSet_empty {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] : AmpleSet ∅

The empty set in a vector space is ample.

theorem AmpleSet.union {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {s : Set F} {t : Set F} (hs : AmpleSet s) (ht : AmpleSet t) : AmpleSet (s ∪ t)

The union of two ample sets is ample.

theorem AmpleSet.image {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {s : Set E} (h : AmpleSet s) (L : E ≃ᵃL[ℝ] F) : AmpleSet (⇑L '' s)

Images of ample sets under continuous affine equivalences are ample.

theorem AmpleSet.image_iff {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {s : Set E} (L : E ≃ᵃL[ℝ] F) : AmpleSet (⇑L '' s) ↔ AmpleSet s

A set is ample iff its image under a continuous affine equivalence is.

theorem AmpleSet.preimage {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {s : Set F} (h : AmpleSet s) (L : E ≃ᵃL[ℝ] F) : AmpleSet (⇑L ⁻¹' s)

Pre-images of ample sets under continuous affine equivalences are ample.

theorem AmpleSet.preimage_iff {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {s : Set F} (L : E ≃ᵃL[ℝ] F) : AmpleSet (⇑L ⁻¹' s) ↔ AmpleSet s

A set is ample iff its pre-image under a continuous affine equivalence is.

theorem AmpleSet.vadd {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] {s : Set E} (h : AmpleSet s) {y : E} : AmpleSet (y +ᵥ s)

Affine translations of ample sets are ample.

theorem AmpleSet.vadd_iff {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] {s : Set E} {y : E} : AmpleSet (y +ᵥ s) ↔ AmpleSet s

A set is ample iff its affine translation is.