Theorems · Inductive type · functional analysis

SchwartzMap

(E : Type u_5) →
  (F : Type u_6) →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → Type (max u_5 u_6)

A function is a Schwartz function if it is smooth and all derivatives decay faster than any power of ‖x‖.

Defined in

Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Cited by

251 results in Mathlib

Foundations

Depth 157 from the axioms, rests on 3,649 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace