English
A specialized HasFDerivAt result for FourierIntegral with the derivative expressed via fourierSMulRight of the original integral.
Русский
Особый результат HasFDerivAt для FourierIntegral, где производная выражается через fourierSMulRight от исходного интеграла.
LaTeX
$$$\\text{HasFDerivAt}\\left( \\text{fourierIntegral}(...),\\; \\text{fourierIntegral}( ... (\\text{fourierSMulRight } L f) )\\right)$$$
Lean4
theorem _root_.MeasureTheory.AEStronglyMeasurable.fourierSMulRight [SecondCountableTopologyEither V (W →L[ℝ] ℝ)]
[MeasurableSpace V] [BorelSpace V] {L : V →L[ℝ] W →L[ℝ] ℝ} {f : V → E} {μ : Measure V}
(hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun v ↦ fourierSMulRight L f v) μ :=
by
apply AEStronglyMeasurable.const_smul'
have aux0 : Continuous fun p : (W →L[ℝ] ℝ) × E ↦ p.1.smulRight p.2 :=
(ContinuousLinearMap.smulRightL ℝ W E).continuous₂
have aux1 : AEStronglyMeasurable (fun v ↦ (L v, f v)) μ := L.continuous.aestronglyMeasurable.prodMk hf
exact (aux0.comp_aestronglyMeasurable aux1 :)
