Bounds

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

Statistics

Metric	Count
Definitions	0
Theorems norm_iteratedFDerivWithin_comp_left, norm_iteratedFDerivWithin_le_of_bilinear, norm_iteratedFDerivWithin_le_of_bilinear_aux, norm_iteratedFDerivWithin_le_of_bilinear_of_le_one, norm_iteratedFDeriv_comp_left, norm_iteratedFDeriv_le_of_bilinear, norm_iteratedFDeriv_le_of_bilinear_of_le_one, norm_iteratedFDerivWithin_clm_apply, norm_iteratedFDerivWithin_clm_apply_const, norm_iteratedFDerivWithin_comp_le, norm_iteratedFDerivWithin_comp_le_aux, norm_iteratedFDerivWithin_mul_le, norm_iteratedFDerivWithin_prod_le, norm_iteratedFDerivWithin_smul_le, norm_iteratedFDeriv_clm_apply, norm_iteratedFDeriv_clm_apply_const, norm_iteratedFDeriv_comp_le, norm_iteratedFDeriv_comp_le', norm_iteratedFDeriv_mul_le, norm_iteratedFDeriv_prod_le, norm_iteratedFDeriv_smul_le	21
Total	21

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_iteratedFDerivWithin_comp_left 📖	mathematical	ContDiffWithinAt UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership 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	Real Real.instLE Norm.norm ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin DFunLike.coe ContinuousLinearMap RingHom.id funLike Real.instMul hasOpNorm	—	norm_compContinuousMultilinearMap_le iteratedFDerivWithin_comp_left
norm_iteratedFDerivWithin_le_of_bilinear 📖	mathematical	ContDiffOn UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership 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	Real Real.instLE Norm.norm ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin DFunLike.coe ContinuousLinearMap RingHom.id funLike topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 Real.instMul hasOpNorm toSeminormedAddCommGroup RingHomIsometric.ids toNormedSpace Finset.sum Real.instAddCommMonoid Finset.range Real.instNatCast Nat.choose	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids RingHomIsometric.ids RingHomCompTriple.ids instContinuousAddULift topologicalAddGroup smulCommClass continuousConstSMul LinearIsometryEquiv.apply_symm_apply opNorm_le_bound norm_nonneg mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing LinearIsometryEquiv.norm_map le_opNorm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono ContinuousLinearEquiv.uniqueDiffOn_preimage_iff ContDiff.comp_contDiffOn LinearIsometryEquiv.contDiff ContDiffOn.comp_continuousLinearMap ContDiffOn.of_le LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right norm_iteratedFDerivWithin_le_of_bilinear_aux LE.le.trans Finset.sum_congr Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_nonneg' Real.instZeroLEOneClass
norm_iteratedFDerivWithin_le_of_bilinear_aux 📖	mathematical	ContDiffOn WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	Real Real.instLE Norm.norm ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin DFunLike.coe ContinuousLinearMap RingHom.id funLike topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 Real.instMul hasOpNorm toSeminormedAddCommGroup RingHomIsometric.ids toNormedSpace Finset.sum Real.instAddCommMonoid Finset.range Real.instNatCast Nat.choose	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids norm_iteratedFDerivWithin_zero Finset.sum_congr zero_add Finset.sum_singleton Nat.choose_self Nat.cast_one one_mul le_opNorm₂ Nat.cast_succ topologicalAddGroup smulCommClass continuousConstSMul ContDiffOn.of_le Nat.cast_le WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero ContDiffOn.fderivWithin mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_precompR_le Finset.sum_nonneg Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Nat.cast_nonneg' Real.instZeroLEOneClass norm_nonneg Finset.mem_range norm_iteratedFDerivWithin_fderivWithin norm_precompL_le iteratedFDerivWithin_congr fderivWithin_of_bilinear ContDiffOn.differentiableOn ne_of_gt Nat.cast_pos' NeZero.charZero_one Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.instIsOrderedAddMonoid zero_le Nat.instCanonicallyOrderedAdd Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat ContDiff.comp₂_contDiffOn IsBoundedBilinearMap.contDiff isBoundedBilinearMap iteratedFDerivWithin_add_apply' ContDiffOn.contDiffWithinAt LE.le.trans norm_add_le add_le_add le_of_eq Distrib.leftDistribClass mul_assoc Finset.sum_choose_succ_mul
norm_iteratedFDerivWithin_le_of_bilinear_of_le_one 📖	mathematical	ContDiffOn UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership 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 Real Real.instLE Norm.norm ContinuousLinearMap RingHom.id ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 hasOpNorm toSeminormedAddCommGroup RingHomIsometric.ids toNormedSpace Real.instOne	ContinuousMultilinearMap ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin DFunLike.coe funLike Finset.sum Real.instAddCommMonoid Finset.range Real.instMul Real.instNatCast Nat.choose	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids LE.le.trans norm_iteratedFDerivWithin_le_of_bilinear mul_le_of_le_one_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Nat.cast_nonneg' Real.instZeroLEOneClass norm_nonneg
norm_iteratedFDeriv_comp_left 📖	mathematical	ContDiffAt 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	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 iteratedFDeriv DFunLike.coe ContinuousLinearMap RingHom.id funLike Real.instMul hasOpNorm	—	norm_iteratedFDerivWithin_comp_left ContDiffAt.contDiffWithinAt uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.mem_univ
norm_iteratedFDeriv_le_of_bilinear 📖	mathematical	ContDiff 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	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 iteratedFDeriv DFunLike.coe ContinuousLinearMap RingHom.id funLike topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 Real.instMul hasOpNorm toSeminormedAddCommGroup RingHomIsometric.ids toNormedSpace Finset.sum Real.instAddCommMonoid Finset.range Real.instNatCast Nat.choose	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids Finset.sum_congr norm_iteratedFDerivWithin_le_of_bilinear ContDiff.contDiffOn uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul Set.mem_univ
norm_iteratedFDeriv_le_of_bilinear_of_le_one 📖	mathematical	ContDiff 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 Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 hasOpNorm toSeminormedAddCommGroup RingHomIsometric.ids toNormedSpace Real.instOne	ContinuousMultilinearMap ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv DFunLike.coe funLike Finset.sum Real.instAddCommMonoid Finset.range Real.instMul Real.instNatCast Nat.choose	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids Finset.sum_congr norm_iteratedFDerivWithin_le_of_bilinear_of_le_one ContDiff.contDiffOn uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul Set.mem_univ

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_iteratedFDerivWithin_clm_apply 📖	mathematical	ContDiffOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniqueDiffOn NormedAddCommGroup.toAddCommGroup Set Set.instMembership 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 CommSemiring.toSemiring instCommSemiringENat	Real Real.instLE Norm.norm ContinuousMultilinearMap ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin DFunLike.coe ContinuousLinearMap.funLike Finset.sum Real.instAddCommMonoid Finset.range Real.instMul Real.instNatCast Nat.choose ContinuousLinearMap.toSeminormedAddCommGroup	—	RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.opNorm_flip ContinuousLinearMap.opNorm_le_bound zero_le_one Real.instZeroLEOneClass one_mul le_refl ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
norm_iteratedFDerivWithin_clm_apply_const 📖	mathematical	ContDiffWithinAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniqueDiffOn NormedAddCommGroup.toAddCommGroup Set Set.instMembership 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 CommSemiring.toSemiring instCommSemiringENat	Real Real.instLE Norm.norm ContinuousMultilinearMap ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin DFunLike.coe ContinuousLinearMap.funLike Real.instMul NormedAddCommGroup.toNorm ContinuousLinearMap.toSeminormedAddCommGroup	—	RingHomIsometric.ids smulCommClass_self LE.le.trans SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing ContinuousLinearMap.opNorm_le_bound norm_nonneg ContinuousLinearMap.apply_apply mul_comm ContinuousLinearMap.le_opNorm
norm_iteratedFDerivWithin_comp_le 📖	mathematical	ContDiffOn 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 NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.MapsTo Set Set.instMembership Real Real.instLE Norm.norm ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin Monoid.toNatPow Real.instMonoid	Real.instMul Real.instNatCast Nat.factorial	—	RingHomInvPair.ids ContinuousLinearEquiv.uniqueDiffOn_preimage_iff LinearIsometryEquiv.apply_symm_apply ContDiff.comp_contDiffOn LinearIsometryEquiv.contDiff ContDiffOn.of_le ContDiffOn.comp_continuousLinearMap LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right ULift.ext norm_iteratedFDerivWithin_comp_le_aux
norm_iteratedFDerivWithin_comp_le_aux 📖	mathematical	ContDiffOn WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.MapsTo Set Set.instMembership Real Real.instLE Norm.norm ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin Monoid.toNatPow Real.instMonoid	Real.instMul Real.instNatCast Nat.factorial	—	Nat.case_strong_induction_on norm_iteratedFDerivWithin_zero Nat.cast_one one_mul pow_zero mul_one le_rfl Nat.cast_lt WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero LE.le.trans norm_nonneg bot_le covariant_swap_add_of_covariant_add Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le pow_one RingHomIsometric.ids smulCommClass_self ContDiffOn.fderivWithin Nat.cast_succ le_imp_le_of_le_of_le add_le_add_left WithTop.addRightMono Nat.mono_cast le_refl ContDiffOn.of_le Nat.cast_le IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass iteratedFDerivWithin_succ_eq_comp_right LinearIsometryEquiv.norm_map add_le_add tsub_le_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub ContinuousLinearMap.topologicalAddGroup iteratedFDerivWithin_congr fderivWithin_comp ContDiffOn.differentiableOn ne_of_gt Nat.cast_pos' NeZero.charZero_one Right.add_pos_of_nonneg_of_pos zero_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat ContDiffOn.comp LT.lt.le ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one ContinuousLinearMap.norm_compL_le Finset.sum_le_sum Real.instIsOrderedAddMonoid mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono mul_le_mul_of_nonneg_left Nat.cast_nonneg' Real.instZeroLEOneClass mul_nonneg le_of_lt IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Nat.factorial_pos pow_nonneg Finset.sum_congr Nat.cast_choose Finset.mem_range_succ_iff div_eq_inv_mul mul_inv Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_one_cast inv_mul_cancel₀ pow_add inv_le_one_of_one_le₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_pos Real.instNontrivial mul_assoc Finset.sum_const Finset.card_range nsmul_eq_mul Nat.cast_mul
norm_iteratedFDerivWithin_mul_le 📖	mathematical	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership 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	Real Real.instLE Norm.norm ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Fin.fintype iteratedFDerivWithin Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Finset.sum Real.instAddCommMonoid Finset.range Real.instMul Real.instNatCast Nat.choose	—	ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one IsScalarTower.right Algebra.to_smulCommClass ContinuousLinearMap.opNorm_mul_le
norm_iteratedFDerivWithin_prod_le 📖	mathematical	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership 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	Real Real.instLE Norm.norm ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Fin.fintype iteratedFDerivWithin Finset.prod CommRing.toCommMonoid NormedCommRing.toCommRing Finset.sum Sym Real.instAddCommMonoid Finset.sym Real.instMul Real.instNatCast Multiset.multinomial Sym.toMultiset Real.instCommMonoid Multiset.count	—	Finset.induction norm_iteratedFDerivWithin_zero NormOneClass.norm_one Finset.sum_congr Sym.eq_nil_of_card_zero Multiset.multinomial.congr_simp Multiset.multinomial_zero Nat.cast_one mul_one Finset.sum_const Finset.card_singleton one_smul iteratedFDerivWithin_succ_const norm_zero Finset.sup_empty Finset.prod_insert le_trans norm_iteratedFDerivWithin_mul_le contDiffOn_prod Finset.sum_coe_sort Finset.sum_equiv Equiv.symm_comp_self CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId Finset.prod_congr Finset.univ_sigma_univ Finset.sum_sigma Finset.sum_range Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_imp_le_of_le_of_le mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing WithTop.addLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero mul_nonneg Nat.cast_nonneg' Real.instZeroLEOneClass norm_nonneg le_refl Finset.mul_sum le_of_eq Sym.count_coe_fill_self_of_notMem Sym.multinomial_coe_fill_of_notMem Sym.count_coe_fill_of_ne Nat.cast_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
norm_iteratedFDerivWithin_smul_le 📖	mathematical	ContDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership 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	Real Real.instLE Norm.norm ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.sum Real.instAddCommMonoid Finset.range Real.instMul Real.instNatCast Nat.choose NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	—	ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one NormedSpace.toIsBoundedSMul ContinuousLinearMap.opNorm_lsmul_le
norm_iteratedFDeriv_clm_apply 📖	mathematical	ContDiff ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing 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 CommSemiring.toSemiring instCommSemiringENat	Real Real.instLE Norm.norm ContinuousMultilinearMap ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv DFunLike.coe ContinuousLinearMap.funLike Finset.sum Real.instAddCommMonoid Finset.range Real.instMul Real.instNatCast Nat.choose ContinuousLinearMap.toSeminormedAddCommGroup	—	RingHomIsometric.ids smulCommClass_self Finset.sum_congr norm_iteratedFDerivWithin_clm_apply ContDiff.contDiffOn uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.mem_univ
norm_iteratedFDeriv_clm_apply_const 📖	mathematical	ContDiffAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing 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 CommSemiring.toSemiring instCommSemiringENat	Real Real.instLE Norm.norm ContinuousMultilinearMap ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv DFunLike.coe ContinuousLinearMap.funLike Real.instMul NormedAddCommGroup.toNorm ContinuousLinearMap.toSeminormedAddCommGroup	—	RingHomIsometric.ids smulCommClass_self norm_iteratedFDerivWithin_clm_apply_const ContDiffAt.contDiffWithinAt uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.mem_univ
norm_iteratedFDeriv_comp_le 📖	mathematical	ContDiff 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 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 iteratedFDeriv Monoid.toNatPow Real.instMonoid	Real.instMul Real.instNatCast Nat.factorial	—	norm_iteratedFDeriv_comp_le' Set.subset_univ uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContDiff.contDiffOn
norm_iteratedFDeriv_comp_le' 📖	mathematical	Set Set.instHasSubset Set.range UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContDiffOn ContDiff 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 Real Real.instLE Norm.norm ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin iteratedFDeriv Monoid.toNatPow Real.instMonoid	Real.instMul Real.instNatCast Nat.factorial	—	norm_iteratedFDerivWithin_comp_le ContDiff.contDiffOn uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.mem_univ
norm_iteratedFDeriv_mul_le 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing 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	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Fin.fintype iteratedFDeriv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Finset.sum Real.instAddCommMonoid Finset.range Real.instMul Real.instNatCast Nat.choose	—	Finset.sum_congr norm_iteratedFDerivWithin_mul_le ContDiff.contDiffOn uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.mem_univ
norm_iteratedFDeriv_prod_le 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing 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	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Fin.fintype iteratedFDeriv Finset.prod CommRing.toCommMonoid NormedCommRing.toCommRing Finset.sum Sym Real.instAddCommMonoid Finset.sym Real.instMul Real.instNatCast Multiset.multinomial Sym.toMultiset Real.instCommMonoid Multiset.count	—	iteratedFDerivWithin_univ Finset.sum_congr Finset.prod_congr norm_iteratedFDerivWithin_prod_le ContDiff.contDiffOn uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.mem_univ
norm_iteratedFDeriv_smul_le 📖	mathematical	ContDiff NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing 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	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.sum Real.instAddCommMonoid Finset.range Real.instMul Real.instNatCast Nat.choose NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing	—	ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one NormedSpace.toIsBoundedSMul ContinuousLinearMap.opNorm_lsmul_le

---

← Back to Index