TemperateGrowth

📁 Source: Mathlib/Analysis/Distribution/TemperateGrowth.lean

Statistics

Metric	Count
Definitions HasTemperateGrowth, HasTemperateGrowth, integrablePower	3
Theorems hasTemperateGrowth, bilinear_hasTemperateGrowth, hasTemperateGrowth, hasTemperateGrowth_ofReal, add, comp, comp', const, fun_add, fun_mul, fun_neg, fun_pow, fun_smul, fun_sub, id, id', isBigO, isBigO_uniform, mul, neg, norm_iteratedFDeriv_le_uniform, norm_iteratedFDeriv_le_uniform_aux, of_fderiv, pow, smul, sub, sum, zero, hasTemperateGrowth_ofReal, hasTemperateGrowth_iff_isBigO, hasTemperateGrowth_inner_left, hasTemperateGrowth_inner_right, hasTemperateGrowth_norm_sq, hasTemperateGrowth_one_add_norm_sq_rpow, hasTemperateGrowth, instHasTemperateGrowth, exists_eLpNorm_lt_top, exists_integrable, instHasTemperateGrowth, integrable_pow_neg_integrablePower, integrable_of_le_of_pow_mul_le, integral_pow_mul_le_of_le_of_pow_mul_le, pow_mul_le_of_le_of_pow_mul_le	43
Total	46

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasTemperateGrowth 📖	mathematical	—	Function.HasTemperateGrowth DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike equivLike	—	RingHomInvPair.ids ContinuousLinearMap.hasTemperateGrowth

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bilinear_hasTemperateGrowth 📖	mathematical	Function.HasTemperateGrowth	DFunLike.coe 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 funLike topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain 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	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Function.hasTemperateGrowth_iff_isBigO ContDiff.comp Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsBoundedBilinearMap.contDiff isBoundedBilinearMap ContDiff.prodMk Function.HasTemperateGrowth.isBigO_uniform RingHomIsometric.ids norm_iteratedFDeriv_le_of_bilinear le_top Asymptotics.IsBigO.trans Asymptotics.IsBigO.of_norm_le Asymptotics.IsBigO.const_mul_left Asymptotics.IsBigO.sum mul_assoc pow_add Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass Asymptotics.IsBigO.norm_left
hasTemperateGrowth 📖	mathematical	—	Function.HasTemperateGrowth DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField funLike	—	Function.HasTemperateGrowth.of_fderiv fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace RingHomIsometric.ids smulCommClass_self differentiable LE.le.trans le_opNorm pow_one mul_add Distrib.leftDistribClass mul_one covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le

Function

Definitions

Name	Category	Theorems
HasTemperateGrowth 📖	MathDef	15 math math: HasTemperateGrowth.id', hasTemperateGrowth_inner_right, ContinuousLinearEquiv.hasTemperateGrowth, HasTemperateGrowth.const, HasTemperateGrowth.id, hasTemperateGrowth_iff_isBigO, HasTemperateGrowth.zero, hasTemperateGrowth_norm_sq, HasCompactSupport.hasTemperateGrowth, ContinuousLinearMap.hasTemperateGrowth, hasTemperateGrowth_inner_left, RCLike.hasTemperateGrowth_ofReal, Complex.hasTemperateGrowth_ofReal, hasTemperateGrowth_one_add_norm_sq_rpow, SchwartzMap.hasTemperateGrowth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasTemperateGrowth_iff_isBigO 📖	mathematical	—	HasTemperateGrowth ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Top.top instTopENat Asymptotics.IsBigO 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 Real.norm Filter Filter.instTop iteratedFDeriv Monoid.toNatPow Real.instMonoid Real.instAdd Real.instOne Norm.norm NormedAddCommGroup.toNorm	—	norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Real.norm_of_nonneg le_of_lt add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one norm_nonneg
hasTemperateGrowth_inner_left 📖	mathematical	—	HasTemperateGrowth Real InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner	—	ContinuousLinearMap.hasTemperateGrowth SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids RingHomIsometric.starRingEnd CStarRing.to_normedStarGroup instCStarRingReal
hasTemperateGrowth_inner_right 📖	mathematical	—	HasTemperateGrowth Real InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner	—	ContinuousLinearMap.hasTemperateGrowth SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul
hasTemperateGrowth_norm_sq 📖	mathematical	—	HasTemperateGrowth Real InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	RingHomIsometric.ids smulCommClass_self HasTemperateGrowth.of_fderiv SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul fderiv_norm_sq RingHomIsometric.starRingEnd CStarRing.to_normedStarGroup instCStarRingReal ContinuousLinearMap.hasTemperateGrowth Differentiable.norm_sq differentiable_id norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass norm_norm one_mul Nat.instAtLeastTwoHAddOfNat add_pow_two le_add_of_nonneg_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_of_lt add_pos_of_pos_of_nonneg pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one mul_nonneg IsOrderedRing.toPosMulMono mul_pos Mathlib.Meta.NormNum.instAtLeastTwo norm_nonneg
hasTemperateGrowth_one_add_norm_sq_rpow 📖	mathematical	—	HasTemperateGrowth Real InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instPow Real.instAdd Real.instOne Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	Nat.instAtLeastTwoHAddOfNat lt_add_of_lt_add_left IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.NormNum.isNNRat_lt_true Real.instIsStrictOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_add Nat.cast_zero Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul ContDiffOn.rpow_const_of_ne contDiffOn_fun_id LT.lt.ne' lt_trans IsOpen.uniqueDiffOn PerfectSpace.not_isolated instPerfectSpace IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalSemiring.toContinuousAdd isOpen_lt' instOrderTopologyReal HasTemperateGrowth.comp' exists_nat_ge Real.instIsOrderedRing Real.instArchimedean LE.le.trans le_sup_left le_sup_right Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono IsStrictOrderedRing.toPosMulStrictMono PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.Positivity.log_pos_of_isNNRat Mathlib.Tactic.FieldSimp.NF.cons_pos PosMulReflectLE.toPosMulReflectLT Real.instZeroLEOneClass zero_lt_one NeZero.one GroupWithZero.toNontrivial Finset.sum_nonneg norm_nonneg Real.contDiffAt_rpow_const norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin iteratedDerivWithin_eq_iteratedDeriv iteratedDeriv_eq_iterate Real.iter_deriv_rpow_const norm_mul NormedDivisionRing.toNormMulClass mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono Finset.single_le_sum one_div lt_of_lt_of_le LT.lt.le Real.abs_rpow_le_abs_rpow AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.rpow_natCast Real.rpow_le_rpow le_of_lt abs_pos_of_pos Mathlib.Meta.Positivity.pos_of_isNNRat IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add Real.rpow_le_rpow_of_exponent_le neg_sub Real.rpow_neg_eq_inv_rpow inv_pos_of_pos inv_lt_comm₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Mathlib.Meta.NormNum.isNat_lt_true Real.rpow_def_of_pos Real.exp_monotone le_trans mul_le_mul_of_nonneg_left sub_le_sub_right Nat.mono_cast Mathlib.Meta.Positivity.log_pos_of_isNat le_refl pow_le_pow_left₀ div_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial HasTemperateGrowth.fun_add HasTemperateGrowth.const hasTemperateGrowth_norm_sq

Function.Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasTemperateGrowth_ofReal 📖	mathematical	—	Function.HasTemperateGrowth Real Complex Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.ofReal	—	ContinuousLinearMap.hasTemperateGrowth

Function.HasTemperateGrowth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	Function.HasTemperateGrowth	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Function.hasTemperateGrowth_iff_isBigO ContDiff.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup iteratedFDeriv_add ContDiff.of_le le_top Filter.univ_mem' le_add_iff_nonneg_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le norm_nonneg Asymptotics.IsBigO.add Asymptotics.IsBigO.trans Asymptotics.IsBigO.pow_of_le_right
comp 📖	—	Function.HasTemperateGrowth	—	—	comp' PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul contDiffOn_univ iteratedFDerivWithin_univ norm_iteratedFDeriv_le_uniform
comp' 📖	—	Set Set.instHasSubset Set.range UniqueDiffOn Real Real.semiring NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContDiffOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Top.top instTopENat Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDerivWithin Real.instMul Monoid.toNatPow Real.instMonoid Real.instAdd Real.instOne NormedAddCommGroup.toNorm Function.HasTemperateGrowth	—	—	ContDiffOn.comp_contDiff norm_iteratedFDeriv_le_uniform norm_iteratedFDeriv_zero zero_le Nat.instCanonicallyOrderedAdd add_comm add_pow Finset.mul_sum Finset.sum_congr one_pow mul_one 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 mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono pow_le_pow_left₀ norm_nonneg Nat.cast_nonneg' Real.instZeroLEOneClass le_refl mul_pow mul_comm mul_left_comm mul_assoc pow_le_pow_right₀ IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le mul_le_mul_right Nat.instMulLeftMono mul_nonneg pow_nonneg IsOrderedRing.toZeroLEOneClass Finset.sum_mul covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass add_pos_of_pos_of_nonneg Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one le_self_pow₀ one_le_mul_of_one_le_of_one_le norm_iteratedFDeriv_comp_le' le_top pow_mul pow_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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 Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.pow_zero
const 📖	mathematical	—	Function.HasTemperateGrowth	—	of_fderiv RingHomIsometric.ids smulCommClass_self fderiv_fun_const zero differentiable_const pow_zero mul_one
fun_add 📖	mathematical	Function.HasTemperateGrowth	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	add
fun_mul 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace Real Real.normedField NormedRing.toSeminormedRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	mul
fun_neg 📖	mathematical	Function.HasTemperateGrowth	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	neg
fun_pow 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace Real Real.normedField NormedRing.toSeminormedRing	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	pow
fun_smul 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule	—	smul
fun_sub 📖	mathematical	Function.HasTemperateGrowth	SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub
id 📖	mathematical	—	Function.HasTemperateGrowth	—	RingHomIsometric.ids smulCommClass_self of_fderiv fderiv_id' IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace const differentiable_id pow_one one_mul covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Real.instZeroLEOneClass
id' 📖	mathematical	—	Function.HasTemperateGrowth	—	id
isBigO 📖	mathematical	Function.HasTemperateGrowth	Asymptotics.IsBigO ContinuousMultilinearMap Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype Real.norm Top.top Filter Filter.instTop iteratedFDeriv Monoid.toNatPow Real.instMonoid Real.instAdd Real.instOne Norm.norm NormedAddCommGroup.toNorm	—	Function.hasTemperateGrowth_iff_isBigO
isBigO_uniform 📖	mathematical	Function.HasTemperateGrowth	Asymptotics.IsBigO ContinuousMultilinearMap Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype Real.norm Top.top Filter Filter.instTop iteratedFDeriv Monoid.toNatPow Real.instMonoid Real.instAdd Real.instOne Norm.norm NormedAddCommGroup.toNorm	—	Asymptotics.IsBigO.trans Asymptotics.isBigO_of_le Real.norm_of_nonneg le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one norm_nonneg pow_le_pow_right₀ Real.instZeroLEOneClass IsOrderedRing.toPosMulMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Finset.le_sup Nat.instNoMaxOrder isBigO
mul 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace Real Real.normedField NormedRing.toSeminormedRing	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	ContinuousLinearMap.bilinear_hasTemperateGrowth IsScalarTower.right Algebra.to_smulCommClass
neg 📖	mathematical	Function.HasTemperateGrowth	Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	ContDiff.neg SeminormedAddCommGroup.toIsTopologicalAddGroup iteratedFDeriv_neg_apply norm_neg
norm_iteratedFDeriv_le_uniform 📖	mathematical	Function.HasTemperateGrowth	Real Real.instLE Real.instZero Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv Real.instMul Monoid.toNatPow Real.instMonoid Real.instAdd Real.instOne NormedAddCommGroup.toNorm	—	isBigO_uniform Asymptotics.IsBigO.exists_nonneg Real.norm_of_nonneg le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one norm_nonneg mul_nonneg IsOrderedRing.toPosMulMono
norm_iteratedFDeriv_le_uniform_aux 📖	mathematical	Function.HasTemperateGrowth	Real Real.instLE Real.instZero Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv Real.instMul Monoid.toNatPow Real.instMonoid Real.instAdd Real.instOne NormedAddCommGroup.toNorm	—	norm_iteratedFDeriv_le_uniform
of_fderiv 📖	—	Function.HasTemperateGrowth ContinuousLinearMap Real 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 NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing fderiv Differentiable Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instMul Monoid.toNatPow Real.instMonoid Real.instAdd Real.instOne	—	—	RingHomIsometric.ids smulCommClass_self contDiff_succ_iff_fderiv instIsEmptyFalse norm_iteratedFDeriv_zero IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass iteratedFDeriv_succ_eq_comp_right LinearIsometryEquiv.norm_map
pow 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace Real Real.normedField NormedRing.toSeminormedRing	Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	pow_zero const pow_succ mul
smul 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	Pi.smul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule	—	ContinuousLinearMap.bilinear_hasTemperateGrowth NormedSpace.toIsBoundedSMul Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
sub 📖	mathematical	Function.HasTemperateGrowth	Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	add neg
sum 📖	mathematical	Function.HasTemperateGrowth	Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Finset.induction_on Finset.sum_insert add
zero 📖	mathematical	—	Function.HasTemperateGrowth NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	contDiff_const iteratedFDeriv_zero_fun norm_zero mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing Mathlib.Meta.Positivity.nonneg_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Nat.cast_one norm_nonneg

Function.RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasTemperateGrowth_ofReal 📖	mathematical	—	Function.HasTemperateGrowth Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.ofReal	—	ContinuousLinearMap.hasTemperateGrowth

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasTemperateGrowth 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Top.top instTopENat	Function.HasTemperateGrowth	—	Continuous.norm ContDiff.continuous_iteratedFDeriv le_top Continuous.exists_forall_ge_of_hasCompactSupport instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid AddTorsor.nonempty norm iteratedFDeriv pow_zero mul_one

MeasureTheory.IsFiniteMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasTemperateGrowth 📖	mathematical	—	MeasureTheory.Measure.HasTemperateGrowth	—	CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike neg_zero Real.rpow_zero enorm_one NormedDivisionRing.to_normOneClass

MeasureTheory.Measure

Definitions

Name	Category	Theorems
HasTemperateGrowth 📖	CompData	2 math math: IsAddHaarMeasure.instHasTemperateGrowth, MeasureTheory.IsFiniteMeasure.instHasTemperateGrowth
integrablePower 📖	CompOp	2 math math: SchwartzMap.integral_pow_mul_iteratedFDeriv_le, integrable_pow_neg_integrablePower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_pow_neg_integrablePower 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instPow Real.instAdd Real.instOne Norm.norm NormedAddCommGroup.toNorm Real.instNeg Real.instNatCast integrablePower	—	HasTemperateGrowth.exists_integrable Real.rpow_neg_natCast zpow_neg zpow_natCast

MeasureTheory.Measure.HasTemperateGrowth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eLpNorm_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.instPow Real.instAdd Real.instOne Norm.norm NormedAddCommGroup.toNorm Real.instNeg Real.instNatCast Top.top instTopENNReal	—	MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound MeasureTheory.Measure.instOuterMeasureClass CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike neg_zero Real.rpow_zero CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass eq_or_ne MeasureTheory.eLpNorm_exponent_zero lt_add_of_pos_of_le IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one norm_nonneg exists_integrable Real.instIsStrictOrderedRing div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.le_ceil MeasureTheory.HasFiniteIntegral.mono' MeasureTheory.Integrable.hasFiniteIntegral MeasureTheory.ae_of_all Real.norm_of_nonneg Real.rpow_nonneg LT.lt.le Real.rpow_le_rpow_of_exponent_le IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le neg_le_neg MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top ENNReal.coe_ne_top neg_mul Real.rpow_mul Real.enorm_rpow_of_nonneg le_of_lt Real.rpow_pos_of_pos add_pos_of_pos_of_nonneg Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one NNReal.zero_le_coe MeasureTheory.hasFiniteIntegral_iff_enorm
exists_integrable 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instPow Real.instAdd Real.instOne Norm.norm NormedAddCommGroup.toNorm Real.instNeg Real.instNatCast	—	—

MeasureTheory.Measure.IsAddHaarMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasTemperateGrowth 📖	mathematical	—	MeasureTheory.Measure.HasTemperateGrowth	—	integrable_one_add_norm Nat.cast_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing RCLike.charZero_rclike Nat.cast_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_of_le_of_pow_mul_le 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instMul Monoid.toNatPow Real.instMonoid MeasureTheory.Measure.integrablePower MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.Integrable Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	—	MeasureTheory.Integrable.mono' Nat.instAtLeastTwoHAddOfNat MeasureTheory.Integrable.const_mul MeasureTheory.Measure.integrable_pow_neg_integrablePower MeasureTheory.AEStronglyMeasurable.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.AEStronglyMeasurable.pow MeasureTheory.AEStronglyMeasurable.norm aestronglyMeasurable_id PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass norm_mul NormedDivisionRing.toNormMulClass norm_pow NormedDivisionRing.to_normOneClass norm_norm pow_mul_le_of_le_of_pow_mul_le norm_nonneg
integral_pow_mul_le_of_le_of_pow_mul_le 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instMul Monoid.toNatPow Real.instMonoid MeasureTheory.Measure.integrablePower	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instPow Real.instAdd Real.instOne Real.instNeg	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.integral_const_mul MeasureTheory.integral_mul_const MeasureTheory.integral_mono_of_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_nonneg IsOrderedRing.toZeroLEOneClass norm_nonneg MeasureTheory.Integrable.mul_const MeasureTheory.Integrable.const_mul MeasureTheory.Measure.integrable_pow_neg_integrablePower LE.le.trans pow_mul_le_of_le_of_pow_mul_le le_of_eq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_right
pow_mul_le_of_le_of_pow_mul_le 📖	mathematical	Real Real.instLE Real.instZero Real.instMul Monoid.toNatPow Real.instMonoid	instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instAdd Real.instPow Real.instOne Real.instNeg	—	le_trans mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_nonneg IsOrderedRing.toZeroLEOneClass Nat.instAtLeastTwoHAddOfNat Real.div_rpow le_of_lt add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one zero_le_two Real.instZeroLEOneClass Real.rpow_neg_natCast zpow_neg zpow_natCast div_eq_inv_mul mul_neg mul_one neg_neg Real.rpow_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_right le_total mul_le_mul IsOrderedRing.toMulPosMono LE.le.trans pow_le_one₀ Real.one_le_rpow_of_pos_of_le_one_of_nonpos div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.sub_congr 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.mul_one Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le CancelDenoms.sub_subst CancelDenoms.div_subst CancelDenoms.add_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.add_nonpos Real.rpow_pos_of_pos Real.rpow_natCast mul_assoc Real.rpow_add lt_of_lt_of_le Nat.cast_add neg_add_cancel_comm_assoc Real.rpow_le_rpow_of_nonpos add_pos' Mathlib.Tactic.Ring.add_overlap_pf pow_pos IsStrictOrderedRing.toZeroLEOneClass

---

← Back to Index