English
Schwartz maps form a zero-at-infinity continuous map class, i.e., they vanish at infinity in a controlled manner.
Русский
Картa Шварца образует класс отображений, исчезающих в бесконечности, с контролируемым поведением.
LaTeX
$$$$ \\text{ZeroAtInftyContinuousMapClass } 𝓢(E,F). $$$$
Lean4
instance instZeroAtInftyContinuousMapClass : ZeroAtInftyContinuousMapClass 𝓢(E, F) E F
where
__ := instContinuousMapClass
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 (apply_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]
