seminormAux_smul_le — Mathlib

English

The Schwartz space is closed under scalar multiplication by 𝕜, giving a well-defined action by 𝕜 on Schwartz maps.

Русский

Пространство Schwartz замкнуто относительно скалярного умножения на 𝕜, образуя действие 𝕜 на SchwartzMap.

LaTeX

$$$ (c \\cdot f) : E \\to F \\quad \\text{is SchwartzMap when } f \\text{ is}$$$

Lean4

theorem seminormAux_smul_le (k n : ℕ) (c : 𝕜) (f : 𝓢(E, F)) : (c • f).seminormAux k n ≤ ‖c‖ * f.seminormAux k n :=
  by
  refine
    (c • f).seminormAux_le_bound k n (mul_nonneg (norm_nonneg _) (seminormAux_nonneg _ _ _)) fun x =>
      (decay_smul_aux k n f c x).trans_le ?_
  rw [mul_assoc]
  exact mul_le_mul_of_nonneg_left (f.le_seminormAux k n x) (norm_nonneg _)

Похожие утверждения