internlm/Lean-Github huggingface dataset:
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‖₊
⊢ ∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖ ≤ ENNReal.ofReal ↑C
Tactic:
refine le_trans (lintegral_ofReal_le_lintegral_nnnorm _) ?_
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‖‖₊ ≤ ENNReal.ofReal ↑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‖‖₊ ≤ ENNReal.ofReal ↑C
Tactic:
simp [← hC]
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)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
x : ℝ
⊢ x ^ k • iteratedDeriv n (⇑f) x = g x
Tactic:
simp [← hg, hasTemperateGrowth_smul_apply, iteratedPDeriv_eq_iteratedFDeriv,
  iteratedDeriv_eq_iteratedFDeriv]
Proof state after:
no goals
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k * (|ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖) =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Tactic:
rw [iteratedDeriv_fourierIntegral]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k * (|ξ| ^ k * ‖(-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ‖) =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k * (|ξ| ^ k * ‖(-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ‖) =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Tactic:
rw [norm_smul, mul_rotate' _ ‖_ ^ n‖, mul_rotate' _ ‖_ ^ n‖]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖(-(2 * ↑π * I)) ^ n‖ * (‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k) =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖(-(2 * ↑π * I)) ^ n‖ * (‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k) =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Tactic:
refine congrArg₂ _ (by simp [abs_of_nonneg Real.pi_pos.le]) ?_
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k = ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k = ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Tactic:
simp only [← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_pow n)]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖ * |ξ| ^ k *
      (2 * π) ^ k =
    ‖𝓕
        (fun x =>
          iteratedDeriv k (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) x)
        ξ‖
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖ * |ξ| ^ k *
      (2 * π) ^ k =
    ‖𝓕
        (fun x =>
          iteratedDeriv k (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) x)
        ξ‖
Tactic:
rw [fourierIntegral_iteratedDeriv]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖ * |ξ| ^ k *
      (2 * π) ^ k =
    ‖(2 * ↑π * I * ↑ξ) ^ k •
        𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖ * |ξ| ^ k *
      (2 * π) ^ k =
    ‖(2 * ↑π * I * ↑ξ) ^ k •
        𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖
Tactic:
simp only [hasTemperateGrowth_smul_apply, norm_smul]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖ * ‖𝓕 (fun x => x ^ n • f x) ξ‖
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖ * ‖𝓕 (fun x => x ^ n • f x) ξ‖
Tactic:
rw [mul_assoc, mul_comm]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * (2 * π) ^ k * ‖𝓕 (fun x => x ^ n • f x) ξ‖ = ‖(2 * ↑π * I * ↑ξ) ^ k‖ * ‖𝓕 (fun x => x ^ n • f x) ξ‖
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * (2 * π) ^ k * ‖𝓕 (fun x => x ^ n • f x) ξ‖ = ‖(2 * ↑π * I * ↑ξ) ^ k‖ * ‖𝓕 (fun x => x ^ n • f x) ξ‖
Tactic:
refine congrArg₂ _ ?_ rfl
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * (2 * π) ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * (2 * π) ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖
Tactic:
rw [mul_comm]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k * |ξ| ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k * |ξ| ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖
Tactic:
simp [mul_pow, abs_of_nonneg Real.pi_pos.le]
Proof state after:
no goals
Theorem: SchwartzMap.Real.norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖(-(2 * ↑π * I)) ^ n‖ = (2 * π) ^ n
Tactic:
simp [abs_of_nonneg Real.pi_pos.le]
Proof state after:
no goals
Theorem: SchwartzMap.Real.pow_abs_mul_norm_iteratedDeriv_fourierIntegral
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖ =
    (2 * π) ^ n / (2 * π) ^ k * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
Tactic:
rw [div_mul_eq_mul_div]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖ =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖ / (2 * π) ^ k
Theorem: SchwartzMap.Real.pow_abs_mul_norm_iteratedDeriv_fourierIntegral
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖ =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖ / (2 * π) ^ k
Tactic:
rw [← norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖ =
    (2 * π) ^ k * (|ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖) / (2 * π) ^ k
Theorem: SchwartzMap.Real.pow_abs_mul_norm_iteratedDeriv_fourierIntegral
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖ =
    (2 * π) ^ k * (|ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖) / (2 * π) ^ k
Tactic:
rw [mul_div_cancel_left]
Proof state after:
case ha
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k ≠ 0
Theorem: SchwartzMap.Real.pow_abs_mul_norm_iteratedDeriv_fourierIntegral
Proof state before:
case ha
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k ≠ 0
Tactic:
simp [Real.pi_pos.ne']
Proof state after:
no goals
Theorem: SchwartzMap.Real.norm_fourierIntegral_iteratedDeriv_pow_smul
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖ =
    (2 * π) ^ k / (2 * π) ^ n * (|ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖)
Tactic:
rw [div_mul_eq_mul_div]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖ =
    (2 * π) ^ k * (|ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖) / (2 * π) ^ n
Theorem: SchwartzMap.Real.norm_fourierIntegral_iteratedDeriv_pow_smul
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖ =
    (2 * π) ^ k * (|ξ| ^ k * ‖iteratedDeriv n (fun ζ => 𝓕 (⇑f) ζ) ξ‖) / (2 * π) ^ n
Tactic:
rw [norm_iteratedDeriv_fourierIntegral_eq_norm_fourierIntegral_iteratedDeriv]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖ =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖ / (2 * π) ^ n
Theorem: SchwartzMap.Real.norm_fourierIntegral_iteratedDeriv_pow_smul
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖ =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖ / (2 * π) ^ n
Tactic:
rw [mul_div_cancel_left]
Proof state after:
case ha
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ n ≠ 0
Theorem: SchwartzMap.Real.norm_fourierIntegral_iteratedDeriv_pow_smul
Proof state before:
case ha
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ n ≠ 0
Tactic:
simp [Real.pi_pos.ne']
Proof state after:
no goals
Theorem: ENNReal_rpow_ne_top
Proof state before:
a : ENNReal
p : ℝ
hp : 0 < p
h : a ≠ ⊤
⊢ a ^ p ≠ ⊤
Tactic:
rw [← ENNReal.ofReal_toReal_eq_iff] at h
Proof state after:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ a ^ p ≠ ⊤
Theorem: ENNReal_rpow_ne_top
Proof state before:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ a ^ p ≠ ⊤
Tactic:
rw [← h]
Proof state after:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.ofReal (ENNReal.toReal a) ^ p ≠ ⊤
Theorem: ENNReal_rpow_ne_top
Proof state before:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.ofReal (ENNReal.toReal a) ^ p ≠ ⊤
Tactic:
simp
Proof state after:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.toReal a ≤ 0 → 0 ≤ p
Theorem: ENNReal_rpow_ne_top
Proof state before:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.toReal a ≤ 0 → 0 ≤ p
Tactic:
intros
Proof state after:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
a✝ : ENNReal.toReal a ≤ 0
⊢ 0 ≤ p
Theorem: ENNReal_rpow_ne_top
Proof state before:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
a✝ : ENNReal.toReal a ≤ 0
⊢ 0 ≤ p
Tactic:
exact hp.le
Proof state after:
no goals
Theorem: ENNReal_rpow_lt_top
Proof state before:
a : ENNReal
p : ℝ
hp : 0 < p
h : a < ⊤
⊢ a ^ p < ⊤
Tactic:
rw [lt_top_iff_ne_top] at h ⊢
Proof state after:
a : ENNReal
p : ℝ
hp : 0 < p
h : a ≠ ⊤
⊢ a ^ p ≠ ⊤
Theorem: ENNReal_rpow_lt_top
Proof state before:
a : ENNReal
p : ℝ
hp : 0 < p
h : a ≠ ⊤
⊢ a ^ p ≠ ⊤
Tactic:
exact ENNReal_rpow_ne_top hp h
Proof state after:
no goals
Theorem: SchwartzMap.coeFn_add
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : 𝓢(E, F)
⊢ ⇑(f + g) = ⇑f + ⇑g
Tactic:
ext x
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : 𝓢(E, F)
x : E
⊢ (f + g) x = (⇑f + ⇑g) x
Theorem: SchwartzMap.coeFn_add
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : 𝓢(E, F)
x : E
⊢ (f + g) x = (⇑f + ⇑g) x
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.decay₁
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
⊢ ∀ (k n : ℕ), ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Tactic:
intro k n
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Theorem: SchwartzMap.decay₁
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Tactic:
have := @one_add_le_sup_seminorm_apply ℝ E F _ _ _ _ _ _ _ ⟨k, n⟩ k n (by simp) (by simp) f
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
this :
  ∀ (x : E),
    (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
      2 ^ (k, n).1 * (Finset.sup (Finset.Iic (k, n)) fun m => SchwartzMap.seminorm ℝ m.1 m.2) f
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Theorem: SchwartzMap.decay₁
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
this :
  ∀ (x : E),
    (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
      2 ^ (k, n).1 * (Finset.sup (Finset.Iic (k, n)) fun m => SchwartzMap.seminorm ℝ m.1 m.2) f
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Tactic:
simp at this
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
this :
  ∀ (x : E),
    (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
      2 ^ k * (Finset.sup (Finset.Iic (k, n)) fun m => SchwartzMap.seminorm ℝ m.1 m.2) f
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Theorem: SchwartzMap.decay₁
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
this :
  ∀ (x : E),
    (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
      2 ^ k * (Finset.sup (Finset.Iic (k, n)) fun m => SchwartzMap.seminorm ℝ m.1 m.2) f
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Tactic:
use ((2 : ℝ) ^ k) * Finset.sup (Finset.Iic (k, n)) (fun m => SchwartzMap.seminorm ℝ m.1 m.2) f
Proof state after:
no goals
Theorem: SchwartzMap.decay₁
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
⊢ k ≤ (k, n).1
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.decay₁
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
⊢ n ≤ (k, n).2
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.decay_of_decay₁
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h : ∀ (k n : ℕ), ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
intro k n
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h : ∀ (k n : ℕ), ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
k n : ℕ
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Theorem: SchwartzMap.decay_of_decay₁
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h : ∀ (k n : ℕ), ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
k n : ℕ
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
specialize h k n
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
h : ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Theorem: SchwartzMap.decay_of_decay₁
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
h : ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
rcases h with ⟨C, hC⟩
Proof state after:
case intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Theorem: SchwartzMap.decay_of_decay₁
Proof state before:
case intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
use C
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Theorem: SchwartzMap.decay_of_decay₁
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
intro x
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Theorem: SchwartzMap.decay_of_decay₁
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
specialize hC x
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Theorem: SchwartzMap.decay_of_decay₁
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
refine le_trans ?_ hC
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖