Documentation Verification Report

Gamma

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

Statistics

Metric	Count
Definitions	0
Theorems `integral_exp_neg_mul_rpow`, `integral_exp_neg_rpow`, `integral_rpow_mul_exp_neg_mul_rpow`, `integral_rpow_mul_exp_neg_rpow`, `integral_exp_neg_mul_rpow`, `integral_exp_neg_rpow`, `integral_rpow_mul_exp_neg_mul_rpow`, `integral_rpow_mul_exp_neg_rpow`	8
Total	8

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_exp_neg_mul_rpow` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `Real.instLT` `Real.instZero`	`MeasureTheory.integral` `Complex` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `FiniteDimensional.rclike_to_real` `instRCLike` `measurableSpace` `borelSpace` `MeasureTheory.MeasureSpace.volume` `Real.exp` `Real.instMul` `Real.instNeg` `Real.instPow` `Norm.norm` `instNorm` `Real.pi` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.Gamma` `Real.instAdd`	—	`FiniteDimensional.rclike_to_real` `borelSpace` `Nat.instAtLeastTwoHAddOfNat` `Real.rpow_zero` `one_mul` `zero_add` `Real.Gamma_add_one` `div_ne_zero` `two_ne_zero` `CharZero.NeZero.two` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `sub_eq_zero_of_eq` `Mathlib.Tactic.Ring.mul_congr` `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.Tactic.Ring.div_congr` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.mul_one` `integral_rpow_mul_exp_neg_mul_rpow` `lt_of_not_ge` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Meta.NormNum.isNat_lt_true`
`integral_exp_neg_rpow` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`MeasureTheory.integral` `Complex` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `FiniteDimensional.rclike_to_real` `instRCLike` `measurableSpace` `borelSpace` `MeasureTheory.MeasureSpace.volume` `Real.exp` `Real.instNeg` `Real.instPow` `Norm.norm` `instNorm` `Real.instMul` `Real.pi` `Real.Gamma` `Real.instAdd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`FiniteDimensional.rclike_to_real` `borelSpace` `Nat.instAtLeastTwoHAddOfNat` `Real.rpow_zero` `one_mul` `zero_add` `Real.Gamma_add_one` `div_ne_zero` `two_ne_zero` `CharZero.NeZero.two` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `sub_eq_zero_of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `integral_rpow_mul_exp_neg_rpow` `lt_of_not_ge` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Meta.NormNum.isNat_lt_true`
`integral_rpow_mul_exp_neg_mul_rpow` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `Real.instLT` `Real.instNeg` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instZero`	`MeasureTheory.integral` `Complex` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `FiniteDimensional.rclike_to_real` `instRCLike` `measurableSpace` `borelSpace` `MeasureTheory.MeasureSpace.volume` `Real.instMul` `Real.instPow` `Norm.norm` `instNorm` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `Real.instAdd` `Real.Gamma`	—	`Nat.instAtLeastTwoHAddOfNat` `FiniteDimensional.rclike_to_real` `borelSpace` `integral_comp_polarCoord_symm` `polarCoord_target` `norm_polarCoord_symm` `MeasureTheory.setIntegral_prod_mul` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `MeasureTheory.Measure.volume_eq_prod` `mul_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `MeasureTheory.integral_const` `Real.instCompleteSpace` `MeasureTheory.measureReal_restrict_apply` `MeasurableSet.univ` `Set.univ_inter` `Real.volume_real_Ioo_of_le` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `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_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `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` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.pi_nonneg` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `sub_neg_eq_add` `mul_comm` `MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `abs_eq_self` `LT.lt.le` `Set.mem_Ioi` `Real.rpow_add` `Real.rpow_one` `integral_rpow_mul_exp_neg_mul_rpow` `lt_of_not_ge` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_lt` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `add_assoc` `one_add_one_eq_two` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat`
`integral_rpow_mul_exp_neg_rpow` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `Real.instLT` `Real.instNeg` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`MeasureTheory.integral` `Complex` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `FiniteDimensional.rclike_to_real` `instRCLike` `measurableSpace` `borelSpace` `MeasureTheory.MeasureSpace.volume` `Real.instMul` `Real.instPow` `Norm.norm` `instNorm` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `Real.Gamma` `Real.instAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `FiniteDimensional.rclike_to_real` `borelSpace` `integral_comp_polarCoord_symm` `polarCoord_target` `norm_polarCoord_symm` `MeasureTheory.setIntegral_prod_mul` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `MeasureTheory.Measure.volume_eq_prod` `mul_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `MeasureTheory.integral_const` `Real.instCompleteSpace` `MeasureTheory.measureReal_restrict_apply` `MeasurableSet.univ` `Set.univ_inter` `Real.volume_real_Ioo_of_le` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `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_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `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` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.pi_nonneg` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `sub_neg_eq_add` `mul_comm` `MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `abs_eq_self` `LT.lt.le` `Set.mem_Ioi` `Real.rpow_add` `Real.rpow_one` `integral_rpow_mul_exp_neg_rpow` `lt_of_not_ge` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_lt` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `add_assoc` `one_add_one_eq_two` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_exp_neg_mul_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `Real.instPreorder` `Real.exp` `Real.instMul` `Real.instNeg` `Real.instPow` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.Gamma` `Real.instAdd`	—	`Real.rpow_zero` `one_mul` `zero_add` `Real.Gamma_add_one` `one_div_ne_zero` `ne_of_gt` `mul_assoc` `integral_rpow_mul_exp_neg_mul_rpow` `neg_one_lt_zero` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`integral_exp_neg_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `Real.instPreorder` `Real.exp` `Real.instNeg` `Real.instPow` `Real.Gamma` `Real.instAdd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`Real.rpow_zero` `one_mul` `zero_add` `Real.Gamma_add_one` `one_div_ne_zero` `ne_of_gt` `integral_rpow_mul_exp_neg_rpow` `neg_one_lt_zero` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`integral_rpow_mul_exp_neg_mul_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instNeg` `Real.instOne`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `Real.instPreorder` `Real.instMul` `Real.instPow` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instAdd` `Real.Gamma`	—	`MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Real.mul_rpow` `le_of_lt` `Real.rpow_pos_of_pos` `Real.rpow_mul` `inv_mul_cancel₀` `ne_of_gt` `Real.rpow_one` `mul_assoc` `Real.rpow_add` `neg_mul` `neg_add_cancel` `Real.rpow_zero` `one_mul` `MeasureTheory.integral_comp_mul_left_Ioi` `MulZeroClass.mul_zero` `smul_eq_mul` `MeasureTheory.integral_const_mul` `integral_rpow_mul_exp_neg_rpow` `Real.rpow_neg_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.div_pf`
`integral_rpow_mul_exp_neg_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instNeg` `Real.instOne`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `Real.instPreorder` `Real.instMul` `Real.instPow` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.Gamma` `Real.instAdd`	—	`MeasureTheory.integral_comp_rpow_Ioi` `one_div_ne_zero` `ne_of_gt` `abs_eq_self` `Real.instIsOrderedAddMonoid` `le_of_lt` `one_div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.rpow_mul` `one_div_mul_cancel` `Real.rpow_one` `mul_assoc` `div_mul_eq_mul_div` `one_mul` `Real.rpow_add` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf'` `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.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `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.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `add_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Real.Gamma_eq_integral` `div_pos` `neg_lt_iff_pos_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add`

---

← Back to Index