Theorems · Theorem · functional analysis

SchwartzMap.fourier_evalCLM_eq

∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] (𝕜' : Type u_4) [inst_5 : NormedField 𝕜'] {F : Type u_5}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F] {G : Type u_6} [inst_8 : NormedAddCommGroup G]
  [inst_9 : NormedSpace ℂ G] [inst_10 : NormedSpace 𝕜' G] [inst_11 : SMulCommClass ℝ 𝕜' G]
  (f : SchwartzMap V (F →L[ℝ] G)) (m : F),
  FourierTransform.fourier ((SchwartzMap.evalCLM 𝕜' V G m) f) =
    (SchwartzMap.evalCLM 𝕜' V G m) (FourierTransform.fourier f)

Defined in

Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpaceNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedSpaceSMulCommClass