Differentiation

📁 Source: Mathlib/MeasureTheory/Covering/Differentiation.lean

Statistics

Metric	Count
Definitions `limRatio`, `limRatioMeas`	2
Theorems `ae_eventually_measure_pos`, `ae_eventually_measure_zero_of_singular`, `ae_tendsto_average`, `ae_tendsto_average_norm_sub`, `ae_tendsto_div`, `ae_tendsto_limRatio`, `ae_tendsto_limRatioMeas`, `ae_tendsto_lintegral_div`, `ae_tendsto_lintegral_div'`, `ae_tendsto_lintegral_enorm_sub_div`, `ae_tendsto_lintegral_enorm_sub_div'_of_integrable`, `ae_tendsto_lintegral_enorm_sub_div_of_integrable`, `ae_tendsto_measure_inter_div`, `ae_tendsto_measure_inter_div_of_measurableSet`, `ae_tendsto_rnDeriv`, `ae_tendsto_rnDeriv_of_absolutelyContinuous`, `aemeasurable_limRatio`, `eventually_filterAt_integrableOn`, `eventually_measure_lt_top`, `exists_measurable_supersets_limRatio`, `le_mul_withDensity`, `limRatioMeas_measurable`, `measure_le_mul_of_subset_limRatioMeas_lt`, `measure_le_of_frequently_le`, `measure_limRatioMeas_top`, `measure_limRatioMeas_zero`, `mul_measure_le_of_subset_lt_limRatioMeas`, `null_of_frequently_le_of_frequently_ge`, `withDensity_le_mul`, `withDensity_limRatioMeas_eq`	30
Total	32

VitaliFamily

Definitions

Name	Category	Theorems
`limRatio` 📖	CompOp	3 math math: `ae_tendsto_limRatio`, `exists_measurable_supersets_limRatio`, `aemeasurable_limRatio`
`limRatioMeas` 📖	CompOp	7 math math: `withDensity_limRatioMeas_eq`, `withDensity_le_mul`, `le_mul_withDensity`, `measure_limRatioMeas_zero`, `limRatioMeas_measurable`, `measure_limRatioMeas_top`, `ae_tendsto_limRatioMeas`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eventually_measure_pos` 📖	mathematical	—	`Filter.Eventually` `Set` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.instCanonicallyOrderedAdd` `le_antisymm` `FineSubfamilyOn.measure_le_tsum` `FineSubfamilyOn.covering_mem` `tsum_zero` `bot_le`
`ae_eventually_measure_zero_of_singular` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`Filter.Eventually` `Filter.Tendsto` `Set` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `le_antisymm` `IsScalarTower.right` `Set.inter_union_compl` `MeasureTheory.measure_mono` `Set.union_subset_union` `subset_refl` `Set.instReflSubset` `Set.inter_subset_right` `MeasureTheory.measure_union_le` `add_zero` `mul_comm` `ENNReal.mul_inv_cancel` `LT.lt.ne'` `ENNReal.coe_pos` `ENNReal.coe_ne_top` `one_mul` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `measure_le_of_frequently_le` `MeasureTheory.Measure.smul_absolutelyContinuous` `MulZeroClass.mul_zero` `bot_le` `exists_seq_strictAnti_tendsto` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.ae_all_iff` `instCountableNat` `Filter.mp_mem` `ae_eventually_measure_pos` `Filter.univ_mem'` `tendsto_order` `ENNReal.instOrderTopology` `ENNReal.not_lt_zero` `ENNReal.lt_iff_exists_nnreal_btwn` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `eventually_measure_lt_top` `ENNReal.div_lt_iff` `LT.lt.ne` `lt_imp_lt_of_le_of_le` `le_of_lt` `le_refl` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `ENNReal.coe_le_coe_of_le` `ENNReal.mul_lt_mul_left` `ne_of_gt`
`ae_tendsto_average` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.Eventually` `Filter.Tendsto` `Set` `MeasureTheory.average` `MeasureTheory.Measure.restrict` `filterAt` `nhds` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `ae_eventually_measure_pos` `ae_tendsto_average_norm_sub` `Filter.univ_mem'` `tendsto_iff_norm_sub_tendsto_zero` `squeeze_zero'` `Filter.Eventually.of_forall` `norm_nonneg` `eventually_filterAt_integrableOn` `eventually_measure_lt_top` `MeasureTheory.setAverage_const` `LT.lt.ne'` `LT.lt.ne` `IsScalarTower.right` `MeasureTheory.setAverage_eq'` `MeasureTheory.integral_sub` `MeasureTheory.integrable_inv_smul_measure` `MeasureTheory.integrableOn_const` `enorm_ne_top` `MeasureTheory.norm_integral_le_integral_norm`
`ae_tendsto_average_norm_sub` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.Eventually` `Filter.Tendsto` `Set` `Real` `MeasureTheory.average` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `MeasureTheory.Measure.restrict` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `filterAt` `nhds` `Real.pseudoMetricSpace` `Real.instZero` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `ae_tendsto_lintegral_enorm_sub_div` `Filter.univ_mem'` `Filter.Tendsto.comp` `ENNReal.tendsto_toReal` `ENNReal.zero_ne_top` `Filter.Tendsto.congr'` `eventually_filterAt_integrableOn` `eventually_measure_lt_top` `ENNReal.toReal_div` `div_eq_inv_mul` `MeasureTheory.setAverage_eq` `MeasureTheory.Integrable.norm` `MeasureTheory.Integrable.sub` `MeasureTheory.integrableOn_const` `LT.lt.ne` `enorm_ne_top` `MeasureTheory.lintegral_coe_eq_integral` `ENNReal.toReal_ofReal` `MeasureTheory.integral_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `NNReal.coe_nonneg`
`ae_tendsto_div` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`Filter.Eventually` `ENNReal` `Filter.Tendsto` `Set` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.exists_countable_dense_no_zero_top` `CanLift.prf` `ENNReal.canLift` `null_of_frequently_le_of_frequently_ge` `ENNReal.coe_lt_coe` `Filter.Frequently.mono` `ENNReal.div_le_iff_le_mul` `LT.lt.ne'` `LE.le.trans_lt` `bot_le` `LT.lt.le` `ENNReal.mul_le_of_le_div` `MeasureTheory.ae_ball_iff` `Prop.countable` `Filter.mp_mem` `Filter.univ_mem'` `tendsto_of_no_upcrossings` `ENNReal.instOrderTopology` `ENNReal.instDenselyOrdered` `Filter.isBounded_le_of_top` `Filter.isBounded_ge_of_bot`
`ae_tendsto_limRatio` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`Filter.Eventually` `Filter.Tendsto` `Set` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `limRatio` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `ae_tendsto_div` `Filter.univ_mem'` `tendsto_nhds_limUnder`
`ae_tendsto_limRatioMeas` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`Filter.Eventually` `Filter.Tendsto` `Set` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `limRatioMeas` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `aemeasurable_limRatio` `ae_tendsto_limRatio` `Filter.univ_mem'`
`ae_tendsto_lintegral_div` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace`	`Filter.Eventually` `Filter.Tendsto` `Set` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.lintegral_congr_ae` `Filter.EventuallyEq.symm` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.mp_mem` `ae_tendsto_lintegral_div'` `Filter.univ_mem'` `MeasureTheory.ae_restrict_of_ae`
`ae_tendsto_lintegral_div'` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`Filter.Eventually` `Filter.Tendsto` `Set` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.isFiniteMeasure_withDensity` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.rnDeriv_withDensity` `MeasureTheory.sigmaFinite_of_locallyFinite` `ae_tendsto_rnDeriv` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `Filter.univ_mem'` `Filter.Tendsto.congr'` `eventually_filterAt_measurableSet` `MeasureTheory.withDensity_apply`
`ae_tendsto_lintegral_enorm_sub_div` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.Eventually` `Filter.Tendsto` `Set` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `ENorm.enorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.LocallyIntegrable.exists_nat_integrableOn` `ae_tendsto_lintegral_enorm_sub_div_of_integrable` `MeasureTheory.integrable_indicator_iff` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `Filter.mp_mem` `MeasureTheory.ae_all_iff` `instCountableNat` `Filter.univ_mem'` `Set.mem_univ` `Filter.Tendsto.congr'` `eventually_filterAt_measurableSet` `eventually_filterAt_subset_of_nhds` `IsOpen.mem_nhds` `MeasureTheory.setLIntegral_congr_fun` `Set.indicator_of_mem`
`ae_tendsto_lintegral_enorm_sub_div'_of_integrable` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.StronglyMeasurable`	`Filter.Eventually` `Filter.Tendsto` `Set` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `ENorm.enorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.StronglyMeasurable.isSeparable_range` `instCountableNat` `MeasureTheory.ae_ball_iff` `ae_tendsto_lintegral_div'` `MeasureTheory.StronglyMeasurable.enorm` `MeasureTheory.StronglyMeasurable.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.StronglyMeasurable.indicator` `MeasureTheory.stronglyMeasurable_const` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem` `ne_of_lt` `MeasureTheory.lintegral_mono` `enorm_sub_le` `MeasureTheory.lintegral_add_left` `ENNReal.add_lt_add` `MeasureTheory.integrable_indicator_iff` `MeasureTheory.integrableOn_const_iff` `enorm_ne_top` `MeasureTheory.Measure.FiniteSpanningSetsIn.finite` `Filter.mp_mem` `ae_eventually_measure_pos` `Filter.univ_mem'` `MeasureTheory.Measure.FiniteSpanningSetsIn.spanning` `Set.mem_univ` `Filter.Tendsto.congr'` `eventually_filterAt_measurableSet` `eventually_filterAt_subset_of_nhds` `IsOpen.mem_nhds` `MeasureTheory.setLIntegral_congr_fun` `Set.indicator_of_mem` `ENNReal.tendsto_nhds_zero` `Nat.instAtLeastTwoHAddOfNat` `Set.mem_range_self` `EMetric.mem_closure_iff` `ENNReal.half_pos` `ne_of_gt` `eventually_measure_lt_top` `tendsto_order` `ENNReal.instOrderTopology` `ENNReal.div_le_of_le_mul` `edist_triangle_right` `MeasureTheory.lintegral_add_right` `measurable_const` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LT.lt.le` `ENNReal.div_lt_iff` `LT.lt.ne'` `LT.lt.ne` `MeasureTheory.lintegral_const` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `le_of_lt` `add_mul` `Distrib.rightDistribClass` `ENNReal.add_halves`
`ae_tendsto_lintegral_enorm_sub_div_of_integrable` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.Eventually` `Filter.Tendsto` `Set` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `ENorm.enorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Integrable.congr` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `ae_tendsto_lintegral_enorm_sub_div'_of_integrable` `Filter.univ_mem'` `Filter.Tendsto.congr` `MeasureTheory.lintegral_congr_ae` `MeasureTheory.ae_restrict_of_ae`
`ae_tendsto_measure_inter_div` 📖	mathematical	—	`Filter.Eventually` `Filter.Tendsto` `Set` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Set.instInter` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_mono` `MeasureTheory.Measure.restrict_le_self` `ae_tendsto_measure_inter_div_of_measurableSet` `MeasureTheory.measurableSet_toMeasurable` `MeasureTheory.ae_restrict_of_ae_restrict_of_subset` `MeasureTheory.subset_toMeasurable` `Filter.mp_mem` `MeasureTheory.ae_restrict_mem` `Filter.univ_mem'` `Set.indicator_of_mem` `Filter.Tendsto.congr'` `eventually_filterAt_measurableSet` `MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite`
`ae_tendsto_measure_inter_div_of_measurableSet` 📖	mathematical	`MeasurableSet`	`Filter.Eventually` `Filter.Tendsto` `Set` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Set.instInter` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `Set.indicator` `instZeroENNReal` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.rnDeriv_restrict_self` `MeasureTheory.sigmaFinite_of_locallyFinite` `ae_tendsto_rnDeriv` `MeasureTheory.Measure.isLocallyFiniteMeasure_of_le` `MeasureTheory.Measure.restrict_le_self` `Filter.univ_mem'` `MeasureTheory.Measure.restrict_apply'` `Set.inter_comm`
`ae_tendsto_rnDeriv` 📖	mathematical	—	`Filter.Eventually` `Filter.Tendsto` `Set` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.rnDeriv` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.haveLebesgueDecomposition_add` `MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.Measure.instOuterMeasureClass` `ae_eventually_measure_zero_of_singular` `MeasureTheory.Measure.singularPart.instIsLocallyFiniteMeasure` `MeasureTheory.Measure.mutuallySingular_singularPart` `MeasureTheory.Measure.rnDeriv_withDensity` `MeasureTheory.Measure.measurable_rnDeriv` `ae_tendsto_rnDeriv_of_absolutelyContinuous` `MeasureTheory.Measure.withDensity.instIsLocallyFiniteMeasure` `MeasureTheory.withDensity_absolutelyContinuous` `Filter.mp_mem` `Filter.univ_mem'` `ENNReal.add_div` `zero_add` `Filter.Tendsto.add` `ENNReal.instContinuousAdd`
`ae_tendsto_rnDeriv_of_absolutelyContinuous` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`Filter.Eventually` `Filter.Tendsto` `Set` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt` `nhds` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.rnDeriv` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.rnDeriv_withDensity` `MeasureTheory.sigmaFinite_of_locallyFinite` `limRatioMeas_measurable` `Filter.mp_mem` `withDensity_limRatioMeas_eq` `ae_tendsto_limRatioMeas` `Filter.univ_mem'`
`aemeasurable_limRatio` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `limRatio`	—	`ENNReal.aemeasurable_of_exist_almost_disjoint_supersets` `exists_measurable_supersets_limRatio`
`eventually_filterAt_integrableOn` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.Eventually` `Set` `MeasureTheory.IntegrableOn` `filterAt`	—	`Filter.mp_mem` `eventually_filterAt_subset_of_nhds` `Filter.univ_mem'` `MeasureTheory.IntegrableOn.mono_set`
`eventually_measure_lt_top` 📖	mathematical	—	`Filter.Eventually` `Set` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal` `filterAt`	—	`Filter.Eventually.filter_mono` `inf_le_left` `MeasureTheory.Measure.FiniteAtFilter.eventually` `MeasureTheory.Measure.finiteAt_nhds`
`exists_measurable_supersets_limRatio` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal`	`MeasurableSet` `Set` `Set.instHasSubset` `setOf` `ENNReal` `ENNReal.instPartialOrder` `limRatio` `ENNReal.ofNNReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Set.instInter` `instZeroENNReal`	—	`MeasureTheory.Add.sigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasurableSet.union` `MeasureTheory.measurableSet_toMeasurable` `MeasurableSet.iUnion` `instCountableNat` `Set.mem_iUnion` `MeasureTheory.subset_toMeasurable` `MeasureTheory.mem_spanningSetsIndex` `LT.lt.ne` `lt_of_le_of_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_right` `MeasureTheory.measure_spanningSets_lt_top` `IsScalarTower.right` `MeasureTheory.Measure.measure_toMeasurable_add_inter_left` `measure_le_of_frequently_le` `MeasureTheory.isLocallyFiniteMeasureSMulNNReal` `tendsto_nhds_limUnder` `tendsto_order` `ENNReal.instOrderTopology` `Filter.Frequently.mono` `Filter.Eventually.frequently` `filterAt_neBot` `MeasureTheory.Measure.coe_nnreal_smul_apply` `ENNReal.div_le_iff_le_mul` `LT.lt.ne'` `LE.le.trans_lt` `bot_le` `LT.lt.le` `MeasureTheory.Measure.measure_toMeasurable_add_inter_right` `Set.inter_comm` `MeasureTheory.Measure.AbsolutelyContinuous.smul_left` `MeasureTheory.Measure.AbsolutelyContinuous.rfl` `ENNReal.mul_le_of_le_div` `lt_irrefl` `ENNReal.mul_lt_mul_left` `ne_of_gt` `lt_of_le_of_ne'` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `Set.inter_subset_left` `MeasureTheory.measure_toMeasurable` `ENNReal.coe_lt_coe_of_lt` `Set.inter_union_distrib_left` `Set.union_inter_distrib_right` `Set.inter_self` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_union_left` `Set.iUnion_inter` `Set.inter_iUnion` `Set.subset_union_right` `le_antisymm` `LE.le.trans` `MeasureTheory.measure_union_le` `ae_tendsto_div` `zero_add` `MeasureTheory.measure_iUnion_le` `ENNReal.tsum_le_tsum` `tsum_zero`
`le_mul_withDensity` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous` `MeasurableSet` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `MeasureTheory.Measure.withDensity` `limRatioMeas`	—	`LT.lt.ne'` `LT.lt.trans` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `limRatioMeas_measurable` `IsScalarTower.right` `le_trans` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_right` `le_of_eq` `measure_limRatioMeas_zero` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `nonpos_iff_eq_zero` `LE.le.trans` `Eq.le` `measure_limRatioMeas_top` `MeasurableSet.inter` `measurableSet_Ico` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `MeasureTheory.withDensity_apply` `ENNReal.coe_zpow` `measure_le_mul_of_subset_limRatioMeas_lt` `LT.lt.trans_le` `MeasureTheory.lintegral_const` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `MeasureTheory.lintegral_mono_ae` `MeasureTheory.ae_restrict_iff'` `Filter.Eventually.of_forall` `add_comm` `ENNReal.zpow_add` `ENNReal.coe_ne_top` `zpow_one` `le_imp_le_of_le_of_le` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `le_refl` `MeasureTheory.lintegral_const_mul` `measure_eq_measure_preimage_add_measure_tsum_Ico_zpow` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `ENNReal.tsum_le_tsum`
`limRatioMeas_measurable` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`Measurable` `ENNReal` `ENNReal.measurableSpace` `limRatioMeas`	—	`aemeasurable_limRatio`
`measure_le_mul_of_subset_limRatioMeas_lt` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous` `Set` `Set.instHasSubset` `setOf` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `limRatioMeas` `ENNReal.ofNNReal`	`Preorder.toLE` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`ae_tendsto_limRatioMeas` `IsScalarTower.right` `measure_le_of_frequently_le` `MeasureTheory.isLocallyFiniteMeasureSMulNNReal` `tendsto_order` `ENNReal.instOrderTopology` `Filter.Frequently.mono` `Filter.Eventually.frequently` `filterAt_neBot` `MeasureTheory.Measure.coe_nnreal_smul_apply` `ENNReal.div_le_iff_le_mul` `LT.lt.ne'` `LE.le.trans_lt` `bot_le` `LT.lt.le` `Set.inter_union_compl` `MeasureTheory.measure_union_le` `MeasureTheory.Measure.instOuterMeasureClass` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `MeasureTheory.measure_mono` `Set.inter_subset_right` `add_zero` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `Set.inter_subset_left`
`measure_le_of_frequently_le` 📖	—	`MeasureTheory.Measure.AbsolutelyContinuous` `Filter.Frequently` `Set` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `filterAt`	—	—	`ENNReal.le_of_forall_pos_le_add` `Set.exists_isOpen_le_add` `MeasureTheory.Measure.WeaklyRegular.toOuterRegular` `MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite` `PseudoEMetricSpace.pseudoMetrizableSpace` `LT.lt.ne'` `ENNReal.coe_pos` `fineSubfamilyOn_of_frequently` `Filter.Frequently.and_eventually` `Filter.Eventually.and` `eventually_filterAt_mem_setsAt` `eventually_filterAt_subset_of_nhds` `IsOpen.mem_nhds` `Filter.Frequently.mono` `FineSubfamilyOn.measure_le_tsum_of_absolutelyContinuous` `ENNReal.tsum_le_tsum` `FineSubfamilyOn.covering_mem` `MeasureTheory.measure_iUnion` `Encodable.countable` `FineSubfamilyOn.index_countable` `FineSubfamilyOn.covering_disjoint_subtype` `FineSubfamilyOn.measurableSet_u` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.iUnion_subset`
`measure_limRatioMeas_top` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `setOf` `limRatioMeas` `Top.top` `instTopENNReal` `instZeroENNReal`	—	`MeasureTheory.measure_null_of_locally_null` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.exists_isOpen_measure_lt_top` `inter_mem_nhdsWithin` `IsOpen.mem_nhds` `le_antisymm` `MeasureTheory.measure_ne_top_of_subset` `Set.inter_subset_right` `LT.lt.ne` `mul_comm` `div_eq_mul_inv` `ENNReal.le_div_iff_mul_le` `LT.lt.ne'` `LT.lt.trans_le` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `mul_measure_le_of_subset_lt_limRatioMeas` `ENNReal.Tendsto.mul_const` `tendsto_inv_iff` `ENNReal.instContinuousInv` `ENNReal.tendsto_coe_nhds_top` `Filter.tendsto_id` `ge_of_tendsto` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `NNReal.instIsOrderedRing` `NNReal.instArchimedean` `ENNReal.inv_top` `MulZeroClass.zero_mul` `Filter.eventually_atTop` `bot_le`
`measure_limRatioMeas_zero` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `setOf` `limRatioMeas` `instZeroENNReal`	—	`MeasureTheory.measure_null_of_locally_null` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.exists_isOpen_measure_lt_top` `inter_mem_nhdsWithin` `IsOpen.mem_nhds` `le_antisymm` `MeasureTheory.measure_ne_top_of_subset` `Set.inter_subset_right` `LT.lt.ne` `measure_le_mul_of_subset_limRatioMeas_lt` `ENNReal.Tendsto.mul_const` `ENNReal.tendsto_coe` `nhdsWithin_le_nhds` `ge_of_tendsto` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `nhdsGT_neBot` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing` `MulZeroClass.zero_mul` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `bot_le`
`mul_measure_le_of_subset_lt_limRatioMeas` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous` `Set` `Set.instHasSubset` `setOf` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `limRatioMeas`	`Preorder.toLE` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike`	—	`ae_tendsto_limRatioMeas` `IsScalarTower.right` `measure_le_of_frequently_le` `MeasureTheory.Measure.AbsolutelyContinuous.smul_left` `MeasureTheory.Measure.AbsolutelyContinuous.rfl` `tendsto_order` `ENNReal.instOrderTopology` `Filter.Frequently.mono` `Filter.Eventually.frequently` `filterAt_neBot` `MeasureTheory.Measure.coe_nnreal_smul_apply` `ENNReal.mul_le_of_le_div` `LT.lt.le` `Set.inter_union_compl` `MeasureTheory.measure_union_le` `MeasureTheory.Measure.instOuterMeasureClass` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `MeasureTheory.measure_mono` `Set.inter_subset_right` `smul_zero` `add_zero` `Set.inter_subset_left`
`null_of_frequently_le_of_frequently_ge` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Filter.Frequently` `Set` `ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `filterAt`	`instZeroENNReal`	—	`MeasureTheory.measure_null_of_locally_null` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.exists_isOpen_measure_lt_top` `inter_mem_nhdsWithin` `IsOpen.mem_nhds` `lt_irrefl` `measure_le_of_frequently_le` `IsScalarTower.right` `MeasureTheory.isLocallyFiniteMeasureSMulNNReal` `ENNReal.mul_lt_mul_left` `ne_of_gt` `lt_of_le_of_ne'` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `MeasureTheory.measure_ne_top_of_subset` `Set.inter_subset_right` `LT.lt.ne` `ENNReal.coe_lt_coe_of_lt` `MeasureTheory.Measure.smul_absolutelyContinuous`
`withDensity_le_mul` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous` `MeasurableSet` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.withDensity` `limRatioMeas` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofNNReal`	—	`LT.lt.ne'` `LT.lt.trans` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `limRatioMeas_measurable` `IsScalarTower.right` `le_trans` `MeasurableSet.inter` `MeasurableSingletonClass.measurableSet_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `ENNReal.instT2Space` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.withDensity_apply` `ENNReal.instCanonicallyOrderedAdd` `MeasureTheory.lintegral_eq_zero_iff` `MeasureTheory.ae_restrict_iff'` `Filter.Eventually.of_forall` `zero_le` `le_of_eq` `MeasureTheory.withDensity_absolutelyContinuous` `nonpos_iff_eq_zero` `LE.le.trans` `MeasureTheory.measure_mono` `Set.inter_subset_right` `Eq.le` `measure_limRatioMeas_top` `measurableSet_Ico` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `MeasureTheory.lintegral_mono_ae` `LT.lt.le` `MeasureTheory.lintegral_const` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `mul_assoc` `ENNReal.zpow_add` `ENNReal.coe_ne_top` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.coe_zpow` `mul_measure_le_of_subset_lt_limRatioMeas` `lt_of_lt_of_le` `ENNReal.coe_lt_coe` `sub_eq_add_neg` `zpow_add₀` `mul_one` `mul_lt_mul_of_pos_left` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `zpow_neg_one` `inv_lt_one_of_one_lt₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `zpow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `NNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `measure_eq_measure_preimage_add_measure_tsum_Ico_zpow` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `ENNReal.tsum_le_tsum`
`withDensity_limRatioMeas_eq` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.Measure.withDensity` `limRatioMeas`	—	`MeasureTheory.Measure.ext` `le_antisymm` `ENNReal.Tendsto.mul` `ENNReal.Tendsto.pow` `ENNReal.tendsto_coe` `nhdsWithin_le_nhds` `one_pow` `NeZero.charZero_one` `ENNReal.instCharZero` `tendsto_const_nhds` `ge_of_tendsto` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `nhdsGT_neBot` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing` `one_mul` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `withDensity_le_mul` `ENNReal.Tendsto.mul_const` `le_mul_withDensity`

---

← Back to Index