feat: construct a smooth function on a manifold equal to one on a giv…

…en closed set and with given support (#6067)

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

@@ -75,10 +75,10 @@ variable {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E
 ### Covering by supports of smooth bump functions
 
 In this section we define `SmoothBumpCovering ι I M s` to be a collection of
-`SmoothBumpFunction`s such that their supports is a locally finite family of sets and for each `x
-∈ s` some function `f i` from the collection is equal to `1` in a neighborhood of `x`. A covering of
-this type is useful to construct a smooth partition of unity and can be used instead of a partition
-of unity in some proofs.
+`SmoothBumpFunction`s such that their supports is a locally finite family of sets and for each
+`x ∈ s` some function `f i` from the collection is equal to `1` in a neighborhood of `x`. A covering
+of this type is useful to construct a smooth partition of unity and can be used instead of a
+partition of unity in some proofs.
 
 We prove that on a smooth finite dimensional real manifold with `σ`-compact Hausdorff topology, for
 any `U : M → Set M` such that `∀ x ∈ s, U x ∈ 𝓝 x` there exists a `SmoothBumpCovering ι I M s`
@@ -103,10 +103,15 @@ This covering can be used, e.g., to construct a partition of unity and to prove
 Whitney embedding theorem. -/
 -- porting note: was @[nolint has_nonempty_instance]
 structure SmoothBumpCovering (s : Set M := univ) where
+  /-- The center point of each bump in the smooth covering. -/
   c : ι → M
+  /-- A smooth bump function around `c i`. -/
   toFun : ∀ i, SmoothBumpFunction I (c i)
+  /-- All the bump functions in the covering are centered at points in `s`. -/
   c_mem' : ∀ i, c i ∈ s
+  /-- Around each point, there are only finitely many nonzero bump functions in the family. -/
   locallyFinite' : LocallyFinite fun i => support (toFun i)
+  /-- Around each point in `s`, one of the bump functions is equal to `1`. -/
   eventuallyEq_one' : ∀ x ∈ s, ∃ i, toFun i =ᶠ[𝓝 x] 1
 #align smooth_bump_covering SmoothBumpCovering
 
@@ -117,10 +122,15 @@ structure SmoothBumpCovering (s : Set M := univ) where
 * for all `x ∈ s` the sum `∑ᶠ i, f i x` equals one;
 * for all `x`, the sum `∑ᶠ i, f i x` is less than or equal to one. -/
 structure SmoothPartitionOfUnity (s : Set M := univ) where
+  /-- The family of functions forming the partition of unity. -/
   toFun : ι → C^∞⟮I, M; 𝓘(ℝ), ℝ⟯
+  /-- Around each point, there are only finitely many nonzero functions in the family. -/
   locallyFinite' : LocallyFinite fun i => support (toFun i)
+  /-- All the functions in the partition of unity are nonnegative. -/
   nonneg' : ∀ i x, 0 ≤ toFun i x
+  /-- The functions in the partition of unity add up to `1` at any point of `s`. -/
   sum_eq_one' : ∀ x ∈ s, ∑ᶠ i, toFun i x = 1
+  /-- The functions in the partition of unity add up to at most `1` everywhere. -/
   sum_le_one' : ∀ x, ∑ᶠ i, toFun i x ≤ 1
 #align smooth_partition_of_unity SmoothPartitionOfUnity
 
@@ -146,6 +156,14 @@ theorem sum_eq_one {x} (hx : x ∈ s) : ∑ᶠ i, f i x = 1 :=
   f.sum_eq_one' x hx
 #align smooth_partition_of_unity.sum_eq_one SmoothPartitionOfUnity.sum_eq_one
 
+theorem exists_pos_of_mem {x} (hx : x ∈ s) : ∃ i, 0 < f i x := by
+  by_contra h
+  push_neg at h
+  have H : ∀ i, f i x = 0 := fun i ↦ le_antisymm (h i) (f.nonneg i x)
+  have := f.sum_eq_one hx
+  simp_rw [H] at this
+  simpa
+
 theorem sum_le_one (x : M) : ∑ᶠ i, f i x ≤ 1 :=
   f.sum_le_one' x
 #align smooth_partition_of_unity.sum_le_one SmoothPartitionOfUnity.sum_le_one
@@ -463,9 +481,10 @@ end SmoothBumpCovering
 
 variable (I)
 
-/-- Given two disjoint closed sets in a Hausdorff σ-compact finite dimensional manifold, there
-exists an infinitely smooth function that is equal to `0` on one of them and is equal to one on the
-other. -/
+/-- Given two disjoint closed sets `s, t` in a Hausdorff σ-compact finite dimensional manifold,
+there exists an infinitely smooth function that is equal to `0` on `s` and to `1` on `t`.
+See also `exists_smooth_zero_iff_one_iff_of_closed`, which ensures additionally that
+`f` is equal to `0` exactly on `s` and to `1` exactly on `t`. -/
 theorem exists_smooth_zero_one_of_closed [T2Space M] [SigmaCompactSpace M] {s t : Set M}
     (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
     ∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
@@ -497,7 +516,7 @@ instance [Inhabited ι] (s : Set M) : Inhabited (SmoothPartitionOfUnity ι I M s
 variable [T2Space M] [SigmaCompactSpace M]
 
 /-- If `X` is a paracompact normal topological space and `U` is an open covering of a closed set
-`s`, then there exists a `BumpCovering ι X s` that is subordinate to `U`. -/
+`s`, then there exists a `SmoothPartitionOfUnity ι M s` that is subordinate to `U`. -/
 theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (ho : ∀ i, IsOpen (U i))
     (hU : s ⊆ ⋃ i, U i) : ∃ f : SmoothPartitionOfUnity ι I M s, f.IsSubordinate U := by
   haveI : LocallyCompactSpace H := I.locally_compact
@@ -512,6 +531,18 @@ theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (h
     exact ⟨f, f.smooth, hf⟩
 #align smooth_partition_of_unity.exists_is_subordinate SmoothPartitionOfUnity.exists_isSubordinate
 
+theorem exists_isSubordinate_chartAt_source_of_isClosed {s : Set M} (hs : IsClosed s) :
+    ∃ f : SmoothPartitionOfUnity s I M s,
+      f.IsSubordinate (fun x ↦ (chartAt H (x : M)).source) := by
+  apply exists_isSubordinate _ hs _ (fun i ↦ (chartAt H _).open_source) (fun x hx ↦ ?_)
+  exact mem_iUnion_of_mem ⟨x, hx⟩ (mem_chart_source H x)
+
+variable (M)
+theorem exists_isSubordinate_chartAt_source :
+    ∃ f : SmoothPartitionOfUnity M I M univ, f.IsSubordinate (fun x ↦ (chartAt H x).source) := by
+  apply exists_isSubordinate _ isClosed_univ _ (fun i ↦ (chartAt H _).open_source) (fun x _ ↦ ?_)
+  exact mem_iUnion_of_mem x (mem_chart_source H x)
+
 end SmoothPartitionOfUnity
 
 variable [SigmaCompactSpace M] [T2Space M] {t : M → Set F} {n : ℕ∞}
@@ -590,3 +621,111 @@ theorem Metric.exists_smooth_forall_closedBall_subset {M} [MetricSpace M] [Chart
   rw [← Metric.emetric_closedBall (hδ0 _).le]
   exact hδ i x hx
 #align metric.exists_smooth_forall_closed_ball_subset Metric.exists_smooth_forall_closedBall_subset
+
+lemma IsOpen.exists_msmooth_support_eq_aux {s : Set H} (hs : IsOpen s) :
+    ∃ f : H → ℝ, f.support = s ∧ Smooth I 𝓘(ℝ) f ∧ Set.range f ⊆ Set.Icc 0 1 := by
+  have h's : IsOpen (I.symm ⁻¹' s) := I.continuous_symm.isOpen_preimage _ hs
+  rcases h's.exists_smooth_support_eq with ⟨f, f_supp, f_diff, f_range⟩
+  refine ⟨f ∘ I, ?_, ?_, ?_⟩
+  · rw [support_comp_eq_preimage, f_supp, ← preimage_comp]
+    simp only [ModelWithCorners.symm_comp_self, preimage_id_eq, id_eq]
+  · exact f_diff.comp_contMDiff contMDiff_model
+  · exact Subset.trans (range_comp_subset_range _ _) f_range
+
+/-- Given an open set in a finite-dimensional real manifold, there exists a nonnegative smooth
+function with support equal to `s`. -/
+theorem IsOpen.exists_msmooth_support_eq (hs : IsOpen s) :
+    ∃ f : M → ℝ, f.support = s ∧ Smooth I 𝓘(ℝ) f ∧ ∀ x, 0 ≤ f x := by
+  rcases SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source I M with ⟨f, hf⟩
+  have A : ∀ (c : M), ∃ g : H → ℝ,
+      g.support = (chartAt H c).target ∩ (chartAt H c).symm ⁻¹' s ∧
+      Smooth I 𝓘(ℝ) g ∧ Set.range g ⊆ Set.Icc 0 1 := by
+    intro i
+    apply IsOpen.exists_msmooth_support_eq_aux
+    exact LocalHomeomorph.preimage_open_of_open_symm _ hs
+  choose g g_supp g_diff hg using A
+  have h'g : ∀ c x, 0 ≤ g c x := fun c x ↦ (hg c (mem_range_self (f := g c) x)).1
+  have h''g : ∀ c x, 0 ≤ f c x * g c (chartAt H c x) :=
+    fun c x ↦ mul_nonneg (f.nonneg c x) (h'g c _)
+  refine ⟨fun x ↦ ∑ᶠ c, f c x * g c (chartAt H c x), ?_, ?_, ?_⟩
+  · refine support_eq_iff.2 ⟨fun x hx ↦ ?_, fun x hx ↦ ?_⟩
+    · apply ne_of_gt
+      have B : ∃ c, 0 < f c x * g c (chartAt H c x) := by
+        obtain ⟨c, hc⟩ : ∃ c, 0 < f c x := f.exists_pos_of_mem (mem_univ x)
+        refine ⟨c, mul_pos hc ?_⟩
+        apply lt_of_le_of_ne (h'g _ _) (Ne.symm _)
+        rw [← mem_support, g_supp, ← mem_preimage, preimage_inter]
+        have Hx : x ∈ tsupport (f c) := subset_tsupport _ (ne_of_gt hc)
+        simp [(chartAt H c).left_inv (hf c Hx), hx, (chartAt H c).map_source (hf c Hx)]
+      apply finsum_pos' (fun c ↦ h''g c x) B
+      apply (f.locallyFinite.point_finite x).subset
+      apply compl_subset_compl.2
+      rintro c (hc : f c x = 0)
+      simpa only [mul_eq_zero] using Or.inl hc
+    · apply finsum_eq_zero_of_forall_eq_zero
+      intro c
+      by_cases Hx : x ∈ tsupport (f c)
+      · suffices g c (chartAt H c x) = 0 by simp only [this, mul_zero]
+        rw [← nmem_support, g_supp, ← mem_preimage, preimage_inter]
+        contrapose! hx
+        simp only [mem_inter_iff, mem_preimage, (chartAt H c).left_inv (hf c Hx)] at hx
+        exact hx.2
+      · have : x ∉ support (f c) := by contrapose! Hx; exact subset_tsupport _ Hx
+        rw [nmem_support] at this
+        simp [this]
+  · apply SmoothPartitionOfUnity.smooth_finsum_smul
+    intro c x hx
+    apply (g_diff c (chartAt H c x)).comp
+    exact contMDiffAt_of_mem_maximalAtlas (SmoothManifoldWithCorners.chart_mem_maximalAtlas I _)
+      (hf c hx)
+  · intro x
+    apply finsum_nonneg (fun c ↦ h''g c x)
+
+/-- Given an open set `s` containing a closed set `t` in a finite-dimensional real manifold, there
+exists a smooth function with support equal to `s`, taking values in `[0,1]`, and equal to `1`
+exactly on `t`. -/
+theorem exists_msmooth_support_eq_eq_one_iff
+    {s t : Set M} (hs : IsOpen s) (ht : IsClosed t) (h : t ⊆ s) :
+    ∃ f : M → ℝ, Smooth I 𝓘(ℝ) f ∧ range f ⊆ Icc 0 1 ∧ support f = s
+      ∧ (∀ x, x ∈ t ↔ f x = 1) := by
+  /- Take `f` with support equal to `s`, and `g` with support equal to `tᶜ`. Then `f / (f + g)`
+  satisfies the conclusion of the theorem. -/
+  rcases hs.exists_msmooth_support_eq I with ⟨f, f_supp, f_diff, f_pos⟩
+  rcases ht.isOpen_compl.exists_msmooth_support_eq I with ⟨g, g_supp, g_diff, g_pos⟩
+  have A : ∀ x, 0 < f x + g x := by
+    intro x
+    by_cases xs : x ∈ support f
+    · have : 0 < f x := lt_of_le_of_ne (f_pos x) (Ne.symm xs)
+      linarith [g_pos x]
+    · have : 0 < g x := by
+        apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
+        rw [← mem_support, g_supp]
+        contrapose! xs
+        simp at xs
+        exact h.trans f_supp.symm.subset xs
+      linarith [f_pos x]
+  refine ⟨fun x ↦ f x / (f x + g x), ?_, ?_, ?_, ?_⟩
+  -- show that `f / (f + g)` is smooth
+  · exact f_diff.div₀ (f_diff.add g_diff) (fun x ↦ ne_of_gt (A x))
+  -- show that the range is included in `[0, 1]`
+  · refine range_subset_iff.2 (fun x ↦ ⟨div_nonneg (f_pos x) (A x).le, ?_⟩)
+    apply div_le_one_of_le _ (A x).le
+    simpa only [le_add_iff_nonneg_right] using g_pos x
+  -- show that the support is `s`
+  · have B : support (fun x ↦ f x + g x) = univ := eq_univ_of_forall (fun x ↦ (A x).ne')
+    simp only [support_div, f_supp, B, inter_univ]
+  -- show that the function equals one exactly on `t`
+  · intro x
+    simp [div_eq_one_iff_eq (A x).ne', self_eq_add_right, ← nmem_support, g_supp]
+
+/-- Given two disjoint closed sets `s, t` in a Hausdorff σ-compact finite dimensional manifold,
+there exists an infinitely smooth function that is equal to `0` exactly on `s` and to `1`
+exactly on `t`. See also `exists_smooth_zero_one_of_closed` for a slightly weaker version. -/
+theorem exists_msmooth_zero_iff_one_iff_of_closed {s t : Set M}
+    (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
+    ∃ f : M → ℝ, Smooth I 𝓘(ℝ) f ∧ range f ⊆ Icc 0 1 ∧ (∀ x, x ∈ s ↔ f x = 0)
+      ∧ (∀ x, x ∈ t ↔ f x = 1) := by
+  rcases exists_msmooth_support_eq_eq_one_iff I hs.isOpen_compl ht hd.subset_compl_left with
+    ⟨f, f_diff, f_range, fs, ft⟩
+  refine ⟨f, f_diff, f_range, ?_, ft⟩
+  simp [← nmem_support, fs]