Defs

📁 Source: Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

Statistics

Metric	Count
Definitions iteratedDeriv, iteratedDerivWithin	2
Theorems hasFPowerSeriesAt, continuous_iteratedDeriv, continuous_iteratedDeriv', differentiable_iteratedDeriv, differentiable_iteratedDeriv', continuousOn_iteratedDerivWithin, differentiableOn_iteratedDerivWithin, differentiableWithinAt_iteratedDerivWithin, contDiffOn_iff_continuousOn_differentiableOn_deriv, contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, contDiffOn_of_continuousOn_differentiableOn_deriv, contDiffOn_of_differentiableOn_deriv, contDiff_iff_iteratedDeriv, contDiff_nat_iff_iteratedDeriv, contDiff_of_differentiable_iteratedDeriv, iteratedDerivWithin_congr_right_of_isOpen, iteratedDerivWithin_const, iteratedDerivWithin_const_zero, iteratedDerivWithin_eq_equiv_comp, iteratedDerivWithin_eq_iterate, iteratedDerivWithin_eq_iteratedDeriv, iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedDerivWithin_fun_const_zero, iteratedDerivWithin_of_isOpen, iteratedDerivWithin_of_isOpen_eq_iterate, iteratedDerivWithin_one, iteratedDerivWithin_succ, iteratedDerivWithin_succ', iteratedDerivWithin_univ, iteratedDerivWithin_zero, iteratedDeriv_const, iteratedDeriv_const_zero, iteratedDeriv_eq_equiv_comp, iteratedDeriv_eq_iterate, iteratedDeriv_eq_iteratedFDeriv, iteratedDeriv_fun_const_zero, iteratedDeriv_one, iteratedDeriv_succ, iteratedDeriv_succ', iteratedDeriv_zero, iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod, iteratedFDerivWithin_eq_equiv_comp, iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod, iteratedFDeriv_eq_equiv_comp, norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin, norm_iteratedFDeriv_eq_norm_iteratedDeriv	46
Total	48

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFPowerSeriesAt 📖	mathematical	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	HasFPowerSeriesAt FormalMultilinearSeries.ofScalars NormedField.toField NormedRing.toRing NormedCommRing.toNormedRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid iteratedDeriv AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FormalMultilinearSeries.ext IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ContinuousMultilinearMap.ext_ring Finite.of_fintype HasFPowerSeriesOnBall.factorial_smul FormalMultilinearSeries.apply_eq_prod_smul_coeff FormalMultilinearSeries.coeff_ofScalars IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Field.isDomain div_eq_iff Nat.cast_zero ne_of_gt Nat.factorial_pos mul_comm Finset.prod_const Fintype.card_fin one_pow one_mul nsmul_eq_mul iteratedDeriv_eq_iteratedFDeriv

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_iteratedDeriv 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup iteratedDeriv	—	contDiff_iff_iteratedDeriv of_le le_rfl
continuous_iteratedDeriv' 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup iteratedDeriv	—	continuous_iteratedDeriv le_refl
differentiable_iteratedDeriv 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace iteratedDeriv	—	contDiff_iff_iteratedDeriv of_le ENat.add_one_natCast_le_withTop_of_lt IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instIsOrderedAddMonoid
differentiable_iteratedDeriv' 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne WithTop.one AddMonoidWithOne.toOne	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace iteratedDeriv	—	differentiable_iteratedDeriv Nat.cast_lt WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_iteratedDerivWithin 📖	mathematical	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	ContinuousOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup iteratedDerivWithin	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedDerivWithin_eq_equiv_comp continuousOn_iteratedFDerivWithin
differentiableOn_iteratedDerivWithin 📖	mathematical	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	DifferentiableOn NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace iteratedDerivWithin	—	ContDiffWithinAt.differentiableWithinAt_iteratedDerivWithin Set.insert_eq_of_mem

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableWithinAt_iteratedDerivWithin 📖	mathematical	ContDiffWithinAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Set Set.instInsert	DifferentiableWithinAt NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace iteratedDerivWithin	—	smulCommClass_self RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul iteratedDerivWithin_eq_equiv_comp differentiableWithinAt_iteratedFDerivWithin

(root)

Definitions

Name	Category	Theorems
iteratedDeriv 📖	CompOp	155 math math: iteratedDeriv_zero, iteratedDeriv_scomp_two, Real.iteratedDerivWithin_cos_Ioo, Real.iteratedDeriv_odd_cos, iteratedDeriv_fun_sum, Complex.iteratedDeriv_even_cosh, iteratedDeriv_fun_add, iteratedDeriv_succ, PeriodPair.iteratedDeriv_weierstrassPExcept_self, Complex.hasSum_taylorSeries_of_entire, iteratedDeriv_pow, Complex.iteratedDeriv_odd_sinh, PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self, Real.iteratedDeriv_even_cosh, iteratedDeriv_div_const, iteratedDeriv_comp_const_mul, Complex.hasSum_taylorSeries_on_ball, Complex.taylorSeries_eq_of_entire, iteratedDeriv_scomp_three, Real.iteratedDerivWithin_cos_Icc, iteratedDeriv_scomp_eq_sum_orderedFinpartition, LSeries_iteratedDeriv, Complex.taylorSeries_eq_on_ball', AnalyticAt.exists_eventuallyEq_sum_add_pow_mul, iteratedDeriv_succ', iteratedDeriv_smul_const, iteratedDeriv_const_mul, iteratedDeriv_fun_const_smul, taylor_mean_remainder_lagrange_iteratedDeriv, iteratedDerivWithin_eq_iteratedDeriv, iteratedDeriv_const_sub, ProbabilityTheory.iteratedDeriv_mgf, iteratedDeriv_fun_id_zero, iteratedDeriv_comp_sub_const, ProbabilityTheory.iteratedDeriv_complexMGF, Complex.differentiable_iteratedDeriv_sin, iteratedDeriv_const_smul, Real.abs_iteratedDeriv_cos_le_one, Complex.iteratedDeriv_odd_sin, ProbabilityTheory.exists_cgf_eq_iteratedDeriv_two_cgf_mul, Real.iteratedDeriv_add_one_cosh, Real.iteratedDeriv_add_one_sinh, contDiff_iff_iteratedDeriv, iteratedDeriv_fun_id, DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul, Real.iteratedDeriv_add_one_cos, contDiff_nat_iff_iteratedDeriv, iteratedDeriv_mul, ContDiff.continuous_iteratedDeriv, Real.iteratedDerivWithin_sinh_Icc, iteratedDeriv_add, iteratedDeriv_const_zero, eqOn_iteratedDeriv_cotTerm, Real.iteratedDerivWithin_sin_Icc, Real.iteratedDeriv_odd_sinh, iteratedFDeriv_eq_equiv_comp, iteratedDeriv_comp_const_smul, iteratedDeriv_vcomp_three, ModularFormClass.qExpansion_coeff, iteratedDeriv_const_add, ContDiff.differentiable_iteratedDeriv, iteratedDeriv_comp_neg, ProbabilityTheory.differentiableAt_iteratedDeriv_mgf, Real.differentiable_iteratedDeriv_cos, iteratedDeriv_vcomp_eq_sum_orderedFinpartition, Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le, iteratedDeriv_eq_equiv_comp, Real.iteratedDeriv_even_cos, iteratedDeriv_comp_const_add, Complex.iteratedDeriv_add_one_sinh, ProbabilityTheory.iteratedDeriv_mgf_zero, Complex.iteratedDeriv_even_cos, Complex.iteratedDeriv_add_one_sin, Complex.hasSum_taylorSeries_on_emetric_ball, iteratedDeriv_fun_const_smul_field, Complex.iteratedDeriv_add_one_cos, Real.iteratedDeriv_fourier, iteratedDeriv_fun_const_zero, iteratedDeriv_comp_two, iteratedDeriv_eq_iterate, AnalyticAt.hasFPowerSeriesAt, Real.iteratedDeriv_odd_cosh, Filter.EventuallyEq.iteratedDeriv_eq, AnalyticAt.exists_eq_sum_add_pow_mul, ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf, Complex.taylorSeries_eq_on_eball, LSeries.iteratedDeriv_alternating, Real.iteratedDerivWithin_sinh_Ioo, Real.iteratedDeriv_even_sinh, iteratedDeriv_comp_const_sub, iteratedDerivWithin_univ, ProbabilityTheory.iteratedDeriv_two_cgf, Real.iteratedDeriv_add_one_sin, Real.differentiable_iteratedDeriv_sin, iteratedDeriv_eq_iteratedFDeriv, Real.iteratedDeriv_even_sin, iteratedDeriv_comp_eq_sum_orderedFinpartition, Complex.taylorSeries_eq_on_emetric_ball, iteratedDeriv_exp_const_mul, Real.abs_iteratedDeriv_sin_le_one, Complex.taylorSeries_eq_on_ball, Complex.iteratedDeriv_odd_cos, Real.differentiable_iteratedDeriv_cosh, iteratedDeriv_mul_const_field, iteratedDeriv_comp_add_const, ProbabilityTheory.iteratedDeriv_two_cgf_eq_integral, iteratedDerivWithin_of_isOpen, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable, iteratedDeriv_comp_three, Complex.iteratedDeriv_even_sin, Real.iteratedDerivWithin_cosh_Icc, iteratedDeriv_const_smul_field, Complex.iteratedDeriv_even_sinh, iteratedDeriv_one, Complex.differentiable_iteratedDeriv_sinh, Complex.taylorSeries_eq_on_eball', iteratedDeriv_id, Complex.iteratedDeriv_add_one_cosh, SchwartzMap.le_seminorm', Real.iteratedDeriv_odd_sin, Real.differentiable_iteratedDeriv_sinh, ContDiff.differentiable_iteratedDeriv', InnerProductSpace.laplacian_eq_iteratedDeriv_real, iteratedDeriv_cexp_const_mul, iteratedDeriv_const_mul_field, iteratedDeriv_fun_pow_zero, Real.iteratedDeriv_fourierIntegral, Real.iteratedDerivWithin_cosh_Ioo, iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod, Complex.differentiable_iteratedDeriv_cos, iteratedDeriv_vcomp_two, iteratedDeriv_fun_mul, iteratedDeriv_neg, ArithmeticFunction.iteratedDeriv_LSeries_alternating, DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul, Complex.iteratedDeriv_odd_cosh, iteratedDeriv_sub, Complex.taylorSeries_eq_of_entire', norm_iteratedFDeriv_eq_norm_iteratedDeriv, ProbabilityTheory.analyticAt_iteratedDeriv_mgf, ProbabilityTheory.variance_tilted_mul, Set.EqOn.iteratedDeriv_of_isOpen, iteratedDeriv_sum, ProbabilityTheory.analyticOn_iteratedDeriv_mgf, ContDiff.continuous_iteratedDeriv', Complex.taylorSeries_eq_on_emetric_ball', natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero, iteratedDeriv_fun_sub, iteratedDeriv_const, iteratedDeriv_fun_neg, Real.iteratedDerivWithin_sin_Ioo, Complex.hasSum_taylorSeries_on_eball, Complex.differentiable_iteratedDeriv_cosh, ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf
iteratedDerivWithin 📖	CompOp	83 math math: iteratedDerivWithin_sub, Real.iteratedDerivWithin_cos_Ioo, iteratedDerivWithin_fun_const_zero, iteratedDerivWithin_const_mul_field, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, iteratedDerivWithin_vcomp_two, iteratedDerivWithin_comp_two, Filter.EventuallyEq.iteratedDerivWithin_eq, iteratedDerivWithin_tsum_cexp_eq, iteratedDerivWithin_const_zero, differentiableOn_iteratedDerivWithin_cotTerm, contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm, ContDiffWithinAt.differentiableWithinAt_iteratedDerivWithin, Real.iteratedDerivWithin_cos_Icc, iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedDerivWithin_eq_iterate, iteratedDerivWithin_mul_const, iteratedDerivWithin_one, iteratedDerivWithin_const_add, ContDiffOn.continuousOn_iteratedDerivWithin, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, iteratedDerivWithin_const_sub, iteratedDerivWithin_eq_iteratedDeriv, iteratedDerivWithin_smul_const, iteratedFDerivWithin_eq_equiv_comp, iteratedDerivWithin_const_smul_field, iteratedDerivWithin_sum, iteratedDerivWithin_comp_three, iteratedDerivWithin_of_isOpen_eq_iterate, iteratedDerivWithin_fun_const_smul_field, iteratedDerivWithin_scomp_eq_sum_orderedFinpartition, Real.iteratedDerivWithin_sinh_Icc, iteratedDerivWithin_zpow, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet, ContDiffOn.differentiableOn_iteratedDerivWithin, iteratedDerivWithin_zero, iteratedDerivWithin_scomp_three, Real.iteratedDerivWithin_sin_Icc, iteratedDerivWithin_one_div, iteratedDerivWithin_fun_id, taylorWithinEval_succ, iteratedDerivWithin_neg, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, iteratedDerivWithin_const_smul, iteratedDerivWithin_const, iteratedDerivWithin_pow, InnerProductSpace.laplacianWithin_eq_iteratedDerivWithin_real, iteratedDerivWithin_comp_const_smul, iteratedDerivWithin_mul, iteratedDerivWithin_fun_sum, Real.iteratedDerivWithin_sinh_Ioo, iteratedDerivWithin_fun_const_smul, iteratedDerivWithin_univ, iteratedDerivWithin_smul, iteratedDerivWithin_eq_equiv_comp, iteratedDerivWithin_succ, iteratedDerivWithin_of_isOpen, iteratedDerivWithin_succ', iteratedDerivWithin_fun_add, iteratedDerivWithin_id, Real.iteratedDerivWithin_cosh_Icc, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, iteratedDerivWithin_comp_eq_sum_orderedFinpartition, iteratedDerivWithin_const_mul, iteratedDerivWithin_add, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition, iteratedDerivWithin_scomp_two, Real.iteratedDerivWithin_cosh_Ioo, iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod, norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin, iteratedDerivWithin_congr_right_of_isOpen, eqOn_iteratedDerivWithin_cotTerm_integerComplement, contDiffOn_iff_continuousOn_differentiableOn_deriv, taylor_within_apply, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert, iteratedDerivWithin_mul_const_field, iteratedDerivWithin_fun_neg, Real.iteratedDerivWithin_sin_Ioo, differentiableAt_iteratedDerivWithin_cexp, iteratedDerivWithin_vcomp_three, iteratedDerivWithin_congr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffOn_iff_continuousOn_differentiableOn_deriv 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	ContDiffOn WithTop.some ENat ContinuousOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup iteratedDerivWithin DifferentiableOn	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self contDiffOn_iff_continuousOn_differentiableOn RingHomInvPair.ids iteratedFDerivWithin_eq_equiv_comp
contDiffOn_nat_iff_continuousOn_differentiableOn_deriv 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	ContDiffOn WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ContinuousOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup iteratedDerivWithin DifferentiableOn	—	contDiffOn_iff_continuousOn_differentiableOn_deriv IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
contDiffOn_of_continuousOn_differentiableOn_deriv 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup iteratedDerivWithin DifferentiableOn NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace	ContDiffOn WithTop.some ENat	—	contDiffOn_of_continuousOn_differentiableOn SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedFDerivWithin_eq_equiv_comp
contDiffOn_of_differentiableOn_deriv 📖	mathematical	DifferentiableOn NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace iteratedDerivWithin	ContDiffOn WithTop.some ENat	—	contDiffOn_of_differentiableOn SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomInvPair.ids iteratedFDerivWithin_eq_equiv_comp
contDiff_iff_iteratedDeriv 📖	mathematical	—	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop.some ENat Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup iteratedDeriv Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomInvPair.ids iteratedFDeriv_eq_equiv_comp
contDiff_nat_iff_iteratedDeriv 📖	mathematical	—	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup iteratedDeriv Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	—	WithTop.coe_natCast contDiff_iff_iteratedDeriv IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
contDiff_of_differentiable_iteratedDeriv 📖	mathematical	Differentiable NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace iteratedDeriv	ContDiff WithTop.some ENat	—	contDiff_iff_iteratedDeriv Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul le_of_lt
iteratedDerivWithin_congr_right_of_isOpen 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	Set.EqOn iteratedDerivWithin Set Set.instInter	—	iteratedDerivWithin_of_isOpen
iteratedDerivWithin_const 📖	mathematical	—	iteratedDerivWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	iteratedDerivWithin_zero iteratedDerivWithin_succ' derivWithin_fun_const
iteratedDerivWithin_const_zero 📖	mathematical	—	iteratedDerivWithin Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	iteratedDerivWithin_fun_const_zero
iteratedDerivWithin_eq_equiv_comp 📖	mathematical	—	iteratedDerivWithin ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm ContinuousMultilinearMap.piFieldEquiv iteratedFDerivWithin	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
iteratedDerivWithin_eq_iterate 📖	mathematical	—	iteratedDerivWithin Nat.iterate derivWithin NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	iteratedDerivWithin_zero iteratedDerivWithin_succ Function.iterate_succ' derivWithin_congr
iteratedDerivWithin_eq_iteratedDeriv 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ContDiffAt WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set Set.instMembership	iteratedDerivWithin iteratedDeriv	—	iteratedDerivWithin.eq_1 iteratedDeriv.eq_1 iteratedFDerivWithin_eq_iteratedFDeriv
iteratedDerivWithin_eq_iteratedFDerivWithin 📖	mathematical	—	iteratedDerivWithin DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NormedField.toNormedSpace ContinuousMultilinearMap.funLike iteratedFDerivWithin AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	—
iteratedDerivWithin_fun_const_zero 📖	mathematical	—	iteratedDerivWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	iteratedDerivWithin_const
iteratedDerivWithin_of_isOpen 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	Set.EqOn iteratedDerivWithin iteratedDeriv	—	iteratedFDerivWithin_of_isOpen
iteratedDerivWithin_of_isOpen_eq_iterate 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	Set.EqOn iteratedDerivWithin Nat.iterate deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	—	Set.EqOn.trans iteratedDerivWithin_of_isOpen iteratedDeriv_eq_iterate Set.eqOn_refl
iteratedDerivWithin_one 📖	mathematical	—	iteratedDerivWithin derivWithin NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	iteratedFDerivWithin_one_apply AccPt.uniqueDiffWithinAt fderivWithin_zero_of_not_accPt derivWithin_zero_of_not_accPt
iteratedDerivWithin_succ 📖	mathematical	—	iteratedDerivWithin derivWithin NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	iteratedDerivWithin_eq_iteratedFDerivWithin SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedFDerivWithin_succ_apply_left RingHomInvPair.ids iteratedFDerivWithin_eq_equiv_comp RingHomCompTriple.ids LinearIsometryEquiv.comp_fderivWithin AccPt.uniqueDiffWithinAt derivWithin.eq_1 IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul Finset.prod_const_one one_smul fderivWithin_zero_of_not_accPt derivWithin_zero_of_not_accPt
iteratedDerivWithin_succ' 📖	mathematical	—	iteratedDerivWithin derivWithin NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	iteratedDerivWithin_eq_iterate
iteratedDerivWithin_univ 📖	mathematical	—	iteratedDerivWithin Set.univ iteratedDeriv	—	iteratedDerivWithin.eq_1 iteratedDeriv.eq_1 iteratedFDerivWithin_univ
iteratedDerivWithin_zero 📖	mathematical	—	iteratedDerivWithin	—	—
iteratedDeriv_const 📖	mathematical	—	iteratedDeriv NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	iteratedDeriv_zero iteratedDeriv_succ' deriv_const'
iteratedDeriv_const_zero 📖	mathematical	—	iteratedDeriv Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	iteratedDeriv_fun_const_zero
iteratedDeriv_eq_equiv_comp 📖	mathematical	—	iteratedDeriv ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm ContinuousMultilinearMap.piFieldEquiv iteratedFDeriv	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
iteratedDeriv_eq_iterate 📖	mathematical	—	iteratedDeriv Nat.iterate deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	iteratedDerivWithin_univ derivWithin_univ iteratedDerivWithin_eq_iterate
iteratedDeriv_eq_iteratedFDeriv 📖	mathematical	—	iteratedDeriv DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NormedField.toNormedSpace ContinuousMultilinearMap.funLike iteratedFDeriv AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	—
iteratedDeriv_fun_const_zero 📖	mathematical	—	iteratedDeriv NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	iteratedDeriv_const
iteratedDeriv_one 📖	mathematical	—	iteratedDeriv deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	iteratedFDeriv_one_apply fderiv_eq_smul_deriv one_smul
iteratedDeriv_succ 📖	mathematical	—	iteratedDeriv deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	iteratedDerivWithin_univ derivWithin_univ iteratedDerivWithin_succ
iteratedDeriv_succ' 📖	mathematical	—	iteratedDeriv deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	iteratedDeriv_eq_iterate Function.iterate_succ_apply
iteratedDeriv_zero 📖	mathematical	—	iteratedDeriv	—	—
iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NormedField.toNormedSpace ContinuousMultilinearMap.funLike iteratedFDerivWithin SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.prod CommRing.toCommMonoid Field.toCommRing Finset.univ Fin.fintype iteratedDerivWithin	—	iteratedDerivWithin_eq_iteratedFDerivWithin ContinuousMultilinearMap.map_smul_univ mul_one
iteratedFDerivWithin_eq_equiv_comp 📖	mathematical	—	iteratedFDerivWithin NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing EquivLike.toFunLike LinearIsometryEquiv.instEquivLike ContinuousMultilinearMap.piFieldEquiv iteratedDerivWithin	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedDerivWithin_eq_equiv_comp Function.comp_assoc LinearIsometryEquiv.self_comp_symm
iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NormedField.toNormedSpace ContinuousMultilinearMap.funLike iteratedFDeriv SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.prod CommRing.toCommMonoid Field.toCommRing Finset.univ Fin.fintype iteratedDeriv	—	iteratedDeriv_eq_iteratedFDeriv ContinuousMultilinearMap.map_smul_univ mul_one
iteratedFDeriv_eq_equiv_comp 📖	mathematical	—	iteratedFDeriv NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing EquivLike.toFunLike LinearIsometryEquiv.instEquivLike ContinuousMultilinearMap.piFieldEquiv iteratedDeriv	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedDeriv_eq_equiv_comp Function.comp_assoc LinearIsometryEquiv.self_comp_symm
norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NormedField.toNormedSpace ContinuousMultilinearMap.hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Fin.fintype iteratedFDerivWithin NormedAddCommGroup.toNorm iteratedDerivWithin	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedDerivWithin_eq_equiv_comp LinearIsometryEquiv.norm_map
norm_iteratedFDeriv_eq_norm_iteratedDeriv 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NormedField.toNormedSpace ContinuousMultilinearMap.hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Fin.fintype iteratedFDeriv NormedAddCommGroup.toNorm iteratedDeriv	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedDeriv_eq_equiv_comp LinearIsometryEquiv.norm_map

---

← Back to Index