internlm/Lean-Github huggingface dataset:
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‖ ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
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 ≤ (1 + ‖x‖) ^ k
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 ≤ (1 + ‖x‖) ^ k
Tactic:
simp [pow_le_pow_left]
Proof state after:
no goals
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
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)
r : ℝ
⊢ ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
intro 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)
r : ℝ
n : ℕ
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
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)
r : ℝ
n : ℕ
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
generalize hk : ⌈r⌉₊ = k
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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
rcases decay₁ f k n 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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
refine And.intro ?_ ?_
Proof state after:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ 0 ≤ C

case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ 0 ≤ C

case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
. specialize hC 0  simp at hC
  exact le_trans (norm_nonneg _) hC
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
. intro x
  specialize hC x
  have h_pos : 0 < 1 + ‖x‖ := add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _)
  rw [Real.rpow_neg h_pos.le]
  rw [mul_comm, inv_mul_eq_div]
  rw [le_div_iff' (Real.rpow_pos_of_pos h_pos _)]
  refine le_trans ?_ hC
  refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
  rw [← Real.rpow_nat_cast]
  refine Real.rpow_le_rpow_of_exponent_le (by simp) ?_
  simp [← hk]
  exact Nat.le_ceil _
Proof state after:
no goals
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ 0 ≤ C
Tactic:
specialize hC 0
Proof state after:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : (1 + ‖0‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) 0‖ ≤ C
⊢ 0 ≤ C
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : (1 + ‖0‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) 0‖ ≤ C
⊢ 0 ≤ C
Tactic:
simp at hC
Proof state after:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ‖iteratedFDeriv ℝ n (⇑f) 0‖ ≤ C
⊢ 0 ≤ C
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ‖iteratedFDeriv ℝ n (⇑f) 0‖ ≤ C
⊢ 0 ≤ C
Tactic:
exact le_trans (norm_nonneg _) hC
Proof state after:
no goals
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
intro x
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
specialize hC x
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
have h_pos : 0 < 1 + ‖x‖ := add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _)
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
rw [Real.rpow_neg h_pos.le]
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * ((1 + ‖x‖) ^ r)⁻¹
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * ((1 + ‖x‖) ^ r)⁻¹
Tactic:
rw [mul_comm, inv_mul_eq_div]
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C / (1 + ‖x‖) ^ r
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C / (1 + ‖x‖) ^ r
Tactic:
rw [le_div_iff' (Real.rpow_pos_of_pos h_pos _)]
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Tactic:
refine le_trans ?_ hC
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r ≤ (1 + ‖x‖) ^ k
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r ≤ (1 + ‖x‖) ^ k
Tactic:
rw [← Real.rpow_nat_cast]
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r ≤ (1 + ‖x‖) ^ ↑k
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r ≤ (1 + ‖x‖) ^ ↑k
Tactic:
refine Real.rpow_le_rpow_of_exponent_le (by simp) ?_
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ r ≤ ↑k
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ r ≤ ↑k
Tactic:
simp [← hk]
Proof state after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ r ≤ ↑⌈r⌉₊
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ r ≤ ↑⌈r⌉₊
Tactic:
exact Nat.le_ceil _
Proof state after:
no goals
Theorem: SchwartzMap.norm_iteratedFDeriv_le_pow_one_add_norm
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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ 1 ≤ 1 + ‖x‖
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
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)
p : ℝ
hp : 0 < p
q : ℝ
⊢ ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Tactic:
intro 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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Tactic:
generalize hr : q / p = r
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Tactic:
rcases norm_iteratedFDeriv_le_pow_one_add_norm f r n with ⟨C, ⟨hC_nonneg, hC⟩⟩
Proof state after:
case intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Tactic:
use C ^ p
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
⊢ 0 ≤ C ^ p ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
⊢ 0 ≤ C ^ p ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Tactic:
have hC_pow : 0 ≤ C ^ p := Real.rpow_nonneg hC_nonneg _
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hC_pow : 0 ≤ C ^ p
⊢ 0 ≤ C ^ p ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hC_pow : 0 ≤ C ^ p
⊢ 0 ≤ C ^ p ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Tactic:
refine And.intro hC_pow ?_
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hC_pow : 0 ≤ C ^ p
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hC_pow : 0 ≤ C ^ p
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hC_pow : 0 ≤ C ^ p
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)