Theorem: W21.norm_nonneg (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : W21
f : ℝ → ℂ
t : ℝ
⊢ 0 t ≤ ‖f t‖
Tactic:
simp
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : W21
f : ℝ → ℂ
⊢ 0 ≤ (4 * π ^ 2)⁻¹
Tactic:
positivity
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : W21
f : ℝ → ℂ
t : ℝ
⊢ 0 t ≤ ‖deriv (deriv f) t‖
Tactic:
simp
State after:
no goals