Theorem: Function.hasTemperateGrowth_innerSL (ForML/IntegralAgainst.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ HasTemperateGrowth fun x => (innerSL ℝ) x
Tactic:
refine ⟨contDiff_const.clm_apply contDiff_id, ?_⟩
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro n
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨1, 1, ?_⟩
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 * (1 + ‖x‖) ^ 1

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 * (1 + ‖x‖) ^ 1
Tactic:
intro x
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 * (1 + ‖x‖) ^ 1

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 * (1 + ‖x‖) ^ 1
Tactic:
simp
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 + ‖x‖

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 + ‖x‖
Tactic:
cases n with
| zero => simp
| succ n =>
  simp [iteratedFDeriv_succ_eq_comp_right]
  simp_rw [fderiv_innerSL_apply]
  cases n with
  | zero =>
    simp
    refine le_trans (norm_innerSL_le_one ℝ) (by simp)
  | succ n =>
    rw [iteratedFDeriv_const_of_ne]
    . change ‖0‖ ≤ _
      simp
    . simp
State after:
no goals

State before:
case zero
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ‖iteratedFDeriv ℝ Nat.zero (fun x => (innerSL ℝ) x) x‖ ≤ 1 + ‖x‖
Tactic:
simp
State after:
no goals

State before:
case succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ (Nat.succ n) (fun x => (innerSL ℝ) x) x‖ ≤ 1 + ‖x‖
Tactic:
simp [iteratedFDeriv_succ_eq_comp_right]
State after:
case succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ n (fun y => fderiv ℝ (fun x => (innerSL ℝ) x) y) x‖ ≤ 1 + ‖x‖

State before:
case succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ n (fun y => fderiv ℝ (fun x => (innerSL ℝ) x) y) x‖ ≤ 1 + ‖x‖
Tactic:
simp_rw [fderiv_innerSL_apply]
State after:
case succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ n (fun y => innerSL ℝ) x‖ ≤ 1 + ‖x‖

State before:
case succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ n (fun y => innerSL ℝ) x‖ ≤ 1 + ‖x‖
Tactic:
cases n with
| zero =>
  simp
  refine le_trans (norm_innerSL_le_one ℝ) (by simp)
| succ n =>
  rw [iteratedFDeriv_const_of_ne]
  . change ‖0‖ ≤ _
    simp
  . simp
State after:
no goals

State before:
case succ.zero
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ‖iteratedFDeriv ℝ Nat.zero (fun y => innerSL ℝ) x‖ ≤ 1 + ‖x‖
Tactic:
simp
State after:
case succ.zero
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ‖innerSL ℝ‖ ≤ 1 + ‖x‖

State before:
case succ.zero
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ‖innerSL ℝ‖ ≤ 1 + ‖x‖
Tactic:
refine le_trans (norm_innerSL_le_one ℝ) (by simp)
State after:
no goals

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ 1 ≤ 1 + ‖x‖
Tactic:
simp
State after:
no goals

State before:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ (Nat.succ n) (fun y => innerSL ℝ) x‖ ≤ 1 + ‖x‖
Tactic:
rw [iteratedFDeriv_const_of_ne]
State after:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖0 x‖ ≤ 1 + ‖x‖

case succ.succ.hn
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ Nat.succ n ≠ 0

State before:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖0 x‖ ≤ 1 + ‖x‖

case succ.succ.hn
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ Nat.succ n ≠ 0
Tactic:
. change ‖0‖ ≤ _
  simp
State after:
case succ.succ.hn
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ Nat.succ n ≠ 0

State before:
case succ.succ.hn
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ Nat.succ n ≠ 0
Tactic:
. simp
State after:
no goals

State before:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖0 x‖ ≤ 1 + ‖x‖
Tactic:
change ‖0‖ ≤ _
State after:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖0‖ ≤ 1 + ‖x‖

State before:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖0‖ ≤ 1 + ‖x‖
Tactic:
simp
State after:
no goals

State before:
case succ.succ.hn
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ Nat.succ n ≠ 0
Tactic:
simp
State after:
no goals