Compactly supported functions

Stream: Is there code for X?

[Yoh Tanimoto]

I am trying to show that for any f in C₀(X, ℝ) there is a sequence gn with compact support such that gn tends to f. In doing this, I noticed that the norm of C₀(X, ℝ) is defined through BoundedContinuousFunction. On the other hand, to construct gn, I need to multiply with a compactly supported function by Urysohn's lemma and the result is in C₀(X, ℝ), which is an extension of C(X, ℝ) but not of BCF. Is there any nice way to do this?

[Jireh Loreaux]

Do we not have a constructor from compactly supported functions to C_0? Also, an #mwe would help.

[Jireh Loreaux]

Doesn't seem like it, but I didn't check carefully. I think the thing to do is to add this constructor.

[Yoh Tanimoto]

thanks for your reply!

import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.UrysohnsLemma
import Mathlib.Topology.ContinuousFunction.ZeroAtInfty
open ZeroAtInfty Filter Urysohns

variable {X : Type*} [TopologicalSpace X] [LocallyCompactSpace X]
 [T2Space X]

example (f : C₀(X, ℂ))
 : ∃ (g : ℕ → C₀(X ,ℂ)), ∀ (n : ℕ), HasCompactSupport (g n) ∧ Filter.Tendsto g Filter.atTop (nhds f) := by
 have h : ∀ (n : ℕ), ∃ (gn : C₀(X, ℂ)), HasCompactSupport gn ∧ ‖f - gn‖ ≤ 1/((n : ℝ)+1) := by
  intro n
  have h1 : ∃ (gn : C₀(X, ℂ)), HasCompactSupport gn ∧ ∀ (x : X), ‖(f - gn) x‖ < 1 / (↑n + 1) := by
   sorry -- by Urysohn
  have h21 : 0 < 1 / ((n : ℝ)+1) := by
   exact Nat.one_div_pos_of_nat
  obtain ⟨gn, hgn⟩ := h1
  use gn
  constructor
  exact hgn.left
  apply (BoundedContinuousFunction.norm_le (le_of_lt h21)).mpr hgn.right

I was hoping that this would work. Instead, the error message seems to say that f - gn is C₀(X, ℝ), while the norm is defined for BoundedContinuousFunction.

[Matt Diamond]

@Yoh Tanimoto are you referring to the error on the last line?

[Matt Diamond]

I think the problem is that you're passing in a proof of a < relation, but norm_le (as the name suggests) requires a ≤ relation

[Matt Diamond]

the error message is definitely unhelpful... technically it tells you the problem but it's so verbose that it's difficult to spot the actual issue

[Yoh Tanimoto]

ah! I thought it was a problem of the type of f - gn... Thank you!

[Matt Diamond]

no problem!

[Matt Diamond]

FYI, if you're curious, I believe the reason this works is that we have an instance that enables the coercion from C₀(_, _) to BCF: docs#ZeroAtInftyContinuousMap.instBoundedContinuousMapClass

I think this might've been what you were asking about in your original message

[Yoh Tanimoto]

ah yes, I didn't understand that it meant that there was the coercion. great!