Exponential

📁 Source: Mathlib/Probability/Distributions/Exponential.lean

Statistics

Metric	Count
Definitions `expMeasure`, `exponentialCDFReal`, `exponentialPDF`, `exponentialPDFReal`	4
Theorems `cdf_expMeasure_eq`, `cdf_expMeasure_eq_integral`, `cdf_expMeasure_eq_lintegral`, `exp_neg_integrableOn_Ioc`, `exponentialCDFReal_eq`, `exponentialCDFReal_eq_integral`, `exponentialCDFReal_eq_lintegral`, `exponentialPDFReal_nonneg`, `exponentialPDFReal_pos`, `exponentialPDF_eq`, `exponentialPDF_of_neg`, `exponentialPDF_of_nonneg`, `hasDerivAt_neg_exp_mul_exp`, `isProbabilityMeasureExponential`, `isProbabilityMeasure_expMeasure`, `lintegral_exponentialPDF_eq_antiDeriv`, `lintegral_exponentialPDF_eq_one`, `lintegral_exponentialPDF_of_nonpos`, `measurable_exponentialPDFReal`, `stronglyMeasurable_exponentialPDFReal`	20
Total	24

ProbabilityTheory

Definitions

Name	Category	Theorems
`expMeasure` 📖	CompOp	8 math math: `cdf_expMeasure_eq`, `isProbabilityMeasure_expMeasure`, `exponentialCDFReal_eq_integral`, `cdf_expMeasure_eq_integral`, `exponentialCDFReal_eq`, `cdf_expMeasure_eq_lintegral`, `isProbabilityMeasureExponential`, `exponentialCDFReal_eq_lintegral`
`exponentialCDFReal` 📖	CompOp	—
`exponentialPDF` 📖	CompOp	8 math math: `lintegral_exponentialPDF_eq_one`, `lintegral_exponentialPDF_eq_antiDeriv`, `exponentialPDF_eq`, `lintegral_exponentialPDF_of_nonpos`, `exponentialPDF_of_nonneg`, `exponentialPDF_of_neg`, `cdf_expMeasure_eq_lintegral`, `exponentialCDFReal_eq_lintegral`
`exponentialPDFReal` 📖	CompOp	6 math math: `exponentialPDFReal_nonneg`, `exponentialPDFReal_pos`, `exponentialCDFReal_eq_integral`, `cdf_expMeasure_eq_integral`, `measurable_exponentialPDFReal`, `stronglyMeasurable_exponentialPDFReal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cdf_expMeasure_eq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `expMeasure` `Real.instLE` `Real.decidableLE` `Real.instSub` `Real.instOne` `Real.exp` `Real.instNeg` `Real.instMul`	—	`cdf_expMeasure_eq_lintegral` `lintegral_exponentialPDF_eq_antiDeriv` `ENNReal.toReal_ofReal_eq_iff` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le` `le_rfl`
`cdf_expMeasure_eq_integral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `expMeasure` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `Real.instPreorder` `exponentialPDFReal`	—	`cdf_gammaMeasure_eq_integral` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`cdf_expMeasure_eq_lintegral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `expMeasure` `ENNReal.toReal` `MeasureTheory.lintegral` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `Real.instPreorder` `exponentialPDF`	—	`cdf_gammaMeasure_eq_lintegral` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`exp_neg_integrableOn_Ioc` 📖	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.instNeg` `Real.instMul` `Set.Ioc` `Real.instPreorder` `MeasureTheory.MeasureSpace.volume`	—	`neg_mul_eq_neg_mul` `MeasureTheory.IntegrableOn.mono_set` `exp_neg_integrableOn_Ioi` `Set.Ioc_subset_Ioi_self`
`exponentialCDFReal_eq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `expMeasure` `Real.instLE` `Real.decidableLE` `Real.instSub` `Real.instOne` `Real.exp` `Real.instNeg` `Real.instMul`	—	`cdf_expMeasure_eq`
`exponentialCDFReal_eq_integral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `expMeasure` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `Real.instPreorder` `exponentialPDFReal`	—	`cdf_expMeasure_eq_integral`
`exponentialCDFReal_eq_lintegral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `expMeasure` `ENNReal.toReal` `MeasureTheory.lintegral` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `Real.instPreorder` `exponentialPDF`	—	`cdf_expMeasure_eq_lintegral`
`exponentialPDFReal_nonneg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `exponentialPDFReal`	—	`gammaPDFReal_nonneg` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`exponentialPDFReal_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`exponentialPDFReal`	—	`gammaPDFReal_pos` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`exponentialPDF_eq` 📖	mathematical	—	`exponentialPDF` `ENNReal.ofReal` `Real` `Real.instLE` `Real.instZero` `Real.decidableLE` `Real.instMul` `Real.exp` `Real.instNeg`	—	`exponentialPDF.eq_1` `exponentialPDFReal.eq_1` `gammaPDFReal.eq_1` `Real.rpow_one` `Real.Gamma_one` `div_one` `sub_self` `Real.rpow_zero` `mul_one`
`exponentialPDF_of_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`exponentialPDF` `ENNReal` `instZeroENNReal`	—	`gammaPDF_of_neg`
`exponentialPDF_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`exponentialPDF` `ENNReal.ofReal` `Real.instMul` `Real.exp` `Real.instNeg`	—	`exponentialPDF_eq`
`hasDerivAt_neg_exp_mul_exp` 📖	mathematical	—	`HasDerivAt` `Real` `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.instNeg` `Real.exp` `Real.instMul`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `neg_mul` `one_mul` `mul_comm` `mul_neg` `mul_one` `neg_neg` `HasDerivAt.const_mul` `HasDerivAt.exp` `hasDerivAt_id`
`isProbabilityMeasureExponential` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.IsProbabilityMeasure` `Real.measurableSpace` `expMeasure`	—	`isProbabilityMeasure_expMeasure`
`isProbabilityMeasure_expMeasure` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.IsProbabilityMeasure` `Real.measurableSpace` `expMeasure`	—	`isProbabilityMeasure_gammaMeasure` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`lintegral_exponentialPDF_eq_antiDeriv` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.lintegral` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `Real.instPreorder` `exponentialPDF` `ENNReal.ofReal` `Real.instLE` `Real.decidableLE` `Real.instSub` `Real.instOne` `Real.exp` `Real.instNeg` `Real.instMul`	—	`lintegral_Iic_eq_lintegral_Iio_add_Icc` `lintegral_exponentialPDF_of_nonpos` `le_refl` `zero_add` `exponentialPDF_eq` `MeasureTheory.setLIntegral_congr_fun` `measurableSet_Icc` `BorelSpace.opensMeasurable` `Real.borelSpace` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ENNReal.toReal_eq_toReal_iff'` `ne_of_lt` `MeasureTheory.IntegrableOn.setLIntegral_lt_top` `integrableOn_Icc_iff_integrableOn_Ioc` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.noAtoms_volume` `enorm_ne_top` `MeasureTheory.Integrable.const_mul` `exp_neg_integrableOn_Ioc` `ENNReal.ofReal_ne_top` `MeasureTheory.integral_eq_lintegral_of_nonneg_ae` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.exp_pos` `MeasureTheory.Integrable.aestronglyMeasurable` `MeasureTheory.IntegrableOn.eq_1` `intervalIntegral.intervalIntegral_eq_integral_uIoc` `smul_eq_mul` `one_mul` `MeasureTheory.integral_Icc_eq_integral_Ioc` `Set.uIoc_of_le` `intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le` `Real.instCompleteSpace` `Continuous.rexp` `continuous_mul_left` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.continuousOn` `Continuous.comp'` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasDerivWithinAt.congr_simp` `neg_mul` `HasDerivAt.hasDerivWithinAt` `hasDerivAt_neg_exp_mul_exp` `ENNReal.toReal_ofReal_eq_iff` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.exp_le_one_iff` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.neg_congr` `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` `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.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `MulZeroClass.mul_zero` `neg_zero` `Real.exp_zero` `mul_one` `sub_neg_eq_add` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `measurableSet_Iic` `instClosedIicTopology` `lt_of_not_ge` `ENNReal.ofReal_eq_zero` `MeasureTheory.lintegral_zero` `ENNReal.ofReal_zero`
`lintegral_exponentialPDF_eq_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.lintegral` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `exponentialPDF` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`lintegral_gammaPDF_eq_one` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`lintegral_exponentialPDF_of_nonpos` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`MeasureTheory.lintegral` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iio` `Real.instPreorder` `exponentialPDF` `ENNReal` `instZeroENNReal`	—	`lintegral_gammaPDF_of_nonpos`
`measurable_exponentialPDFReal` 📖	mathematical	—	`Measurable` `Real` `Real.measurableSpace` `exponentialPDFReal`	—	`measurable_gammaPDFReal`
`stronglyMeasurable_exponentialPDFReal` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.measurableSpace` `exponentialPDFReal`	—	`stronglyMeasurable_gammaPDFReal`

---

← Back to Index