Mathlib Map

Theorems · Definition · real analysis

ftaylorSeries

(𝕜 : Type u) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type uF} →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → (E → F) → E → FormalMultilinearSeries 𝕜 E F

Formal Taylor series associated to a function.

Defined in
Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Cited by
11 results in Mathlib
Foundations
Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ContDiffPointwiseHolderAt.comp_of_differentiableAt · cited by 3ContDiffPointwiseHolderAt…AnalyticOnNhd.hasFTaylorSeriesUpToOn · cited by 1AnalyticOnNhd.hasFTaylorS…ContDiff.ftaylorSeries · cited by 1ContDiff.ftaylorSeriesAnalyticWithinAt.exists_hasFTaylorSeriesUpToOn · cited by 1AnalyticWithinAt.exists_h…ftaylorSeriesWithin_univ · cited by 1ftaylorSeriesWithin_univiteratedFDeriv_comp · cited by 1iteratedFDeriv_compAbsolutelyMonotoneOn.of_contDiff · cited by 0AbsolutelyMonotoneOn.of_c…Filter.EventuallyEq.ftaylorSeries · cited by 0EventuallyEq.ftaylorSeriesftaylorSeries_zero · cited by 0ftaylorSeries_zerocontDiff_iff_ftaylorSeries · cited by 0contDiff_iff_ftaylorSeriesftaylorSeries_fun_zero · cited by 0ftaylorSeries_fun_zeroNormedAddCommGroup · cited by 15752NormedAddCommGroupNormedSpace · cited by 12499NormedSpaceNontriviallyNormedField · cited by 8742NontriviallyNormedFieldFormalMultilinearSeries · cited by 615FormalMultilinearSeriesiteratedFDeriv · cited by 211iteratedFDerivftaylorSeriesCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by11

Results whose statement or proof uses this declaration.