TaylorSeries

📁 Source: Mathlib/Analysis/Complex/TaylorSeries.lean

Statistics

Metric	Count
Definitions	0
Theorems hasSum_taylorSeries_of_entire, hasSum_taylorSeries_on_ball, hasSum_taylorSeries_on_eball, hasSum_taylorSeries_on_emetric_ball, taylorSeries_eq_of_entire, taylorSeries_eq_of_entire', taylorSeries_eq_on_ball, taylorSeries_eq_on_ball', taylorSeries_eq_on_eball, taylorSeries_eq_on_eball', taylorSeries_eq_on_emetric_ball, taylorSeries_eq_on_emetric_ball'	12
Total	12

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasSum_taylorSeries_of_entire 📖	mathematical	Differentiable Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	HasSum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Module.toDistribMulAction instInv instNatCast Nat.factorial Monoid.toNatPow instSub iteratedDeriv SummationFilter.unconditional	—	hasSum_taylorSeries_on_eball Differentiable.differentiableOn Metric.mem_eball edist_lt_top
hasSum_taylorSeries_on_ball 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Metric.ball Set Set.instMembership	HasSum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Module.toDistribMulAction instInv instNatCast Nat.factorial Monoid.toNatPow instSub iteratedDeriv SummationFilter.unconditional	—	exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Metric.mem_ball' Metric.pos_of_mem_ball CanLift.prf NNReal.canLift LT.lt.le Metric.eball_coe mem_ball_zero_iff HasFPowerSeriesOnBall.hasSum_iteratedFDeriv DifferentiableOn.hasFPowerSeriesOnBall DifferentiableOn.mono Metric.closedBall_subset_ball instCharZero Finset.prod_const Finset.card_fin mul_one ContinuousMultilinearMap.map_smul_univ add_sub_cancel
hasSum_taylorSeries_on_eball 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace Set Set.instMembership	HasSum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Module.toDistribMulAction instInv instNatCast Nat.factorial Monoid.toNatPow instSub iteratedDeriv SummationFilter.unconditional	—	exists_between ENNReal.instDenselyOrdered Metric.mem_eball' CanLift.prf ENNReal.canLift ne_top_of_lt hasSum_taylorSeries_on_ball Metric.eball_coe DifferentiableOn.mono Metric.eball_subset_eball LT.lt.le
hasSum_taylorSeries_on_emetric_ball 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace Set Set.instMembership	HasSum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Module.toDistribMulAction instInv instNatCast Nat.factorial Monoid.toNatPow instSub iteratedDeriv SummationFilter.unconditional	—	hasSum_taylorSeries_on_eball
taylorSeries_eq_of_entire 📖	mathematical	Differentiable Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Module.toDistribMulAction instInv instNatCast Nat.factorial Monoid.toNatPow instSub iteratedDeriv SummationFilter.unconditional	—	HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_taylorSeries_of_entire
taylorSeries_eq_of_entire' 📖	mathematical	Differentiable Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup instMul instInv instNatCast Nat.factorial iteratedDeriv InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instSub SummationFilter.unconditional	—	mul_right_comm smul_eq_mul mul_assoc taylorSeries_eq_of_entire instCompleteSpace
taylorSeries_eq_on_ball 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Metric.ball Set Set.instMembership	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Module.toDistribMulAction instInv instNatCast Nat.factorial Monoid.toNatPow instSub iteratedDeriv SummationFilter.unconditional	—	HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_taylorSeries_on_ball
taylorSeries_eq_on_ball' 📖	mathematical	Complex Set Set.instMembership Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DifferentiableOn DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup instMul instInv instNatCast Nat.factorial iteratedDeriv InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instSub SummationFilter.unconditional	—	mul_right_comm smul_eq_mul mul_assoc taylorSeries_eq_on_ball instCompleteSpace
taylorSeries_eq_on_eball 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace Set Set.instMembership	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Module.toDistribMulAction instInv instNatCast Nat.factorial Monoid.toNatPow instSub iteratedDeriv SummationFilter.unconditional	—	HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_taylorSeries_on_eball
taylorSeries_eq_on_eball' 📖	mathematical	Complex Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace instNormedField DifferentiableOn DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup instMul instInv instNatCast Nat.factorial iteratedDeriv InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instSub SummationFilter.unconditional	—	mul_right_comm smul_eq_mul mul_assoc taylorSeries_eq_on_eball instCompleteSpace
taylorSeries_eq_on_emetric_ball 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace Set Set.instMembership	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Module.toDistribMulAction instInv instNatCast Nat.factorial Monoid.toNatPow instSub iteratedDeriv SummationFilter.unconditional	—	taylorSeries_eq_on_eball
taylorSeries_eq_on_emetric_ball' 📖	mathematical	Complex Set Set.instMembership Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace instNormedField DifferentiableOn DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup instMul instInv instNatCast Nat.factorial iteratedDeriv InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instSub SummationFilter.unconditional	—	taylorSeries_eq_on_eball'

---

← Back to Index