Theorems · Theorem · functional analysis

SchwartzMap.seminorm_apply

∀ (𝕜 : 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),
  (SchwartzMap.seminorm 𝕜 k n) f = sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}

The seminorm is given by infimum over all c such that the estimate ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ c holds. Note that it is usually better to use seminorm_le_bound or le_seminorm instead of this lemma.

Defined in

Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedFieldNormedSpaceSMulCommClass