lemma proved tactic proof

`taylorWithinEval_one_univ`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 616lemma taylorWithinEval_one_univ (H : ℝ → ℝ) (x : ℝ) :
 617  taylorWithinEval H 1 Set.univ 0 x = H 0 + deriv H 0 * x := by

proof body

Tactic-mode proof.

 618  have h := taylorWithinEval_succ_real H 0 0 x
 619  -- simplify the Taylor term at order 1
 620  have h' :
 621      taylorWithinEval H 1 Set.univ 0 x = H 0 + x * deriv H 0 := by
 622    simp [taylor_within_zero_eval, iteratedDerivWithin_univ, iteratedDerivWithin_one,
 623      iteratedDeriv_one, derivWithin_univ, sub_eq_add_neg] at h
 624    simpa [mul_comm] using h
 625  simpa [mul_comm] using h'
 626

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

taylorWithinEval_two_univ in IndisputableMonolith.Cost.FunctionalEquation decl_use

depends on (3)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
taylorWithinEval_succ_real in IndisputableMonolith.Cost.FunctionalEquation decl_use