English
The derivative of the Fourier integral with respect to the spatial variable is given by the Fourier transform of the negated bilinear action, i.e., the derivative equals the Fourier transform of fourierSMulRight L f with a minus flip.
Русский
Производная по пространственной переменной Фурье-интеграла равна Фурье-преобразованию преобразования fourierSMulRight с отрицательным L.flip.
LaTeX
$$$\\text{fderiv} \\;\\text{(fourierIntegral)} = \\text{fourierIntegral}( \\text{fourierSMulRight } ( -L.flip ) f)$$$
Lean4
/-- Main theorem of this section: if both `f` and `x ↦ ‖x‖ * ‖f x‖` are integrable, then the
Fourier transform of `f` has a Fréchet derivative (everywhere in its domain) and its derivative is
the Fourier transform of `smulRight L f`. -/
theorem hasFDerivAt_fourierIntegral [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] {μ : Measure V}
(hf : Integrable f μ) (hf' : Integrable (fun v : V ↦ ‖v‖ * ‖f v‖) μ) (w : W) :
HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w)
w :=
by
let F : W → V → E := fun w' v ↦ 𝐞 (-L v w') • f v
let F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-L v w') • fourierSMulRight L f v
let B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
have h0 (w' : W) : Integrable (F w') μ :=
(fourierIntegral_convergent_iff continuous_fourierChar
(by apply L.continuous₂ : Continuous (fun p : V × W ↦ L.toLinearMap₁₂ p.1 p.2)) w').2
hf
have h1 : ∀ᶠ w' in 𝓝 w, AEStronglyMeasurable (F w') μ := Eventually.of_forall (fun w' ↦ (h0 w').aestronglyMeasurable)
have h3 : AEStronglyMeasurable (F' w) μ :=
by
refine .smul ?_ hf.1.fourierSMulRight
refine (continuous_fourierChar.comp ?_).aestronglyMeasurable
fun_prop
have h4 : (∀ᵐ v ∂μ, ∀ (w' : W), w' ∈ Metric.ball w 1 → ‖F' w' v‖ ≤ B v) :=
by
filter_upwards with v w' _
rw [Circle.norm_smul _ (fourierSMulRight L f v)]
exact norm_fourierSMulRight_le L f v
have h5 : Integrable B μ := by simpa only [← mul_assoc] using hf'.const_mul (2 * π * ‖L‖)
have h6 : ∀ᵐ v ∂μ, ∀ w', w' ∈ Metric.ball w 1 → HasFDerivAt (fun x ↦ F x v) (F' w' v) w' :=
ae_of_all _ (fun v w' _ ↦ hasFDerivAt_fourierChar_smul L f v w')
exact hasFDerivAt_integral_of_dominated_of_fderiv_le one_pos h1 (h0 w) h3 h4 h5 h6
