feat: fintsupport of (smooth) partitions of unity (#10015)

From sphere-eversion: the result is used there for smooth partitions of unity, but also holds in the continuous setting.

In passing,
- use `Type*` (not `Type _`) in `sum_finsupport_smul_eq_finsum`,
- tag `SmoothPartitionOfUnity.toPartitionOfUnity` with @simps.

Author: grunweg

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

@@ -166,6 +166,7 @@ theorem sum_le_one (x : M) : ∑ᶠ i, f i x ≤ 1 :=
 #align smooth_partition_of_unity.sum_le_one SmoothPartitionOfUnity.sum_le_one
 
 /-- Reinterpret a smooth partition of unity as a continuous partition of unity. -/
+@[simps]
 def toPartitionOfUnity : PartitionOfUnity ι M s :=
   { f with toFun := fun i => f i }
 #align smooth_partition_of_unity.to_partition_of_unity SmoothPartitionOfUnity.toPartitionOfUnity
@@ -232,6 +233,64 @@ theorem finsum_smul_mem_convex {g : ι → M → F} {t : Set F} {x : M} (hx : x
   ht.finsum_mem (fun _ => f.nonneg _ _) (f.sum_eq_one hx) hg
 #align smooth_partition_of_unity.finsum_smul_mem_convex SmoothPartitionOfUnity.finsum_smul_mem_convex
 
+section finsupport
+
+variable {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M)
+
+/-- The support of a smooth partition of unity at a point `x₀` as a `Finset`.
+  This is the set of `i : ι` such that `x₀ ∈ support f i`, i.e. `f i ≠ x₀`. -/
+def finsupport : Finset ι := ρ.toPartitionOfUnity.finsupport x₀
+
+@[simp]
+theorem mem_finsupport {i : ι} : i ∈ ρ.finsupport x₀ ↔ i ∈ support fun i ↦ ρ i x₀ :=
+  ρ.toPartitionOfUnity.mem_finsupport x₀
+
+@[simp]
+theorem coe_finsupport : (ρ.finsupport x₀ : Set ι) = support fun i ↦ ρ i x₀ :=
+  ρ.toPartitionOfUnity.coe_finsupport x₀
+
+theorem sum_finsupport (hx₀ : x₀ ∈ s) : ∑ i in ρ.finsupport x₀, ρ i x₀ = 1 :=
+  ρ.toPartitionOfUnity.sum_finsupport hx₀
+
+theorem sum_finsupport' (hx₀ : x₀ ∈ s) {I : Finset ι} (hI : ρ.finsupport x₀ ⊆ I) :
+    ∑ i in I, ρ i x₀ = 1 :=
+  ρ.toPartitionOfUnity.sum_finsupport' hx₀ hI
+
+theorem sum_finsupport_smul_eq_finsum {A : Type*} [AddCommGroup A] [Module ℝ A] (φ : ι → M → A) :
+    ∑ i in ρ.finsupport x₀, ρ i x₀ • φ i x₀ = ∑ᶠ i, ρ i x₀ • φ i x₀ :=
+  ρ.toPartitionOfUnity.sum_finsupport_smul_eq_finsum φ
+
+end finsupport
+
+section fintsupport -- smooth partitions of unity have locally finite `tsupport`
+variable {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M)
+
+/-- The `tsupport`s of a smooth partition of unity are locally finite. -/
+theorem finite_tsupport : {i | x₀ ∈ tsupport (ρ i)}.Finite :=
+  ρ.toPartitionOfUnity.finite_tsupport _
+
+/-- The tsupport of a partition of unity at a point `x₀` as a `Finset`.
+  This is the set of `i : ι` such that `x₀ ∈ tsupport f i`. -/
+def fintsupport (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 _
+
+theorem finsupport_subset_fintsupport : ρ.finsupport x₀ ⊆ ρ.fintsupport x₀ :=
+  ρ.toPartitionOfUnity.finsupport_subset_fintsupport x₀
+
+theorem eventually_finsupport_subset : ∀ᶠ y in 𝓝 x₀, ρ.finsupport y ⊆ ρ.fintsupport x₀ :=
+  ρ.toPartitionOfUnity.eventually_finsupport_subset x₀
+
+end fintsupport
+
+section IsSubordinate
+
 /-- A smooth partition of unity `f i` is subordinate to a family of sets `U i` indexed by the same
 type if for each `i` the closure of the support of `f i` is a subset of `U i`. -/
 def IsSubordinate (f : SmoothPartitionOfUnity ι I M s) (U : ι → Set M) :=
@@ -267,6 +326,8 @@ theorem IsSubordinate.smooth_finsum_smul {g : ι → M → F} (hf : f.IsSubordin
   hf.contMDiff_finsum_smul ho hg
 #align smooth_partition_of_unity.is_subordinate.smooth_finsum_smul SmoothPartitionOfUnity.IsSubordinate.smooth_finsum_smul
 
+end IsSubordinate
+
 end SmoothPartitionOfUnity
 
 namespace BumpCovering

Mathlib/Topology/PartitionOfUnity.lean

@@ -180,7 +180,7 @@ section finsupport
 variable {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X)
 
 /-- The support of a partition of unity at a point `x₀` as a `Finset`.
-  This is the set of `i : ι` such that `f i` doesn't vanish at `x₀`. -/
+  This is the set of `i : ι` such that `x₀ ∈ support f i`, i.e. `f i ≠ x₀`. -/
 def finsupport : Finset ι := (ρ.locallyFinite.point_finite x₀).toFinset
 
 @[simp]
@@ -210,7 +210,7 @@ theorem sum_finsupport' (hx₀ : x₀ ∈ s) {I : Finset ι} (hI : ρ.finsupport
   simp only [Finset.mem_sdiff, ρ.mem_finsupport, mem_support, Classical.not_not] at hx
   exact hx.2
 
-theorem sum_finsupport_smul_eq_finsum {M : Type _} [AddCommGroup M] [Module ℝ M] (φ : ι → X → M) :
+theorem sum_finsupport_smul_eq_finsum {M : Type*} [AddCommGroup M] [Module ℝ M] (φ : ι → X → M) :
     ∑ i in ρ.finsupport x₀, ρ i x₀ • φ i x₀ = ∑ᶠ i, ρ i x₀ • φ i x₀ := by
   apply (finsum_eq_sum_of_support_subset _ _).symm
   have : (fun i ↦ (ρ i) x₀ • φ i x₀) = (fun i ↦ (ρ i) x₀) • (fun i ↦ φ i x₀) :=
@@ -220,6 +220,44 @@ theorem sum_finsupport_smul_eq_finsum {M : Type _} [AddCommGroup M] [Module ℝ
 
 end finsupport
 
+section fintsupport -- partitions of unity have locally finite `tsupport`
+
+variable {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X)
+
+/-- The `tsupport`s of a partition of unity are locally finite. -/
+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
+
+/-- The tsupport of a partition of unity at a point `x₀` as a `Finset`.
+  This is the set of `i : ι` such that `x₀ ∈ tsupport f i`. -/
+def fintsupport (x₀ : X) : 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₀ := by
+  apply (ρ.locallyFinite.closure.eventually_subset (fun _ ↦ isClosed_closure) x₀).mono
+  intro y hy z hz
+  rw [PartitionOfUnity.mem_fintsupport_iff] at *
+  exact hy hz
+
+theorem finsupport_subset_fintsupport : ρ.finsupport x₀ ⊆ ρ.fintsupport x₀ := fun i hi ↦ by
+  rw [ρ.mem_fintsupport_iff]
+  apply subset_closure
+  exact (ρ.mem_finsupport x₀).mp hi
+
+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
+
+end fintsupport
+
 /-- If `f` is a partition of unity on `s : Set X` and `g : X → E` is continuous at every point of
 the topological support of some `f i`, then `fun x ↦ f i x • g x` is continuous on the whole space.
 -/