IntegralRepresentation

📁 Source: Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean

Statistics

Metric	Count
Definitions rpowIntegrand₀₁	1
Theorems cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one, exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁, monotoneOn_cfcₙ_rpowIntegrand₀₁, aestronglyMeasurable_rpowIntegrand₀₁, continuousOn_rpowIntegrand₀₁, continuousOn_rpowIntegrand₀₁_Ici, continuousOn_rpowIntegrand₀₁_uncurry, exists_measure_rpow_eq_integral, integrableOn_rpowIntegrand₀₁_Ici, integrableOn_rpowIntegrand₀₁_Ioi, integral_rpowIntegrand₀₁_eq_rpow_mul_const, integral_rpowIntegrand₀₁_one_pos, le_integral_rpowIntegrand₀₁_one, rpowIntegrand₀₁_apply_mul, rpowIntegrand₀₁_apply_mul', rpowIntegrand₀₁_apply_mul_eqOn_Ici, rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one, rpowIntegrand₀₁_eqOn_pow_div, rpowIntegrand₀₁_eq_pow_div, rpowIntegrand₀₁_le_rpow_sub_one, rpowIntegrand₀₁_le_rpow_sub_two_mul_self, rpowIntegrand₀₁_monotoneOn, rpowIntegrand₀₁_nonneg, rpowIntegrand₀₁_one_ge_rpow_sub_two, rpowIntegrand₀₁_zero_left, rpowIntegrand₀₁_zero_right, rpow_eq_const_mul_integral	27
Total	28

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one 📖	mathematical	Real Set Set.instMembership Set.Ioo Real.instPreorder Real.instZero Real.instOne Real.instLT Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	cfcₙ IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup Real.rpowIntegrand₀₁ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid Real.instPow Real.instSub Real.instInv	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing cfcₙ_congr Set.EqOn.mono Real.rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one cfcₙ_smul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsScalarTower.left Pi.isScalarTower IsScalarTower.right ContinuousOn.mono Real.continuousOn_rpowIntegrand₀₁_Ici zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike ContinuousOn.comp' ContinuousOn.const_smul continuousOn_id' MulZeroClass.mul_zero Real.rpowIntegrand₀₁_zero_right cfcₙ_comp_smul RCLike.uniqueNonUnitalContinuousFunctionalCalculus TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Set.MapsTo.image_subset Set.MapsTo.mono_left IsSelfAdjoint.of_nonneg
exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ 📖	mathematical	NNReal Set Set.instMembership Set.Ioo PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal instOneNNReal	MeasureTheory.IntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup cfcₙ IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedSpace.toModule Real.normedField Real.rpowIntegrand₀₁ NNReal.toReal Set.Ioi Real.instPreorder Real.instZero instPowNNReal MeasureTheory.integral NonUnitalNormedRing.toNormedAddCommGroup MeasureTheory.Measure.restrict	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Real.exists_measure_rpow_eq_integral Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Nat.cast_zero le_csSup_of_le IsCompact.bddAbove instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Real.continuousOn_rpowIntegrand₀₁_uncurry MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem MeasureTheory.ae_restrict_mem measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology Filter.univ_mem' Real.norm_of_nonneg Real.rpowIntegrand₀₁_nonneg le_of_lt Real.rpowIntegrand₀₁_monotoneOn le_csSup quasispectrum.isCompact instProperSpaceReal MeasureTheory.hasFiniteIntegral_norm_iff Real.rpowIntegrand₀₁_zero_right integrableOn_cfcₙ secondCountableTopologyEither_of_left instSecondCountableTopologyReal IsSelfAdjoint.of_nonneg IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar nnrpow_eq_cfcₙ_real TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace NonUnitalSeminormedRing.toIsTopologicalRing cfcₙ_congr cfcₙ_setIntegral LE.le.isSelfAdjoint
monotoneOn_cfcₙ_rpowIntegrand₀₁ 📖	mathematical	Real Set Set.instMembership Set.Ioo Real.instPreorder Real.instZero Real.instOne Real.instLT	MonotoneOn PartialOrder.toPreorder cfcₙ IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace IsScalarTower.complexToReal NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup Complex Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalCStarAlgebra.toIsScalarTower SMulCommClass.complexToReal NonUnitalCStarAlgebra.toSMulCommClass IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus IsStarNormal.instNonUnitalContinuousFunctionalCalculus Real.rpowIntegrand₀₁ Set.Ici MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower SMulCommClass.complexToReal NonUnitalCStarAlgebra.toSMulCommClass IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus IsStarNormal.instNonUnitalContinuousFunctionalCalculus cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one CStarAlgebra.instNonnegSpectrumClass' smul_le_smul_of_nonneg_left IsOrderedModule.toPosSMulMono instIsOrderedModule Real.instStarOrderedRing StarModule.complexToReal NonUnitalCStarAlgebra.toStarModule cfcₙ.congr_simp Real.one_rpow inv_one one_mul monotoneOn_one_sub_one_add_inv_real Mathlib.Meta.Positivity.smul_nonneg_of_pos_of_nonneg inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing le_of_lt Real.rpow_pos_of_pos

Real

Definitions

Name	Category	Theorems
rpowIntegrand₀₁ 📖	CompOp	27 math math: continuousOn_rpowIntegrand₀₁_uncurry, integrableOn_rpowIntegrand₀₁_Ioi, rpowIntegrand₀₁_monotoneOn, rpow_eq_const_mul_integral, rpowIntegrand₀₁_zero_right, aestronglyMeasurable_rpowIntegrand₀₁, rpowIntegrand₀₁_le_rpow_sub_two_mul_self, rpowIntegrand₀₁_apply_mul_eqOn_Ici, integral_rpowIntegrand₀₁_one_pos, rpowIntegrand₀₁_zero_left, rpowIntegrand₀₁_nonneg, rpowIntegrand₀₁_apply_mul, rpowIntegrand₀₁_eq_pow_div, continuousOn_rpowIntegrand₀₁_Ici, le_integral_rpowIntegrand₀₁_one, CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁, CFC.cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one, rpowIntegrand₀₁_le_rpow_sub_one, continuousOn_rpowIntegrand₀₁, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, integral_rpowIntegrand₀₁_eq_rpow_mul_const, rpowIntegrand₀₁_apply_mul', rpowIntegrand₀₁_one_ge_rpow_sub_two, exists_measure_rpow_eq_integral, rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one, integrableOn_rpowIntegrand₀₁_Ici, rpowIntegrand₀₁_eqOn_pow_div

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_rpowIntegrand₀₁ 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace measurableSpace MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace rpowIntegrand₀₁ MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi	—	ContinuousOn.aestronglyMeasurable secondCountableTopologyEither_of_right instSecondCountableTopologyReal BorelSpace.opensMeasurable borelSpace PseudoEMetricSpace.pseudoMetrizableSpace continuousOn_rpowIntegrand₀₁ measurableSet_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid
continuousOn_rpowIntegrand₀₁ 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace rpowIntegrand₀₁ Set.Ioi	—	ContinuousOn.congr ContinuousOn.rpow_const continuousOn_id' LT.lt.ne' ContinuousOn.div₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousOn.fun_mul continuousOn_const ContinuousOn.fun_add IsTopologicalSemiring.toContinuousAdd instLawfulOrderLT_mathlib instIsPreorder_mathlib instOrderedAddOfAddRightMonoOfAddRightReflectLE covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le instOrderedRingOfIsStrictOrderedRing instIsStrictOrderedRing Set.mem_Ioi rpowIntegrand₀₁_eqOn_pow_div
continuousOn_rpowIntegrand₀₁_Ici 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLT	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace rpowIntegrand₀₁ Set.Ici	—	ContinuousOn.uncurry_left continuousOn_rpowIntegrand₀₁_uncurry
continuousOn_rpowIntegrand₀₁_uncurry 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne Set.instHasSubset Set.Ici	ContinuousOn instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace rpowIntegrand₀₁ SProd.sprod Set.instSProd Set.Ioi	—	ContinuousOn.congr ContinuousOn.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousOn.rpow_const ContinuousOn.fst continuousOn_id' ContinuousOn.snd ContinuousOn.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal ContinuousOn.fun_add IsTopologicalSemiring.toContinuousAdd rpowIntegrand₀₁_eq_pow_div le_of_lt
exists_measure_rpow_eq_integral 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne	MeasureTheory.IntegrableOn measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing rpowIntegrand₀₁ Set.Ioi instPow MeasureTheory.integral normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict	—	inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing le_of_lt integral_rpowIntegrand₀₁_one_pos IsScalarTower.right MeasureTheory.Measure.restrict_smul MeasureTheory.Integrable.smul_measure_nnreal integrableOn_rpowIntegrand₀₁_Ioi MeasureTheory.integral_smul_nnreal_measure rpow_eq_const_mul_integral
integrableOn_rpowIntegrand₀₁_Ici 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	MeasureTheory.IntegrableOn MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing rpowIntegrand₀₁ Set.Ici MeasureTheory.MeasureSpace.volume	—	MeasureTheory.IntegrableOn.congr_set_ae integrableOn_rpowIntegrand₀₁_Ioi Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Ioi_ae_eq_Ici noAtoms_volume
integrableOn_rpowIntegrand₀₁_Ioi 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	MeasureTheory.IntegrableOn MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing rpowIntegrand₀₁ Set.Ioi MeasureTheory.MeasureSpace.volume	—	Set.Ioc_union_Ioi_eq_Ioi zero_le_one instZeroLEOneClass MeasureTheory.IntegrableOn.union PseudoEMetricSpace.pseudoMetrizableSpace
integral_rpowIntegrand₀₁_eq_rpow_mul_const 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	MeasureTheory.integral normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi rpowIntegrand₀₁ instMul instPow	—	LE.le.eq_or_lt add_zero sub_self MulZeroClass.mul_zero MeasureTheory.integral_zero zero_rpow LT.lt.ne' MulZeroClass.zero_mul Set.EqOn.mono Set.Ioi_subset_Ici_self rpowIntegrand₀₁_apply_mul_eqOn_Ici LT.lt.le MeasureTheory.setIntegral_congr_fun measurableSet_Ioi BorelSpace.opensMeasurable borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid smul_eq_mul integral_smul_const instCompleteSpace mul_comm MeasureTheory.integral_comp_mul_deriv_Ioi ContinuousOn.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuousOn_const continuousOn_id' Filter.Tendsto.const_mul_atTop instIsStrictOrderedRing Filter.tendsto_id IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivWithinAt.congr_simp mul_one HasDerivWithinAt.const_mul hasDerivWithinAt_id Set.image_mul_left_Ioi PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono continuousOn_rpowIntegrand₀₁ Set.image_mul_left_Ici integrableOn_rpowIntegrand₀₁_Ici MeasureTheory.integrableOn_congr_fun measurableSet_Ici instClosedIciTopology MeasureTheory.Integrable.mul_const zero_le_one instZeroLEOneClass
integral_rpowIntegrand₀₁_one_pos 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne	instLT MeasureTheory.integral normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi rpowIntegrand₀₁	—	Nat.instAtLeastTwoHAddOfNat neg_div neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid one_div_neg IsOrderedRing.toPosMulMono instIsOrderedRing lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Nat.cast_one 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_nonpos_of_le le_integral_rpowIntegrand₀₁_one
le_integral_rpowIntegrand₀₁_one 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne	instLE DivInvMonoid.toDiv instDivInvMonoid instNeg instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instSub MeasureTheory.integral normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi rpowIntegrand₀₁	—	Nat.instAtLeastTwoHAddOfNat div_div neg_div one_div one_rpow mul_neg mul_one MeasureTheory.integral_const_mul integral_Ioi_rpow_of_lt lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.neg_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_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_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.mul_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.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one add_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.mul_assoc_rev MeasureTheory.setIntegral_mono_on instIsOrderedAddMonoid instIsOrderedModule instStarOrderedRing RCLike.instStarModuleReal IsScalarTower.right Algebra.to_smulCommClass instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal MeasureTheory.Integrable.const_mul integrableOn_Ioi_rpow_of_lt zero_le_one measurableSet_Ioi BorelSpace.opensMeasurable borelSpace instClosedIicTopology rpowIntegrand₀₁_one_ge_rpow_sub_two le_of_lt MeasureTheory.setIntegral_mono_set integrableOn_rpowIntegrand₀₁_Ioi MeasureTheory.ae_restrict_of_forall_mem rpowIntegrand₀₁_nonneg Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass Set.Ioi_subset_Ioi
rpowIntegrand₀₁_apply_mul 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	rpowIntegrand₀₁ instMul instPow instSub	—	mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing rpowIntegrand₀₁_eq_pow_div zero_le_one instZeroLEOneClass MulZeroClass.zero_mul zero_rpow Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.neg_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Set.mem_Ioo neg_eq_zero sub_eq_zero_of_eq MulZeroClass.mul_zero add_zero div_zero mul_one mul_assoc mul_div_assoc mul_rpow 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.add_pf_add_lt div_mul_eq_div_mul_one_div div_self one_mul mul_comm
rpowIntegrand₀₁_apply_mul' 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	instMul rpowIntegrand₀₁ instPow	—	rpowIntegrand₀₁_apply_mul mul_assoc rpow_one sub_add_cancel rpow_add'
rpowIntegrand₀₁_apply_mul_eqOn_Ici 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	Set.EqOn instMul rpowIntegrand₀₁ instPow Set.Ici	—	rpowIntegrand₀₁_apply_mul'
rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one 📖	mathematical	Real instLT instZero	Set.EqOn rpowIntegrand₀₁ instMul instPow instSub instOne Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id instInv Set.Ici instPreorder	—	IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add 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.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial one_div rpow_sub_one LT.lt.ne' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.inv_congr 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_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf one_rpow inv_one mul_comm
rpowIntegrand₀₁_eqOn_pow_div 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	Set.EqOn rpowIntegrand₀₁ DivInvMonoid.toDiv instDivInvMonoid instMul instPow instSub instAdd Set.Ioi	—	rpowIntegrand₀₁_eq_pow_div le_of_lt
rpowIntegrand₀₁_eq_pow_div 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	rpowIntegrand₀₁ DivInvMonoid.toDiv instDivInvMonoid instMul instPow instSub instAdd	—	Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.neg_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing neg_eq_zero sub_eq_zero_of_eq zero_rpow LT.lt.ne' inv_zero zero_add zero_sub mul_neg MulZeroClass.zero_mul neg_zero zero_div ne_of_gt add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_of_le_of_ne' inv_eq_one_div div_sub_div one_mul mul_one add_sub_cancel_left Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons 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₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero rpow_pos_of_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial rpow_sub_one
rpowIntegrand₀₁_le_rpow_sub_one 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	rpowIntegrand₀₁ instPow instSub	—	add_zero sub_self MulZeroClass.mul_zero rpow_nonneg rpowIntegrand₀₁_eq_pow_div div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing le_of_lt lt_of_le_of_ne' le_refl 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.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_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.div_congr 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.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul 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 div_eq_one_iff_eq mul_one
rpowIntegrand₀₁_le_rpow_sub_two_mul_self 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLT instLE	rpowIntegrand₀₁ instMul instPow instSub instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat rpowIntegrand₀₁_eq_pow_div le_of_lt div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing rpow_pos_of_pos le_refl 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.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_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.div_congr 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_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 rpow_sub_one ne_of_gt Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.instAtLeastTwo
rpowIntegrand₀₁_monotoneOn 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	MonotoneOn rpowIntegrand₀₁ Set.Ici	—	add_zero sub_self MulZeroClass.mul_zero rpowIntegrand₀₁_nonneg mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono instIsOrderedRing sub_le_sub_left IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add inv_anti₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Right.add_pos_of_nonneg_of_pos lt_of_le_of_ne' add_le_add_right rpow_nonneg
rpowIntegrand₀₁_nonneg 📖	mathematical	Real instLT instZero instLE	rpowIntegrand₀₁	—	eq_or_lt_of_le' zero_rpow ne_of_gt inv_zero zero_add zero_sub mul_neg MulZeroClass.zero_mul neg_zero mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing le_of_lt rpow_pos_of_pos sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid inv_anti₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono 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.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_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt
rpowIntegrand₀₁_one_ge_rpow_sub_two 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	instMul DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instPow instSub rpowIntegrand₀₁	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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 Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add rpow_sub lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr 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.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing neg_neg_of_pos instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing rpow_one Mathlib.Tactic.Ring.mul_congr 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 RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_one mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono mul_div_assoc one_div_mul_one_div one_div_le_one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_pos Mathlib.Meta.Positivity.pos_of_isNat instNontrivial lt_of_lt_of_le add_pos' IsOrderedAddMonoid.toAddLeftMono le_of_not_gt Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_neg_of_lt le_of_lt rpow_pos_of_pos rpowIntegrand₀₁_eq_pow_div Mathlib.Tactic.Linarith.add_neg zero_le_one instZeroLEOneClass
rpowIntegrand₀₁_zero_left 📖	mathematical	Real instLT instZero	rpowIntegrand₀₁	—	zero_rpow LT.lt.ne' inv_zero zero_add zero_sub mul_neg MulZeroClass.zero_mul neg_zero
rpowIntegrand₀₁_zero_right 📖	mathematical	—	rpowIntegrand₀₁ Real instZero	—	add_zero sub_self MulZeroClass.mul_zero
rpow_eq_const_mul_integral 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne instLE	instPow instMul instInv MeasureTheory.integral normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi rpowIntegrand₀₁	—	eq_or_lt_of_le' zero_rpow 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.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_zero_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing sub_eq_zero_of_eq rpowIntegrand₀₁_zero_right MeasureTheory.integral_zero MulZeroClass.mul_zero ne_of_gt integral_rpowIntegrand₀₁_one_pos integral_rpowIntegrand₀₁_eq_rpow_mul_const mul_comm mul_assoc mul_inv_cancel₀ mul_one

---

← Back to Index