internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
case refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ((hasTemperateGrowth_smul
            (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
          f)
        x)
    Filter.atTop (nhds 0)

case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ((hasTemperateGrowth_smul
            (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
          f)
        (-x))
    Filter.atTop (nhds 0)
Tactic:
. exact Filter.Tendsto.mono_left (zero_at_infty _) atTop_le_cocompact
Proof state after:
case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ((hasTemperateGrowth_smul
            (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
          f)
        (-x))
    Filter.atTop (nhds 0)
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
case h_cover
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
Tactic:
refine aecover_Ioc ?_ ?_ <;> simp [Filter.tendsto_neg_atBot_iff, tendsto_nat_cast_atTop_atTop]
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
case refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ((hasTemperateGrowth_smul
            (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
          f)
        x)
    Filter.atTop (nhds 0)
Tactic:
exact Filter.Tendsto.mono_left (zero_at_infty _) atTop_le_cocompact
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ((hasTemperateGrowth_smul
            (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
          f)
        (-x))
    Filter.atTop (nhds 0)
Tactic:
refine Filter.Tendsto.comp ?_ Filter.tendsto_neg_atTop_atBot
Proof state after:
case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (⇑((hasTemperateGrowth_smul
          (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
        f))
    Filter.atBot (nhds 0)
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (⇑((hasTemperateGrowth_smul
          (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
        f))
    Filter.atBot (nhds 0)
Tactic:
exact Filter.Tendsto.mono_left (zero_at_infty _) atBot_le_cocompact
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
Tactic:
induction n with
| zero => simp
| succ n IH =>
  rw [iteratedDeriv_succ]
  conv => lhs; arg 1; intro x; arg 1; intro z
  simp only [iteratedDeriv_eq_iteratedPDeriv]
  rw [fourierIntegral_deriv]
  simp only [← iteratedDeriv_eq_iteratedPDeriv]
  rw [IH]
  simp [pow_succ, smul_smul]
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegral_iteratedDeriv
Proof state before:
case zero
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => iteratedDeriv Nat.zero (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.zero • 𝓕 (fun x => f x) ξ
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegral_iteratedDeriv
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => iteratedDeriv (Nat.succ n) (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun x => 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 : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (iteratedDeriv n fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun x => f x) ξ
Theorem: SchwartzMap.Real.fourierIntegral_iteratedDeriv
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (iteratedDeriv n fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun x => f x) ξ
Tactic:
conv => lhs; arg 1; intro x; arg 1; intro z
Proof state after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (fun z => iteratedDeriv n (fun y => f y) z) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun x => f x) ξ
Theorem: SchwartzMap.Real.fourierIntegral_iteratedDeriv
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (fun z => iteratedDeriv n (fun y => f y) z) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun x => f x) ξ
Tactic:
simp only [iteratedDeriv_eq_iteratedPDeriv]
Proof state after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (fun z => ((iteratedPDeriv ℝ fun x => 1) f) z) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Theorem: SchwartzMap.Real.fourierIntegral_iteratedDeriv
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ 𝓕 (fun x => deriv (fun z => ((iteratedPDeriv ℝ fun x => 1) f) z) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Tactic:
rw [fourierIntegral_deriv]
Proof state after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => ((iteratedPDeriv ℝ fun x => 1) f) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Theorem: SchwartzMap.Real.fourierIntegral_iteratedDeriv
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => ((iteratedPDeriv ℝ fun x => 1) f) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Tactic:
simp only [← iteratedDeriv_eq_iteratedPDeriv]
Proof state after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => iteratedDeriv n (⇑f) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Theorem: SchwartzMap.Real.fourierIntegral_iteratedDeriv
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => iteratedDeriv n (⇑f) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Tactic:
rw [IH]
Proof state after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Theorem: SchwartzMap.Real.fourierIntegral_iteratedDeriv
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
Tactic:
simp [pow_succ, smul_smul]
Proof state after:
no goals
Theorem: SchwartzMap.Real.norm_fourierIntegral_le_integral_norm
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => f x) ξ‖ ≤ ∫ (x : ℝ), ‖f x‖
Tactic:
simpa [Real.fourierIntegral_def] using
  norm_integral_le_of_norm_le f.integrable.norm
    (Filter.eventually_of_forall (by simp [norm_smul]))
Proof state after:
no goals
Theorem: SchwartzMap.Real.norm_fourierIntegral_le_integral_norm
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ∀ (x : ℝ), ‖↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x‖ ≤ ‖f x‖
Tactic:
simp [norm_smul]
Proof state after:
no goals
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case zero
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
⊢ (iteratedDeriv Nat.zero fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ Nat.zero),
      Nat.choose Nat.zero i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.zero - i) (⇑f) x
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
⊢ (iteratedDeriv (Nat.succ n) fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x
Tactic:
rw [iteratedDeriv_succ, IH]
Proof state after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
⊢ (deriv fun x =>
      ∑ i in Finset.range (Nat.succ n),
        Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x) =
    fun x =>
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
⊢ (deriv fun x =>
      ∑ i in Finset.range (Nat.succ n),
        Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x) =
    fun x =>
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x
Tactic:
funext x
Proof state after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
⊢ deriv
      (fun x =>
        ∑ i in Finset.range (Nat.succ n),
          Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x)
      x =
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
⊢ deriv
      (fun x =>
        ∑ i in Finset.range (Nat.succ n),
          Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x)
      x =
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x
Tactic:
simp only [smul_smul]
Proof state after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
⊢ deriv
      (fun x =>
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) x)
      x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
⊢ deriv
      (fun x =>
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) x)
      x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
have hf (i) := (f.smooth ⊤).differentiable_iteratedDeriv i (WithTop.coe_lt_top _)
Proof state after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ deriv
      (fun x =>
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) x)
      x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ deriv
      (fun x =>
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) x)
      x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
rw [deriv_sum fun i _ ↦ ((differentiable_pow _).smul (hf _)).const_smul _ _]
Proof state after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ i in Finset.range (Nat.succ n),
      deriv (fun y => (Nat.choose n i * Nat.descFactorial k i) • y ^ (k - i) • iteratedDeriv (n - i) (⇑f) y) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ i in Finset.range (Nat.succ n),
      deriv (fun y => (Nat.choose n i * Nat.descFactorial k i) • y ^ (k - i) • iteratedDeriv (n - i) (⇑f) y) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
simp only [deriv_const_smul _ ((differentiable_pow _).smul (hf _) _)]
Proof state after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) • deriv (fun y => y ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) y) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) • deriv (fun y => y ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) y) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
simp only [deriv_smul (differentiable_pow _ _) (hf _ _)]
Proof state after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) •
        (x ^ (k - x_1) • deriv (iteratedDeriv (n - x_1) ⇑f) x +
          deriv (fun x => x ^ (k - x_1)) x • iteratedDeriv (n - x_1) (⇑f) x) =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) •
        (x ^ (k - x_1) • deriv (iteratedDeriv (n - x_1) ⇑f) x +
          deriv (fun x => x ^ (k - x_1)) x • iteratedDeriv (n - x_1) (⇑f) x) =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
simp only [smul_add, Finset.sum_add_distrib]
Proof state after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • deriv (iteratedDeriv (n - x_1) ⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          deriv (fun x => x ^ (k - x_1)) x • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x