internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h.refine_2
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) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
conv => rhs; rw [Finset.sum_range_succ]
Proof state after:
case succ.h.refine_2
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) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
          (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
        (Nat.choose n (Nat.succ n) * Nat.descFactorial k (n + 1)) • x ^ (k - (n + 1)) • iteratedDeriv (n - n) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h.refine_2
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) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
          (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
        (Nat.choose n (Nat.succ n) * Nat.descFactorial k (n + 1)) • x ^ (k - (n + 1)) • iteratedDeriv (n - n) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
simp only [Nat.choose_succ_self, zero_mul, zero_smul, add_zero]
Proof state after:
case succ.h.refine_2
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) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h.refine_2
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) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
rw [Finset.sum_range_succ']
Proof state after:
case succ.h.refine_2
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)
⊢ ∑ k_1 in Finset.range n,
        (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x +
      (Nat.choose n 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (n - 0 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h.refine_2
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)
⊢ ∑ k_1 in Finset.range n,
        (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x +
      (Nat.choose n 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (n - 0 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
simp only [Nat.choose_zero_right, Nat.descFactorial_zero, mul_one, Nat.sub_zero, one_smul]
Proof state after:
case succ.h.refine_2
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)
⊢ ∑ k_1 in Finset.range n,
        (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x +
      x ^ k • iteratedDeriv (n + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      x ^ k • iteratedDeriv (Nat.succ n) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h.refine_2
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)
⊢ ∑ k_1 in Finset.range n,
        (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x +
      x ^ k • iteratedDeriv (n + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      x ^ k • iteratedDeriv (Nat.succ n) (⇑f) x
Tactic:
rw [add_left_inj]
Proof state after:
case succ.h.refine_2
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)
⊢ ∑ k_1 in Finset.range n,
      (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
        x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
      (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h.refine_2
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)
⊢ ∑ k_1 in Finset.range n,
      (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
        x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
      (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x
Tactic:
refine Finset.sum_congr rfl ?_
Proof state after:
case succ.h.refine_2
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 ∈ Finset.range n,
    (Nat.choose n (x_1 + 1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - (x_1 + 1) + 1) (⇑f) x =
      (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h.refine_2
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 ∈ Finset.range n,
    (Nat.choose n (x_1 + 1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - (x_1 + 1) + 1) (⇑f) x =
      (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x
Tactic:
intro i hi
Proof state after:
case succ.h.refine_2
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 : ℕ
hi : i ∈ Finset.range n
⊢ (Nat.choose n (i + 1) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - (i + 1) + 1) (⇑f) x =
    (Nat.choose n (Nat.succ i) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h.refine_2
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 : ℕ
hi : i ∈ Finset.range n
⊢ (Nat.choose n (i + 1) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - (i + 1) + 1) (⇑f) x =
    (Nat.choose n (Nat.succ i) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x
Tactic:
replace hi : i.succ ≤ n := by simpa [Finset.mem_range] using hi
Proof state after:
case succ.h.refine_2
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 : ℕ
hi : Nat.succ i ≤ n
⊢ (Nat.choose n (i + 1) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - (i + 1) + 1) (⇑f) x =
    (Nat.choose n (Nat.succ i) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
case succ.h.refine_2
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 : ℕ
hi : Nat.succ i ≤ n
⊢ (Nat.choose n (i + 1) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - (i + 1) + 1) (⇑f) x =
    (Nat.choose n (Nat.succ i) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x
Tactic:
simp [Nat.add_one, ← Nat.succ_sub hi]
Proof state after:
no goals
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof state before:
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 : ℕ
hi : i ∈ Finset.range n
⊢ Nat.succ i ≤ n
Tactic:
simpa [Finset.mem_range] using hi
Proof state after:
no goals
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x‖ ≤ C
Tactic:
generalize hg : hasTemperateGrowth_smul (Function.hasTemperateGrowth_pow k)
    (iteratedPDeriv ℝ (fun _ ↦ 1 : Fin n → ℝ) f) = g
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x‖ ≤ C
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x‖ ≤ C
Tactic:
have (x : ℝ) : x ^ k • iteratedDeriv n f x = g x := by
  simp [← hg, hasTemperateGrowth_smul_apply, iteratedPDeriv_eq_iteratedFDeriv,
    iteratedDeriv_eq_iteratedFDeriv]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∀ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x = g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x‖ ≤ C
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∀ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x = g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x‖ ≤ C
Tactic:
simp only [this]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∀ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x = g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∀ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x = g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Tactic:
clear this
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Tactic:
have := g.integrable.hasFiniteIntegral
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : HasFiniteIntegral fun x => g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : HasFiniteIntegral fun x => g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Tactic:
rw [HasFiniteIntegral, lt_top_iff_ne_top, WithTop.ne_top_iff_exists] at this
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∃ a, ↑a = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∃ a, ↑a = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Tactic:
rcases this with ⟨C, hC⟩
Proof state after:
case intro
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
case intro
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Tactic:
use C.val
Proof state after:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ 0 ≤ ↑C ∧ ‖∫ (x : ℝ), g x‖ ≤ ↑C
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ 0 ≤ ↑C ∧ ‖∫ (x : ℝ), g x‖ ≤ ↑C
Tactic:
refine And.intro C.prop ?_
Proof state after:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ‖∫ (x : ℝ), g x‖ ≤ ↑C
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ‖∫ (x : ℝ), g x‖ ≤ ↑C
Tactic:
refine le_trans (norm_integral_le_lintegral_norm _) ?_
Proof state after:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ENNReal.toReal (∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖) ≤ ↑C
Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound
Proof state before:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ENNReal.toReal (∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖) ≤ ↑C
Tactic:
refine ENNReal.toReal_le_of_le_ofReal C.prop ?_
Proof state after:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖ ≤ ENNReal.ofReal ↑C