feat(Analysis/Distribution/SchwartzMap): projection to ZeroAtInfty and corresponding type class (#9987)

Adds a characterization of ZeroAtInfty in terms of norms and uses one direction to show that every Schwartz function is zero at infinity.
We also add a few lemmas that characterize elements of the `cocompact` filter in terms of norm estimates.

Author: mcdoll

Mathlib.lean

@@ -811,6 +811,7 @@ import Mathlib.Analysis.Normed.Group.SemiNormedGroupCat.Completion
 import Mathlib.Analysis.Normed.Group.SemiNormedGroupCat.Kernels
 import Mathlib.Analysis.Normed.Group.Seminorm
 import Mathlib.Analysis.Normed.Group.Tannery
+import Mathlib.Analysis.Normed.Group.ZeroAtInfty
 import Mathlib.Analysis.Normed.MulAction
 import Mathlib.Analysis.Normed.Order.Basic
 import Mathlib.Analysis.Normed.Order.Lattice

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -9,7 +9,7 @@ import Mathlib.Analysis.Calculus.ContDiff.Bounds
 import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
 import Mathlib.Analysis.LocallyConvex.WithSeminorms
 import Mathlib.Topology.Algebra.UniformFilterBasis
-import Mathlib.Topology.ContinuousFunction.Bounded
+import Mathlib.Analysis.Normed.Group.ZeroAtInfty
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 #align_import analysis.schwartz_space from "leanprover-community/mathlib"@"e137999b2c6f2be388f4cd3bbf8523de1910cd2b"
@@ -119,6 +119,9 @@ protected theorem continuous (f : 𝓢(E, F)) : Continuous f :=
   (f.smooth 0).continuous
 #align schwartz_map.continuous SchwartzMap.continuous
 
+instance instContinuousMapClass : ContinuousMapClass 𝓢(E, F) E F where
+  map_continuous := SchwartzMap.continuous
+
 /-- Every Schwartz function is differentiable. -/
 protected theorem differentiable (f : 𝓢(E, F)) : Differentiable ℝ f :=
   (f.smooth 1).differentiable rfl.le
@@ -976,6 +979,11 @@ section BoundedContinuousFunction
 
 open scoped BoundedContinuousFunction
 
+instance instBoundedContinuousMapClass : BoundedContinuousMapClass 𝓢(E, F) E F :=
+  { instContinuousMapClass with
+    map_bounded := fun f ↦ ⟨2 * (SchwartzMap.seminorm ℝ 0 0) f,
+      (BoundedContinuousFunction.dist_le_two_norm' (norm_le_seminorm ℝ f))⟩ }
+
 /-- Schwartz functions as bounded continuous functions -/
 def toBoundedContinuousFunction (f : 𝓢(E, F)) : E →ᵇ F :=
   BoundedContinuousFunction.ofNormedAddCommGroup f (SchwartzMap.continuous f)
@@ -1024,8 +1032,7 @@ def toBoundedContinuousFunctionCLM : 𝓢(E, F) →L[𝕜] E →ᵇ F :=
       simp only [Seminorm.comp_apply, coe_normSeminorm, Finset.sup_singleton,
         schwartzSeminormFamily_apply_zero, Seminorm.smul_apply, one_smul, ge_iff_le,
         BoundedContinuousFunction.norm_le (map_nonneg _ _)]
-      intro x
-      exact norm_le_seminorm 𝕜 _ _ }
+      exact norm_le_seminorm 𝕜 _ }
 #align schwartz_map.to_bounded_continuous_function_clm SchwartzMap.toBoundedContinuousFunctionCLM
 
 @[simp]
@@ -1048,4 +1055,75 @@ theorem delta_apply (x₀ : E) (f : 𝓢(E, F)) : delta 𝕜 F x₀ f = f x₀ :
 
 end BoundedContinuousFunction
 
+section ZeroAtInfty
+
+open scoped ZeroAtInfty
+
+variable [ProperSpace E]
+
+instance instZeroAtInftyContinuousMapClass : ZeroAtInftyContinuousMapClass 𝓢(E, F) E F :=
+  { instContinuousMapClass with
+    zero_at_infty := by
+      intro f
+      apply zero_at_infty_of_norm_le
+      intro ε hε
+      use (SchwartzMap.seminorm ℝ 1 0) f / ε
+      intro x hx
+      rw [div_lt_iff hε] at hx
+      have hxpos : 0 < ‖x‖ := by
+        rw [norm_pos_iff']
+        intro hxzero
+        simp only [hxzero, norm_zero, zero_mul, ← not_le] at hx
+        exact hx (map_nonneg (SchwartzMap.seminorm ℝ 1 0) f)
+      have := norm_pow_mul_le_seminorm ℝ f 1 x
+      rw [pow_one, ← le_div_iff' hxpos] at this
+      apply lt_of_le_of_lt this
+      rwa [div_lt_iff' hxpos] }
+
+/-- Schwartz functions as continuous functions vanishing at infinity. -/
+def toZeroAtInfty (f : 𝓢(E, F)) : C₀(E, F) where
+  toFun := f
+  zero_at_infty' := zero_at_infty f
+
+@[simp] theorem toZeroAtInfty_apply (f : 𝓢(E, F)) (x : E) : f.toZeroAtInfty x = f x :=
+  rfl
+
+@[simp] theorem toZeroAtInfty_toBCF (f : 𝓢(E, F)) :
+    f.toZeroAtInfty.toBCF = f.toBoundedContinuousFunction := by
+  ext; rfl
+
+variable (𝕜 E F)
+variable [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
+
+/-- The inclusion map from Schwartz functions to continuous functions vanishing at infinity as a
+linear map. -/
+def toZeroAtInftyLM : 𝓢(E, F) →ₗ[𝕜] C₀(E, F) where
+  toFun f := f.toZeroAtInfty
+  map_add' f g := by ext; exact add_apply
+  map_smul' a f := by ext; exact smul_apply
+
+@[simp] theorem toZeroAtInftyLM_apply (f : 𝓢(E, F)) (x : E) : toZeroAtInftyLM 𝕜 E F f x = f x :=
+  rfl
+
+/-- The inclusion map from Schwartz functions to continuous functions vanishing at infinity as a
+continuous linear map. -/
+def toZeroAtInftyCLM : 𝓢(E, F) →L[𝕜] C₀(E, F) :=
+  { toZeroAtInftyLM 𝕜 E F with
+    cont := by
+      change Continuous (toZeroAtInftyLM 𝕜 E F)
+      refine'
+        Seminorm.continuous_from_bounded (schwartz_withSeminorms 𝕜 E F)
+          (norm_withSeminorms 𝕜 (C₀(E, F))) _ fun _ => ⟨{0}, 1, fun f => _⟩
+      haveI : MulAction NNReal (Seminorm 𝕜 𝓢(E, F)) := Seminorm.instDistribMulAction.toMulAction
+      simp only [Seminorm.comp_apply, coe_normSeminorm, Finset.sup_singleton,
+        schwartzSeminormFamily_apply_zero, Seminorm.smul_apply, one_smul, ge_iff_le,
+        ← ZeroAtInftyContinuousMap.norm_toBCF_eq_norm,
+        BoundedContinuousFunction.norm_le (map_nonneg _ _)]
+      exact norm_le_seminorm 𝕜 _ }
+
+@[simp] theorem toZeroAtInftyCLM_apply (f : 𝓢(E, F)) (x : E) : toZeroAtInftyCLM 𝕜 E F f x = f x :=
+  rfl
+
+end ZeroAtInfty
+
 end SchwartzMap

Mathlib/Analysis/Normed/Group/ZeroAtInfty.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2024 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
+
+import Mathlib.Topology.ContinuousFunction.ZeroAtInfty
+
+/-!
+# ZeroAtInftyContinuousMapClass in normed additive groups
+
+In this file we give a characterization of the predicate `zero_at_infty` from
+`ZeroAtInftyContinuousMapClass`. A continuous map `f` is zero at infinity if and only if
+for every `ε > 0` there exists a `r : ℝ` such that for all `x : E` with `r < ‖x‖` it holds that
+`‖f x‖ < ε`.
+-/
+
+open Topology Filter
+
+variable {E F 𝓕 : Type*}
+variable [SeminormedAddGroup E] [SeminormedAddCommGroup F]
+variable [FunLike 𝓕 E F] [ZeroAtInftyContinuousMapClass 𝓕 E F]
+
+theorem ZeroAtInftyContinuousMapClass.norm_le (f : 𝓕) (ε : ℝ) (hε : 0 < ε) :
+    ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε := by
+  have h := zero_at_infty f
+  rw [tendsto_zero_iff_norm_tendsto_zero, tendsto_def] at h
+  specialize h (Metric.ball 0 ε) (Metric.ball_mem_nhds 0 hε)
+  rcases Metric.closedBall_compl_subset_of_mem_cocompact h 0 with ⟨r, hr⟩
+  use r
+  intro x hr'
+  suffices x ∈ (fun x ↦ ‖f x‖) ⁻¹' Metric.ball 0 ε by aesop
+  apply hr
+  aesop
+
+variable [ProperSpace E]
+
+theorem zero_at_infty_of_norm_le (f : E → F)
+    (h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε) :
+    Tendsto f (cocompact E) (𝓝 0) := by
+  rw [tendsto_zero_iff_norm_tendsto_zero]
+  intro s hs
+  rw [mem_map, Metric.mem_cocompact_iff_closedBall_compl_subset 0]
+  rw [Metric.mem_nhds_iff] at hs
+  rcases hs with ⟨ε, hε, hs⟩
+  rcases h ε hε with ⟨r, hr⟩
+  use r
+  intro
+  aesop

Mathlib/Topology/MetricSpace/Bounded.lean

@@ -172,6 +172,31 @@ theorem cobounded_le_cocompact : cobounded α ≤ cocompact α :=
 #align comap_dist_right_at_top_le_cocompact Metric.cobounded_le_cocompactₓ
 #align comap_dist_left_at_top_le_cocompact Metric.cobounded_le_cocompactₓ
 
+theorem isCobounded_iff_closedBall_compl_subset {s : Set α} (c : α) :
+    IsCobounded s ↔ ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s := by
+  rw [← isBounded_compl_iff, isBounded_iff_subset_closedBall c]
+  apply exists_congr
+  intro r
+  rw [compl_subset_comm]
+
+theorem _root_.Bornology.IsCobounded.closedBall_compl_subset {s : Set α} (hs : IsCobounded s)
+    (c : α) : ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s :=
+  (isCobounded_iff_closedBall_compl_subset c).mp hs
+
+theorem closedBall_compl_subset_of_mem_cocompact {s : Set α} (hs : s ∈ cocompact α) (c : α) :
+    ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s :=
+  IsCobounded.closedBall_compl_subset (cobounded_le_cocompact hs) c
+
+theorem mem_cocompact_of_closedBall_compl_subset [ProperSpace α] (c : α)
+    (h : ∃ r, (closedBall c r)ᶜ ⊆ s) : s ∈ cocompact α := by
+  rcases h with ⟨r, h⟩
+  rw [Filter.mem_cocompact]
+  exact ⟨closedBall c r, isCompact_closedBall c r, h⟩
+
+theorem mem_cocompact_iff_closedBall_compl_subset [ProperSpace α] (c : α) :
+    s ∈ cocompact α ↔ ∃ r, (closedBall c r)ᶜ ⊆ s :=
+  ⟨(closedBall_compl_subset_of_mem_cocompact · _), mem_cocompact_of_closedBall_compl_subset _⟩
+
 /-- Characterization of the boundedness of the range of a function -/
 theorem isBounded_range_iff {f : β → α} : IsBounded (range f) ↔ ∃ C, ∀ x y, dist (f x) (f y) ≤ C :=
   isBounded_iff.trans <| by simp only [forall_range_iff]