-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma hasFTaylorSeriesUpTo_fourierIntegral {N : WithTop ℕ∞}
    (hf : ∀ (n : ℕ), n ≤ N → Integrable (fun v ↦ ‖v‖^n * ‖f v‖) μ)
    (h'f : AEStronglyMeasurable f μ) :
    HasFTaylorSeriesUpTo N (fourierIntegral 𝐞 μ L.toLinearMap₂ f)
      (fun w n ↦ fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v ↦ fourierPowSMulRight L f v n) 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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v => fourierPowSMulRight L f v (n + 1)) μ
⊢ Integrable (fun v => fourierSMulRight L (fun v => fourierPowSMulRight L f v n) v) μ

Tactic:
apply (I₂.const_mul ((2 * π * ‖L‖))).mono' (h'f.fourierPowSMulRight L n).fourierSMulRight

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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v => fourierPowSMulRight L f v (n + 1)) μ
⊢ ∀ᵐ (a : V) ∂μ,
    ‖fourierSMulRight L (fun v => fourierPowSMulRight L f v n) a‖ ≤ 2 * π * ‖L‖ * (‖a‖ * ‖fourierPowSMulRight L f a n‖)

Proof state:
case fderiv
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v => fourierPowSMulRight L f v (n + 1)) μ
⊢ HasFDerivAt (fun y => fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n) y)
    (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n.succ) w).curryLeft w

Tactic:
have I₄ : Integrable
    (fun v ↦ fourierSMulRight L (fun v ↦ fourierPowSMulRight L f v n) v) μ := by
  apply (I₂.const_mul ((2 * π * ‖L‖))).mono' (h'f.fourierPowSMulRight L n).fourierSMulRight
  filter_upwards with v
  exact (norm_fourierSMulRight_le _ _ _).trans (le_of_eq (by ring))

Result:
case fderiv
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v => fourierPowSMulRight L f v (n + 1)) μ
I₄ : Integrable (fun v => fourierSMulRight L (fun v => fourierPowSMulRight L f v n) v) μ
⊢ HasFDerivAt (fun y => fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n) y)
    (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n.succ) w).curryLeft w

Proof state:
case fderiv
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v => fourierPowSMulRight L f v (n + 1)) μ
I₄ : Integrable (fun v => fourierSMulRight L (fun v => fourierPowSMulRight L f v n) v) μ
E :
  (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v (n + 1)) w).curryLeft =
    fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L fun v => fourierPowSMulRight L f v n) w
⊢ HasFDerivAt (fun y => fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n) y)
    (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n.succ) w).curryLeft w

Tactic:
exact E ▸ hasFDerivAt_fourierIntegral L I₁ I₂ w

Result:
no goals

Proof state:
case fderiv
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
⊢ HasFDerivAt (fun y => fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n) y)
    (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n.succ) w).curryLeft w

Tactic:
have I₃ : Integrable (fun v ↦ fourierPowSMulRight L f v (n + 1)) μ :=
  integrable_fourierPowSMulRight L (hf (n + 1) (ENat.add_one_natCast_le_withTop_of_lt hn)) h'f

Result:
case fderiv
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v => fourierPowSMulRight L f v (n + 1)) μ
⊢ HasFDerivAt (fun y => fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n) y)
    (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n.succ) w).curryLeft w