Theorems · Theorem · functional analysis

SchwartzMap.integral_pow_mul_iteratedFDeriv_le

∀ (𝕜 : Type u_2) {D : Type u_4} {V : Type u_9} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace ℝ D] [inst_3 : NormedAddCommGroup V] [inst_4 : NormedSpace ℝ V] [inst_5 : NormedSpace 𝕜 V]
  [inst_6 : MeasurableSpace D] (μ : MeasureTheory.Measure D) [hμ : μ.HasTemperateGrowth] (f : SchwartzMap D V)
  (k n : ℕ),
  ∫ (x : D), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ∂μ ≤
    (2 ^ μ.integrablePower * ∫ (x : D), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) *
      ((SchwartzMap.seminorm 𝕜 0 n) f + (SchwartzMap.seminorm 𝕜 (k + μ.integrablePower) n) f)

Defined in

Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedSpaceMeasurableSpaceMeasureTheory.Measure.HasTemperateGrowth