English
There exists a continuous function with compact support which lies between 0 and 1 everywhere and is 1 on a given closed region and 0 on another region, as per Urysohns lemma variations.
Русский
Существуют непрерывные функции с компактной поддержкой, между 0 и 1, достигающие 1 на одной области и 0 на другой, согласно вариациям леммы Урьсёна.
LaTeX
$$$\exists f \in C(X, \mathbb{R}), HasCompactSupport f, \forall x\; f(x) \in Icc(0,1)$$$
Lean4
/-- 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 [g, 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 [g, 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 (S x).tsum_lt_tsum (i := n) (fun i ↦ I i x) (by simp [fnx, u_pos n]) 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 (S x).tsum_le_tsum (fun n ↦ I n x) u_sum
