internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.Real.fourierIntegral_neg
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => -f x) ξ = -𝓕 (fun x => f x) ξ
Tactic:
simpa [Real.fourierIntegral_def] using integral_neg _
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegral_sub
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => f x - g x) ξ = 𝓕 (fun x => f x) ξ - 𝓕 (fun x => g x) ξ
Tactic:
simpa [Real.fourierIntegral_def, smul_sub] using
  integral_sub (integrable_fourierIntegrand f ξ) (integrable_fourierIntegrand g ξ)
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegral_sum
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
ι : Type u_2
s : Finset ι
f : ι → 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => ∑ i in s, (f i) x) ξ = ∑ i in s, 𝓕 (fun x => (f i) x) ξ
Tactic:
simpa [Real.fourierIntegral_def, Finset.smul_sum] using
  integral_finset_sum s fun i _ ↦ Real.integrable_fourierIntegrand (f i) ξ
Proof state after:
no goals
Theorem: SchwartzMap.Real.hasDerivAt_fourierIntegral
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ HasDerivAt (fun ξ => 𝓕 (fun x => f x) ξ) (-((2 * ↑π * I) • 𝓕 (fun x => x • f x) ξ)) ξ
Tactic:
refine .congr_deriv (_root_.hasDerivAt_fourierIntegral f.integrable ?_ ξ) ?_
Proof state after:
case refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ Integrable fun x => x • f x

case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) ξ = -((2 * ↑π * I) • 𝓕 (fun x => x • f x) ξ)
Theorem: SchwartzMap.Real.hasDerivAt_fourierIntegral
Proof state before:
case refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ Integrable fun x => x • f x
Tactic:
exact (hasTemperateGrowth_smul Function.hasTemperateGrowth_id f).integrable
Proof state after:
no goals
Theorem: SchwartzMap.Real.hasDerivAt_fourierIntegral
Proof state before:
case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) ξ = -((2 * ↑π * I) • 𝓕 (fun x => x • f x) ξ)
Tactic:
simp [Real.fourierIntegral_def, integral_neg,
  ← smul_smul (2 * π * I), smul_comm _ (2 * π * I), integral_smul]
Proof state after:
no goals
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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
Proof state after:
no goals
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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
Proof state after:
no goals
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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]
Proof 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) ξ)
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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) ?_
Proof 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) ξ)
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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 ξ
Proof 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) ξ) ξ
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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]
Proof 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) ξ)
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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 ?_
Proof 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) ξ
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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 _ ?_
Proof 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) ξ
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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')]
Proof 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) ξ
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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 _
Proof state after:
no goals
Theorem: SchwartzMap.Real.contDiff_fourierIntegral
Proof 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
Proof state after:
no goals
Theorem: SchwartzMap.Real.iteratedDeriv_fourierIntegral
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
Tactic:
induction n generalizing ξ with
| zero => simp
| succ n IH =>
  rw [iteratedDeriv_succ]
  conv => lhs; arg 1; intro ζ
  simp only [IH, ← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_pow n)]
  rw [deriv_const_smul _ (differentiable_fourierIntegral _ ξ), deriv_fourierIntegral]
  simp [hasTemperateGrowth_smul_apply, pow_succ', smul_smul, mul_comm (_ ^ n)]
Proof state after:
no goals
Theorem: SchwartzMap.Real.iteratedDeriv_fourierIntegral
Proof state before:
case zero
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ iteratedDeriv Nat.zero (fun ξ => 𝓕 (fun x => f x) ξ) ξ =
    (-(2 * ↑π * I)) ^ Nat.zero • 𝓕 (fun x => x ^ Nat.zero • f x) ξ
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.Real.iteratedDeriv_fourierIntegral
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ iteratedDeriv (Nat.succ n) (fun ξ => 𝓕 (fun x => f x) ξ) ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Tactic:
rw [iteratedDeriv_succ]
Proof state after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv (iteratedDeriv n fun ξ => 𝓕 (fun x => f x) ξ) ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Theorem: SchwartzMap.Real.iteratedDeriv_fourierIntegral
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv (iteratedDeriv n fun ξ => 𝓕 (fun x => f x) ξ) ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Tactic:
conv => lhs; arg 1; intro ζ
Proof state after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv (fun ζ => iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ζ) ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Theorem: SchwartzMap.Real.iteratedDeriv_fourierIntegral
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv (fun ζ => iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ζ) ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Tactic:
simp only [IH, ← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_pow n)]
Proof state after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv
      (fun ζ =>
        (-(2 * ↑π * I)) ^ n •
          𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ζ)
      ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Theorem: SchwartzMap.Real.iteratedDeriv_fourierIntegral
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv
      (fun ζ =>
        (-(2 * ↑π * I)) ^ n •
          𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ζ)
      ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Tactic:
rw [deriv_const_smul _ (differentiable_fourierIntegral _ ξ), deriv_fourierIntegral]
Proof state after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ (-(2 * ↑π * I)) ^ n •
      -((2 * ↑π * I) •
          𝓕 (fun x => x • ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ) =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Theorem: SchwartzMap.Real.iteratedDeriv_fourierIntegral
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ (-(2 * ↑π * I)) ^ n •
      -((2 * ↑π * I) •
          𝓕 (fun x => x • ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ) =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
Tactic:
simp [hasTemperateGrowth_smul_apply, pow_succ', smul_smul, mul_comm (_ ^ n)]
Proof state after:
no goals
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
Tactic:
have := intervalIntegral.integral_deriv_smul_eq_sub (a := a) (b := b)
  (u := fun x ↦ Real.fourierChar[-(x * ξ)])
  (v := fun x ↦ f x)
  (u' := fun x ↦ (-ξ) • (2 * π * I * Real.fourierChar[-(x * ξ)]))
  (v' := fun x ↦ deriv f x)
  (fun x _ ↦ .comp_of_tower x (Real.hasDerivAt_fourierChar _) (hasDerivAt_mul_const ξ).neg)
  (fun x _ ↦ f.differentiableAt.hasDerivAt)
  (Continuous.continuousOn <|
    .const_smul (.mul continuous_const (continuous_mul_right ξ).neg.realFourierChar) _)
  (by simpa [derivCLM_apply ℝ] using (derivCLM ℝ f).continuous.continuousOn)
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (fun x => -ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) x • (fun x => f x) x +
        (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) x • (fun x => deriv (⇑f) x) x =
    (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) b • (fun x => f x) b -
      (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) a • (fun x => f x) a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (fun x => -ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) x • (fun x => f x) x +
        (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) x • (fun x => deriv (⇑f) x) x =
    (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) b • (fun x => f x) b -
      (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) a • (fun x => f x) a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
Tactic:
simp only at this
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
Tactic:
rw [← this]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x
Tactic:
refine intervalIntegral.integral_congr ?_
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ Set.EqOn
    (fun x =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    (fun x =>
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x)
    (Set.uIcc a b)
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ Set.EqOn
    (fun x =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    (fun x =>
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x)
    (Set.uIcc a b)
Tactic:
intro x _
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (fun x =>
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
          (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
      x =
    (fun x =>
        (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x)
      x