Theorems · Theorem · harmonic analysis

VectorFourier.fourierIntegral_continuousLinearMap_apply

∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {V : Type u_5} {W : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : MeasurableSpace V] [BorelSpace V]
  [inst_5 : NormedAddCommGroup W] [inst_6 : NormedSpace 𝕜 W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V}
  {L : V →L[𝕜] W →L[𝕜] 𝕜} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ℝ F] [inst_9 : NormedAddCommGroup E]
  [inst_10 : NormedSpace ℂ E] {f : V → F →L[ℝ] E} {a : F} {w : W},
  Continuous ⇑e →
    MeasureTheory.Integrable f μ →
      (VectorFourier.fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) f w) a =
        VectorFourier.fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x => (f x) a) w

Defined in

Mathlib.Analysis.Fourier.FourierTransform

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace