theorem
proved
quartic_second_derivative
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.GeneralizedDAlembert.SecondDerivative on GitHub at line 22.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
19namespace GeneralizedDAlembert
20namespace SecondDerivative
21
22private theorem quartic_second_derivative :
23 deriv (deriv (fun t : ℝ => t^4)) = fun t => 12*t^2 := by
24 funext t
25 rw [show deriv (fun t : ℝ => t^4) = fun t => 4*t^3 by
26 funext x
27 norm_num [deriv_pow]]
28 rw [show deriv (fun t : ℝ => 4*t^3) t = 4 * (3*t^2) by
29 norm_num [deriv_const_mul, deriv_pow]]
30 ring
31
32theorem quartic_not_aczel_second_derivative_identity :
33 ¬ AczelSecondDerivativeIdentity (fun t : ℝ => t^4) := by
34 intro h
35 rcases h with ⟨ψ, hψ⟩
36 have h1 := hψ 1
37 rw [quartic_second_derivative] at h1
38 norm_num at h1
39
40end SecondDerivative
41end GeneralizedDAlembert
42end Foundation
43end IndisputableMonolith