FaaDiBruno

📁 Source: Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Statistics

Metric	Count
Definitions compAlongOrderedFinpartition, taylorComp, OrderedFinpartition, applyOrderedFinpartition, atomic, compAlongOrderedFinpartition, compAlongOrderedFinpartitionL, compAlongOrderedFinpartitionₗ, emb, embSigma, equivSigma, eraseLeft, eraseMiddle, extend, extendEquiv, extendLeft, extendMiddle, index, instFintype, instInhabited, instUniqueOne, instUniqueZero, invEmbedding, length, partSize, instDecidableEqOrderedFinpartition, decEq	27
Theorems compAlongOrderedFinpartition_apply, taylorComp_sub_taylorComp_isBigO, taylorComp_sub_taylorComp_isLittleO, comp, applyOrderedFinpartition_apply, applyOrderedFinpartition_update_left, applyOrderedFinpartition_update_right, atomic_emb, atomic_length, atomic_partSize, compAlongOrderFinpartition_apply, compAlongOrderedFinpartitionL_apply, compAlongOrderedFinpartitionₗ_apply_apply, cover, default_eq, disjoint, emb_injective, emb_invEmbedding, emb_ne_emb_of_ne, emb_strictMono, emb_zero, exists_inverse, ext, ext_iff, extendEquiv_apply, extendLeft_length, extendLeft_partSize, extendMiddle_length, extendMiddle_partSize, extend_none, extend_some, index_extendMiddle_zero, injective_embSigma, length_le, length_pos, neZero_length, neZero_partSize, norm_applyOrderedFinpartition_le, norm_compAlongOrderedFinpartitionL_apply_le, norm_compAlongOrderedFinpartitionL_le, norm_compAlongOrderedFinpartition_le, norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le, one_lt_partSize_index_zero, partSize_eq_one_of_range_emb_eq_singleton, partSize_le, partSize_pos, parts_strictMono, prod_sigma_eq_prod, range_emb_extendMiddle_ne_singleton_zero, range_extendLeft_zero, sum_sigma_eq_sum, analyticOn_taylorComp	52
Total	79

FormalMultilinearSeries

Definitions

Name	Category	Theorems
compAlongOrderedFinpartition 📖	CompOp	1 math math: compAlongOrderedFinpartition_apply
taylorComp 📖	CompOp	7 math math: iteratedFDeriv_comp, taylorComp_sub_taylorComp_isBigO, taylorComp_sub_taylorComp_isLittleO, HasFTaylorSeriesUpToOn.comp, analyticOn_taylorComp, iteratedFDerivWithin_comp, iteratedFDerivWithin_comp_of_eventually_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compAlongOrderedFinpartition_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.funLike compAlongOrderedFinpartition OrderedFinpartition.length OrderedFinpartition.applyOrderedFinpartition OrderedFinpartition.partSize	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
taylorComp_sub_taylorComp_isBigO 📖	mathematical	Filter.IsBoundedUnder Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype Asymptotics.IsBigO NormedAddCommGroup.toNorm ContinuousMultilinearMap.instSub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	taylorComp	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Asymptotics.IsBigO.sum Asymptotics.IsBigO.trans Asymptotics.IsBigO.of_norm_le OrderedFinpartition.norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le Asymptotics.IsBigO.add Filter.IsBoundedUnder.isBigO_one NormedDivisionRing.to_normOneClass OrderedFinpartition.length_le OrderedFinpartition.partSize_le Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass Asymptotics.IsBigO.pow Asymptotics.IsBigO.norm_left Asymptotics.IsBigO.prod_left Asymptotics.isBigO_pi Asymptotics.IsBigO.norm_norm mul_assoc one_pow one_mul Asymptotics.IsBigO.const_mul_left Finset.prod_congr Finset.prod_const_one mul_one Asymptotics.IsBigO.finsetProd
taylorComp_sub_taylorComp_isLittleO 📖	mathematical	Filter.IsBoundedUnder Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype Asymptotics.IsLittleO NormedAddCommGroup.toNorm ContinuousMultilinearMap.instSub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	taylorComp	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul taylorComp_sub_taylorComp_isBigO Asymptotics.isBigO_fst_prod Asymptotics.isBigO_snd_prod Asymptotics.IsLittleO.prod_left Asymptotics.isLittleO_pi

HasFTaylorSeriesUpToOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	HasFTaylorSeriesUpToOn Set.MapsTo	FormalMultilinearSeries.taylorComp	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids smulCommClass_self Finset.sum_congr Finset.univ_unique Finset.sum_singleton Matrix.zero_empty zero_eq' ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instContinuousConstSMul ContinuousMultilinearMap.instSMulCommClass WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero OrderedFinpartition.length_le OrderedFinpartition.partSize_le fderivWithin LE.le.trans_lt RingHomIsometric.ids hasFDerivWithinAt LT.lt.ne_bot RingHomCompTriple.ids Fintype.sum_option HasFDerivWithinAt.linear_multilinear_comp HasFDerivWithinAt.comp HasFDerivWithinAt.fun_sum Finset.sum_sigma' Fintype.sum_equiv ContinuousLinearMap.ext ContinuousMultilinearMap.ext ContinuousMultilinearMap.sum_apply ContinuousLinearMap.coe_sum' Finset.sum_apply continuousOn_finset_sum Continuous.comp_continuousOn ContinuousLinearMap.continuous_uncurry_of_multilinear Finite.of_fintype ContinuousOn.prodMk ContinuousOn.comp cont LE.le.trans continuousOn continuousOn_pi

OrderedFinpartition

Definitions

Name	Category	Theorems
applyOrderedFinpartition 📖	CompOp	6 math math: norm_applyOrderedFinpartition_le, compAlongOrderFinpartition_apply, applyOrderedFinpartition_apply, applyOrderedFinpartition_update_left, FormalMultilinearSeries.compAlongOrderedFinpartition_apply, applyOrderedFinpartition_update_right
atomic 📖	CompOp	4 math math: atomic_length, atomic_emb, default_eq, atomic_partSize
compAlongOrderedFinpartition 📖	CompOp	5 math math: norm_compAlongOrderedFinpartition_le, compAlongOrderedFinpartitionₗ_apply_apply, compAlongOrderedFinpartitionL_apply, compAlongOrderFinpartition_apply, norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le
compAlongOrderedFinpartitionL 📖	CompOp	3 math math: norm_compAlongOrderedFinpartitionL_apply_le, compAlongOrderedFinpartitionL_apply, norm_compAlongOrderedFinpartitionL_le
compAlongOrderedFinpartitionₗ 📖	CompOp	1 math math: compAlongOrderedFinpartitionₗ_apply_apply
emb 📖	CompOp	17 math math: norm_applyOrderedFinpartition_le, disjoint, prod_sigma_eq_prod, emb_zero, emb_invEmbedding, cover, applyOrderedFinpartition_apply, atomic_emb, emb_injective, applyOrderedFinpartition_update_left, exists_inverse, parts_strictMono, ext_iff, range_extendLeft_zero, emb_strictMono, applyOrderedFinpartition_update_right, sum_sigma_eq_sum
embSigma 📖	CompOp	1 math math: injective_embSigma
equivSigma 📖	CompOp	—
eraseLeft 📖	CompOp	—
eraseMiddle 📖	CompOp	—
extend 📖	CompOp	3 math math: extendEquiv_apply, extend_some, extend_none
extendEquiv 📖	CompOp	1 math math: extendEquiv_apply
extendLeft 📖	CompOp	4 math math: extendLeft_partSize, extendLeft_length, range_extendLeft_zero, extend_none
extendMiddle 📖	CompOp	4 math math: extendMiddle_length, extendMiddle_partSize, extend_some, index_extendMiddle_zero
index 📖	CompOp	5 math math: emb_zero, emb_invEmbedding, index_extendMiddle_zero, applyOrderedFinpartition_update_right, one_lt_partSize_index_zero
instFintype 📖	CompOp	6 math math: iteratedDeriv_scomp_eq_sum_orderedFinpartition, iteratedDerivWithin_scomp_eq_sum_orderedFinpartition, iteratedDeriv_vcomp_eq_sum_orderedFinpartition, iteratedDeriv_comp_eq_sum_orderedFinpartition, iteratedDerivWithin_comp_eq_sum_orderedFinpartition, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition
instInhabited 📖	CompOp	1 math math: default_eq
instUniqueOne 📖	CompOp	—
instUniqueZero 📖	CompOp	—
invEmbedding 📖	CompOp	2 math math: emb_invEmbedding, applyOrderedFinpartition_update_right
length 📖	CompOp	35 math math: extendEquiv_apply, norm_compAlongOrderedFinpartition_le, disjoint, norm_compAlongOrderedFinpartitionL_apply_le, iteratedDeriv_scomp_eq_sum_orderedFinpartition, extendMiddle_length, atomic_length, prod_sigma_eq_prod, compAlongOrderedFinpartitionₗ_apply_apply, iteratedDerivWithin_scomp_eq_sum_orderedFinpartition, neZero_length, extendLeft_partSize, iteratedDeriv_vcomp_eq_sum_orderedFinpartition, compAlongOrderedFinpartitionL_apply, length_pos, compAlongOrderFinpartition_apply, iteratedDeriv_comp_eq_sum_orderedFinpartition, extendMiddle_partSize, length_le, emb_injective, norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le, applyOrderedFinpartition_update_left, exists_inverse, parts_strictMono, extendLeft_length, extend_some, ext_iff, range_extendLeft_zero, iteratedDerivWithin_comp_eq_sum_orderedFinpartition, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition, extend_none, FormalMultilinearSeries.compAlongOrderedFinpartition_apply, applyOrderedFinpartition_update_right, sum_sigma_eq_sum, norm_compAlongOrderedFinpartitionL_le
partSize 📖	CompOp	35 math math: norm_compAlongOrderedFinpartition_le, norm_applyOrderedFinpartition_le, partSize_pos, disjoint, norm_compAlongOrderedFinpartitionL_apply_le, iteratedDeriv_scomp_eq_sum_orderedFinpartition, prod_sigma_eq_prod, emb_zero, compAlongOrderedFinpartitionₗ_apply_apply, iteratedDerivWithin_scomp_eq_sum_orderedFinpartition, extendLeft_partSize, iteratedDeriv_vcomp_eq_sum_orderedFinpartition, compAlongOrderedFinpartitionL_apply, cover, applyOrderedFinpartition_apply, iteratedDeriv_comp_eq_sum_orderedFinpartition, extendMiddle_partSize, emb_injective, neZero_partSize, norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le, applyOrderedFinpartition_update_left, exists_inverse, parts_strictMono, partSize_le, ext_iff, range_extendLeft_zero, iteratedDerivWithin_comp_eq_sum_orderedFinpartition, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition, emb_strictMono, FormalMultilinearSeries.compAlongOrderedFinpartition_apply, atomic_partSize, applyOrderedFinpartition_update_right, one_lt_partSize_index_zero, sum_sigma_eq_sum, norm_compAlongOrderedFinpartitionL_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
applyOrderedFinpartition_apply 📖	mathematical	—	applyOrderedFinpartition DFunLike.coe ContinuousMultilinearMap partSize DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.funLike emb	—	—
applyOrderedFinpartition_update_left 📖	mathematical	—	applyOrderedFinpartition Function.update length ContinuousMultilinearMap partSize DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DFunLike.coe ContinuousMultilinearMap.funLike emb	—	Function.update_self Function.update_of_ne
applyOrderedFinpartition_update_right 📖	mathematical	—	applyOrderedFinpartition Function.update length index DFunLike.coe ContinuousMultilinearMap partSize DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.funLike emb invEmbedding	—	Function.update_self Function.update_comp_eq_of_injective StrictMono.injective emb_strictMono emb_invEmbedding Function.update_of_ne Function.update_comp_eq_of_notMem_range disjoint Set.mem_univ Set.mem_range Set.disjoint_right
atomic_emb 📖	mathematical	—	emb atomic	—	—
atomic_length 📖	mathematical	—	length atomic	—	—
atomic_partSize 📖	mathematical	—	partSize atomic	—	—
compAlongOrderFinpartition_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.funLike compAlongOrderedFinpartition length applyOrderedFinpartition	—	—
compAlongOrderedFinpartitionL_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap length partSize DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap.funLike ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.normedAddCommGroup' Fin.fintype ContinuousMultilinearMap.instContinuousConstSMul ContinuousMultilinearMap.instSMulCommClass ContinuousLinearMap.funLike compAlongOrderedFinpartitionL compAlongOrderedFinpartition	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instContinuousConstSMul ContinuousMultilinearMap.instSMulCommClass
compAlongOrderedFinpartitionₗ_apply_apply 📖	mathematical	—	DFunLike.coe MultilinearMap length ContinuousMultilinearMap partSize DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.addCommMonoid ContinuousMultilinearMap.instModule MultilinearMap.instFunLikeForall LinearMap RingHom.id Semiring.toNonAssocSemiring IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing MultilinearMap.addCommMonoid MultilinearMap.instModule ContinuousMultilinearMap.instSMulCommClass LinearMap.instFunLike compAlongOrderedFinpartitionₗ compAlongOrderedFinpartition	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self ContinuousMultilinearMap.instSMulCommClass
cover 📖	mathematical	—	Set Set.instMembership Set.range partSize emb	—	—
default_eq 📖	mathematical	—	OrderedFinpartition instInhabited atomic	—	—
disjoint 📖	mathematical	—	Set.PairwiseDisjoint Set length OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.range partSize emb	—	—
emb_injective 📖	mathematical	—	length partSize emb	—	Mathlib.Tactic.Contrapose.contrapose₁ disjoint Set.mem_univ Set.disjoint_iff_forall_ne Set.mem_range_self StrictMono.injective emb_strictMono
emb_invEmbedding 📖	mathematical	—	emb index invEmbedding	—	exists_inverse
emb_ne_emb_of_ne 📖	—	—	—	—	emb_injective
emb_strictMono 📖	mathematical	—	StrictMono partSize PartialOrder.toPreorder Fin.instPartialOrder emb	—	—
emb_zero 📖	mathematical	—	emb index partSize neZero_partSize	—	le_antisymm neZero_partSize emb_invEmbedding StrictMono.monotone emb_strictMono
exists_inverse 📖	mathematical	—	emb length partSize	—	cover
ext 📖	—	length partSize emb	—	—	—
ext_iff 📖	mathematical	—	length partSize emb	—	ext
extendEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv OrderedFinpartition length EquivLike.toFunLike Equiv.instEquivLike extendEquiv extend	—	—
extendLeft_length 📖	mathematical	—	length extendLeft	—	—
extendLeft_partSize 📖	mathematical	—	partSize extendLeft Fin.cons length	—	—
extendMiddle_length 📖	mathematical	—	length extendMiddle	—	—
extendMiddle_partSize 📖	mathematical	—	partSize extendMiddle Function.update length	—	—
extend_none 📖	mathematical	—	extend length extendLeft	—	—
extend_some 📖	mathematical	—	extend length extendMiddle	—	—
index_extendMiddle_zero 📖	mathematical	—	index extendMiddle	—	neZero_partSize Mathlib.Tactic.Contrapose.contrapose₁ emb_ne_emb_of_ne emb_invEmbedding
injective_embSigma 📖	mathematical	—	OrderedFinpartition embSigma	—	—
length_le 📖	mathematical	—	length	—	Fintype.card_fin Fintype.card_le_of_injective partSize_pos StrictMono.injective parts_strictMono
length_pos 📖	mathematical	—	length	—	—
neZero_length 📖	mathematical	—	MulZeroClass.toZero Nat.instMulZeroClass length	—	LT.lt.ne' length_pos
neZero_partSize 📖	mathematical	—	MulZeroClass.toZero Nat.instMulZeroClass partSize	—	NeZero.of_pos partSize_pos
norm_applyOrderedFinpartition_le 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm applyOrderedFinpartition Real.instMul ContinuousMultilinearMap partSize DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype Finset.prod Real.instCommMonoid Finset.univ emb	—	ContinuousMultilinearMap.le_opNorm
norm_compAlongOrderedFinpartitionL_apply_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap length partSize DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap.hasOpNorm ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.normedSpace' DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.normedAddCommGroup' ContinuousMultilinearMap.instContinuousConstSMul ContinuousMultilinearMap.instSMulCommClass ContinuousLinearMap.funLike compAlongOrderedFinpartitionL ContinuousMultilinearMap.hasOpNorm'	—	LE.le.trans_eq IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self ContinuousMultilinearMap.instSMulCommClass ContinuousLinearMap.le_of_opNorm_le RingHomIsometric.ids norm_compAlongOrderedFinpartitionL_le one_mul
norm_compAlongOrderedFinpartitionL_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap length ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup partSize ContinuousMultilinearMap.instModule 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing 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 ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.normedAddCommGroup' Fin.fintype ContinuousMultilinearMap.instContinuousConstSMul ContinuousMultilinearMap.instSMulCommClass ContinuousLinearMap.hasOpNorm ContinuousMultilinearMap.seminormedAddCommGroup' ContinuousMultilinearMap.seminormedAddCommGroup ContinuousMultilinearMap.normedSpace' ContinuousMultilinearMap.normedSpace AddCommGroup.toAddCommMonoid compAlongOrderedFinpartitionL Real.instOne	—	MultilinearMap.mkContinuousLinear_norm_le zero_le_one Real.instZeroLEOneClass
norm_compAlongOrderedFinpartition_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype compAlongOrderedFinpartition Real.instMul length Finset.prod Real.instCommMonoid Finset.univ partSize	—	ContinuousMultilinearMap.opNorm_le_bound mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg Finset.prod_nonneg Real.instZeroLEOneClass compAlongOrderFinpartition_apply mul_assoc prod_sigma_eq_prod Finset.prod_mul_distrib ContinuousMultilinearMap.le_opNorm_mul_prod_of_le norm_applyOrderedFinpartition_le
norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype ContinuousMultilinearMap.instSub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup compAlongOrderedFinpartition Real.instAdd Real.instMul length Real.instNatCast Monoid.toNatPow Real.instMonoid Real.instMax NormedAddCommGroup.toNorm Pi.normedAddCommGroup partSize ContinuousMultilinearMap.normedAddCommGroup' Pi.instSub Finset.prod Real.instCommMonoid Finset.univ	—	SeminormedAddCommGroup.toIsTopologicalAddGroup norm_sub_le_norm_sub_add_norm_sub add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LE.le.trans smulCommClass_self IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instContinuousConstSMul ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.norm_image_sub_le Fintype.card_fin mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_compAlongOrderedFinpartitionL_apply_le Nat.cast_nonneg' Real.instZeroLEOneClass pow_nonneg IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono le_max_of_le_left norm_nonneg norm_compAlongOrderedFinpartition_le
one_lt_partSize_index_zero 📖	mathematical	—	partSize index	—	neZero_length Nat.card_range_of_injective StrictMono.injective emb_strictMono Nat.card_eq_fintype_card Fintype.card_fin eq_or_ne ssubset_of_subset_of_ne Set.instIsNonstrictStrictOrderSubsetSSubset Set.instAntisymmSubset neZero_partSize emb_zero Fintype.card_ofFinset Fintype.card_unique Set.Finite.card_lt_card Set.finite_range Finite.of_fintype LT.lt.trans_le Nat.instAtLeastTwoHAddOfNat one_lt_two Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid partSize_pos Set.toFinset_singleton Finset.card_pair LT.lt.ne LE.le.trans_lt parts_strictMono Fin.pos_iff_ne_zero' Nat.card_mono Subtype.finite
partSize_eq_one_of_range_emb_eq_singleton 📖	—	Set.range partSize emb Set Set.instSingletonSet	—	—	Set.card_range_of_injective StrictMono.injective emb_strictMono Fintype.card_fin Fintype.card_congr' Fintype.card_unique
partSize_le 📖	mathematical	—	partSize	—	Fintype.card_fin Fintype.card_le_of_injective StrictMono.injective emb_strictMono
partSize_pos 📖	mathematical	—	partSize	—	—
parts_strictMono 📖	mathematical	—	StrictMono length PartialOrder.toPreorder Fin.instPartialOrder emb partSize partSize_pos	—	—
prod_sigma_eq_prod 📖	mathematical	—	Finset.prod length Finset.univ Fin.fintype partSize emb	—	Finset.prod_sigma' Fintype.prod_equiv
range_emb_extendMiddle_ne_singleton_zero 📖	—	—	—	—	eq_or_ne neZero_partSize Function.update_self Set.mem_range_self
range_extendLeft_zero 📖	mathematical	—	Set.range partSize extendLeft length neZero_length emb Set Set.instSingletonSet	—	neZero_length Set.range_const Fin.cons_zero
sum_sigma_eq_sum 📖	mathematical	—	Finset.sum length Finset.univ Fin.fintype partSize emb	—	Finset.sum_sigma' Fintype.sum_equiv

(root)

Definitions

Name	Category	Theorems
OrderedFinpartition 📖	CompData	9 math math: OrderedFinpartition.extendEquiv_apply, iteratedDeriv_scomp_eq_sum_orderedFinpartition, iteratedDerivWithin_scomp_eq_sum_orderedFinpartition, iteratedDeriv_vcomp_eq_sum_orderedFinpartition, iteratedDeriv_comp_eq_sum_orderedFinpartition, OrderedFinpartition.injective_embSigma, OrderedFinpartition.default_eq, iteratedDerivWithin_comp_eq_sum_orderedFinpartition, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition
instDecidableEqOrderedFinpartition 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticOn_taylorComp 📖	mathematical	AnalyticOn ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.normedAddCommGroup' Fin.fintype ContinuousMultilinearMap.normedSpace' smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Set.MapsTo	FormalMultilinearSeries.taylorComp	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self Finset.analyticOn_fun_sum ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instContinuousConstSMul ContinuousMultilinearMap.instSMulCommClass AnalyticOnNhd.comp_analyticOn ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear AnalyticOn.prod AnalyticOn.comp AnalyticOn.pi Set.mapsTo_univ

instDecidableEqOrderedFinpartition

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

---

← Back to Index