hasFTaylorSeriesUpToOn_succ_iff_left

English

If hN holds for top order, HasFTaylorSeriesUpToOn N f p s is equivalent to HasFTaylorSeriesUpToOn N (shifted) with p shifted and derivative data.

Русский

Если верно условие для верхнего порядка, HasFTaylorSeriesUpToOn N f p s эквивалентно HasFTaylorSeriesUpToOn N (сдвинутому) с p shift и данными производной.

LaTeX

$$$$\text{HasFTaylorSeriesUpToOn}(N,f,p,s) \iff \Big(\forall x\in s, (p x 0).\text{curry0} = f x\Big) \land \Big(\forall x\in s, HasFDerivWithinAt (\lambda y, p y 0) (p x 1).\text{curryLeft} s x\Big) \land \text{HasFTaylorSeriesUpToOn}(N, (\lambda x, \text{continuousMultilinearCurryFin1}(p x 1)), (\lambda x, (p x).shift), s\Big).$$$$

Lean4

/-- `p` is a Taylor series of `f` up to `n+1` if and only if `p` is a Taylor series up to `n`, and
`p (n + 1)` is a derivative of `p n`. -/
theorem hasFTaylorSeriesUpToOn_succ_iff_left {n : ℕ} :
    HasFTaylorSeriesUpToOn (n + 1) f p s ↔
      HasFTaylorSeriesUpToOn n f p s ∧
        (∀ x ∈ s, HasFDerivWithinAt (fun y => p y n) (p x n.succ).curryLeft s x) ∧
          ContinuousOn (fun x => p x (n + 1)) s :=
  by
  constructor
  · exact fun h ↦ ⟨h.of_le (mod_cast Nat.le_succ n), h.fderivWithin _ (mod_cast lt_add_one n), h.cont (n + 1) le_rfl⟩
  · intro h
    constructor
    · exact h.1.zero_eq
    · intro m hm
      by_cases h' : m < n
      · exact h.1.fderivWithin m (mod_cast h')
      · have : m = n := Nat.eq_of_lt_succ_of_not_lt (mod_cast hm) h'
        rw [this]
        exact h.2.1
    · intro m hm
      by_cases h' : m ≤ n
      · apply h.1.cont m (mod_cast h')
      · have : m = n + 1 := le_antisymm (mod_cast hm) (not_le.1 h')
        rw [this]
        exact h.2.2

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