NormPow

📁 Source: Mathlib/Analysis/InnerProductSpace/NormPow.lean

Statistics

Metric	Count
Definitions	0
Theorems norm_rpow, fderiv_norm_rpow, norm_rpow, contDiff_norm_rpow, differentiable_norm_rpow, enorm_fderiv_norm_rpow_le, fderiv_norm_rpow, hasDerivAt_abs_rpow, hasDerivAt_norm_rpow, hasFDerivAt_norm_rpow, nnnorm_fderiv_norm_rpow_le, norm_fderiv_norm_id_rpow, norm_fderiv_norm_rpow_le	13
Total	13

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_rpow 📖	mathematical	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Real.instLT Real.instOne	Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instPow Norm.norm NormedAddCommGroup.toNorm	—	comp contDiff_norm_rpow

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fderiv_norm_rpow 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike Real.instLT Real.instOne	fderiv Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing RCLike.innerProductSpace ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.instMul Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat ContinuousLinearMap.comp SeminormedAddCommGroup.toAddCommGroup RingHomCompTriple.ids DFunLike.coe Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.funLike innerSL	—	HasFDerivAt.fderiv RingHomCompTriple.ids Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalAddGroup.toContinuousAdd IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasFDerivAt.comp hasFDerivAt_norm_rpow DifferentiableAt.hasFDerivAt
norm_rpow 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike Real.instLT Real.instOne	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm	—	comp ContDiff.differentiable contDiff_norm_rpow one_ne_zero NeZero.charZero_one WithTop.charZero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiff_norm_rpow 📖	mathematical	Real Real.instLT Real.instOne	ContDiff DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup RCLike.toInnerProductSpaceReal WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Real.instPow Norm.norm NormedAddCommGroup.toNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup contDiff_one_iff_fderiv HasFDerivAt.differentiableAt Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup hasFDerivAt_norm_rpow fderiv_norm_rpow norm_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass smul_zero RingHomIsometric.ids tendsto_zero_iff_norm_tendsto_zero tendsto_of_tendsto_of_tendsto_of_le_of_le instOrderTopologyReal tendsto_const_nhds ContinuousAt.fun_mul continuousAt_const ContinuousAt.comp' Real.continuousAt_rpow_const covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le ContinuousAt.norm continuousAt_id' Real.zero_rpow sub_ne_zero_of_ne LT.lt.ne' MulZeroClass.mul_zero norm_nonneg Eq.le norm_fderiv_norm_id_rpow ContinuousAt.smul ContinuousLinearMap.continuousSMul RingHomSurjective.ids IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology Continuous.continuousAt ContinuousLinearMap.continuous
differentiable_norm_rpow 📖	mathematical	Real Real.instLT Real.instOne	Differentiable DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm	—	HasFDerivAt.differentiableAt Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup hasFDerivAt_norm_rpow
enorm_fderiv_norm_rpow_le 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	ENNReal Preorder.toLE ENNReal.instPartialOrder ENorm.enorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Real.pseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing SeminormedAddGroup.toContinuousENorm fderiv Real.instPow Norm.norm NormedAddCommGroup.toNorm NNReal.toReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal ENNReal.instPowReal Real.instSub Real.instOne	—	RingHomIsometric.ids ENNReal.coe_rpow_of_nonneg sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid NNReal.one_le_coe LT.lt.le nnnorm_fderiv_norm_rpow_le
fderiv_norm_rpow 📖	mathematical	Real Real.instLT Real.instOne	fderiv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing RCLike.innerProductSpace ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.instMul Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.funLike innerSL	—	HasFDerivAt.fderiv Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalAddGroup.toContinuousAdd IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivAt_norm_rpow
hasDerivAt_abs_rpow 📖	mathematical	Real Real.instLT Real.instOne	HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Real.instPow abs Real.lattice Real.instAddGroup Real.instMul Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	hasDerivAt_norm_rpow
hasDerivAt_norm_rpow 📖	mathematical	Real Real.instLT Real.instOne	HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Real.instPow Norm.norm Real.norm Real.instMul Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup conj_trivial instTrivialStarReal one_mul HasFDerivAt.hasDerivAt hasFDerivAt_norm_rpow
hasFDerivAt_norm_rpow 📖	mathematical	Real Real.instLT Real.instOne	HasFDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike InnerProductSpace.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.innerProductSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Real.instPow Norm.norm NormedAddCommGroup.toNorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Real.normedCommRing Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.instMul Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.funLike innerSL	—	Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup norm_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass smul_zero RingHomIsometric.ids sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid HasFDerivAt.eq_1 hasFDerivAtFilter_iff_isLittleO Real.zero_rpow LT.lt.ne' LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike sub_zero Real.rpow_one_add' norm_nonneg ne_of_gt add_pos' Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Asymptotics.IsBigO.mul_isLittleO NormedDivisionRing.toNormMulClass Asymptotics.isBigO_refl Asymptotics.isLittleO_const_iff ContinuousAt.tendsto ContinuousAt.rpow_const ContinuousAt.norm continuousAt_id LT.lt.le Asymptotics.isBigO_norm_left HasStrictFDerivAt.hasFDerivAt Real.rpow_natCast_mul Nat.cast_smul_eq_nsmul smul_smul Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.RingNF.int_rawCast_neg 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.zero_mul Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.mul_one HasStrictFDerivAt.rpow_const hasStrictFDerivAt_norm_sq isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors Nat.instCharZero
nnnorm_fderiv_norm_rpow_le 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	Preorder.toLE NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Real.pseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing fderiv Real.instPow Norm.norm NormedAddCommGroup.toNorm NNReal.toReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring instSemiringNNReal NNReal.instPowReal Real.instSub Real.instOne	—	norm_fderiv_norm_rpow_le
norm_fderiv_norm_id_rpow 📖	mathematical	Real Real.instLT Real.instOne	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.pseudoMetricSpace Real.instAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal ContinuousLinearMap.hasOpNorm fderiv Real.instPow NormedAddCommGroup.toNorm Real.instMul Real.instSub	—	Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup fderiv_norm_rpow norm_smul NormedSpace.toNormSMulClass RingHomIsometric.ids norm_mul NormedDivisionRing.toNormMulClass Real.norm_rpow_of_nonneg norm_nonneg norm_norm abs_eq_self Real.instIsOrderedAddMonoid LE.le.trans zero_le_one Real.instZeroLEOneClass LT.lt.le mul_assoc innerSL_apply_norm Real.rpow_add_one' Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing sub_eq_zero_of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero 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.zero_mul
norm_fderiv_norm_rpow_le 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike Real.instLT Real.instOne	Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Real.pseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal ContinuousLinearMap.hasOpNorm fderiv Real.instPow NormedAddCommGroup.toNorm Real.instMul Real.instSub	—	Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat RingHomCompTriple.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup Differentiable.fderiv_norm_rpow norm_smul NormedSpace.toNormSMulClass RingHomIsometric.ids norm_mul NormedDivisionRing.toNormMulClass Real.norm_rpow_of_nonneg norm_nonneg norm_norm abs_eq_self Real.instIsOrderedAddMonoid LE.le.trans zero_le_one Real.instZeroLEOneClass LT.lt.le mul_assoc mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing LE.le.trans_eq ContinuousLinearMap.opNorm_comp_le Real.rpow_nonneg innerSL_apply_norm Real.rpow_add_one' Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt sub_eq_zero_of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero 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.zero_mul le_of_lt lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial

---

← Back to Index