Theorem: fourierIntegral_self_add_deriv_deriv (PrimeNumberTheoremAnd/Fourier.lean)

State before:
f : W21
u : ℝ
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Tactic:
have l1 : Integrable (fun x => (((π : ℂ) ^ 2)⁻¹ * 4⁻¹) * deriv (deriv f) x) := by
  apply Integrable.const_mul ; simpa [iteratedDeriv_succ] using f.integrable le_rfl
State after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u

State before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Tactic:
have l4 : Differentiable ℝ f := f.differentiable
State after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u

State before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Tactic:
have l5 : Differentiable ℝ (deriv f) := f.deriv.differentiable
State after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u

State before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Tactic:
simp [f.hf, l1, add_mul, Real.fourierIntegral_deriv f.hf' l5 f.hf'', Real.fourierIntegral_deriv f.hf l4 f.hf']
State after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ 𝓕 f.toFun u + ↑u ^ 2 * 𝓕 f.toFun u =
    𝓕 (fun x => f.toFun x) u - (↑π ^ 2)⁻¹ * 4⁻¹ * (2 * ↑π * I * ↑u * (2 * ↑π * I * ↑u * 𝓕 f.toFun u))

State before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ 𝓕 f.toFun u + ↑u ^ 2 * 𝓕 f.toFun u =
    𝓕 (fun x => f.toFun x) u - (↑π ^ 2)⁻¹ * 4⁻¹ * (2 * ↑π * I * ↑u * (2 * ↑π * I * ↑u * 𝓕 f.toFun u))
Tactic:
field_simp [pi_ne_zero]
State after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ (𝓕 f.toFun u + ↑u ^ 2 * 𝓕 f.toFun u) * (↑π ^ 2 * 4) =
    𝓕 (fun x => f.toFun x) u * (↑π ^ 2 * 4) - 2 * ↑π * I * ↑u * (2 * ↑π * I * ↑u * 𝓕 f.toFun u)

State before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ (𝓕 f.toFun u + ↑u ^ 2 * 𝓕 f.toFun u) * (↑π ^ 2 * 4) =
    𝓕 (fun x => f.toFun x) u * (↑π ^ 2 * 4) - 2 * ↑π * I * ↑u * (2 * ↑π * I * ↑u * 𝓕 f.toFun u)
Tactic:
ring_nf
State after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ 𝓕 f.toFun u * ↑u ^ 2 * ↑π ^ 2 * 4 + 𝓕 f.toFun u * ↑π ^ 2 * 4 =
    -(𝓕 f.toFun u * ↑u ^ 2 * ↑π ^ 2 * I ^ 2 * 4) + 𝓕 (fun x => f.toFun x) u * ↑π ^ 2 * 4

State before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ 𝓕 f.toFun u * ↑u ^ 2 * ↑π ^ 2 * 4 + 𝓕 f.toFun u * ↑π ^ 2 * 4 =
    -(𝓕 f.toFun u * ↑u ^ 2 * ↑π ^ 2 * I ^ 2 * 4) + 𝓕 (fun x => f.toFun x) u * ↑π ^ 2 * 4
Tactic:
simp
State after:
no goals

State before:
f : W21
u : ℝ
⊢ Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
Tactic:
apply Integrable.const_mul
State after:
case h
f : W21
u : ℝ
⊢ Integrable (fun x => deriv (deriv f.toFun) x) volume

State before:
case h
f : W21
u : ℝ
⊢ Integrable (fun x => deriv (deriv f.toFun) x) volume
Tactic:
simpa [iteratedDeriv_succ] using f.integrable le_rfl
State after:
no goals