hasFTaylorSeriesUpToOn_succ_nat_iff_right

English

For natural numbers n, HasFTaylorSeriesUpToOn (n+1) f p s is equivalent to HasFTaylorSeriesUpToOn n f p s plus a derivative condition for the n-th term and continuity of the (n+1)-st term.

Русский

Для натурального n HasFTaylorSeriesUpToOn (n+1) f p s эквивалентно HasFTaylorSeriesUpToOn n f p s плюс условие производной для n-й термы и непрерывность (n+1)-й термы.

LaTeX

$$$$\text{HasFTaylorSeriesUpToOn}(n+1,f,p,s) \iff \Big(\text{HasFTaylorSeriesUpToOn}(n,f,p,s) \land \Big( \forall x\in s, \text{HasFDerivWithinAt}(\lambda y, p y n, s, x)\Big) \land \text{ContinuousOn}(\lambda x, p x (n+1), s)\Big)$$$$

Lean4

/-- `p` is a Taylor series of `f` up to `n+1` if and only if `p.shift` is a Taylor series up to `n`
for `p 1`, which is a derivative of `f`. Version for `n : ℕ`. -/
theorem hasFTaylorSeriesUpToOn_succ_nat_iff_right {n : ℕ} :
    HasFTaylorSeriesUpToOn (n + 1 : ℕ) f p s ↔
      (∀ x ∈ s, (p x 0).curry0 = f x) ∧
        (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
          HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) (fun x => (p x).shift) s :=
  by
  constructor
  · intro H
    refine ⟨H.zero_eq, H.fderivWithin 0 (Nat.cast_lt.2 (Nat.succ_pos n)), ?_⟩
    exact H.shift_of_succ
  · rintro ⟨Hzero_eq, Hfderiv_zero, Htaylor⟩
    constructor
    · exact Hzero_eq
    · intro m (hm : (m : WithTop ℕ∞) < n.succ) x (hx : x ∈ s)
      rcases m with - | m
      · exact Hfderiv_zero x hx
      · have A : (m : WithTop ℕ∞) < n := by
          rw [Nat.cast_lt] at hm ⊢
          exact Nat.lt_of_succ_lt_succ hm
        have :
          HasFDerivWithinAt (𝕜 := 𝕜) (continuousMultilinearCurryRightEquiv' 𝕜 m E F ∘ (p · m.succ))
            ((p x).shift m.succ).curryLeft s x :=
          Htaylor.fderivWithin _ A x hx
        rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff' (f' := ((p x).shift m.succ).curryLeft)] at this
        convert this
        ext y v
        change (p x (Nat.succ (Nat.succ m))) (cons y v) = (p x m.succ.succ) (snoc (cons y (init v)) (v (last _)))
        rw [← cons_snoc_eq_snoc_cons, snoc_init_self]
    · intro m (hm : (m : WithTop ℕ∞) ≤ n.succ)
      rcases m with - | m
      · have : DifferentiableOn 𝕜 (fun x => p x 0) s := fun x hx => (Hfderiv_zero x hx).differentiableWithinAt
        exact this.continuousOn
      · refine (continuousMultilinearCurryRightEquiv' 𝕜 m E F).comp_continuousOn_iff.mp ?_
        refine Htaylor.cont _ ?_
        rw [Nat.cast_le] at hm ⊢
        exact Nat.lt_succ_iff.mp hm

Похожие утверждения