Theorems · Theorem · harmonic analysis

VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
  {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {K N : ℕ∞},
  ContDiff ℝ (↑N) f →
    (∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ) →
      ∀ {k n : ℕ},
        ↑k ≤ K →
          ↑n ≤ N →
            ∀ (v : V) (w : W),
              |(L v) w| ^ n *
                  ‖iteratedFDeriv ℝ k
                      (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w‖ ≤
                ‖v‖ ^ n * (2 * Real.pi * ‖L‖) ^ 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 the k-th derivative of the Fourier integral of f, multiplied by (L v w) ^ n, in terms of integrals of iterated derivatives of f (of order up to n) multiplied by ‖v‖ ^ i (for i ≤ k).

Defined in

Mathlib.Analysis.Fourier.FourierTransformDeriv

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMeasureTheory.Measure.IsAddHaarMeasure