Theorems · Theorem · functional analysis

SchwartzMap.seminorm_le_bound

∀ (𝕜 : Type u_2) {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap E F) {M : ℝ},
  0 ≤ M → (∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M) → (SchwartzMap.seminorm 𝕜 k n) f ≤ M

If one controls the seminorm for every x, then one controls the seminorm.

Defined in

Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Cited by

2 results in Mathlib

Foundations

Depth 218 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedFieldNormedSpaceSMulCommClass