-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
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

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w

Tactic:
have h5 : Integrable B μ := by simpa only [← mul_assoc] using hf'.const_mul (2 * π * ‖L‖)

Result:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
h5 : Integrable B μ
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w

Tactic:
let F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-L v w') • fourierSMulRight L f v

Result:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w

Tactic:
let B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖

Result:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w

Tactic:
let F : W → V → E := fun w' v ↦ 𝐞 (-L v w') • f v

Result:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
⊢ Continuous fun v => -(L v) w

Tactic:
fun_prop

Result:
no goals