From b6781655df78715c7aafddf10af5597127fc7cfb Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 11 Mar 2024 22:25:07 +0100 Subject: [PATCH] Move basic properties of ample sets into ToMathlib; show unions of ample sets are ample. --- SphereEversion.lean | 1 + SphereEversion/Local/AmpleSet.lean | 57 +--------- .../ToMathlib/Analysis/Convex/AmpleSet.lean | 100 ++++++++++++++++++ 3 files changed, 104 insertions(+), 54 deletions(-) create mode 100644 SphereEversion/ToMathlib/Analysis/Convex/AmpleSet.lean diff --git a/SphereEversion.lean b/SphereEversion.lean index 0ff4d0f4..31e9a152 100644 --- a/SphereEversion.lean +++ b/SphereEversion.lean @@ -30,6 +30,7 @@ import SphereEversion.Notations import SphereEversion.ToMathlib.Analysis.Calculus import SphereEversion.ToMathlib.Analysis.Calculus.AffineMap import SphereEversion.ToMathlib.Analysis.ContDiff +import SphereEversion.ToMathlib.Analysis.Convex.AmpleSet import SphereEversion.ToMathlib.Analysis.Convex.Basic import SphereEversion.ToMathlib.Analysis.CutOff import SphereEversion.ToMathlib.Analysis.InnerProductSpace.CrossProduct diff --git a/SphereEversion/Local/AmpleSet.lean b/SphereEversion/Local/AmpleSet.lean index ccdf8056..5494a76f 100644 --- a/SphereEversion/Local/AmpleSet.lean +++ b/SphereEversion/Local/AmpleSet.lean @@ -1,5 +1,4 @@ -import Mathlib.Analysis.Convex.Normed -import SphereEversion.ToMathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv +import SphereEversion.ToMathlib.Analysis.Convex.AmpleSet /-! # Ample subsets of real vector spaces @@ -22,63 +21,13 @@ without any link between those structures, but we will only be using these for f vector spaces with their natural topology. -/ - -/-! ## Definition and invariance -/ - +/-! ## Subspaces of codimension at least 2 have ample complement -/ open Set AffineMap - open scoped Convex Matrix variable {E F : Type*} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] - -variable [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] - -/-- A subset of a topological real vector space is ample if the convex hull of each of its -connected components is the full space. -/ -def AmpleSet (s : Set F) : Prop := - ∀ x ∈ s, convexHull ℝ (connectedComponentIn s x) = univ - -/-- Images of ample sets under continuous affine equivalences are ample. -/ -theorem AmpleSet.image {s : Set E} (h : AmpleSet s) (L : E ≃ᵃL[ℝ] F) : - AmpleSet (L '' s) := by - intro x hx - rw [L.image_eq_preimage] at hx - have : L '' connectedComponentIn s (L.symm x) = connectedComponentIn (L '' s) x := by - conv_rhs => rw [← L.apply_symm_apply x] - exact (L.toHomeomorph).image_connectedComponentIn hx - rw [← this] - -- if/when #11298 lands, switch order of this lemma - refine (AffineMap.image_convexHull _ L.toAffineMap).symm.trans ?_ - rw [h (L.symm x) hx, image_univ] - exact L.surjective.range_eq - -/-- Preimages of ample sets under continuous affine equivalences are ample. -/ -theorem AmpleSet.preimage {s : Set F} (h : AmpleSet s) (L : E ≃ᵃL[ℝ] F) : AmpleSet (L ⁻¹' s) := by - rw [← L.image_symm_eq_preimage]; exact h.image L.symm - -open scoped Pointwise - -/-- Translating an ample set is ample. -/ -theorem AmpleSet.vadd [ContinuousAdd E] {s : Set E} (h : AmpleSet s) {y : E} : - AmpleSet (y +ᵥ s) := by - show AmpleSet ((ContinuousAffineEquiv.constVAdd ℝ E y) '' s) - exact AmpleSet.image h _ - -/-! ## Trivial examples -/ - -/-- A whole vector space is ample. -/ -theorem ampleSet_univ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] : - AmpleSet (univ : Set F) := by - intro x _ - rw [connectedComponentIn_univ, PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ] - --- unused -/-- The empty set in a vector space is ample. -/ -theorem ampleSet_empty : AmpleSet (∅ : Set F) := fun _ h ↦ False.elim h - - -/-! ## Subspaces of codimension at least 2 have ample complement -/ + [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] section Lemma213 diff --git a/SphereEversion/ToMathlib/Analysis/Convex/AmpleSet.lean b/SphereEversion/ToMathlib/Analysis/Convex/AmpleSet.lean new file mode 100644 index 00000000..5d32e75a --- /dev/null +++ b/SphereEversion/ToMathlib/Analysis/Convex/AmpleSet.lean @@ -0,0 +1,100 @@ +/- +Copyright (c) 2021 Anatole Dedecker. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anatole Dedecker, Michael Rothgang, Floris van Doorn +-/ +import Mathlib.Analysis.Convex.Normed +import SphereEversion.ToMathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv + +/-! +# Ample subsets of real vector spaces + +In this file we study ample set in real vector spaces. A set is ample if all its connected +component have full convex hull. + +## 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.vadd`: in particular, ampleness is invariant under affine translations + +TODO: migrate proof to this file... +- `AmpleSet.xxx`: a linear subspace with 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 -/ + +open Set + +variable {F : Type*} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] + +/-- A subset of a topological real vector space is ample +if the convex hull of each of its connected components is the full space. -/ +def AmpleSet (s : Set F) : Prop := + ∀ x ∈ s, convexHull ℝ (connectedComponentIn s x) = univ + +/-- A whole vector space is ample. -/ +@[simp] +theorem ampleSet_univ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] : + AmpleSet (univ : Set F) := by + intro x _ + rw [connectedComponentIn_univ, PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ] + +/-- The empty set in a vector space is ample. -/ +@[simp] +theorem ampleSet_empty : AmpleSet (∅ : Set F) := fun _ h ↦ False.elim h -- or `by intro _ _; trivial` + +/-- The union of two ample sets is ample. -/ +theorem AmpleSet.union {s t : Set F} (hs : AmpleSet s) (ht : AmpleSet t) : AmpleSet (s ∪ t) := by + intro x hx + rcases hx with (h | h) + -- The connected component of x ∈ s in s ∪ t contains the connected component of x in s, + -- similarly for `t`. + · rw [← Set.univ_subset_iff, ← hs x h] + apply convexHull_mono + apply connectedComponentIn_mono + apply subset_union_left + · rw [← Set.univ_subset_iff, ← ht x h] + apply convexHull_mono + apply connectedComponentIn_mono + apply subset_union_right + +variable {E : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] + +/-- Images of ample sets under continuous affine equivalences are ample. -/ +theorem AmpleSet.image {s : Set E} (h : AmpleSet s) (L : E ≃ᵃL[ℝ] F) : + AmpleSet (L '' s) := fun x hx ↦ by + rw [L.image_eq_preimage] at hx + have : L '' connectedComponentIn s (L.symm x) = connectedComponentIn (L '' s) x := by + conv_rhs => rw [← L.apply_symm_apply x] + exact (L.toHomeomorph).image_connectedComponentIn hx + rw [← this] + -- if/when #11298 lands, switch order of this lemma + refine (AffineMap.image_convexHull _ L.toAffineMap).symm.trans ?_ + rw [h (L.symm x) hx, image_univ] + exact L.surjective.range_eq + +/-- Preimages of ample sets under continuous affine equivalences are ample. -/ +theorem AmpleSet.preimage {s : Set F} (h : AmpleSet s) (L : E ≃ᵃL[ℝ] F) : AmpleSet (L ⁻¹' s) := by + rw [← L.image_symm_eq_preimage]; exact h.image L.symm + +open scoped Pointwise +/-- Affine translations of ample sets are ample. -/ +theorem AmpleSet.vadd [ContinuousAdd E] {s : Set E} (h : AmpleSet s) {y : E} : + AmpleSet (y +ᵥ s) := by + show AmpleSet ((ContinuousAffineEquiv.constVAdd ℝ E y) '' s) + exact AmpleSet.image h _