compCLM_apply — Mathlib

English

Let g be a function with temperate growth and a suitable upper bound; for any Schwartz map f : E → F, the composition operator on Schwartz space acts by precomposition: compCLM 𝕜 g f = f ∘ g.

Русский

Пусть g обладает темпериранным ростом и удовлетворяет нужному ограничению роста; для любой Schwartz‑графики f: E → F композиционная операция на пространстве Шварца действует как предобразование: compCLM 𝕜 g f = f ∘ g.

LaTeX

$$$compCLM_{\mathbb{k}}(g)\, f = f \circ g$$$

Lean4

@[simp]
theorem compCLM_apply {g : D → E} (hg : g.HasTemperateGrowth)
    (hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ x, ‖x‖ ≤ C * (1 + ‖g x‖) ^ k) (f : 𝓢(E, F)) : compCLM 𝕜 hg hg_upper f = f ∘ g :=
  rfl

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