Layercake

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

Statistics

Metric	Count
Definitions	0
Theorems integral_eq_integral_Ioc_meas_le, integral_eq_integral_meas_le, integral_eq_integral_meas_lt, countable_meas_le_ne_meas_lt, lintegral_comp_eq_lintegral_meas_le_mul, lintegral_comp_eq_lintegral_meas_le_mul_of_measurable, lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite, lintegral_comp_eq_lintegral_meas_lt_mul, lintegral_eq_lintegral_meas_le, lintegral_eq_lintegral_meas_lt, meas_le_ae_eq_meas_lt	11
Total	11

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_meas_le_ne_meas_lt 📖	mathematical	—	Set.Countable setOf ENNReal DFunLike.coe Measure Set Measure.instFunLike Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	Set.Countable.mono countable_image_gt_image_Ioi ENNReal.instOrderTopology ENNReal.instSecondCountableTopology lt_of_le_of_ne measure_mono Measure.instOuterMeasureClass le_of_lt LT.lt.trans_le
lintegral_comp_eq_lintegral_meas_le_mul 📖	mathematical	Filter.EventuallyLE Real Real.instLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero Real.instZero AEMeasurable Real.measurableSpace IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup MeasureSpace.volume Real.measureSpace Filter.Eventually MeasureSpace.toMeasurableSpace Measure.restrict Set.Ioi Real.instPreorder	lintegral ENNReal.ofReal intervalIntegral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Set setOf	—	Measure.instOuterMeasureClass AEMeasurable.exists_measurable_nonneg aemeasurable_Ioi_of_forall_Ioc instIsCountablyGenerated_atTop instOrderTopologyReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace ae_mono Measure.restrict_mono Set.Ioc_subset_Ioi_self le_rfl IntegrableOn.congr_fun_ae Set.Ioc_eq_empty_of_le LT.lt.le GT.gt.lt integrableOn_empty Measurable.max BorelSpace.opensMeasurable HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid measurable_const le_max_right Filter.mp_mem Filter.univ_mem' max_eq_left lintegral_congr_ae measure_congr intervalIntegral.integral_congr_ae Set.uIoc_of_le ae_restrict_iff' measurableSet_Ioc instClosedIicTopology lintegral_comp_eq_lintegral_meas_le_mul_of_measurable
lintegral_comp_eq_lintegral_meas_le_mul_of_measurable 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Measurable Real.measurableSpace IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup MeasureSpace.volume Real.measureSpace	lintegral ENNReal.ofReal intervalIntegral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureSpace.toMeasurableSpace Measure.restrict Set.Ioi Real.instPreorder ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike setOf	—	Measure.instOuterMeasureClass intervalIntegral.integral_of_le integral_congr_ae ae_restrict_of_ae_restrict_of_subset Set.Ioc_subset_Ioi_self intervalIntegral.integral_zero ENNReal.ofReal_zero lintegral_const MulZeroClass.zero_mul Filter.mp_mem Filter.univ_mem' MulZeroClass.mul_zero lintegral_congr_ae Measure.restrict_apply Set.univ_inter Real.volume_Ioi eq_top_iff ofReal_integral_eq_lintegral_ofReal ae_restrict_mem measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid LT.lt.le lintegral_const_mul Measurable.comp ENNReal.measurable_ofReal ENNReal.top_mul setLIntegral_mono' mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid measure_mono Set.setOf_subset_setOf_of_imp LE.le.trans le_of_lt lintegral_mono_set ENNReal.mul_top measurableSet_lt instSecondCountableTopologyReal measurable_const ENNReal.ofReal_le_ofReal intervalIntegral.integral_mono_interval le_rfl LT.lt.trans setLIntegral_le_lintegral Mathlib.Tactic.Contrapose.contrapose₂ not_bddAbove_iff Set.Ioc_subset_Ioc_right ae_restrict_iUnion_iff instCountableNat Set.iUnion_Ioc_eq_Ioi_self_iff exists_nat_ge Real.instIsOrderedRing Real.instArchimedean ae_restrict_eq Set.Ioc_eq_empty Filter.principal_empty inf_of_le_right le_csSup restrict_Ioo_eq_restrict_Ioc Real.noAtoms_volume exists_seq_strictMono_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instNontrivial TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace exists_lt_of_lt_csSup Set.nonempty_of_mem Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_order Set.mem_iUnion exists_seq_strictAnti_tendsto instNoMaxOrderOfNontrivial measurableSet_le Set.disjoint_iff_inter_eq_empty Set.disjoint_left measure_empty lt_top_iff_ne_top Mathlib.Tactic.Push.not_and_eq LE.le.trans_lt le_antisymm not_lt integral_nonneg_of_ae IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology integral_eq_zero_iff_of_nonneg_ae lt_irrefl lt_of_le_of_lt measure_union_le zero_add Measure.restrict_le_self Set.eq_univ_iff_forall le_or_gt setLIntegral_congr_fun MeasurableSet.compl ae_mono Measure.restrict_mono lintegral_add_compl add_zero measurableSet_Ioi Set.inter_eq_left LT.lt.trans_le Set.mem_Ioi Set.Ioc_union_Ioi_eq_Ioi Set.Ioc_disjoint_Ioi lintegral_union lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite instSFiniteOfSigmaFinite
lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Measurable Real.measurableSpace IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup MeasureSpace.volume Real.measureSpace	lintegral ENNReal.ofReal intervalIntegral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureSpace.toMeasurableSpace Measure.restrict Set.Ioi Real.instPreorder ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike setOf	—	eq_or_lt_of_le Measure.instOuterMeasureClass Filter.mp_mem self_mem_ae_restrict measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.univ_mem' ofReal_integral_eq_lintegral_ofReal intervalIntegral.integral_of_le lintegral_congr lintegral_indicator measurableSet_Ioi lintegral_lintegral_swap instSFiniteOfSigmaFinite Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Set.indicator_of_mem Set.indicator_of_notMem measurableSet_region_between_oc measurable_zero MeasurableSet.univ AEMeasurable.indicator₀ Measurable.aemeasurable Measurable.comp ENNReal.measurable_ofReal measurable_snd MeasurableSet.nullMeasurableSet mul_one MulZeroClass.mul_zero MulZeroClass.zero_mul lintegral_const_mul' ENNReal.mul_ne_top ENNReal.ofReal_ne_top lintegral_indicator₀ Measurable.nullMeasurable measurableSet_Ici instClosedIciTopology lintegral_one Measure.restrict_apply Set.univ_inter Set.indicator_mul_left mul_assoc one_mul mul_comm
lintegral_comp_eq_lintegral_meas_lt_mul 📖	mathematical	Filter.EventuallyLE Real Real.instLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero Real.instZero AEMeasurable Real.measurableSpace IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup MeasureSpace.volume Real.measureSpace Filter.Eventually MeasureSpace.toMeasurableSpace Measure.restrict Set.Ioi Real.instPreorder	lintegral ENNReal.ofReal intervalIntegral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Set setOf Real.instLT	—	Measure.instOuterMeasureClass lintegral_comp_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'
lintegral_eq_lintegral_meas_le 📖	mathematical	Filter.EventuallyLE Real Real.instLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero Real.instZero AEMeasurable Real.measurableSpace	lintegral ENNReal.ofReal MeasureSpace.toMeasurableSpace Real.measureSpace Measure.restrict MeasureSpace.volume Set.Ioi Real.instPreorder DFunLike.coe Set ENNReal setOf	—	Measure.instOuterMeasureClass intervalIntegrable_const Real.locallyFinite_volume enorm_ne_top lintegral_comp_eq_lintegral_meas_le_mul Filter.Eventually.of_forall zero_le_one Real.instZeroLEOneClass mul_one ENNReal.ofReal_one intervalIntegral.integral_const Real.instCompleteSpace sub_zero
lintegral_eq_lintegral_meas_lt 📖	mathematical	Filter.EventuallyLE Real Real.instLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero Real.instZero AEMeasurable Real.measurableSpace	lintegral ENNReal.ofReal MeasureSpace.toMeasurableSpace Real.measureSpace Measure.restrict MeasureSpace.volume Set.Ioi Real.instPreorder DFunLike.coe Set ENNReal setOf Real.instLT	—	Measure.instOuterMeasureClass lintegral_eq_lintegral_meas_le lintegral_congr_ae Filter.mp_mem meas_le_ae_eq_meas_lt Measure.restrict.instNoAtoms Real.noAtoms_volume Filter.univ_mem'
meas_le_ae_eq_meas_lt 📖	mathematical	—	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass DFunLike.coe Set setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	Set.Countable.measure_zero countable_meas_le_ne_meas_lt

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_eq_integral_Ioc_meas_le 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.EventuallyLE Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero 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.Ioc Real.instPreorder MeasureTheory.Measure.real setOf	—	MeasureTheory.Measure.instOuterMeasureClass integral_eq_integral_meas_le MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero nullMeasurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Set.Ioc_subset_Ioi_self Filter.Eventually.of_forall MeasureTheory.measure_eq_zero_iff_ae_notMem Filter.mp_mem Filter.univ_mem' not_lt MeasureTheory.measureReal_def ENNReal.toReal_eq_zero_iff MeasureTheory.measure_mono_null lt_of_lt_of_le
integral_eq_integral_meas_le 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.EventuallyLE Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero 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 MeasureTheory.Measure.real setOf	—	MeasureTheory.Measure.instOuterMeasureClass integral_eq_integral_meas_lt MeasureTheory.integral_congr_ae Filter.mp_mem MeasureTheory.meas_le_ae_eq_meas_lt MeasureTheory.Measure.restrict.instNoAtoms Real.noAtoms_volume Filter.univ_mem'
integral_eq_integral_meas_lt 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.EventuallyLE Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero 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 MeasureTheory.Measure.real setOf Real.instLT	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.lintegral_eq_lintegral_meas_lt aemeasurable Real.borelSpace PseudoEMetricSpace.pseudoMetrizableSpace lintegral_lt_top measure_gt_lt_top instHasSolidNormReal IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid MeasureTheory.integral_eq_lintegral_of_nonneg_ae aestronglyMeasurable Filter.Eventually.of_forall MeasureTheory.measureReal_nonneg Measurable.aestronglyMeasurable instSecondCountableTopologyReal BorelSpace.opensMeasurable Measurable.ennreal_toReal Antitone.measurable ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology HasSolidNorm.orderClosedTopology MeasureTheory.measure_mono lt_of_le_of_lt MeasureTheory.setLIntegral_congr_fun measurableSet_Ioi instClosedIicTopology ENNReal.ofReal_toReal LT.lt.ne ENNReal.toReal_eq_toReal_iff'

---

← Back to Index