Theorems · Theorem · harmonic analysis

Real.pow_mul_norm_iteratedFDeriv_fourier_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {f : V → E} {K N : ℕ∞},
  ContDiff ℝ (↑N) f →
    (∀ (k n : ℕ),
        ↑k ≤ K → ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) MeasureTheory.volume) →
      ∀ {k n : ℕ},
        ↑k ≤ K →
          ↑n ≤ N →
            ∀ (w : V),
              ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (FourierTransform.fourier f) w‖ ≤
                (2 * Real.pi) ^ k * (2 * ↑k + 2) ^ n *
                  ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

One can bound ‖w‖^n * ‖D^k (𝓕 f) w‖ in terms of integrals of the derivatives of f (or order at most n) multiplied by powers of v (of order at most k).

Defined in

Mathlib.Analysis.Fourier.FourierTransformDeriv

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpace