ExpDecay

📁 Source: Mathlib/MeasureTheory/Integral/ExpDecay.lean

Statistics

Metric	Count
Definitions	0
Theorems exp_neg_integrableOn_Ioi, integrable_of_isBigO_exp_neg	2
Total	2

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp_neg_integrableOn_Ioi 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.IntegrableOn MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp Real.instMul Real.instNeg Set.Ioi Real.instPreorder MeasureTheory.MeasureSpace.volume	—	Filter.Tendsto.div_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.neg IsTopologicalRing.toContinuousNeg Filter.Tendsto.comp Real.tendsto_exp_atBot Filter.Tendsto.const_mul_atTop_of_neg Real.instIsStrictOrderedRing neg_neg_iff_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Filter.tendsto_id MeasureTheory.integrableOn_Ioi_deriv_of_nonneg' IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology HasDerivAt.congr_simp neg_mul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mul_one mul_neg neg_neg IsUnit.mul_div_cancel_right LT.lt.ne' HasDerivAt.div_const HasDerivAt.neg HasDerivAt.exp HasDerivAt.const_mul hasDerivAt_id LT.lt.le Real.exp_pos
integrable_of_isBigO_exp_neg 📖	mathematical	Real Real.instLT Real.instZero ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ici Real.instPreorder Asymptotics.IsBigO Real.norm Filter.atTop Real.exp Real.instMul Real.instNeg	MeasureTheory.IntegrableOn MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Set.Ioi MeasureTheory.MeasureSpace.volume	—	integrableOn_Ici_iff_integrableOn_Ioi instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace PseudoEMetricSpace.pseudoMetrizableSpace Real.noAtoms_volume enorm_ne_top MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal atTop_isMeasurablyGenerated instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousOn.locallyIntegrableOn Real.locallyFinite_volume secondCountableTopologyEither_of_right measurableSet_Ici Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial exp_neg_integrableOn_Ioi

---

← Back to Index