Theorems · Definition · functional analysis

ContDiffMapSupportedIn.seminorm

(𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    (n : ℕ∞) → (K : TopologicalSpace.Compacts E) → ℕ → Seminorm 𝕜 (ContDiffMapSupportedIn E F n K)

The seminorms on the space 𝓓^{n}_{K}(E, F) given by the sup norm of the iterated derivatives. In the scope Distributions.Seminorm, we denote them by N[𝕜; F]_{K, n, i} (or N[𝕜]_{K, n, i}), or simply by N[𝕜; F]_{K, i} (or N[𝕜; F]_{K, i}) when n = ∞.

Defined in

Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Cited by

15 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedSpaceSMulCommClass