internlm/Lean-Github huggingface dataset:
Theorem: bound_forall_range
Proof state before:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∃ k C, ∀ (x : E), f n x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases h with ⟨k_m, C_m, hC_m⟩
Proof state after:
case succ.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases h_ind with ⟨k_i, C_i, ⟨hC_i_nonneg, hC_i⟩⟩
Proof state after:
case succ.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨max k_i k_m, max C_i C_m, ?_⟩
Proof state after:
case succ.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ 0 ≤ max C_i C_m ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ 0 ≤ max C_i C_m ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
refine And.intro (le_trans hC_i_nonneg (by simp)) ?_
Proof state after:
case succ.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
intro i hi x
Proof state after:
case succ.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
hi : i < Nat.succ n
x : E
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
hi : i < Nat.succ n
x : E
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
simp [Nat.lt_succ] at hi
Proof state after:
case succ.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi : i ≤ n
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi : i ≤ n
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
cases lt_or_eq_of_le hi with
| inl hi =>
  specialize hC_i i hi x
  refine le_trans hC_i ?_
  refine mul_le_mul ?_ (pow_le_pow_right ?_ ?_) ?_ (le_trans hC_i_nonneg ?_) <;> simp
| inr hi =>
  rw [hi]
  specialize hC_m x
  refine le_trans hC_m ?_
  refine mul_le_mul ?_ (pow_le_pow_right ?_ ?_) ?_ (le_trans hC_i_nonneg ?_) <;> simp
Proof state after:
no goals
Theorem: bound_forall_range
Proof state before:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind :
  (∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k) → ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro i hi
Proof state after:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind :
  (∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k) → ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
i : ℕ
hi : i < n
⊢ ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Theorem: bound_forall_range
Proof state before:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind :
  (∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k) → ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
i : ℕ
hi : i < n
⊢ ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine h _ ?_
Proof state after:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind :
  (∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k) → ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
i : ℕ
hi : i < n
⊢ i < Nat.succ n
Theorem: bound_forall_range
Proof state before:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind :
  (∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k) → ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
i : ℕ
hi : i < n
⊢ i < Nat.succ n
Tactic:
exact lt_trans hi (Nat.lt_succ_self _)
Proof state after:
no goals
Theorem: bound_forall_range
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 → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ C_i ≤ max C_i C_m
Tactic:
simp
Proof state after:
no goals
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro.inl
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i < n
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
specialize hC_i i hi x
Proof state after:
case succ.intro.intro.intro.intro.intro.inl
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i < n
hC_i : f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro.inl
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i < n
hC_i : f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
refine le_trans hC_i ?_
Proof state after:
case succ.intro.intro.intro.intro.intro.inl
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i < n
hC_i : f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ C_i * (1 + ‖x‖) ^ k_i ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro.inl
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i < n
hC_i : f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ C_i * (1 + ‖x‖) ^ k_i ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
refine mul_le_mul ?_ (pow_le_pow_right ?_ ?_) ?_ (le_trans hC_i_nonneg ?_) <;> simp
Proof state after:
no goals
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro.inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
rw [hi]
Proof state after:
case succ.intro.intro.intro.intro.intro.inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
⊢ f n x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro.inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
⊢ f n x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
specialize hC_m x
Proof state after:
case succ.intro.intro.intro.intro.intro.inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
hC_m : f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ f n x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro.inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
hC_m : f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ f n x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
refine le_trans hC_m ?_
Proof state after:
case succ.intro.intro.intro.intro.intro.inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
hC_m : f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ C_m * (1 + ‖x‖) ^ k_m ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Theorem: bound_forall_range
Proof state before:
case succ.intro.intro.intro.intro.intro.inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
hC_m : f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ C_m * (1 + ‖x‖) ^ k_m ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
refine mul_le_mul ?_ (pow_le_pow_right ?_ ?_) ?_ (le_trans hC_i_nonneg ?_) <;> simp
Proof state after:
no goals
Theorem: bound_forall
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
ι : Type u_3
s : Finset ι
f : ι → E → ℝ
h : ∀ i ∈ s, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i ∈ s, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
sorry
Proof state after:
no goals
Theorem: Function.HasTemperateGrowth.bound_forall_range
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
⊢ ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
simp
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.bound_forall_range
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine _root_.bound_forall_range n ?_
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
⊢ ∀ i < n, ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.bound_forall_range
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
⊢ ∀ i < n, ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro i _
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
i : ℕ
a✝ : i < n
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.bound_forall_range
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
i : ℕ
a✝ : i < n
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
exact hf.2 i
Proof state after:
no goals
Theorem: Function.HasTemperateGrowth.fderiv
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
hf : HasTemperateGrowth f
⊢ HasTemperateGrowth fun x => _root_.fderiv ℝ f x
Tactic:
refine ⟨hf.1.fderiv_right le_top, ?_⟩
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
hf : HasTemperateGrowth f
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.fderiv
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
hf : HasTemperateGrowth f
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
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
hf : HasTemperateGrowth f
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.fderiv
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
hf : HasTemperateGrowth f
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases bound_forall_range (n + 2) hf with ⟨k, C, ⟨_, hC⟩⟩
Proof state after:
case intro.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
hf : HasTemperateGrowth f
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.fderiv
Proof state before:
case intro.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
hf : HasTemperateGrowth f
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨k, C, ?_⟩
Proof state after:
case intro.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
hf : HasTemperateGrowth f
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.fderiv
Proof state before:
case intro.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
hf : HasTemperateGrowth f
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro x
Proof state after:
case intro.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
hf : HasTemperateGrowth f
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.fderiv
Proof state before:
case intro.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
hf : HasTemperateGrowth f
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
suffices : ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Proof state after:
case intro.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
hf : HasTemperateGrowth f
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
this : ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k

case this
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k