English
If HasFTaylorSeriesUpToOn n f p s and for every m the derivatives agree on s with q, then HasFTaylorSeriesUpToOn n f q s.
Русский
Если HasFTaylorSeriesUpToOn n f p s и для каждого m производные совпадают на s с q, то HasFTaylorSeriesUpToOn n f q s.
LaTeX
$$HasFTaylorSeriesUpToOn\ n f p s → (∀ m : Nat, le m.cast n → EqOn (p · m) (q · m) s) → HasFTaylorSeriesUpToOn n f q s$$
Lean4
theorem congr_series {q} (hp : HasFTaylorSeriesUpToOn n f p s) (hpq : ∀ m : ℕ, m ≤ n → EqOn (p · m) (q · m) s) :
HasFTaylorSeriesUpToOn n f q s
where
zero_eq x hx := by simp only [← (hpq 0 (zero_le n) hx), hp.zero_eq x hx]
fderivWithin m hm x
hx := by
refine ((hp.fderivWithin m hm x hx).congr' (hpq m hm.le).symm hx).congr_fderiv ?_
refine congrArg _ (hpq (m + 1) ?_ hx)
exact ENat.add_one_natCast_le_withTop_of_lt hm
cont m hm := (hp.cont m hm).congr (hpq m hm).symm
