internlm/Lean-Github huggingface dataset:
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n : ℕ
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
have hf_bound := hf.bound_forall_range (n + 1)
Proof state after:
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n : ℕ
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n : ℕ
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
have hg_bound := hg.bound_forall_range (n + 1)
Proof state after:
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n : ℕ
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n : ℕ
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases hf_bound with ⟨k_f, C_f, ⟨hC_f_nonneg, hC_f⟩⟩
Proof state after:
case intro.intro.intro
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n : ℕ
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case intro.intro.intro
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n : ℕ
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases hg_bound with ⟨k_g, C_g, ⟨_, hC_g⟩⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case intro.intro.intro.intro.intro.intro
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
use k_f + k_g
Proof state after:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ ∃ C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ (k_f + k_g)
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ ∃ C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ (k_f + k_g)
Tactic:
use 2 ^ n * C_f * C_g
Proof state after:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ ↑(2 ^ n) * C_f * C_g * (1 + ‖x‖) ^ (k_f + k_g)
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ ↑(2 ^ n) * C_f * C_g * (1 + ‖x‖) ^ (k_f + k_g)
Tactic:
intro x
Proof state after:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ ↑(2 ^ n) * C_f * C_g * (1 + ‖x‖) ^ (k_f + k_g)
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ ↑(2 ^ n) * C_f * C_g * (1 + ‖x‖) ^ (k_f + k_g)
Tactic:
refine le_trans (norm_iteratedFDeriv_clm_apply hf.1 hg.1 _ le_top) ?_
Proof state after:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ∑ i in Finset.range (n + 1), ↑(Nat.choose n i) * ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖ ≤
    ↑(2 ^ n) * C_f * C_g * (1 + ‖x‖) ^ (k_f + k_g)
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ∑ i in Finset.range (n + 1), ↑(Nat.choose n i) * ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖ ≤
    ↑(2 ^ n) * C_f * C_g * (1 + ‖x‖) ^ (k_f + k_g)
Tactic:
simp [mul_assoc]
Proof state after:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ∑ x_1 in Finset.range (n + 1), ↑(Nat.choose n x_1) * (‖iteratedFDeriv ℝ x_1 f x‖ * ‖iteratedFDeriv ℝ (n - x_1) g x‖) ≤
    2 ^ n * (C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g)))
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ∑ x_1 in Finset.range (n + 1), ↑(Nat.choose n x_1) * (‖iteratedFDeriv ℝ x_1 f x‖ * ‖iteratedFDeriv ℝ (n - x_1) g x‖) ≤
    2 ^ n * (C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g)))
Tactic:
norm_cast
Proof state after:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ∑ x_1 in Finset.range (n + 1), ↑(Nat.choose n x_1) * (‖iteratedFDeriv ℝ x_1 f x‖ * ‖iteratedFDeriv ℝ (n - x_1) g x‖) ≤
    ↑(2 ^ n) * (C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g)))
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ∑ x_1 in Finset.range (n + 1), ↑(Nat.choose n x_1) * (‖iteratedFDeriv ℝ x_1 f x‖ * ‖iteratedFDeriv ℝ (n - x_1) g x‖) ≤
    ↑(2 ^ n) * (C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g)))
Tactic:
refine Finset.sum_range_choose_mul_le_pow_two_mul_real ?_
Proof state after:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ∀ i ∈ Finset.range (n + 1),
    ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖ ≤ C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ∀ i ∈ Finset.range (n + 1),
    ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖ ≤ C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Tactic:
intro i hi
Proof state after:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖ ≤ C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖ ≤ C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Tactic:
refine le_trans (mul_le_mul (hC_f i hi x) (hC_g (n - i) ?_ x) (norm_nonneg _) ?_) ?_
Proof state after:
case h.refine_1
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ n - i ∈ Finset.range (n + 1)

case h.refine_2
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ 0 ≤ C_f * (1 + ‖x‖) ^ k_f

case h.refine_3
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ C_f * (1 + ‖x‖) ^ k_f * (C_g * (1 + ‖x‖) ^ k_g) ≤ C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h.refine_2
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ 0 ≤ C_f * (1 + ‖x‖) ^ k_f

case h.refine_3
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ C_f * (1 + ‖x‖) ^ k_f * (C_g * (1 + ‖x‖) ^ k_g) ≤ C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Tactic:
. simp [hC_f_nonneg]
Proof state after:
case h.refine_3
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ C_f * (1 + ‖x‖) ^ k_f * (C_g * (1 + ‖x‖) ^ k_g) ≤ C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h.refine_3
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ C_f * (1 + ‖x‖) ^ k_f * (C_g * (1 + ‖x‖) ^ k_g) ≤ C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Tactic:
refine le_of_eq ?_
Proof state after:
case h.refine_3
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ C_f * (1 + ‖x‖) ^ k_f * (C_g * (1 + ‖x‖) ^ k_g) = C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h.refine_3
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ C_f * (1 + ‖x‖) ^ k_f * (C_g * (1 + ‖x‖) ^ k_g) = C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Tactic:
ring_nf
Proof state after:
no goals