lemma
proved
tactic proof
taylorWithinEval_two_univ
show as:
view Lean formalization →
formal statement (Lean)
627lemma taylorWithinEval_two_univ (H : ℝ → ℝ) (x : ℝ) :
628 taylorWithinEval H 2 Set.univ 0 x =
629 H 0 + deriv H 0 * x + (deriv (deriv H) 0) / 2 * x^2 := by
proof body
Tactic-mode proof.
630 have h := taylorWithinEval_succ_real H 1 0 x
631 have h0 :
632 taylorWithinEval H 2 Set.univ 0 x =
633 taylorWithinEval H 1 Set.univ 0 x +
634 (((2 : ℝ) * (Nat.factorial 1))⁻¹ * (x - 0) ^ 2) *
635 iteratedDerivWithin 2 H Set.univ 0 := by
636 simpa [one_add_one_eq_two] using h
637 -- expand the order-2 Taylor polynomial using the order-1 formula
638 have h1 : taylorWithinEval H 1 Set.univ 0 x = H 0 + deriv H 0 * x :=
639 taylorWithinEval_one_univ H x
640 -- simplify the order-2 increment
641 have h2 : iteratedDerivWithin 2 H Set.univ 0 = deriv (deriv H) 0 := by
642 simp [iteratedDerivWithin_univ, iteratedDeriv_succ, iteratedDeriv_one]
643 -- rewrite and normalize coefficients
644 calc
645 taylorWithinEval H 2 Set.univ 0 x
646 = taylorWithinEval H 1 Set.univ 0 x +
647 (((2 : ℝ) * (Nat.factorial 1))⁻¹ * (x - 0) ^ 2) *
648 iteratedDerivWithin 2 H Set.univ 0 := by
649 exact h0
650 _ = (H 0 + deriv H 0 * x) +
651 (((2 : ℝ) * (Nat.factorial 1))⁻¹ * x^2) * (deriv (deriv H) 0) := by
652 simp [h1, h2, sub_eq_add_neg, pow_two, mul_comm, mul_left_comm, mul_assoc]
653 _ = H 0 + deriv H 0 * x + (deriv (deriv H) 0) / 2 * x^2 := by
654 simp [Nat.factorial_one, mul_comm, mul_left_comm, mul_assoc, div_eq_mul_inv]
655