feat: a compact Gdelta set is a level set of a compactly supported fu…

…nction (#10101)

Mathlib/Topology/GDelta.lean

@@ -96,6 +96,8 @@ lemma isGδ_iff_eq_iInter_nat {s : Set X} :
   · rintro ⟨f, hf, rfl⟩
     apply isGδ_iInter_of_isOpen hf
 
+alias ⟨IsGδ.eq_iInter_nat, _⟩ := isGδ_iff_eq_iInter_nat
+
 /-- The intersection of an encodable family of Gδ sets is a Gδ set. -/
 theorem isGδ_iInter [Countable ι'] {s : ι' → Set X} (hs : ∀ i, IsGδ (s i)) : IsGδ (⋂ i, s i) := by
   choose T hTo hTc hTs using hs

Mathlib/Topology/UrysohnsLemma.lean

@@ -6,7 +6,9 @@ Authors: Yury G. Kudryashov
 import Mathlib.Analysis.NormedSpace.AddTorsor
 import Mathlib.LinearAlgebra.AffineSpace.Ordered
 import Mathlib.Topology.ContinuousFunction.Basic
-import Mathlib.Algebra.Order.Support
+import Mathlib.Topology.GDelta
+import Mathlib.Analysis.NormedSpace.FunctionSeries
+import Mathlib.Analysis.SpecificLimits.Basic
 
 #align_import topology.urysohns_lemma from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 
@@ -398,3 +400,68 @@ theorem exists_continuous_one_zero_of_isCompact [RegularSpace X] [LocallyCompact
     exact interior_subset hx
   · have : 0 ≤ f x ∧ f x ≤ 1 := by simpa using h'f x
     simp [this]
+
+/-- Urysohn's lemma: if `s` and `t` are two disjoint sets in a regular locally compact topological
+space `X`, with `s` compact and `t` closed, then there exists a continuous compactly supported
+function `f : X → ℝ` such that
+
+* `f` equals one on `s`;
+* `f` equals zero on `t`;
+* `0 ≤ f x ≤ 1` for all `x`.
+
+Moreover, if `s` is Gδ, one can ensure that `f ⁻¹ {1}` is exactly `s`.
+-/
+theorem exists_continuous_one_zero_of_isCompact_of_isGδ [RegularSpace X] [LocallyCompactSpace X]
+    {s t : Set X} (hs : IsCompact s) (h's : IsGδ s) (ht : IsClosed t) (hd : Disjoint s t) :
+    ∃ f : C(X, ℝ), s = f ⁻¹' {1} ∧ EqOn f 0 t ∧ HasCompactSupport f
+      ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
+  rcases h's.eq_iInter_nat with ⟨U, U_open, hU⟩
+  obtain ⟨m, m_comp, -, sm, mt⟩ : ∃ m, IsCompact m ∧ IsClosed m ∧ s ⊆ interior m ∧ m ⊆ tᶜ :=
+    exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left
+  have A n : ∃ f : C(X, ℝ), EqOn f 1 s ∧ EqOn f 0 (U n ∩ interior m)ᶜ ∧ HasCompactSupport f
+      ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
+    apply exists_continuous_one_zero_of_isCompact hs
+      ((U_open n).inter isOpen_interior).isClosed_compl
+    rw [disjoint_compl_right_iff_subset]
+    exact subset_inter ((hU.subset.trans (iInter_subset U n))) sm
+  choose f fs fm _hf f_range using A
+  obtain ⟨u, u_pos, u_sum, hu⟩ : ∃ (u : ℕ → ℝ), (∀ i, 0 < u i) ∧ Summable u ∧ ∑' i, u i = 1 :=
+    ⟨fun n ↦ 1/2/2^n, fun n ↦ by positivity, summable_geometric_two' 1, tsum_geometric_two' 1⟩
+  let g : X → ℝ := fun x ↦ ∑' n, u n * f n x
+  have hgmc : EqOn g 0 mᶜ := by
+    intro x hx
+    have B n : f n x = 0 := by
+      have : mᶜ ⊆ (U n ∩ interior m)ᶜ := by
+        simpa using (inter_subset_right _ _).trans interior_subset
+      exact fm n (this hx)
+    simp [B]
+  have I n x : u n * f n x ≤ u n := mul_le_of_le_one_right (u_pos n).le (f_range n x).2
+  have S x : Summable (fun n ↦ u n * f n x) := Summable.of_nonneg_of_le
+      (fun n ↦ mul_nonneg (u_pos n).le (f_range n x).1) (fun n ↦ I n x) u_sum
+  refine ⟨⟨g, ?_⟩, ?_, hgmc.mono (subset_compl_comm.mp mt), ?_, fun x ↦ ⟨?_, ?_⟩⟩
+  · apply continuous_tsum (fun n ↦ continuous_const.mul (f n).continuous) u_sum (fun n x ↦ ?_)
+    simpa [abs_of_nonneg, (u_pos n).le, (f_range n x).1] using I n x
+  · apply Subset.antisymm (fun x hx ↦ by simp [fs _ hx, hu]) ?_
+    apply compl_subset_compl.1
+    intro x hx
+    obtain ⟨n, hn⟩ : ∃ n, x ∉ U n := by simpa [hU] using hx
+    have fnx : f n x = 0 := fm _ (by simp [hn])
+    have : g x < 1 := by
+      apply lt_of_lt_of_le ?_ hu.le
+      exact tsum_lt_tsum (i := n) (fun i ↦ I i x) (by simp [fnx, u_pos n]) (S x) u_sum
+    simpa using this.ne
+  · exact HasCompactSupport.of_support_subset_isCompact m_comp
+      (Function.support_subset_iff'.mpr hgmc)
+  · exact tsum_nonneg (fun n ↦ mul_nonneg (u_pos n).le (f_range n x).1)
+  · apply le_trans _ hu.le
+    exact tsum_le_tsum (fun n ↦ I n x) (S x) u_sum
+
+theorem exists_continuous_nonneg_pos [RegularSpace X] [LocallyCompactSpace X] (x : X) :
+    ∃ f : C(X, ℝ), HasCompactSupport f ∧ 0 ≤ (f : X → ℝ) ∧ f x ≠ 0 := by
+  rcases exists_compact_mem_nhds x with ⟨k, hk, k_mem⟩
+  rcases exists_continuous_one_zero_of_isCompact hk isClosed_empty (disjoint_empty k)
+    with ⟨f, fk, -, f_comp, hf⟩
+  refine ⟨f, f_comp, fun x ↦ (hf x).1, ?_⟩
+  have := fk (mem_of_mem_nhds k_mem)
+  simp only [ContinuousMap.coe_mk, Pi.one_apply] at this
+  simp [this]