Documentation

Mathlib.Analysis.Convex.AmpleSet

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 #

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 #

source
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
Instances For
    source
    @[simp]
    theorem ampleSet_univ {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] :
    AmpleSet Set.univ

    A whole vector space is ample.

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

    The empty set in a vector space is ample.

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

    The union of two ample sets is ample.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    Subspaces of codimension at least two have ample complement #

    source
    theorem AmpleSet.of_one_lt_codim {F : Type u_1} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul ℝ F] {E : Submodule ℝ F} (hcodim : 1 < Module.rank ℝ (F ⧸ E)) :
    AmpleSet (↑E)ᶜ

    Let E be a linear subspace in a real vector space. If E has codimension at least two, its complement is ample.