From f16dbd9bba98b3a82e0bc7dd9526770f8f67c317 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Thu, 14 Sep 2023 09:08:47 +0000 Subject: [PATCH] feat: the linear span of a separable set is separable (#7115) --- Mathlib/Analysis/Calculus/ContDiff.lean | 9 +++++++ Mathlib/LinearAlgebra/Finsupp.lean | 28 ++++++++++++++++++++++ Mathlib/Topology/Algebra/Module/Basic.lean | 21 ++++++++++++++++ Mathlib/Topology/Bases.lean | 21 +++++++++++++++- Mathlib/Topology/EMetricSpace/Basic.lean | 20 +++++++++++----- Mathlib/Topology/Separation.lean | 6 +++++ 6 files changed, 98 insertions(+), 7 deletions(-) diff --git a/Mathlib/Analysis/Calculus/ContDiff.lean b/Mathlib/Analysis/Calculus/ContDiff.lean index 1fa670dca1fdc..0ce89c15d7833 100644 --- a/Mathlib/Analysis/Calculus/ContDiff.lean +++ b/Mathlib/Analysis/Calculus/ContDiff.lean @@ -2064,6 +2064,15 @@ theorem ContDiffAt.exists_lipschitzOnWith {f : E' → F'} {x : E'} (hf : ContDif (hf.hasStrictFDerivAt le_rfl).exists_lipschitzOnWith #align cont_diff_at.exists_lipschitz_on_with ContDiffAt.exists_lipschitzOnWith +/-- A `C^1` function with compact support is Lipschitz. -/ +theorem ContDiff.lipschitzWith_of_hasCompactSupport {f : E' → F'} {n : ℕ∞} + (hf : HasCompactSupport f) (h'f : ContDiff 𝕂 n f) (hn : 1 ≤ n) : + ∃ C, LipschitzWith C f := by + obtain ⟨C, hC⟩ := (hf.fderiv 𝕂).exists_bound_of_continuous (h'f.continuous_fderiv hn) + refine ⟨⟨max C 0, le_max_right _ _⟩, ?_⟩ + apply lipschitzWith_of_nnnorm_fderiv_le (h'f.differentiable hn) (fun x ↦ ?_) + simp [← NNReal.coe_le_coe, hC x] + end Real section deriv diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 9449a66530595..1c2353deff8b2 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -1200,6 +1200,34 @@ theorem mem_span_set {m : M} {s : Set M} : exact Finsupp.mem_span_image_iff_total R (v := _root_.id (α := M)) #align mem_span_set mem_span_set +/-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if +`m` can be written as a finite `R`-linear combination of elements of `s`. +The implementation uses a sum indexed by `Fin n` for some `n`. -/ +lemma mem_span_set' {m : M} {s : Set M} : + m ∈ Submodule.span R s ↔ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → s), + ∑ i, f i • (g i : M) = m := by + refine ⟨fun h ↦ ?_, ?_⟩ + · rcases mem_span_set.1 h with ⟨c, cs, rfl⟩ + have A : c.support ≃ Fin c.support.card := Finset.equivFin _ + refine ⟨_, fun i ↦ c (A.symm i), fun i ↦ ⟨A.symm i, cs (A.symm i).2⟩, ?_⟩ + rw [Finsupp.sum, ← Finset.sum_coe_sort c.support] + exact Fintype.sum_equiv A.symm _ (fun j ↦ c j • (j : M)) (fun i ↦ rfl) + · rintro ⟨n, f, g, rfl⟩ + exact Submodule.sum_mem _ (fun i _ ↦ Submodule.smul_mem _ _ (Submodule.subset_span (g i).2)) + +/-- The span of a subset `s` is the union over all `n` of the set of linear combinations of at most +`n` terms belonging to `s`. -/ +lemma span_eq_iUnion_nat (s : Set M) : + (Submodule.span R s : Set M) = ⋃ (n : ℕ), + (fun (f : Fin n → (R × M)) ↦ ∑ i, (f i).1 • (f i).2) '' ({f | ∀ i, (f i).2 ∈ s}) := by + ext m + simp only [SetLike.mem_coe, mem_iUnion, mem_image, mem_setOf_eq, mem_span_set'] + refine exists_congr (fun n ↦ ⟨?_, ?_⟩) + · rintro ⟨f, g, rfl⟩ + exact ⟨fun i ↦ (f i, g i), fun i ↦ (g i).2, rfl⟩ + · rintro ⟨f, hf, rfl⟩ + exact ⟨fun i ↦ (f i).1, fun i ↦ ⟨(f i).2, (hf i)⟩, rfl⟩ + /-- If `Subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`. -/ @[simps] def Module.subsingletonEquiv (R M ι : Type*) [Semiring R] [Subsingleton R] [AddCommMonoid M] diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index 6e15802c0078f..ce94ffeb92249 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/Basic.lean @@ -12,6 +12,7 @@ import Mathlib.Topology.UniformSpace.UniformEmbedding import Mathlib.Algebra.Algebra.Basic import Mathlib.LinearAlgebra.Projection import Mathlib.LinearAlgebra.Pi +import Mathlib.LinearAlgebra.Finsupp #align_import topology.algebra.module.basic from "leanprover-community/mathlib"@"6285167a053ad0990fc88e56c48ccd9fae6550eb" @@ -110,6 +111,21 @@ theorem continuousSMul_induced : @ContinuousSMul R M₁ _ u (t.induced f) := by end LatticeOps +/-- The span of a separable subset with respect to a separable scalar ring is again separable. -/ +lemma TopologicalSpace.IsSeparable.span {R M : Type*} [AddCommMonoid M] [Semiring R] [Module R M] + [TopologicalSpace M] [TopologicalSpace R] [SeparableSpace R] + [ContinuousAdd M] [ContinuousSMul R M] {s : Set M} (hs : IsSeparable s) : + IsSeparable (Submodule.span R s : Set M) := by + rw [span_eq_iUnion_nat] + apply isSeparable_iUnion (fun n ↦ ?_) + apply IsSeparable.image + · have : IsSeparable {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ Set.univ ×ˢ s} := by + apply isSeparable_pi (fun i ↦ (isSeparable_of_separableSpace Set.univ).prod hs) + convert this + simp + · apply continuous_finset_sum _ (fun i _ ↦ ?_) + exact (continuous_fst.comp (continuous_apply i)).smul (continuous_snd.comp (continuous_apply i)) + namespace Submodule variable {α β : Type*} [TopologicalSpace β] @@ -161,6 +177,11 @@ theorem Submodule.le_topologicalClosure (s : Submodule R M) : s ≤ s.topologica subset_closure #align submodule.le_topological_closure Submodule.le_topologicalClosure +theorem Submodule.closure_subset_topologicalClosure_span (s : Set M) : + closure s ⊆ (span R s).topologicalClosure := by + rw [Submodule.topologicalClosure_coe] + exact closure_mono subset_span + theorem Submodule.isClosed_topologicalClosure (s : Submodule R M) : IsClosed (s.topologicalClosure : Set M) := isClosed_closure #align submodule.is_closed_topological_closure Submodule.isClosed_topologicalClosure diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean index 3b259ab25a2e6..05dc1a8c92020 100644 --- a/Mathlib/Topology/Bases.lean +++ b/Mathlib/Topology/Bases.lean @@ -425,7 +425,7 @@ theorem _root_.Set.PairwiseDisjoint.countable_of_nonempty_interior [SeparableSpa set `c`. Beware that this definition does not require that `c` is contained in `s` (to express the latter, use `TopologicalSpace.SeparableSpace s` or `TopologicalSpace.IsSeparable (univ : Set s))`. In metric spaces, the two definitions are -equivalent, see `TopologicalSpace.IsSeparable.SeparableSpace`. -/ +equivalent, see `TopologicalSpace.IsSeparable.separableSpace`. -/ def IsSeparable (s : Set α) := ∃ c : Set α, c.Countable ∧ s ⊆ closure c #align topological_space.is_separable TopologicalSpace.IsSeparable @@ -457,6 +457,25 @@ theorem isSeparable_iUnion {ι : Type*} [Countable ι] {s : ι → Set α} exact (h'c i).trans (closure_mono (subset_iUnion _ i)) #align topological_space.is_separable_Union TopologicalSpace.isSeparable_iUnion +lemma isSeparable_pi {ι : Type*} [Fintype ι] {α : ∀ (_ : ι), Type*} {s : ∀ i, Set (α i)} + [∀ i, TopologicalSpace (α i)] (h : ∀ i, IsSeparable (s i)) : + IsSeparable {f : ∀ i, α i | ∀ i, f i ∈ s i} := by + choose c c_count hc using h + refine ⟨{f | ∀ i, f i ∈ c i}, countable_pi c_count, ?_⟩ + simp_rw [← mem_univ_pi] + dsimp + rw [closure_pi_set] + exact Set.pi_mono (fun i _ ↦ hc i) + +lemma IsSeparable.prod {β : Type*} [TopologicalSpace β] + {s : Set α} {t : Set β} (hs : IsSeparable s) (ht : IsSeparable t) : + IsSeparable (s ×ˢ t) := by + rcases hs with ⟨cs, cs_count, hcs⟩ + rcases ht with ⟨ct, ct_count, hct⟩ + refine ⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩ + rw [closure_prod_eq] + exact Set.prod_mono hcs hct + theorem _root_.Set.Countable.isSeparable {s : Set α} (hs : s.Countable) : IsSeparable s := ⟨s, hs, subset_closure⟩ #align set.countable.is_separable Set.Countable.isSeparable diff --git a/Mathlib/Topology/EMetricSpace/Basic.lean b/Mathlib/Topology/EMetricSpace/Basic.lean index d2f8353d94eeb..a3bf452a74ab9 100644 --- a/Mathlib/Topology/EMetricSpace/Basic.lean +++ b/Mathlib/Topology/EMetricSpace/Basic.lean @@ -809,17 +809,25 @@ theorem subset_countable_closure_of_almost_dense_set (s : Set α) #align emetric.subset_countable_closure_of_almost_dense_set EMetric.subset_countable_closure_of_almost_dense_set open TopologicalSpace in -/-- If a set `s` is separable, then the corresponding subtype is separable in a (pseudo extended) -metric space. This is not obvious, as the countable set whose closure covers `s` does not need in -general to be contained in `s`. -/ -theorem _root_.TopologicalSpace.IsSeparable.separableSpace {s : Set α} (hs : IsSeparable s) : - SeparableSpace s := by +/-- If a set `s` is separable in a (pseudo extended) metric space, then it admits a countable dense +subset. This is not obvious, as the countable set whose closure covers `s` given by the definition +of separability does not need in general to be contained in `s`. -/ +theorem _root_.TopologicalSpace.IsSeparable.exists_countable_dense_subset + {s : Set α} (hs : IsSeparable s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t := by have : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε := fun ε ε0 => by rcases hs with ⟨t, htc, hst⟩ refine ⟨t, htc, hst.trans fun x hx => ?_⟩ rcases mem_closure_iff.1 hx ε ε0 with ⟨y, hyt, hxy⟩ exact mem_iUnion₂.2 ⟨y, hyt, mem_closedBall.2 hxy.le⟩ - rcases subset_countable_closure_of_almost_dense_set _ this with ⟨t, hts, htc, hst⟩ + exact subset_countable_closure_of_almost_dense_set _ this + +open TopologicalSpace in +/-- If a set `s` is separable, then the corresponding subtype is separable in a (pseudo extended) +metric space. This is not obvious, as the countable set whose closure covers `s` does not need in +general to be contained in `s`. -/ +theorem _root_.TopologicalSpace.IsSeparable.separableSpace {s : Set α} (hs : IsSeparable s) : + SeparableSpace s := by + rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, hst⟩ lift t to Set s using hts refine ⟨⟨t, countable_of_injective_of_countable_image (Subtype.coe_injective.injOn _) htc, ?_⟩⟩ rwa [inducing_subtype_val.dense_iff, Subtype.forall] diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index 0d5256cc2801b..a18983414ee9d 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -410,6 +410,12 @@ theorem Ne.nhdsWithin_diff_singleton [T1Space α] {x y : α} (h : x ≠ y) (s : exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h) #align ne.nhds_within_diff_singleton Ne.nhdsWithin_diff_singleton +lemma nhdsWithin_compl_singleton_le [T1Space α] (x y : α) : 𝓝[{x}ᶜ] x ≤ 𝓝[{y}ᶜ] x := by + rcases eq_or_ne x y with rfl|hy + · exact Eq.le rfl + · rw [Ne.nhdsWithin_compl_singleton hy] + exact nhdsWithin_le_nhds + theorem isOpen_setOf_eventually_nhdsWithin [T1Space α] {p : α → Prop} : IsOpen { x | ∀ᶠ y in 𝓝[≠] x, p y } := by refine' isOpen_iff_mem_nhds.mpr fun a ha => _