-- 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:
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 μ
⊢ ∀ (m : ℕ),
    ↑m < N →
      ∀ (x : W),
        HasFDerivAt (fun y => fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v m) y)
          (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v m.succ) x).curryLeft x

Tactic:
intro n hn w

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
⊢ 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:
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)) μ
v : V
⊢ 2 * π * ‖L‖ * ‖v‖ * ‖fourierPowSMulRight L f v n‖ = 2 * π * ‖L‖ * (‖v‖ * ‖fourierPowSMulRight L f v n‖)

Tactic:
ring

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) μ
⊢ 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 ↦ ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ := by
  apply ((hf (n+1) (ENat.add_one_natCast_le_withTop_of_lt hn)).const_mul
      ((2 * π * ‖L‖) ^ n)).mono'
    (continuous_norm.aestronglyMeasurable.mul (h'f.fourierPowSMulRight L n).norm)
  filter_upwards with v
  simp only [Pi.mul_apply, norm_mul, norm_norm]
  calc
  ‖v‖ * ‖fourierPowSMulRight L f v n‖
    ≤ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) := by
      gcongr; apply norm_fourierPowSMulRight_le
  _ = (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖) := by rw [pow_succ]; 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‖) μ
⊢ 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 h.H
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) μ
w' : W
m : Fin n → W
⊢ ((fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v (n + 1)) w).curryLeft w') m =
    ((fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L fun v => fourierPowSMulRight L f v n) w) w') m

Tactic:
rw [curryLeft_apply, fourierIntegral_continuousMultilinearMap_apply' I₃,
  fourierIntegral_continuousLinearMap_apply' I₄,
  fourierIntegral_continuousMultilinearMap_apply' (I₄.apply_continuousLinearMap _)]

Result:
case h.H
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) μ
w' : W
m : Fin n → W
⊢ fourierIntegral 𝐞 μ L.toLinearMap₂ (fun x => (fourierPowSMulRight L f x (n + 1)) (Fin.cons w' m)) w =
    fourierIntegral 𝐞 μ L.toLinearMap₂ (fun x => ((fourierSMulRight L (fun v => fourierPowSMulRight L f v n) x) w') m) w