instSMul — Mathlib

English

Scaling a Schwartz map by a scalar c scales its seminormAux by at most |c|.

Русский

Умножение SchwartzMap на скаляр c не увеличивает seminormAux более чем пропорционально |c|.

LaTeX

$$$ (c \\cdot f).seminormAux_{k,n} \\le |c| \\cdot f.seminormAux_{k,n} $$$

Lean4

instance instSMul : SMul 𝕜 𝓢(E, F) :=
  ⟨fun c f =>
    { toFun := c • (f : E → F)
      smooth' := (f.smooth _).const_smul c
      decay' k
        n :=
        .intro (f.seminormAux k n * ‖c‖) fun x ↦
          calc
            ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ * ‖c‖ :=
              by
              rw [mul_comm _ ‖c‖, ← mul_assoc]
              exact decay_smul_aux k n f c x
            _ ≤ SchwartzMap.seminormAux k n f * ‖c‖ := by
              gcongr
              apply f.le_seminormAux }⟩

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