Integral

📁 Source: Mathlib/Analysis/SpecialFunctions/Pow/Integral.lean

Statistics

Metric	Count
Definitions	0
Theorems lintegral_rpow_eq_lintegral_meas_le_mul, lintegral_rpow_eq_lintegral_meas_lt_mul	2
Total	2

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lintegral_rpow_eq_lintegral_meas_le_mul 📖	mathematical	Filter.EventuallyLE Real Real.instLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero Real.instZero AEMeasurable Real.measurableSpace Real.instLT	lintegral ENNReal.ofReal Real.instPow ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring MeasureSpace.toMeasurableSpace Real.measureSpace Measure.restrict MeasureSpace.volume Set.Ioi Real.instPreorder DFunLike.coe Set setOf Real.instSub Real.instOne	—	Measure.instOuterMeasureClass 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.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.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat 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 Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le integral_rpow sub_add_cancel Real.zero_rpow LT.lt.ne sub_zero Filter.mp_mem self_mem_ae_restrict measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.univ_mem' Real.rpow_nonneg LT.lt.le Set.mem_Ioi intervalIntegral.intervalIntegrable_rpow' lintegral_comp_eq_lintegral_meas_le_mul lintegral_const_mul'' Measurable.aemeasurable measurable_const Measurable.comp_aemeasurable Measurable.ennreal_ofReal measurable_id AEMeasurable.div_const measurableDiv_of_mul_inv ContinuousMul.measurableMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal AEMeasurable.pow Real.hasMeasurablePow ENNReal.ofReal_mul mul_div_cancel₀
lintegral_rpow_eq_lintegral_meas_lt_mul 📖	mathematical	Filter.EventuallyLE Real Real.instLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero Real.instZero AEMeasurable Real.measurableSpace Real.instLT	lintegral ENNReal.ofReal Real.instPow ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring MeasureSpace.toMeasurableSpace Real.measureSpace Measure.restrict MeasureSpace.volume Set.Ioi Real.instPreorder DFunLike.coe Set setOf Real.instSub Real.instOne	—	Measure.instOuterMeasureClass lintegral_rpow_eq_lintegral_meas_le_mul lintegral_congr_ae Filter.mp_mem meas_le_ae_eq_meas_lt Measure.restrict.instNoAtoms Real.noAtoms_volume Filter.univ_mem'

---

← Back to Index