refactor(ToMathlib/Partition,Topology/LocallyFinite): clean up for PRing

* add continuous versions of many results in partition (in a new section) * minor style tweaks: Type*, refine, use \mapsto over =>) * re-use variables and namespacing * small golf (save two lines and subgoals) * Most of these files has been PRed to mathlib.
leanprover-community · Jan 26, 2024 · 34b1e0e · 34b1e0e
1 parent 7774cc1
commit 34b1e0e
Show file tree

Hide file tree

Showing 2 changed files with 71 additions and 65 deletions.
diff --git a/SphereEversion/ToMathlib/Partition.lean b/SphereEversion/ToMathlib/Partition.lean
@@ -1,101 +1,111 @@
-import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm
-import SphereEversion.ToMathlib.Analysis.Convex.Basic
-import SphereEversion.ToMathlib.Topology.LocallyFinite
 import Mathlib.Geometry.Manifold.PartitionOfUnity
-import Mathlib.Geometry.Manifold.ContMDiff.Basic
-import Mathlib.Geometry.Manifold.Algebra.LieGroup
-import Mathlib.Topology.Support
+import SphereEversion.ToMathlib.Topology.LocallyFinite
+import SphereEversion.ToMathlib.Analysis.Convex.Basic
+import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm
 
 noncomputable section
 
 open scoped Topology Filter Manifold BigOperators
 
 open Set Function Filter
 
-section
+section -- unused, but might be nice API: PRed in #10019 (depending on #10020)
 
-variable {ι : Type _} {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type _}
-  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type _} [TopologicalSpace M]
-  [ChartedSpace H M] {s : Set M} {F : Type _} [NormedAddCommGroup F] [NormedSpace ℝ F]
+variable {ι : Type*} {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*}
+  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M]
+  [ChartedSpace H M] {s : Set M} {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 
 variable [FiniteDimensional ℝ E] [SmoothManifoldWithCorners I M]
 
 theorem SmoothPartitionOfUnity.contMDiffAt_sum (ρ : SmoothPartitionOfUnity ι I M s) {n : ℕ∞}
     {x₀ : M} {φ : ι → M → F} (hφ : ∀ i, x₀ ∈ tsupport (ρ i) → ContMDiffAt I 𝓘(ℝ, F) n (φ i) x₀) :
-    ContMDiffAt I 𝓘(ℝ, F) n (fun x => ∑ᶠ i, ρ i x • φ i x) x₀ := by
-  refine' contMDiffAt_finsum (ρ.locallyFinite.smul_left _) fun i => _
+    ContMDiffAt I 𝓘(ℝ, F) n (fun x ↦ ∑ᶠ i, ρ i x • φ i x) x₀ := by
+  refine contMDiffAt_finsum (ρ.locallyFinite.smul_left _) fun i ↦ ?_
   by_cases hx : x₀ ∈ tsupport (ρ i)
   · exact ContMDiffAt.smul ((ρ i).smooth.of_le le_top).contMDiffAt (hφ i hx)
   · exact contMDiffAt_of_not_mem (compl_subset_compl.mpr (tsupport_smul_subset_left (ρ i) (φ i)) hx) n
 
 theorem SmoothPartitionOfUnity.contDiffAt_sum {s : Set E}
     (ρ : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s) {n : ℕ∞} {x₀ : E} {φ : ι → E → F}
     (hφ : ∀ i, x₀ ∈ tsupport (ρ i) → ContDiffAt ℝ n (φ i) x₀) :
-    ContDiffAt ℝ n (fun x => ∑ᶠ i, ρ i x • φ i x) x₀ := by
+    ContDiffAt ℝ n (fun x ↦ ∑ᶠ i, ρ i x • φ i x) x₀ := by
   simp only [← contMDiffAt_iff_contDiffAt] at *
   exact ρ.contMDiffAt_sum hφ
 
 end
 
 section
 
-variable {ι : Type _}
+variable {ι : Type*}
 
-variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type _}
-  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type _} [TopologicalSpace M]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type*}
+  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M]
   [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M]
 
-section
+section -- up to sum_germ, PRed in #10015 (the remainder needs smooth germs)
+
+variable {F : Type*} [AddCommGroup F] [Module ℝ F]
 
-variable {F : Type _} [AddCommGroup F] [Module ℝ F]
+namespace PartitionOfUnity
 
--- TODO [Yury]: this is true for a continuous partition of unity
-theorem SmoothPartitionOfUnity.finite_tsupport {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s)
-    (x : M) : {i | x ∈ tsupport (ρ i)}.Finite := by
+variable {s : Set M} (ρ : PartitionOfUnity ι M s) (x : M)
+
+theorem finite_tsupport : {i | x ∈ tsupport (ρ i)}.Finite := by
   rcases ρ.locallyFinite x with ⟨t, t_in, ht⟩
   apply ht.subset
   rintro i hi
   simp only [inter_comm]
   exact mem_closure_iff_nhds.mp hi t t_in
 
-def SmoothPartitionOfUnity.fintsupport {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x : M) :
-    Finset ι :=
+def fintsupport : Finset ι :=
   (ρ.finite_tsupport x).toFinset
 
-theorem SmoothPartitionOfUnity.mem_fintsupport_iff {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s)
-    (x : M) (i : ι) : i ∈ ρ.fintsupport x ↔ x ∈ tsupport (ρ i) :=
+theorem mem_fintsupport_iff (i : ι) : i ∈ ρ.fintsupport x ↔ x ∈ tsupport (ρ i) :=
   Finite.mem_toFinset _
 
-theorem SmoothPartitionOfUnity.eventually_fintsupport_subset {s : Set M}
-    (ρ : SmoothPartitionOfUnity ι I M s) (x : M) :
-    ∀ᶠ y in 𝓝 x, ρ.fintsupport y ⊆ ρ.fintsupport x := by
-  apply (ρ.locallyFinite.closure.eventually_subset (fun _ => isClosed_closure) x).mono
+theorem eventually_fintsupport_subset : ∀ᶠ y in 𝓝 x, ρ.fintsupport y ⊆ ρ.fintsupport x := by
+  apply (ρ.locallyFinite.closure.eventually_subset (fun _ ↦ isClosed_closure) x).mono
   intro y hy z hz
-  rw [SmoothPartitionOfUnity.mem_fintsupport_iff] at *
+  rw [PartitionOfUnity.mem_fintsupport_iff] at *
   exact hy hz
 
-def SmoothPartitionOfUnity.finsupport {ι : Type _} {E : Type _} [NormedAddCommGroup E]
-    [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type _} [TopologicalSpace H]
-    {I : ModelWithCorners ℝ E H} {M : Type _} [TopologicalSpace M] [ChartedSpace H M]
+end PartitionOfUnity
+
+namespace SmoothPartitionOfUnity
+
+variable {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x : M)
+
+theorem finite_tsupport : {i | x ∈ tsupport (ρ i)}.Finite :=
+  PartitionOfUnity.finite_tsupport ρ.toPartitionOfUnity _
+
+def fintsupport {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x : M) :
+    Finset ι :=
+  (ρ.finite_tsupport x).toFinset
+
+theorem mem_fintsupport_iff (i : ι) : i ∈ ρ.fintsupport x ↔ x ∈ tsupport (ρ i) :=
+  Finite.mem_toFinset _
+
+theorem eventually_fintsupport_subset : ∀ᶠ y in 𝓝 x, ρ.fintsupport y ⊆ ρ.fintsupport x :=
+  ρ.toPartitionOfUnity.eventually_fintsupport_subset _
+
+def finsupport {ι : Type*} {E : Type*} [NormedAddCommGroup E]
+    [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type*} [TopologicalSpace H]
+    {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
     [SmoothManifoldWithCorners I M] {s} (ρ : SmoothPartitionOfUnity ι I M s) (x : M) : Finset ι :=
   ρ.toPartitionOfUnity.finsupport x
 
 /-- Weaker version of `smooth_partition_of_unity.eventually_fintsupport_subset`. -/
-theorem SmoothPartitionOfUnity.finsupport_subset_fintsupport {s : Set M}
-    (ρ : SmoothPartitionOfUnity ι I M s) (x : M) :
-    ρ.finsupport x ⊆ ρ.fintsupport x := fun i hi ↦ by
+theorem finsupport_subset_fintsupport : ρ.finsupport x ⊆ ρ.fintsupport x := fun i hi ↦ by
   rw [ρ.mem_fintsupport_iff]
   apply subset_closure
   exact (ρ.toPartitionOfUnity.mem_finsupport x).mp hi
 
-theorem SmoothPartitionOfUnity.eventually_finsupport_subset {s : Set M}
-    (ρ : SmoothPartitionOfUnity ι I M s) (x : M) :
-    ∀ᶠ y in 𝓝 x, ρ.finsupport y ⊆ ρ.fintsupport x := by
-  apply (ρ.eventually_fintsupport_subset x).mono
-  exact fun y hy => (ρ.finsupport_subset_fintsupport y).trans hy
+theorem eventually_finsupport_subset : ∀ᶠ y in 𝓝 x, ρ.finsupport y ⊆ ρ.fintsupport x :=
+  (ρ.eventually_fintsupport_subset x).mono
+    fun y hy ↦ (ρ.finsupport_subset_fintsupport y).trans hy
 
-theorem SmoothPartitionOfUnity.sum_germ {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) {x : M}
-    (hx : x ∈ interior s := by simp) :
+variable {x} in
+theorem sum_germ (hx : x ∈ interior s := by simp) :
     ∑ i in ρ.fintsupport x, (ρ i : smoothGerm I x) = 1 := by
   have : ∀ᶠ y in 𝓝 x, y ∈ interior s := isOpen_interior.eventually_mem hx
   have : ∀ᶠ y in 𝓝 x, (⇑(∑ i : ι in ρ.fintsupport x, ρ i)) y = 1 := by
@@ -105,17 +115,16 @@ theorem SmoothPartitionOfUnity.sum_germ {s : Set M} (ρ : SmoothPartitionOfUnity
   rw [← smoothGerm.coe_sum]
   exact smoothGerm.coe_eq_coe _ _ 1 this
 
-def SmoothPartitionOfUnity.combine {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (φ : ι → M → F)
-    (x : M) : F :=
+def combine (ρ : SmoothPartitionOfUnity ι I M s) (φ : ι → M → F) (x : M) : F :=
   ∑ᶠ i, ρ i x • φ i x
 
+-- PRed to mathlib as well
 -- TODO: move to Mathlib attribute [simps] SmoothPartitionOfUnity.toPartitionOfUnity
 
-theorem SmoothPartitionOfUnity.germ_combine_mem {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s)
-    (φ : ι → M → F) {x : M}
-    (hx : x ∈ interior s := by simp) :
+variable {x} in
+theorem germ_combine_mem (φ : ι → M → F) (hx : x ∈ interior s := by simp) :
     (ρ.combine φ : Germ (𝓝 x) F) ∈
-      reallyConvexHull (smoothGerm I x) ((fun i => (φ i : Germ (𝓝 x) F)) '' ρ.fintsupport x) := by
+      reallyConvexHull (smoothGerm I x) ((fun i ↦ (φ i : Germ (𝓝 x) F)) '' ρ.fintsupport x) := by
   change x ∈ interior s at hx
   have : (ρ.combine φ : Germ (𝓝 x) F) =
       ∑ i in ρ.fintsupport x, (ρ i : smoothGerm I x) • (φ i : Germ (𝓝 x) F) := by
@@ -125,17 +134,16 @@ theorem SmoothPartitionOfUnity.germ_combine_mem {s : Set M} (ρ : SmoothPartitio
     filter_upwards [ρ.eventually_finsupport_subset x] with x' hx'
     simp_rw [SmoothPartitionOfUnity.combine, Finset.sum_apply, Pi.smul_apply']
     rw [finsum_eq_sum_of_support_subset]
-    refine' Subset.trans _ (Finset.coe_subset.mpr hx')
+    refine Subset.trans ?_ (Finset.coe_subset.mpr hx')
     rw [SmoothPartitionOfUnity.finsupport, PartitionOfUnity.finsupport, Finite.coe_toFinset]
     apply support_smul_subset_left
   rw [this]
-  apply sum_mem_reallyConvexHull
+  refine sum_mem_reallyConvexHull ?_ (ρ.sum_germ hx) (fun i hi ↦ mem_image_of_mem _ hi)
   · intro i _
     apply eventually_of_forall
     apply ρ.nonneg
-  · apply ρ.sum_germ hx
-  · intro i hi
-    exact mem_image_of_mem _ hi
+
+end SmoothPartitionOfUnity
 
 end
 

diff --git a/SphereEversion/ToMathlib/Topology/LocallyFinite.lean b/SphereEversion/ToMathlib/Topology/LocallyFinite.lean
@@ -4,19 +4,17 @@ import Mathlib.Topology.LocallyFinite
 
 open Function Set
 
--- these two lemmas require additional imports compared to what's in mathlib
--- `Algebra.SMulWithZero` is not required in `Topology.LocallyFinite` so far;
--- so it remains to find a nice home for these lemmas...
-theorem LocallyFinite.smul_left {ι : Type*} {α : Type*} [TopologicalSpace α] {M : Type*}
+-- PRed in #10020
+theorem LocallyFinite.smul_left {ι : Type*} {X : Type*} [TopologicalSpace X] {M : Type*}
     {R : Type*} [Zero R] [Zero M] [SMulWithZero R M]
-    {s : ι → α → R} (h : LocallyFinite fun i => support <| s i) (f : ι → α → M) :
-    LocallyFinite fun i => support (s i • f i) :=
+    {s : ι → X → R} (h : LocallyFinite fun i ↦ support <| s i) (f : ι → X → M) :
+    LocallyFinite fun i ↦ support (s i • f i) :=
   h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, zero_smul]
 
-theorem LocallyFinite.smul_right {ι : Type*} {α : Type*} [TopologicalSpace α] {M : Type*}
+theorem LocallyFinite.smul_right {ι : Type*} {X : Type*} [TopologicalSpace X] {M : Type*}
     {R : Type*} [Zero R] [Zero M] [SMulZeroClass R M]
-    {f : ι → α → M} (h : LocallyFinite fun i => support <| f i) (s : ι → α → R) :
-    LocallyFinite fun i => support <| s i • f i :=
+    {f : ι → X → M} (h : LocallyFinite fun i ↦ support <| f i) (s : ι → X → R) :
+    LocallyFinite fun i ↦ support <| s i • f i :=
   h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, smul_zero]
 
 section
@@ -27,8 +25,8 @@ variable {ι X : Type*} [TopologicalSpace X]
 -- See https://github.com/leanprover-community/mathlib4/pull/9813#discussion_r1455617707.
 @[to_additive]
 theorem LocallyFinite.exists_finset_mulSupport_eq {M : Type*} [CommMonoid M] {ρ : ι → X → M}
-    (hρ : LocallyFinite fun i => mulSupport <| ρ i) (x₀ : X) :
-    ∃ I : Finset ι, (mulSupport fun i => ρ i x₀) = I := by
+    (hρ : LocallyFinite fun i ↦ mulSupport <| ρ i) (x₀ : X) :
+    ∃ I : Finset ι, (mulSupport fun i ↦ ρ i x₀) = I := by
   use (hρ.point_finite x₀).toFinset
   rw [Finite.coe_toFinset]
   rfl