Theorem: SchwartzMap.Real.contDiff_fourierIntegral (ForML/SchwartzRealFourier.lean)

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ∞
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ n fun ξ => 𝓕 (fun x => f x) ξ
Tactic:
induction n using ENat.nat_induction generalizing f with
| h0 => simpa [contDiff_zero] using continuous_fourierIntegral f
| hsuc n IH =>
  rw [contDiff_succ_iff_deriv]
  refine And.intro (differentiable_fourierIntegral f) ?_
  conv => arg 3; intro ξ
  simp only [deriv_fourierIntegral]
  refine ContDiff.neg ?_
  refine ContDiff.const_smul _ ?_
  simp only [← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_id')]
  exact IH _
| htop IH => exact contDiff_top.mpr fun n ↦ IH n f
State after:
no goals

State before:
case h0
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ 0 fun ξ => 𝓕 (fun x => f x) ξ
Tactic:
simpa [contDiff_zero] using continuous_fourierIntegral f
State after:
no goals

State before:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑(Nat.succ n) fun ξ => 𝓕 (fun x => f x) ξ
Tactic:
rw [contDiff_succ_iff_deriv]
State after:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ (Differentiable ℝ fun ξ => 𝓕 (fun x => f x) ξ) ∧ ContDiff ℝ (↑n) (deriv fun ξ => 𝓕 (fun x => f x) ξ)

State before:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ (Differentiable ℝ fun ξ => 𝓕 (fun x => f x) ξ) ∧ ContDiff ℝ (↑n) (deriv fun ξ => 𝓕 (fun x => f x) ξ)
Tactic:
refine And.intro (differentiable_fourierIntegral f) ?_
State after:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ (↑n) (deriv fun ξ => 𝓕 (fun x => f x) ξ)

State before:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ (↑n) (deriv fun ξ => 𝓕 (fun x => f x) ξ)
Tactic:
conv => arg 3; intro ξ
State after:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => deriv (fun ξ => 𝓕 (fun x => f x) ξ) ξ

State before:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => deriv (fun ξ => 𝓕 (fun x => f x) ξ) ξ
Tactic:
simp only [deriv_fourierIntegral]
State after:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => -((2 * ↑π * I) • 𝓕 (fun x => x • f x) ξ)

State before:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => -((2 * ↑π * I) • 𝓕 (fun x => x • f x) ξ)
Tactic:
refine ContDiff.neg ?_
State after:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => (2 * ↑π * I) • 𝓕 (fun x => x • f x) ξ

State before:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => (2 * ↑π * I) • 𝓕 (fun x => x • f x) ξ
Tactic:
refine ContDiff.const_smul _ ?_
State after:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => x • f x) ξ

State before:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => x • f x) ξ
Tactic:
simp only [← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_id')]
State after:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x)) f) x) ξ

State before:
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x)) f) x) ξ
Tactic:
exact IH _
State after:
no goals

State before:
case htop
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
IH : ∀ (n : ℕ) (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ⊤ fun ξ => 𝓕 (fun x => f x) ξ
Tactic:
exact contDiff_top.mpr fun n ↦ IH n f
State after:
no goals