Prove2Me

`BookProof.StrichartzWave.fourier_multiplierOp_apply` {m : V β†’ ℝ} (hm : Function.HasTemperateGrowth m) (f : 𝓒(V, β„‚)) (x : V) : (𝓕 (multiplierOp m f) : 𝓒(V, β„‚)) x = ((m x : ℝ) : β„‚)

Proved
BookProof.StrichartzWave.fourier_multiplierOp_apply

by leonardopedro Β· Oct 10, 2026 Β· Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterWaveUnboundedPotential.

BookProof.StrichartzWave.fourier_multiplierOp_apply {m : V β†’ ℝ} (hm : Function.HasTemperateGrowth m) (f : 𝓒(V, β„‚)) (x : V) : (𝓕 (multiplierOp m f) : 𝓒(V, β„‚)) x = ((m x : ℝ) : β„‚) * (𝓕 f : 𝓒(V, β„‚)) x

Formalization note: Lean 4 identifier BookProof.StrichartzWave.fourier_multiplierOp_apply.

Preamble
-- Generated from ChapterWaveUnboundedPotential.lean β€” theorem BookProof.StrichartzWave.fourier_multiplierOp_apply
import Mathlib
import Definitions.Def_ChapterWaveUnboundedPotential
import Definitions.Def_ChapterStrichartzWave
open BookProof.StrichartzWave



open MeasureTheory SchwartzMap FourierTransform ComplexInnerProductSpace ENNReal

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
Formal statement
theorem BookProof.StrichartzWave.fourier_multiplierOp_apply {m : V β†’ ℝ} (hm : Function.HasTemperateGrowth m)
    (f : 𝓒(V, β„‚)) (x : V) :
    (𝓕 (multiplierOp m f) : 𝓒(V, β„‚)) x = ((m x : ℝ) : β„‚) * (𝓕 f : 𝓒(V, β„‚)) x := by sorry

View graph