Taylor

📁 Source: Mathlib/Analysis/Calculus/Taylor.lean

Statistics

Metric	Count
Definitions `taylorCoeffWithin`, `taylorWithin`, `taylorWithinEval`	3
Theorems `taylor_tendsto`, `continuousOn_taylorWithinEval`, `exists_taylor_mean_remainder_bound`, `hasDerivAt_taylorWithinEval_succ`, `hasDerivWithinAt_taylorWithinEval`, `hasDerivWithinAt_taylorWithinEval_at_Icc`, `hasDerivWithinAt_taylor_coeff_within`, `monomial_has_deriv_aux`, `taylorWithinEval_hasDerivAt_Ioo`, `taylorWithinEval_self`, `taylorWithinEval_succ`, `taylorWithin_succ`, `taylor_integral_remainder`, `taylor_integral_remainder_aux`, `taylor_integral_remainder_of_absolutelyContinuous`, `taylor_isLittleO`, `taylor_isLittleO_univ`, `taylor_mean_remainder`, `taylor_mean_remainder_bound`, `taylor_mean_remainder_cauchy`, `taylor_mean_remainder_lagrange`, `taylor_mean_remainder_lagrange_iteratedDeriv`, `taylor_tendsto`, `taylor_within_apply`, `taylor_within_zero_eval`	25
Total	28

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`taylor_tendsto` 📖	mathematical	`Convex` `Real` `semiring` `partialOrder` `instAddCommMonoid` `Algebra.toSMul` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set` `Set.instMembership` `ContDiffOn` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast`	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `instSub` `taylorWithinEval` `normedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Monoid.toPow` `instMonoid` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `nhds` `instZero`	—	`div_eq_inv_mul` `taylor_tendsto`

(root)

Definitions

Name	Category	Theorems
`taylorCoeffWithin` 📖	CompOp	1 math math: `taylorWithin_succ`
`taylorWithin` 📖	CompOp	1 math math: `taylorWithin_succ`
`taylorWithinEval` 📖	CompOp	25 math math: `taylor_integral_remainder`, `taylorWithinEval_hasDerivAt_Ioo`, `hasDerivWithinAt_taylorWithinEval`, `taylor_within_zero_eval`, `taylor_integral_remainder_of_absolutelyContinuous`, `taylor_tendsto`, `taylor_mean_remainder_lagrange_iteratedDeriv`, `taylor_isLittleO_univ`, `taylor_mean_remainder`, `hasDerivWithinAt_taylorWithinEval_at_Icc`, `exists_taylor_mean_remainder_bound`, `hasDerivAt_taylorWithinEval_succ`, `taylorWithinEval_succ`, `Real.taylor_tendsto`, `taylor_isLittleO`, `MeasureTheory.taylorWithinEval_charFun_two_zero`, `taylor_integral_remainder_aux`, `taylorWithinEval_self`, `MeasureTheory.taylorWithinEval_charFun_two_zero'`, `taylor_mean_remainder_cauchy`, `taylor_mean_remainder_bound`, `continuousOn_taylorWithinEval`, `taylor_mean_remainder_lagrange`, `taylor_within_apply`, `MeasureTheory.taylorWithinEval_charFun_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn_taylorWithinEval` 📖	mathematical	`UniqueDiffOn` `Real` `Real.semiring` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContDiffOn` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast`	`ContinuousOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `taylorWithinEval`	—	`taylor_within_apply` `continuousOn_finset_sum` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousOn.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `ContinuousOn.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuousOn_const` `ContinuousOn.pow` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `continuousOn_id` `contDiffOn_nat_iff_continuousOn_differentiableOn_deriv`
`exists_taylor_mean_remainder_bound` 📖	mathematical	`Real` `Real.instLE` `ContDiffOn` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.add` `instAddENat` `WithTop.natCast` `ENat.instNatCast` `WithTop.one` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat` `Set.Icc` `Real.instPreorder`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `taylorWithinEval` `Set.Icc` `Real.instPreorder` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Real.instSub`	—	`eq_or_lt_of_le` `Set.Icc_self` `taylorWithinEval_self` `sub_self` `norm_zero` `zero_pow` `MulZeroClass.mul_zero` `instReflLe` `div_mul_eq_mul_div₀` `taylor_mean_remainder_bound` `ContinuousOn.le_sSup_image_Icc` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `ContinuousOn.norm` `ContDiffOn.continuousOn_iteratedDerivWithin` `Eq.le` `uniqueDiffOn_Icc`
`hasDerivAt_taylorWithinEval_succ` 📖	mathematical	—	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `taylorWithinEval` `derivWithin`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasDerivAt.congr_simp` `taylor_within_apply` `HasDerivAt.smul_const` `IsScalarTower.left` `HasDerivAt.const_mul` `HasDerivAt.pow` `HasDerivAt.sub_const` `hasDerivAt_id` `HasDerivAt.congr_deriv` `HasDerivAt.fun_sum` `Finset.sum_range_succ'` `Nat.cast_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `zero_smul` `add_zero` `Finset.sum_congr` `iteratedDerivWithin_succ'` `Nat.cast_mul` `Nat.cast_add` `Nat.cast_one` `mul_inv_rev` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Real.instIsOrderedAddMonoid` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Nat.cast_pos'` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.factorial_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`hasDerivWithinAt_taylorWithinEval` 📖	mathematical	`UniqueDiffOn` `Real` `Real.semiring` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.instMembership` `Set.instHasSubset` `ContDiffOn` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast` `DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `iteratedDerivWithin`	`HasDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `taylorWithinEval` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instMonoid` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `Real.instMul` `Real.instInv` `Real.instNatCast` `Nat.factorial` `Monoid.toPow` `Real.instSub` `iteratedDerivWithin`	—	`UniqueDiffWithinAt.mono_nhds` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `nhdsWithin_le_iff` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasDerivWithinAt.congr_simp` `taylor_within_zero_eval` `Nat.cast_one` `inv_one` `pow_zero` `mul_one` `zero_add` `one_smul` `iteratedDerivWithin_one` `HasDerivWithinAt.mono` `DifferentiableWithinAt.hasDerivWithinAt` `iteratedDerivWithin_zero` `taylorWithinEval_succ` `add_zero` `Nat.cast_mul` `Nat.cast_add` `Nat.cast_lt` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithTop.charZero` `Nat.instCharZero` `DifferentiableOn.mono` `ContDiffOn.differentiableOn_iteratedDerivWithin` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `add_sub_cancel` `HasDerivWithinAt.add` `ContDiffOn.of_succ` `DifferentiableWithinAt.mono_of_mem_nhdsWithin` `hasDerivWithinAt_taylor_coeff_within` `nhdsWithin_mono` `self_mem_nhdsWithin`
`hasDerivWithinAt_taylorWithinEval_at_Icc` 📖	mathematical	`Real` `Real.instLT` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `ContDiffOn` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast` `DifferentiableOn` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `iteratedDerivWithin`	`HasDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `taylorWithinEval` `Set.Icc` `Real.instPreorder` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instMonoid` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `Real.instMul` `Real.instInv` `Real.instNatCast` `Nat.factorial` `Monoid.toPow` `Real.instSub` `iteratedDerivWithin`	—	`hasDerivWithinAt_taylorWithinEval` `uniqueDiffOn_Icc` `self_mem_nhdsWithin` `Eq.subset` `Set.instReflSubset`
`hasDerivWithinAt_taylor_coeff_within` 📖	mathematical	`UniqueDiffWithinAt` `Real` `Real.semiring` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `DifferentiableWithinAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `iteratedDerivWithin`	`HasDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instMonoid` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `Real.instMul` `Real.instInv` `Real.instAdd` `Real.instNatCast` `Real.instOne` `Nat.factorial` `Monoid.toPow` `Real.instSub` `iteratedDerivWithin` `SubNegMonoid.toSub` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `iteratedDerivWithin_succ` `derivWithin_of_mem_nhdsWithin` `DifferentiableWithinAt.hasDerivWithinAt` `DifferentiableWithinAt.mono_of_mem_nhdsWithin` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `mul_neg` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `neg_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Nat.cast_pos'` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.factorial_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `HasDerivWithinAt.const_mul` `HasDerivAt.hasDerivWithinAt` `monomial_has_deriv_aux` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `zero_add` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `HasDerivWithinAt.smul` `IsScalarTower.left`
`monomial_has_deriv_aux` 📖	mathematical	—	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `Monoid.toPow` `Real.instMonoid` `Real.instSub` `Real.instMul` `Real.instNeg` `Real.instNatCast` `Real.instOne`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasDerivAt.congr_simp` `sub_eq_neg_add` `neg_one_mul` `mul_comm` `mul_assoc` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Nat.cast_add` `Nat.cast_one` `HasDerivAt.pow` `HasDerivAt.add_const` `HasDerivAt.neg` `hasDerivAt_id`
`taylorWithinEval_hasDerivAt_Ioo` 📖	mathematical	`Real` `Real.instLT` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `ContDiffOn` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast` `Set.Icc` `DifferentiableOn` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `iteratedDerivWithin`	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `taylorWithinEval` `Set.Icc` `Real.instPreorder` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instMonoid` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `Real.instMul` `Real.instInv` `Real.instNatCast` `Nat.factorial` `Monoid.toPow` `Real.instSub` `iteratedDerivWithin`	—	`IsOpen.mem_nhds` `isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `nhdsWithin_le_nhds` `HasDerivWithinAt.hasDerivAt` `hasDerivWithinAt_taylorWithinEval` `uniqueDiffOn_Icc` `Set.Ioo_subset_Icc_self` `DifferentiableWithinAt.mono_of_mem_nhdsWithin`
`taylorWithinEval_self` 📖	mathematical	—	`taylorWithinEval`	—	`taylor_within_zero_eval` `taylorWithinEval_succ` `mul_inv_rev` `sub_self` `zero_pow` `MulZeroClass.mul_zero` `zero_smul` `add_zero`
`taylorWithinEval_succ` 📖	mathematical	—	`taylorWithinEval` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Real.instMul` `Real.instInv` `Real.instAdd` `Real.instNatCast` `Real.instOne` `Nat.factorial` `Monoid.toPow` `Real.instSub` `iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField`	—	`taylorWithin_succ` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `PolynomialModule.comp_eval` `Polynomial.eval_sub` `Polynomial.eval_X` `Polynomial.eval_C` `PolynomialModule.eval_single` `mul_inv_rev` `SemigroupAction.mul_smul` `mul_comm` `Nat.factorial_succ` `Nat.cast_mul` `Nat.cast_add` `Nat.cast_one`
`taylorWithin_succ` 📖	mathematical	—	`taylorWithin` `PolynomialModule` `Real` `Real.commRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `instAddCommGroupPolynomialModule` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PolynomialModule.instModule` `LinearMap.instFunLike` `PolynomialModule.comp` `Polynomial` `Real.semiring` `Polynomial.instSub` `Real.instRing` `Polynomial.X` `RingHom` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `PolynomialModule.single` `taylorCoeffWithin`	—	`Finset.sum_range_succ`
`taylor_integral_remainder` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast` `Set.uIcc` `Real.lattice`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `taylorWithinEval` `Set.uIcc` `Real` `Real.lattice` `intervalIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toPow` `Real.instSub` `Real.instNatCast` `Nat.factorial` `iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`eq_or_ne` `Set.uIcc_of_le` `instReflLe` `Set.Icc_self` `taylorWithinEval_self` `sub_self` `intervalIntegral.integral_same` `uniqueDiffOn_Icc` `taylor_integral_remainder_aux` `intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt` `IsScalarTower.left` `Continuous.comp_continuousOn'` `Continuous.div_const` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `continuous_id'` `Continuous.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `continuousOn_const` `continuousOn_id'` `ContDiffOn.continuousOn_iteratedDerivWithin` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `WithTop.charZero` `DifferentiableAt.hasDerivAt` `DifferentiableAt.div_const` `DifferentiableAt.fun_pow` `DifferentiableAt.const_sub` `differentiableAt_id` `DifferentiableOn.hasDerivAt` `DifferentiableOn.mono` `ContDiffOn.differentiableOn_iteratedDerivWithin` `ContinuousOn.intervalIntegrable` `Real.locallyFinite_volume` `Continuous.continuousOn` `ContDiff.continuous_deriv_one` `ContDiff.div_const` `ContDiff.pow` `ContDiff.sub` `contDiff_const` `contDiff_fun_id` `IntervalIntegrable.congr_ae` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.eq_1` `MeasureTheory.ae_restrict_iff'` `measurableSet_uIoc` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.mp_mem` `MeasureTheory.Measure.ae_ne` `Real.noAtoms_volume` `Filter.univ_mem'` `iteratedDerivWithin_succ`
`taylor_integral_remainder_aux` 📖	mathematical	`intervalIntegral` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `iteratedDerivWithin` `Set.uIcc` `Real.lattice` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toPow` `Real.instSub` `Real.instNatCast` `Nat.factorial`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `taylorWithinEval` `Set.uIcc` `Real` `Real.lattice` `intervalIntegral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toPow` `Real.instSub` `Real.instNatCast` `Nat.factorial` `iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`eq_or_ne` `Set.uIcc_of_le` `instReflLe` `Set.Icc_self` `taylorWithinEval_self` `sub_self` `intervalIntegral.integral_same` `taylor_within_zero_eval` `pow_zero` `Nat.cast_one` `div_self` `NeZero.charZero_one` `RCLike.charZero_rclike` `zero_add` `iteratedDerivWithin_one` `one_smul` `Nat.instCanonicallyOrderedAdd` `deriv_div_const` `iteratedDerivWithin_zero` `deriv_const'` `div_one` `zero_smul` `intervalIntegral.integral_zero` `sub_zero` `intervalIntegral.integral_congr_ae` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.ae_ne` `Real.noAtoms_volume` `Filter.univ_mem'` `uniqueDiffOn_Icc` `taylorWithinEval_succ` `mul_inv_rev` `sub_add_eq_sub_sub` `Nat.cast_mul` `Nat.cast_add` `le_refl` `zero_pow` `zero_div` `zero_sub` `intervalIntegral.integral_neg` `deriv_fun_pow` `DifferentiableAt.const_sub` `differentiableAt_id` `deriv_const_sub` `deriv_id''` `neg_smul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.factorial_pos` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `mul_neg` `neg_div` `neg_neg` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `iteratedDerivWithin_succ` `Nat.factorial.eq_2`
`taylor_integral_remainder_of_absolutelyContinuous` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast` `Set.uIcc` `Real.lattice` `AbsolutelyContinuousOnInterval` `Real.pseudoMetricSpace` `iteratedDerivWithin`	`Real` `Real.instSub` `taylorWithinEval` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Set.uIcc` `Real.lattice` `intervalIntegral` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.factorial` `iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace`	—	`eq_or_ne` `Set.uIcc_of_le` `instReflLe` `Set.Icc_self` `taylorWithinEval_self` `sub_self` `intervalIntegral.integral_same` `taylor_integral_remainder_aux` `AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul` `ContDiffOn.absolutelyContinuousOnInterval` `ContDiffOn.div_const` `ContDiffOn.pow` `ContDiffOn.sub` `contDiffOn_const` `contDiffOn_fun_id` `LE.le.eq_or_lt` `uniqueDiffOn_Icc` `ContDiffOn.of_le` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `WithTop.charZero`
`taylor_isLittleO` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set` `Set.instMembership` `ContDiffOn` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast`	`Asymptotics.IsLittleO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `taylorWithinEval` `Monoid.toPow` `Real.instMonoid` `Real.instSub`	—	`taylor_within_zero_eval` `pow_zero` `NormedDivisionRing.to_normOneClass` `tendsto_sub_nhds_zero_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousOn.continuousWithinAt` `ContDiffOn.continuousOn` `Set.eq_singleton_or_nontrivial` `nhdsWithin_singleton` `taylorWithinEval_succ` `mul_inv_rev` `taylorWithinEval_self` `sub_self` `zero_pow` `MulZeroClass.mul_zero` `zero_smul` `add_zero` `uniqueDiffOn_convex` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instIsTopologicalAddGroupReal` `Convex.nontrivial_iff_nonempty_interior` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `sub_zero` `Convex.isLittleO_pow_succ_real` `HasDerivWithinAt.sub` `DifferentiableWithinAt.hasDerivWithinAt` `ContDiffOn.differentiableOn` `Nat.cast_add` `Nat.cast_one` `Unique.instSubsingleton` `WithTop.canonicallyOrderedAdd` `WithTop.charZero` `NeZero.charZero_one` `HasDerivAt.hasDerivWithinAt` `hasDerivAt_taylorWithinEval_succ` `ContDiffOn.derivWithin` `le_rfl`
`taylor_isLittleO_univ` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast`	`Asymptotics.IsLittleO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `taylorWithinEval` `Set.univ` `Monoid.toPow` `Real.instMonoid` `Real.instSub`	—	`nhdsWithin_univ` `taylor_isLittleO` `convex_univ` `Set.mem_univ` `ContDiff.contDiffOn`
`taylor_mean_remainder` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast` `Set.uIcc` `Real.lattice` `DifferentiableOn` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `iteratedDerivWithin` `Set.uIoo` `Real.linearOrder` `ContinuousOn` `HasDerivAt` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal`	`Real` `Set` `Set.instMembership` `Set.uIoo` `Real.linearOrder` `Real.instSub` `taylorWithinEval` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Set.uIcc` `Real.lattice` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.factorial` `iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `exists_ratio_hasDerivAt_eq_ratio_slope` `continuousOn_taylorWithinEval` `uniqueDiffOn_Icc` `taylorWithinEval_hasDerivAt_Ioo`
`taylor_mean_remainder_bound` 📖	mathematical	`Real` `Real.instLE` `ContDiffOn` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.add` `instAddENat` `WithTop.natCast` `ENat.instNatCast` `WithTop.one` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat` `Set.Icc` `Real.instPreorder` `Set` `Set.instMembership` `Norm.norm` `NormedAddCommGroup.toNorm` `iteratedDerivWithin`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `taylorWithinEval` `Set.Icc` `Real.instPreorder` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Real.instSub` `Real.instNatCast` `Nat.factorial`	—	`eq_or_lt_of_le` `Set.mem_singleton_iff` `Set.Icc_self` `taylorWithinEval_self` `sub_self` `norm_zero` `zero_pow` `MulZeroClass.mul_zero` `zero_div` `instReflLe` `ContDiffOn.differentiableOn_iteratedDerivWithin` `Nat.cast_one` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `WithTop.charZero` `uniqueDiffOn_Icc` `norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_eq_abs` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `abs_mul` `abs_pow` `abs_inv` `Real.instIsStrictOrderedRing` `Nat.abs_cast` `mul_le_mul_of_nonneg_left` `pow_le_pow_left₀` `abs_nonneg` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `abs_le_abs_of_nonneg` `sub_nonneg` `LT.lt.le` `sub_le_sub_left` `le_of_lt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_pos'` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.factorial_pos` `LE.le.trans` `norm_nonneg` `mul_nonneg` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Set.Icc_subset_Icc_right` `HasDerivWithinAt.mono` `hasDerivWithinAt_taylorWithinEval_at_Icc` `ContDiffOn.of_succ` `norm_image_sub_le_of_norm_deriv_le_segment'` `Set.right_mem_Icc` `LE.le.trans_eq` `abs_of_nonneg` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.div_pf`
`taylor_mean_remainder_cauchy` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast` `Set.uIcc` `Real.lattice` `DifferentiableOn` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `iteratedDerivWithin` `Set.uIoo` `Real.linearOrder`	`Real` `Set` `Set.instMembership` `Set.uIoo` `Real.linearOrder` `Real.instSub` `taylorWithinEval` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Set.uIcc` `Real.lattice` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.factorial`	—	`continuousOn_id'` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `hasDerivAt_id` `taylor_mean_remainder` `NeZero.charZero_one` `RCLike.charZero_rclike` `div_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `Nat.factorial_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`taylor_mean_remainder_lagrange` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast` `Set.uIcc` `Real.lattice` `DifferentiableOn` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `iteratedDerivWithin` `Set.uIoo` `Real.linearOrder`	`Real` `Set` `Set.instMembership` `Set.uIoo` `Real.linearOrder` `Real.instSub` `taylorWithinEval` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Set.uIcc` `Real.lattice` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.factorial`	—	`Continuous.comp_continuousOn'` `Continuous.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_id'` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `continuousOn_const` `continuousOn_id'` `mul_ne_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `neg_ne_zero` `Nat.cast_add_one_ne_zero` `RCLike.charZero_rclike` `taylor_mean_remainder` `monomial_has_deriv_aux` `sub_self` `zero_pow` `zero_sub` `mul_neg` `neg_div` `div_neg` `neg_mul` `neg_neg` `Nat.cast_mul` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_pos'` `NeZero.charZero_one` `Nat.factorial_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`taylor_mean_remainder_lagrange_iteratedDeriv` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.add` `instAddENat` `WithTop.natCast` `ENat.instNatCast` `WithTop.one` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat` `Set.uIcc` `Real.lattice`	`Real` `Set` `Set.instMembership` `Set.uIoo` `Real.linearOrder` `Real.instSub` `taylorWithinEval` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Set.uIcc` `Real.lattice` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.factorial`	—	`uniqueDiffOn_Icc` `ContDiffOn.differentiableOn_iteratedDerivWithin` `Nat.cast_one` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `WithTop.charZero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `taylor_mean_remainder_lagrange` `ContDiffOn.of_succ` `DifferentiableOn.mono` `Set.Ioo_subset_Icc_self` `iteratedDeriv_eq_iteratedFDeriv` `iteratedDerivWithin_eq_iteratedFDerivWithin` `iteratedFDerivWithin_eq_iteratedFDeriv` `ContDiffOn.contDiffAt` `Icc_mem_nhds_iff` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instNoMaxOrderOfNontrivial` `le_of_lt`
`taylor_tendsto` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set` `Set.instMembership` `ContDiffOn` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast`	`Filter.Tendsto` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `Monoid.toPow` `Real.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `taylorWithinEval` `nhdsWithin` `Real.pseudoMetricSpace` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Asymptotics.IsLittleO.norm_norm` `taylor_isLittleO` `tendsto_zero_iff_norm_tendsto_zero` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `div_eq_inv_mul` `Asymptotics.isLittleO_iff_tendsto` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `Real.instNontrivial` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `sub_eq_zero` `taylorWithinEval_self` `sub_self`
`taylor_within_apply` 📖	mathematical	—	`taylorWithinEval` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Real.instMul` `Real.instInv` `Real.instNatCast` `Nat.factorial` `Monoid.toPow` `Real.instSub` `iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField`	—	`taylor_within_zero_eval` `Finset.sum_congr` `zero_add` `Finset.sum_singleton` `Nat.cast_one` `inv_one` `pow_zero` `mul_one` `iteratedDerivWithin_zero` `one_smul` `taylorWithinEval_succ` `Finset.sum_range_succ` `mul_inv_rev` `Nat.cast_mul` `Nat.cast_add`
`taylor_within_zero_eval` 📖	mathematical	—	`taylorWithinEval`	—	`Finset.sum_congr` `zero_add` `PolynomialModule.map_single` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `PolynomialModule.eval_single` `Finset.sum_singleton` `pow_zero` `Nat.cast_one` `inv_one` `iteratedDerivWithin_zero` `one_smul` `PolynomialModule.eval_lsingle`

---

← Back to Index