internlm/Lean-Github huggingface dataset:
Theorem: Function.HasTemperateGrowth.add
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
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
hC_f_nonneg : 0 ≤ C_f
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ C_g * (1 + ‖x‖) ^ k_g ≤ C_g * (1 + ‖x‖) ^ max k_f k_g
Tactic:
refine mul_le_mul_of_nonneg_left ?_ hC_g_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
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
hC_f_nonneg : 0 ≤ C_f
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ (1 + ‖x‖) ^ k_g ≤ (1 + ‖x‖) ^ max k_f k_g
Theorem: Function.HasTemperateGrowth.add
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
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
hC_f_nonneg : 0 ≤ C_f
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ (1 + ‖x‖) ^ k_g ≤ (1 + ‖x‖) ^ max k_f k_g
Tactic:
exact pow_le_pow_right (by simp) (by simp)
Proof state after:
no goals
Theorem: Function.HasTemperateGrowth.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 : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
hC_f_nonneg : 0 ≤ C_f
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ k_g ≤ max k_f k_g
Tactic:
simp
Proof state after:
no goals
Theorem: Function.HasTemperateGrowth.sub
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
g : E → F
hg : HasTemperateGrowth g
⊢ HasTemperateGrowth fun x => f x - g x
Tactic:
simp_rw [sub_eq_add_neg]
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
g : E → F
hg : HasTemperateGrowth g
⊢ HasTemperateGrowth fun x => f x + -g x
Theorem: Function.HasTemperateGrowth.sub
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
g : E → F
hg : HasTemperateGrowth g
⊢ HasTemperateGrowth fun x => f x + -g x
Tactic:
refine add hf hg.neg
Proof state after:
no goals
Theorem: Function.HasTemperateGrowth.prod
Proof state before:
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Finset ι
f : ι → E → ℝ
hf : ∀ i ∈ s, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth fun x => ∏ i in s, f i x
Tactic:
induction s using Finset.induction with
| empty => simp [hasTemperateGrowth_const]
| @insert i s hi IH =>
  simp only [Finset.mem_insert, forall_eq_or_imp] at hf
  simpa [Finset.prod_insert hi] using HasTemperateGrowth.mul hf.1 (IH hf.2)
Proof state after:
no goals
Theorem: Function.HasTemperateGrowth.prod
Proof state before:
case empty
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → ℝ
hf : ∀ i ∈ ∅, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth fun x => ∏ i in ∅, f i x
Tactic:
simp [hasTemperateGrowth_const]
Proof state after:
no goals
Theorem: Function.HasTemperateGrowth.prod
Proof state before:
case insert
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → ℝ
i : ι
s : Finset ι
hi : i ∉ s
IH : (∀ i ∈ s, HasTemperateGrowth (f i)) → HasTemperateGrowth fun x => ∏ i in s, f i x
hf : ∀ i_1 ∈ insert i s, HasTemperateGrowth (f i_1)
⊢ HasTemperateGrowth fun x => ∏ i in insert i s, f i x
Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at hf
Proof state after:
case insert
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → ℝ
i : ι
s : Finset ι
hi : i ∉ s
IH : (∀ i ∈ s, HasTemperateGrowth (f i)) → HasTemperateGrowth fun x => ∏ i in s, f i x
hf : HasTemperateGrowth (f i) ∧ ∀ a ∈ s, HasTemperateGrowth (f a)
⊢ HasTemperateGrowth fun x => ∏ i in insert i s, f i x
Theorem: Function.HasTemperateGrowth.prod
Proof state before:
case insert
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → ℝ
i : ι
s : Finset ι
hi : i ∉ s
IH : (∀ i ∈ s, HasTemperateGrowth (f i)) → HasTemperateGrowth fun x => ∏ i in s, f i x
hf : HasTemperateGrowth (f i) ∧ ∀ a ∈ s, HasTemperateGrowth (f a)
⊢ HasTemperateGrowth fun x => ∏ i in insert i s, f i x
Tactic:
simpa [Finset.prod_insert hi] using HasTemperateGrowth.mul hf.1 (IH hf.2)
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_continuousMultilinearMap_mkPiRing
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
⊢ HasTemperateGrowth fun x => ContinuousMultilinearMap.mkPiRing ℝ ι x
Tactic:
simp only [← ContinuousMultilinearMap.mkPiRingL_apply]
Proof state after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
⊢ HasTemperateGrowth fun x => (ContinuousMultilinearMap.mkPiRingL ℝ F) x
Theorem: Function.hasTemperateGrowth_continuousMultilinearMap_mkPiRing
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
⊢ HasTemperateGrowth fun x => (ContinuousMultilinearMap.mkPiRingL ℝ F) x
Tactic:
exact hasTemperateGrowth_clm _
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_continuousMultilinearMap_mkPiRing_apply
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
x : F
⊢ HasTemperateGrowth fun m => (ContinuousMultilinearMap.mkPiRing ℝ ι x) m
Tactic:
simp only [ContinuousMultilinearMap.mkPiRing_apply]
Proof state after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
x : F
⊢ HasTemperateGrowth fun m => (∏ i : ι, m i) • x
Theorem: Function.hasTemperateGrowth_continuousMultilinearMap_mkPiRing_apply
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
x : F
⊢ HasTemperateGrowth fun m => (∏ i : ι, m i) • x
Tactic:
refine .smul_const ?_ x
Proof state after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
x : F
⊢ HasTemperateGrowth fun m => ∏ i : ι, m i
Theorem: Function.hasTemperateGrowth_continuousMultilinearMap_mkPiRing_apply
Proof state before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
x : F
⊢ HasTemperateGrowth fun m => ∏ i : ι, m i
Tactic:
exact .prod Finset.univ fun i _ ↦ hasTemperateGrowth_clm (.proj (φ := fun _ ↦ ℝ) i)
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_pow
Proof state before:
n : ℕ
⊢ HasTemperateGrowth fun x => x ^ n
Tactic:
refine And.intro (contDiff_id.pow n) ?_
Proof state after:
n : ℕ
⊢ ∀ (n_1 : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n_1 (fun x => x ^ n) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.hasTemperateGrowth_pow
Proof state before:
n : ℕ
⊢ ∀ (n_1 : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n_1 (fun x => x ^ n) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro i
Proof state after:
n i : ℕ
⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.hasTemperateGrowth_pow
Proof state before:
n i : ℕ
⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
use n - i, Nat.descFactorial n i
Proof state after:
case h
n i : ℕ
⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Theorem: Function.hasTemperateGrowth_pow
Proof state before:
case h
n i : ℕ
⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Tactic:
intro x
Proof state after:
case h
n i : ℕ
x : ℝ
⊢ ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Theorem: Function.hasTemperateGrowth_pow
Proof state before:
case h
n i : ℕ
x : ℝ
⊢ ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Tactic:
rw [norm_iteratedFDeriv_eq_norm_iteratedDeriv, iteratedDeriv_pow]
Proof state after:
case h
n i : ℕ
x : ℝ
⊢ ‖(fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Theorem: Function.hasTemperateGrowth_pow
Proof state before:
case h
n i : ℕ
x : ℝ
⊢ ‖(fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Tactic:
rw [norm_mul, IsROrC.norm_natCast]
Proof state after:
case h
n i : ℕ
x : ℝ
⊢ ↑(Nat.descFactorial n i) * ‖x ^ (n - i)‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Theorem: Function.hasTemperateGrowth_pow
Proof state before:
case h
n i : ℕ
x : ℝ
⊢ ↑(Nat.descFactorial n i) * ‖x ^ (n - i)‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Tactic:
refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg _)
Proof state after:
case h
n i : ℕ
x : ℝ
⊢ ‖x ^ (n - i)‖ ≤ (1 + ‖x‖) ^ (n - i)
Theorem: Function.hasTemperateGrowth_pow
Proof state before:
case h
n i : ℕ
x : ℝ
⊢ ‖x ^ (n - i)‖ ≤ (1 + ‖x‖) ^ (n - i)
Tactic:
simp [pow_le_pow_left]
Proof state after:
no goals
Theorem: fderiv_cexp_real
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ fderiv ℝ (fun x => Complex.exp (f x)) x = Complex.exp (f x) • fderiv ℝ f x
Tactic:
change fderiv ℝ (Complex.exp ∘ f) x = _
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ fderiv ℝ (Complex.exp ∘ f) x = Complex.exp (f x) • fderiv ℝ f x
Theorem: fderiv_cexp_real
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ fderiv ℝ (Complex.exp ∘ f) x = Complex.exp (f x) • fderiv ℝ f x
Tactic:
rw [fderiv.comp x Complex.differentiable_exp.differentiableAt hf]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ ContinuousLinearMap.comp (fderiv ℝ Complex.exp (f x)) (fderiv ℝ f x) = Complex.exp (f x) • fderiv ℝ f x
Theorem: fderiv_cexp_real
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ ContinuousLinearMap.comp (fderiv ℝ Complex.exp (f x)) (fderiv ℝ f x) = Complex.exp (f x) • fderiv ℝ f x
Tactic:
rw [(Complex.hasStrictFDerivAt_exp_real (f x)).hasFDerivAt.fderiv]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ ContinuousLinearMap.comp (Complex.exp (f x) • 1) (fderiv ℝ f x) = Complex.exp (f x) • fderiv ℝ f x
Theorem: fderiv_cexp_real
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ ContinuousLinearMap.comp (Complex.exp (f x) • 1) (fderiv ℝ f x) = Complex.exp (f x) • fderiv ℝ f x
Tactic:
simp [ContinuousLinearMap.one_def]
Proof state after:
no goals
Theorem: iteratedFDeriv_neg_apply'
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
x : E
i : ℕ
f : E → F
⊢ iteratedFDeriv 𝕜 i (fun x => -f x) x = -iteratedFDeriv 𝕜 i f x
Tactic:
rw [← iteratedFDeriv_neg_apply]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
x : E
i : ℕ
f : E → F
⊢ iteratedFDeriv 𝕜 i (fun x => -f x) x = iteratedFDeriv 𝕜 i (-f) x
Theorem: iteratedFDeriv_neg_apply'
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
x : E
i : ℕ
f : E → F
⊢ iteratedFDeriv 𝕜 i (fun x => -f x) x = iteratedFDeriv 𝕜 i (-f) x
Tactic:
rfl
Proof state after:
no goals
Theorem: iteratedFDeriv_const_smul_apply'
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
i : ℕ
a : 𝕜'
f : E → F
x : E
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedFDeriv 𝕜 i (fun x => a • f x) x = a • iteratedFDeriv 𝕜 i f x
Tactic:
rw [← iteratedFDeriv_const_smul_apply hf]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
i : ℕ
a : 𝕜'
f : E → F
x : E
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedFDeriv 𝕜 i (fun x => a • f x) x = iteratedFDeriv 𝕜 i (a • f) x
Theorem: iteratedFDeriv_const_smul_apply'
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
i : ℕ
a : 𝕜'
f : E → F
x : E
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedFDeriv 𝕜 i (fun x => a • f x) x = iteratedFDeriv 𝕜 i (a • f) x
Tactic:
rfl
Proof state after:
no goals
Theorem: SchwartzMap.iteratedDeriv_eq_iteratedPDeriv
Proof state before:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ iteratedDeriv n (⇑f) x = ((iteratedPDeriv ℝ fun x => 1) f) x
Tactic:
simp [iteratedDeriv_eq_iteratedFDeriv, iteratedPDeriv_eq_iteratedFDeriv]
Proof state after:
no goals
Theorem: HasDerivAt.comp_of_tower
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
g' : 𝕜'
f' : F
hf : HasDerivAt f f' (g x)
hg : HasDerivAt g g' x
⊢ HasDerivAt (fun x => f (g x)) (g' • f') x
Tactic:
rw [hasDerivAt_iff_hasFDerivAt] at hf hg ⊢
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ HasFDerivAt (fun x => f (g x)) (ContinuousLinearMap.smulRight 1 (g' • f')) x
Theorem: HasDerivAt.comp_of_tower
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ HasFDerivAt (fun x => f (g x)) (ContinuousLinearMap.smulRight 1 (g' • f')) x
Tactic:
refine HasFDerivAt.congr_fderiv (HasFDerivAt.comp x (hf.restrictScalars 𝕜) hg) ?_
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
      (ContinuousLinearMap.smulRight 1 g') =
    ContinuousLinearMap.smulRight 1 (g' • f')
Theorem: HasDerivAt.comp_of_tower
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
      (ContinuousLinearMap.smulRight 1 g') =
    ContinuousLinearMap.smulRight 1 (g' • f')
Tactic:
refine ContinuousLinearMap.ext ?_
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ ∀ (x : 𝕜),
    (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
          (ContinuousLinearMap.smulRight 1 g'))
        x =
      (ContinuousLinearMap.smulRight 1 (g' • f')) x
Theorem: HasDerivAt.comp_of_tower
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
⊢ ∀ (x : 𝕜),
    (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
          (ContinuousLinearMap.smulRight 1 g'))
        x =
      (ContinuousLinearMap.smulRight 1 (g' • f')) x
Tactic:
intro m
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
m : 𝕜
⊢ (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
        (ContinuousLinearMap.smulRight 1 g'))
      m =
    (ContinuousLinearMap.smulRight 1 (g' • f')) m
Theorem: HasDerivAt.comp_of_tower
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
g' : 𝕜'
f' : F
hf : HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') (g x)
hg : HasFDerivAt g (ContinuousLinearMap.smulRight 1 g') x
m : 𝕜
⊢ (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.smulRight 1 f'))
        (ContinuousLinearMap.smulRight 1 g'))
      m =
    (ContinuousLinearMap.smulRight 1 (g' • f')) m
Tactic:
simp
Proof state after:
no goals
Theorem: deriv.comp_of_tower
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
⊢ deriv (fun x => f (g x)) x = deriv g x • deriv f (g x)
Tactic:
rw [← hasDerivAt_deriv_iff] at hf hg
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
hf : HasDerivAt f (deriv f (g x)) (g x)
hg : HasDerivAt g (deriv g x) x
⊢ deriv (fun x => f (g x)) x = deriv g x • deriv f (g x)
Theorem: deriv.comp_of_tower
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
g : 𝕜 → 𝕜'
f : 𝕜' → F
hf : HasDerivAt f (deriv f (g x)) (g x)
hg : HasDerivAt g (deriv g x) x
⊢ deriv (fun x => f (g x)) x = deriv g x • deriv f (g x)
Tactic:
exact (HasDerivAt.comp_of_tower x hf hg).deriv
Proof state after:
no goals
Theorem: HasDerivAt.of_deriv
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f f' : 𝕜 → F
h : DifferentiableAt 𝕜 f x
h' : _root_.deriv f x = f' x
⊢ HasDerivAt f (f' x) x
Tactic:
rw [← h']
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f f' : 𝕜 → F
h : DifferentiableAt 𝕜 f x
h' : _root_.deriv f x = f' x
⊢ HasDerivAt f (_root_.deriv f x) x