Lebesgue

📁 Source: Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean

Statistics

Metric	Count
Definitions `HaveLebesgueDecomposition`, `measurableLE`, `measurableLEEval`, `rnDeriv`, `singularPart`	5
Theorems `singularPart`, `withDensity_rnDeriv`, `withDensity_rnDeriv`, `add_left`, `lebesgue_decomposition`, `sfinite_of_isFiniteMeasure`, `sum_left`, `iSup_le_le`, `iSup_mem_measurableLE`, `iSup_mem_measurableLE'`, `iSup_monotone`, `iSup_monotone'`, `iSup_succ_eq_sup`, `sup_mem_measurableLE`, `zero_mem_measurableLE`, `haveLebesgueDecomposition`, `rnDeriv_ae_eq_zero`, `singularPart`, `absolutelyContinuous_withDensity_rnDeriv`, `absolutelyContinuous_withDensity_rnDeriv_swap`, `add_sub_of_mutuallySingular`, `eq_rnDeriv`, `eq_rnDeriv₀`, `eq_singularPart`, `eq_withDensity_rnDeriv`, `eq_withDensity_rnDeriv₀`, `exists_positive_of_not_mutuallySingular`, `haveLebesgueDecompositionRnDeriv`, `haveLebesgueDecompositionSMul`, `haveLebesgueDecompositionSMul'`, `haveLebesgueDecompositionSMulRight`, `haveLebesgueDecomposition_add`, `haveLebesgueDecomposition_of_finiteMeasure`, `haveLebesgueDecomposition_of_sigmaFinite`, `haveLebesgueDecomposition_spec`, `haveLebesgueDecomposition_withDensity`, `instHaveLebesgueDecompositionSelf`, `instHaveLebesgueDecompositionSingularPart`, `instHaveLebesgueDecompositionZeroLeft`, `instHaveLebesgueDecompositionZeroRight`, `lintegral_rnDeriv_lt_top`, `lintegral_rnDeriv_lt_top_of_measure_ne_top`, `measurable_rnDeriv`, `measure_sub_rnDeriv`, `measure_sub_singularPart`, `mutuallySingular_singularPart`, `rnDeriv_add`, `rnDeriv_add'`, `rnDeriv_add_of_mutuallySingular`, `rnDeriv_add_singularPart`, `rnDeriv_def`, `rnDeriv_eq_zero`, `rnDeriv_lt_top`, `rnDeriv_ne_top`, `rnDeriv_of_not_haveLebesgueDecomposition`, `rnDeriv_restrict`, `rnDeriv_restrict_self`, `rnDeriv_self`, `rnDeriv_singularPart`, `rnDeriv_smul_left`, `rnDeriv_smul_left'`, `rnDeriv_smul_left_of_ne_top`, `rnDeriv_smul_left_of_ne_top'`, `rnDeriv_smul_right`, `rnDeriv_smul_right'`, `rnDeriv_smul_right_of_ne_top`, `rnDeriv_smul_right_of_ne_top'`, `rnDeriv_withDensity`, `rnDeriv_withDensity₀`, `rnDeriv_zero`, `instIsFiniteMeasure`, `instIsLocallyFiniteMeasure`, `instSigmaFinite`, `singularPart_add`, `singularPart_add_rnDeriv`, `singularPart_def`, `singularPart_eq_restrict`, `singularPart_eq_restrict'`, `singularPart_eq_self`, `singularPart_eq_zero`, `singularPart_eq_zero_of_ac`, `singularPart_le`, `singularPart_of_not_haveLebesgueDecomposition`, `singularPart_restrict`, `singularPart_self`, `singularPart_singularPart`, `singularPart_smul`, `singularPart_smul_right`, `singularPart_withDensity`, `singularPart_zero`, `singularPart_zero_right`, `instIsFiniteMeasure`, `instIsLocallyFiniteMeasure`, `instSigmaFinite`, `withDensity_rnDeriv_eq_zero`, `withDensity_rnDeriv_le`	96
Total	101

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`singularPart` 📖	mathematical	`AEMeasurable`	`MeasureTheory.Measure.singularPart`	—	`mono_measure` `MeasureTheory.Measure.singularPart_le`
`withDensity_rnDeriv` 📖	mathematical	`AEMeasurable`	`MeasureTheory.Measure.withDensity` `MeasureTheory.Measure.rnDeriv`	—	`mono_measure` `MeasureTheory.Measure.withDensity_rnDeriv_le`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`HaveLebesgueDecomposition` 📖	CompData	24 math math: `haveLebesgueDecompositionSMul`, `MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.negPart`, `haveLebesgueDecomposition_withDensity`, `instHaveLebesgueDecompositionSingularPart`, `instHaveLebesgueDecompositionZeroRight`, `MeasureTheory.hasPDF_iff`, `MeasureTheory.HaveLebesgueDecomposition.conv`, `MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.posPart`, `singularPart_def`, `instHaveLebesgueDecompositionSelf`, `MeasureTheory.HasPDF.haveLebesgueDecomposition`, `MeasureTheory.SignedMeasure.not_haveLebesgueDecomposition_iff`, `MeasureTheory.HasPDF.haveLebesgueDecomposition'`, `haveLebesgueDecomposition_of_finiteMeasure`, `MeasureTheory.HaveLebesgueDecomposition.mconv`, `rnDeriv_def`, `haveLebesgueDecompositionRnDeriv`, `haveLebesgueDecomposition_of_sigmaFinite`, `haveLebesgueDecompositionSMulRight`, `HaveLebesgueDecomposition.add_left`, `MeasureTheory.hasPDF_iff_of_aemeasurable`, `instHaveLebesgueDecompositionZeroLeft`, `MutuallySingular.haveLebesgueDecomposition`, `haveLebesgueDecompositionSMul'`
`rnDeriv` 📖	CompOp	136 math math: `InformationTheory.integrable_klFun_rnDeriv_iff`, `rnDeriv_zero`, `rnDeriv_smul_right'`, `rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular`, `MeasureTheory.SignedMeasure.rnDeriv_def`, `lintegral_rnDeriv`, `rnDeriv_mul_rnDeriv'`, `MeasurableEmbedding.rnDeriv_map`, `rnDeriv_add_of_mutuallySingular`, `inv_rnDeriv'`, `ProbabilityTheory.rnDeriv_gaussianReal`, `MeasureTheory.exp_llr_of_ac'`, `MeasureTheory.toReal_rnDeriv_tilted_left`, `rnDeriv_smul_right`, `rnDeriv_smul_left_of_ne_top'`, `rnDeriv_withDensity_right`, `rnDeriv_restrict`, `eq_withDensity_rnDeriv`, `rnDeriv_eq_one_iff_eq`, `setLIntegral_rnDeriv`, `InformationTheory.toReal_klDiv_eq_integral_klFun`, `ProbabilityTheory.posterior_boolKernel_apply_true`, `integral_toReal_rnDeriv'`, `haveLebesgueDecomposition_add`, `measure_sub_singularPart`, `MeasureTheory.rnDeriv_conv`, `rnDeriv_smul_left_of_ne_top`, `rnDeriv_add_singularPart`, `ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure`, `rnDeriv_mul_rnDeriv`, `rnDeriv_lt_top`, `Besicovitch.ae_tendsto_rnDeriv`, `eq_rnDeriv`, `MeasurableEmbedding.rnDeriv_map_aux`, `withDensity_rnDeriv_le`, `Monotone.ae_hasDerivAt`, `lintegral_rnDeriv_lt_top`, `MeasureTheory.MeasurePreserving.withDensity_rnDeriv`, `integral_toReal_rnDeriv`, `lintegral_rnDeriv_le`, `rnDeriv_smul_left'`, `MeasureTheory.setIntegral_rnDeriv_smul`, `InformationTheory.integral_klFun_rnDeriv`, `rnDeriv_smul_right_of_ne_top'`, `ProbabilityTheory.Kernel.eq_rnDeriv_measure`, `InformationTheory.klDiv_eq_lintegral_klFun`, `MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv`, `rnDeriv_add`, `withDensity_rnDeriv_eq_zero`, `MeasureTheory.lintegral_rnDeriv_mul`, `setLIntegral_rnDeriv'`, `eq_rnDeriv₀`, `setIntegral_toReal_rnDeriv'`, `rnDeriv_add_right_of_mutuallySingular'`, `rnDeriv_ne_top`, `withDensity.instIsLocallyFiniteMeasure`, `inv_rnDeriv`, `MeasureTheory.rnDeriv_mconv`, `MeasureTheory.log_rnDeriv_tilted_left_self`, `withDensity.instSigmaFinite`, `MeasureTheory.rnDeriv_mconv'`, `MeasureTheory.setLIntegral_rnDeriv_mul`, `InformationTheory.klDiv_eq_integral_klFun`, `rnDeriv_withDensity_right_of_absolutelyContinuous`, `rnDeriv_eq_zero_of_mutuallySingular`, `rnDeriv_pos`, `rnDeriv_of_not_haveLebesgueDecomposition`, `absolutelyContinuous_withDensity_rnDeriv_swap`, `MeasureTheory.setIntegral_rnDeriv_smul'`, `MeasureTheory.integral_rnDeriv_mul_log`, `rnDeriv_def`, `haveLebesgueDecompositionRnDeriv`, `MeasureTheory.exp_neg_llr`, `MeasureTheory.MeasurePreserving.rnDeriv_comp_aeEq`, `MeasureTheory.exp_neg_llr'`, `rnDeriv_singularPart`, `MeasureTheory.rnDeriv_tilted_left`, `ProbabilityTheory.posterior_boolKernel_apply_false`, `rnDeriv_withDensity`, `MeasureTheory.integral_rnDeriv_smul`, `setIntegral_toReal_rnDeriv_eq_withDensity'`, `MeasureTheory.rnDeriv_conv'`, `AbsolutelyContinuous.withDensity_rnDeriv`, `VitaliFamily.ae_tendsto_rnDeriv_of_absolutelyContinuous`, `VitaliFamily.ae_tendsto_rnDeriv`, `AEMeasurable.withDensity_rnDeriv`, `MeasureTheory.pdf_def`, `inv_rnDeriv_aux`, `rnDeriv_withDensity₀`, `rnDeriv_smul_left`, `rnDeriv_restrict_self`, `StieltjesFunction.ae_hasDerivAt`, `MeasureTheory.withDensityᵥ_rnDeriv_smul`, `rnDeriv_withDensity_left_of_absolutelyContinuous`, `MeasureTheory.integrable_rnDeriv_smul_iff`, `singularPart_add_rnDeriv`, `eq_withDensity_rnDeriv₀`, `MeasureTheory.exp_llr_of_ac`, `MeasureTheory.conv_eq_withDensity_lconvolution_rnDeriv`, `MeasureTheory.condLExp_def`, `ProbabilityTheory.posterior_eq_withDensity_of_countable`, `integrableOn_toReal_rnDeriv`, `setIntegral_toReal_rnDeriv_le`, `measure_sub_rnDeriv`, `MutuallySingular.rnDeriv_ae_eq_zero`, `setIntegral_toReal_rnDeriv_eq_withDensity`, `rnDeriv_withDensity_rnDeriv`, `MeasureTheory.rnDeriv_tilted_right`, `rnDeriv_self`, `absolutelyContinuous_iff_withDensity_rnDeriv_eq`, `MeasureTheory.llr_def`, `measurable_rnDeriv`, `absolutelyContinuous_withDensity_rnDeriv`, `rnDeriv_add'`, `rnDeriv_withDensity_withDensity_rnDeriv_left`, `setLIntegral_rnDeriv_le`, `MeasurableEmbedding.map_withDensity_rnDeriv`, `MeasureTheory.rnDeriv_tilted_left_self`, `rnDeriv_withDensity_withDensity_rnDeriv_right`, `rnDeriv_pos'`, `rnDeriv_le_one_of_le`, `lintegral_rnDeriv_lt_top_of_measure_ne_top`, `rnDeriv_eq_zero`, `MeasureTheory.exp_llr`, `setIntegral_toReal_rnDeriv`, `withDensity.instIsFiniteMeasure`, `MeasureTheory.condLExp_of_not_sub_sigma_measurable`, `haveLebesgueDecomposition_spec`, `MeasureTheory.toReal_rnDeriv_tilted_right`, `rnDeriv_withDensity_left`, `rnDeriv_smul_right_of_ne_top`, `MeasureTheory.integrable_rnDeriv_mul_log_iff`, `withDensity_rnDeriv_eq`, `rnDeriv_le_one_iff_le`, `integrable_toReal_rnDeriv`, `rnDeriv_add_right_of_mutuallySingular`
`singularPart` 📖	CompOp	38 math math: `singularPart_eq_self`, `AEMeasurable.singularPart`, `singularPart_eq_zero`, `instHaveLebesgueDecompositionSingularPart`, `integral_toReal_rnDeriv'`, `haveLebesgueDecomposition_add`, `measure_sub_singularPart`, `MeasureTheory.SignedMeasure.singularPart_totalVariation`, `singularPart_def`, `rnDeriv_add_singularPart`, `singularPart_restrict`, `MeasureTheory.SignedMeasure.singularPart_mutuallySingular`, `singularPart_le`, `singularPart_zero_right`, `singularPart.instSigmaFinite`, `singularPart_withDensity`, `singularPart.instIsFiniteMeasure`, `singularPart_self`, `ProbabilityTheory.Kernel.eq_singularPart_measure`, `MutuallySingular.singularPart`, `rnDeriv_singularPart`, `MeasureTheory.MeasurePreserving.singularPart`, `ProbabilityTheory.Kernel.singularPart_eq_singularPart_measure`, `singularPart_zero`, `MeasurableEmbedding.singularPart_map`, `singularPart.instIsLocallyFiniteMeasure`, `singularPart_add_rnDeriv`, `singularPart_singularPart`, `ProbabilityTheory.Kernel.measurable_singularPart`, `measure_sub_rnDeriv`, `mutuallySingular_singularPart`, `singularPart_of_not_haveLebesgueDecomposition`, `singularPart_smul_right`, `eq_singularPart`, `singularPart_eq_zero_of_ac`, `haveLebesgueDecomposition_spec`, `singularPart_add`, `singularPart_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuous_withDensity_rnDeriv` 📖	mathematical	`AbsolutelyContinuous`	`withDensity` `rnDeriv`	—	`mutuallySingular_singularPart` `Set.inter_union_compl` `le_antisymm` `LE.le.trans` `MeasureTheory.measure_union_le` `instOuterMeasureClass` `ENNReal.instCanonicallyOrderedAdd` `Unique.instSubsingleton` `haveLebesgueDecomposition_add` `MeasureTheory.measure_mono_null` `Set.inter_subset_right` `Set.inter_subset_left` `zero_le`
`absolutelyContinuous_withDensity_rnDeriv_swap` 📖	mathematical	—	`AbsolutelyContinuous` `withDensity` `rnDeriv`	—	`AbsolutelyContinuous.withDensity_rnDeriv` `MeasureTheory.withDensity_absolutelyContinuous` `absolutelyContinuous_of_le` `withDensity_rnDeriv_le`
`add_sub_of_mutuallySingular` 📖	mathematical	`MutuallySingular`	`MeasureTheory.Measure` `instAdd` `instSub`	—	`MutuallySingular.measurableSet_nullSet` `MutuallySingular.restrict_nullSet` `restrict_sub_eq_restrict_sub_restrict` `zero_add` `MeasurableSet.compl` `MutuallySingular.restrict_compl_nullSet` `sub_zero` `restrict_add_restrict_compl` `add_assoc` `Mathlib.Tactic.Abel.subst_into_add` `Mathlib.Tactic.Abel.term_atom` `Mathlib.Tactic.Abel.term_add_const` `Mathlib.Tactic.Abel.const_add_term` `restrict_add`
`eq_rnDeriv` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace` `MutuallySingular` `MeasureTheory.Measure` `instAdd` `withDensity`	`Filter.EventuallyEq` `MeasureTheory.ae` `instFunLike` `instOuterMeasureClass` `rnDeriv`	—	`eq_rnDeriv₀` `Measurable.aemeasurable`
`eq_rnDeriv₀` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `MutuallySingular` `MeasureTheory.Measure` `instAdd` `withDensity`	`Filter.EventuallyEq` `MeasureTheory.ae` `instFunLike` `instOuterMeasureClass` `rnDeriv`	—	`instOuterMeasureClass` `MeasureTheory.withDensity_eq_iff_of_sigmaFinite` `Measurable.aemeasurable` `measurable_rnDeriv` `eq_withDensity_rnDeriv₀`
`eq_singularPart` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace` `MutuallySingular` `MeasureTheory.Measure` `instAdd` `withDensity`	`singularPart`	—	`haveLebesgueDecomposition_spec` `Set.compl_inter` `nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `le_trans` `MeasureTheory.measure_union_le` `instOuterMeasureClass` `add_zero` `le_refl` `ext` `MeasureTheory.withDensity_absolutelyContinuous` `MeasureTheory.measure_mono` `Set.inter_subset_right` `restrict_apply` `add_apply` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left` `Set.diff_eq` `MeasureTheory.AEDisjoint.measure_diff_left`
`eq_withDensity_rnDeriv` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace` `MutuallySingular` `MeasureTheory.Measure` `instAdd` `withDensity`	`rnDeriv`	—	`haveLebesgueDecomposition_spec` `Set.compl_inter` `nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `le_trans` `MeasureTheory.measure_union_le` `instOuterMeasureClass` `add_zero` `le_refl` `ext` `MeasureTheory.measure_mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_right` `Set.inter_subset_left` `restrict_apply` `add_apply` `add_comm` `zero_add` `MeasureTheory.withDensity_absolutelyContinuous` `Set.diff_eq` `MeasureTheory.measure_inter_add_diff` `MeasurableSet.inter`
`eq_withDensity_rnDeriv₀` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `MutuallySingular` `MeasureTheory.Measure` `instAdd` `withDensity`	`rnDeriv`	—	`MeasureTheory.withDensity_congr_ae` `eq_withDensity_rnDeriv`
`exists_positive_of_not_mutuallySingular` 📖	mathematical	`MutuallySingular`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `MeasurableSet` `ENNReal` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike` `Preorder.toLE` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Set.instInter`	—	`IsScalarTower.right` `MeasureTheory.hahn_decomposition` `MeasureTheory.isFiniteMeasureSMulNNReal` `MeasurableSet.inter` `Set.inter_subset_right` `MeasurableSet.compl` `MeasurableSet.iInter` `instCountableNat` `Set.inter_eq_left` `Set.iInter_subset` `Set.inter_assoc` `one_div` `ENNReal.coe_inv` `Unique.instSubsingleton` `NNReal.instCanonicallyOrderedAdd` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `NeZero.charZero_one` `Set.univ_inter` `MeasurableSet.univ` `CanLift.prf` `ENNReal.canLift` `MeasureTheory.measure_ne_top` `ENNReal.coe_eq_zero` `exists_nat_one_div_lt` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.nnreal_coe_pos` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `inv_pos` `NNReal.coe_lt_coe` `mul_lt_mul_iff_left₀` `IsStrictOrderedRing.toMulPosStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `NNReal.coe_mul` `mul_assoc` `NNReal.coe_inv` `mul_inv_cancel₀` `LT.lt.ne'` `mul_one` `le_trans` `ENNReal.coe_le_coe` `ENNReal.coe_mul` `LT.lt.le` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `zero_lt_iff` `not_le` `NNReal.half_lt_self` `CharP.cast_eq_zero` `CharP.ofCharZero` `zero_add` `div_self` `le_zero_iff` `MulZeroClass.mul_zero` `ENNReal.instCanonicallyOrderedAdd` `Mathlib.Tactic.Push.not_and_eq` `MutuallySingular.eq_1` `MeasureTheory.exists_measure_pos_of_not_measure_iUnion_null` `compl_compl` `Set.compl_iInter` `NNReal.instIsOrderedRing` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass`
`haveLebesgueDecompositionRnDeriv` 📖	mathematical	—	`HaveLebesgueDecomposition` `withDensity` `rnDeriv`	—	`haveLebesgueDecomposition_withDensity` `measurable_rnDeriv`
`haveLebesgueDecompositionSMul` 📖	mathematical	—	`HaveLebesgueDecomposition` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `ENNReal.smul_def` `haveLebesgueDecompositionSMul'`
`haveLebesgueDecompositionSMul'` 📖	mathematical	—	`HaveLebesgueDecomposition` `ENNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `haveLebesgueDecomposition_spec` `Measurable.const_smul` `MeasurableSMul.toMeasurableConstSMul` `measurableSMul_of_mul` `MeasurableMul₂.toMeasurableMul` `ENNReal.instMeasurableMul₂` `MutuallySingular.smul` `MeasureTheory.withDensity_smul` `smul_add`
`haveLebesgueDecompositionSMulRight` 📖	mathematical	—	`HaveLebesgueDecomposition` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `haveLebesgueDecomposition_spec` `measurable_const` `zero_smul` `MeasureTheory.withDensity_zero` `add_zero` `Measurable.const_smul` `MeasurableSMul.toMeasurableConstSMul` `ENNReal.instMeasurableSMulNNReal` `MutuallySingular.mono_ac` `AbsolutelyContinuous.rfl` `smul_absolutelyContinuous` `MeasureTheory.withDensity_smul` `ENNReal.smul_def` `MeasureTheory.withDensity_smul_measure` `smul_assoc` `instIsScalarTower` `smul_eq_mul` `ENNReal.coe_inv` `ENNReal.inv_mul_cancel` `ENNReal.coe_ne_top` `one_smul`
`haveLebesgueDecomposition_add` 📖	mathematical	—	`MeasureTheory.Measure` `instAdd` `singularPart` `withDensity` `rnDeriv`	—	`haveLebesgueDecomposition_spec`
`haveLebesgueDecomposition_of_finiteMeasure` 📖	mathematical	—	`HaveLebesgueDecomposition`	—	`exists_seq_tendsto_sSup` `ENNReal.instOrderTopology` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `ENNReal.instMetrizableSpace` `LebesgueDecomposition.zero_mem_measurableLE` `MeasureTheory.lintegral_const` `MulZeroClass.zero_mul` `OrderTop.bddAbove` `MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone` `Measurable.aemeasurable` `iSup_apply` `LebesgueDecomposition.iSup_mem_measurableLE` `Filter.Eventually.of_forall` `instOuterMeasureClass` `LebesgueDecomposition.iSup_monotone'` `tendsto_atTop_iSup` `LinearOrder.supConvergenceClass` `tendsto_nhds_unique` `ENNReal.instT2Space` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_of_tendsto_of_tendsto_of_le_of_le` `tendsto_const_nhds` `MeasureTheory.lintegral_mono` `LebesgueDecomposition.iSup_le_le` `le_rfl` `le_sSup` `LebesgueDecomposition.iSup_mem_measurableLE'` `Measurable.iSup` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `instCountableNat` `MeasureTheory.lintegral_iSup` `LebesgueDecomposition.iSup_monotone` `iSup_le` `le_intro` `MeasureTheory.withDensity_apply` `MeasureTheory.isFiniteMeasure_withDensity` `ne_top_of_le_ne_top` `MeasureTheory.measure_ne_top` `restrict_univ` `MeasurableSet.univ` `exists_positive_of_not_mutuallySingular` `isFiniteMeasure_sub` `MeasureTheory.lintegral_add_left` `measurable_const` `restrict_apply_univ` `add_le_of_le_tsub_right_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `ENNReal.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `ENNReal.instOrderedSub` `MeasurableSet.inter` `sub_apply` `Measurable.add` `ContinuousAdd.measurableMul₂` `ENNReal.instContinuousAdd` `Measurable.indicator` `MeasureTheory.lintegral_indicator` `MeasureTheory.setLIntegral_const` `restrict_apply` `add_assoc` `MeasureTheory.lintegral_inter_add_diff` `Set.inter_comm` `add_comm` `MeasureTheory.measure_inter_add_diff` `add_le_add` `covariant_swap_add_of_covariant_add` `MeasurableSet.diff` `not_lt` `ENNReal.lt_add_right` `LT.lt.ne'` `ENNReal.mul_pos_iff` `ENNReal.coe_pos` `ext` `coe_add` `Pi.add_apply` `add_tsub_cancel_of_le`
`haveLebesgueDecomposition_of_sigmaFinite` 📖	mathematical	—	`HaveLebesgueDecomposition`	—	`MeasurableSet.disjointed` `MeasureTheory.measurableSet_spanningSets` `lt_of_le_of_lt` `MeasureTheory.measure_mono` `instOuterMeasureClass` `disjointed_le` `MeasureTheory.measure_spanningSets_lt_top` `Measurable.indicator` `measurable_rnDeriv` `MutuallySingular.sum_left` `instCountableNat` `restrict_add_restrict_compl` `MutuallySingular.add_right` `mutuallySingular_singularPart` `MutuallySingular.singularPart` `MeasurableSet.compl` `restrict_apply` `Set.compl_inter_self` `MeasureTheory.measure_empty` `compl_compl` `Set.inter_compl_self` `MeasureTheory.withDensity_tsum` `sum_add_sum` `MeasureTheory.withDensity_indicator` `singularPart_add_rnDeriv` `haveLebesgueDecomposition_of_finiteMeasure` `MeasureTheory.isFiniteMeasureRestrict` `MeasureTheory.Restrict.isFiniteMeasure` `MeasureTheory.sum_restrict_disjointed_spanningSets` `Measurable.ennreal_tsum'` `HaveLebesgueDecomposition.sfinite_of_isFiniteMeasure` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite`
`haveLebesgueDecomposition_spec` 📖	mathematical	—	`Measurable` `ENNReal` `ENNReal.measurableSpace` `rnDeriv` `MutuallySingular` `singularPart` `MeasureTheory.Measure` `instAdd` `withDensity`	—	`HaveLebesgueDecomposition.lebesgue_decomposition` `singularPart_def` `rnDeriv_def`
`haveLebesgueDecomposition_withDensity` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`HaveLebesgueDecomposition` `withDensity`	—	`MutuallySingular.zero_left` `zero_add`
`instHaveLebesgueDecompositionSelf` 📖	mathematical	—	`HaveLebesgueDecomposition`	—	`measurable_const` `MutuallySingular.zero_left` `MeasureTheory.withDensity_one` `zero_add`
`instHaveLebesgueDecompositionSingularPart` 📖	mathematical	—	`HaveLebesgueDecomposition` `singularPart`	—	`measurable_zero` `mutuallySingular_singularPart` `MeasureTheory.withDensity_zero` `add_zero`
`instHaveLebesgueDecompositionZeroLeft` 📖	mathematical	—	`HaveLebesgueDecomposition` `MeasureTheory.Measure` `instZero`	—	`MutuallySingular.haveLebesgueDecomposition` `MutuallySingular.zero_left`
`instHaveLebesgueDecompositionZeroRight` 📖	mathematical	—	`HaveLebesgueDecomposition` `MeasureTheory.Measure` `instZero`	—	`MutuallySingular.haveLebesgueDecomposition` `MutuallySingular.zero_right`
`lintegral_rnDeriv_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.lintegral` `rnDeriv` `Top.top` `instTopENNReal`	—	`MeasureTheory.setLIntegral_univ` `lintegral_rnDeriv_lt_top_of_measure_ne_top` `LT.lt.ne` `MeasureTheory.measure_lt_top`
`lintegral_rnDeriv_lt_top_of_measure_ne_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.lintegral` `restrict` `rnDeriv` `Top.top` `instTopENNReal`	—	`MeasureTheory.withDensity_apply` `MeasureTheory.measurableSet_toMeasurable` `le_add_self` `ENNReal.instCanonicallyOrderedAdd` `add_apply` `haveLebesgueDecomposition_add` `MeasureTheory.measure_toMeasurable` `Ne.lt_top` `lt_of_le_of_lt` `MeasureTheory.lintegral_mono_set` `MeasureTheory.subset_toMeasurable` `HaveLebesgueDecomposition.lebesgue_decomposition` `rnDeriv_def` `MeasureTheory.lintegral_zero`
`measurable_rnDeriv` 📖	mathematical	—	`Measurable` `ENNReal` `ENNReal.measurableSpace` `rnDeriv`	—	`haveLebesgueDecomposition_spec` `rnDeriv_of_not_haveLebesgueDecomposition` `measurable_zero`
`measure_sub_rnDeriv` 📖	mathematical	—	`MeasureTheory.Measure` `instSub` `withDensity` `rnDeriv` `singularPart`	—	`singularPart_add_rnDeriv` `add_sub_cancel` `withDensity.instIsFiniteMeasure`
`measure_sub_singularPart` 📖	mathematical	—	`MeasureTheory.Measure` `instSub` `singularPart` `withDensity` `rnDeriv`	—	`rnDeriv_add_singularPart` `add_sub_cancel` `singularPart.instIsFiniteMeasure`
`mutuallySingular_singularPart` 📖	mathematical	—	`MutuallySingular` `singularPart`	—	`haveLebesgueDecomposition_spec` `singularPart_of_not_haveLebesgueDecomposition` `MutuallySingular.zero_left`
`rnDeriv_add` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instAdd` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`instOuterMeasureClass` `MeasureTheory.withDensity_eq_iff` `Measurable.aemeasurable` `measurable_rnDeriv` `Measurable.add` `ContinuousAdd.measurableMul₂` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `ENNReal.instContinuousAdd` `LT.lt.ne` `lintegral_rnDeriv_lt_top` `MeasureTheory.isFiniteMeasureAdd` `haveLebesgueDecomposition_add` `singularPart_add` `MeasureTheory.withDensity_add_left` `add_assoc` `add_comm` `singularPart.instSigmaFinite` `MeasureTheory.Add.sigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite`
`rnDeriv_add'` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instAdd` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`instOuterMeasureClass` `MeasureTheory.withDensity_eq_iff_of_sigmaFinite` `Measurable.aemeasurable` `measurable_rnDeriv` `Measurable.add` `ContinuousAdd.measurableMul₂` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `ENNReal.instContinuousAdd` `haveLebesgueDecomposition_add` `HaveLebesgueDecomposition.add_left` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `singularPart_add` `MeasureTheory.withDensity_add_left` `add_assoc` `add_comm` `singularPart.instSigmaFinite` `MeasureTheory.Add.sigmaFinite`
`rnDeriv_add_of_mutuallySingular` 📖	mathematical	`MutuallySingular`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instAdd`	—	`Filter.mp_mem` `instOuterMeasureClass` `rnDeriv_eq_zero` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `rnDeriv_add'` `Filter.univ_mem'` `add_zero`
`rnDeriv_add_singularPart` 📖	mathematical	—	`MeasureTheory.Measure` `instAdd` `withDensity` `rnDeriv` `singularPart`	—	`add_comm` `singularPart_add_rnDeriv`
`rnDeriv_def` 📖	mathematical	—	`rnDeriv` `HaveLebesgueDecomposition` `MeasureTheory.Measure` `Measurable` `ENNReal` `ENNReal.measurableSpace` `MutuallySingular` `instAdd` `withDensity` `HaveLebesgueDecomposition.lebesgue_decomposition` `Pi.instZero` `instZeroENNReal`	—	`HaveLebesgueDecomposition.lebesgue_decomposition`
`rnDeriv_eq_zero` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `Pi.instZero` `instZeroENNReal` `MutuallySingular`	—	`instOuterMeasureClass` `withDensity_rnDeriv_eq_zero` `MeasureTheory.withDensity_eq_zero_iff` `Measurable.aemeasurable` `measurable_rnDeriv`
`rnDeriv_lt_top` 📖	mathematical	—	`Filter.Eventually` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `rnDeriv` `Top.top` `instTopENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	—	`instOuterMeasureClass` `MeasureTheory.ae_restrict_iff'` `MeasureTheory.measurableSet_spanningSets` `MeasureTheory.ae_lt_top` `measurable_rnDeriv` `LT.lt.ne` `lintegral_rnDeriv_lt_top_of_measure_ne_top` `MeasureTheory.measure_spanningSets_lt_top` `Filter.mp_mem` `MeasureTheory.ae_all_iff` `instCountableNat` `Filter.univ_mem'` `MeasureTheory.mem_spanningSetsIndex`
`rnDeriv_ne_top` 📖	mathematical	—	`Filter.Eventually` `ENNReal` `rnDeriv` `Top.top` `instTopENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	—	`Filter.mp_mem` `instOuterMeasureClass` `rnDeriv_lt_top` `Filter.univ_mem'` `LT.lt.ne`
`rnDeriv_of_not_haveLebesgueDecomposition` 📖	mathematical	`HaveLebesgueDecomposition`	`rnDeriv` `Pi.instZero` `ENNReal` `instZeroENNReal`	—	`HaveLebesgueDecomposition.lebesgue_decomposition` `rnDeriv_def`
`rnDeriv_restrict` 📖	mathematical	`MeasurableSet`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `restrict` `Set.indicator` `instZeroENNReal`	—	`Filter.EventuallyEq.symm` `instOuterMeasureClass` `eq_rnDeriv` `Measurable.indicator` `measurable_rnDeriv` `mutuallySingular_singularPart` `singularPart_restrict` `MeasureTheory.withDensity_indicator` `MeasureTheory.restrict_withDensity` `restrict_add` `haveLebesgueDecomposition_add`
`rnDeriv_restrict_self` 📖	mathematical	`MeasurableSet`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `restrict` `Set.indicator` `instZeroENNReal` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`instOuterMeasureClass` `MeasureTheory.withDensity_indicator_one` `rnDeriv_withDensity` `Measurable.indicator` `measurable_one`
`rnDeriv_self` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`rnDeriv_add_singularPart` `instHaveLebesgueDecompositionSelf` `MeasureTheory.withDensity_one` `instOuterMeasureClass` `MeasureTheory.withDensity_eq_iff_of_sigmaFinite` `Measurable.aemeasurable` `measurable_rnDeriv` `aemeasurable_const` `add_zero` `singularPart_self`
`rnDeriv_singularPart` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `singularPart` `Pi.instZero` `instZeroENNReal`	—	`instOuterMeasureClass` `rnDeriv_eq_zero` `instHaveLebesgueDecompositionSingularPart` `mutuallySingular_singularPart`
`rnDeriv_smul_left` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `NNReal` `instSMul` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `Function.hasSMul`	—	`instOuterMeasureClass` `IsScalarTower.right` `MeasureTheory.withDensity_eq_iff` `Measurable.aemeasurable` `measurable_rnDeriv` `AEMeasurable.const_smul` `MeasurableSMul.toMeasurableConstSMul` `ENNReal.instMeasurableSMulNNReal` `LT.lt.ne` `lintegral_rnDeriv_lt_top` `MeasureTheory.isFiniteMeasureSMulNNReal` `MeasureTheory.withDensity_smul` `haveLebesgueDecomposition_add` `haveLebesgueDecompositionSMul` `singularPart_smul` `smul_add` `singularPart.instSigmaFinite` `MeasureTheory.SMul.sigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite`
`rnDeriv_smul_left'` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `NNReal` `instSMul` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `Function.hasSMul`	—	`instOuterMeasureClass` `IsScalarTower.right` `MeasureTheory.withDensity_eq_iff_of_sigmaFinite` `Measurable.aemeasurable` `measurable_rnDeriv` `AEMeasurable.const_smul` `MeasurableSMul.toMeasurableConstSMul` `ENNReal.instMeasurableSMulNNReal` `MeasureTheory.withDensity_smul` `haveLebesgueDecomposition_add` `haveLebesgueDecompositionSMul` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `singularPart_smul` `smul_add` `singularPart.instSigmaFinite` `MeasureTheory.SMul.sigmaFinite`
`rnDeriv_smul_left_of_ne_top` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Function.hasSMul`	—	`instOuterMeasureClass` `IsScalarTower.right` `rnDeriv_smul_left` `ENNReal.coe_toNNReal`
`rnDeriv_smul_left_of_ne_top'` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Function.hasSMul`	—	`instOuterMeasureClass` `IsScalarTower.right` `rnDeriv_smul_left'` `ENNReal.coe_toNNReal`
`rnDeriv_smul_right` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `NNReal` `instSMul` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `Function.hasSMul` `NNReal.instInv`	—	`AbsolutelyContinuous.ae_le` `IsScalarTower.right` `absolutelyContinuous_smul` `ENNReal.coe_ne_zero` `instOuterMeasureClass` `MeasureTheory.withDensity_eq_iff` `Measurable.aemeasurable` `measurable_rnDeriv` `AEMeasurable.const_smul` `MeasurableSMul.toMeasurableConstSMul` `ENNReal.instMeasurableSMulNNReal` `LT.lt.ne` `lintegral_rnDeriv_lt_top` `MeasureTheory.withDensity_smul` `haveLebesgueDecomposition_add` `haveLebesgueDecompositionSMulRight` `singularPart_smul_right` `ENNReal.smul_def` `MeasureTheory.withDensity_smul_measure` `smul_assoc` `instIsScalarTower` `IsScalarTower.left` `smul_eq_mul` `inv_mul_cancel₀` `one_smul` `singularPart.instSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite`
`rnDeriv_smul_right'` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `NNReal` `instSMul` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `Function.hasSMul` `NNReal.instInv`	—	`AbsolutelyContinuous.ae_le` `IsScalarTower.right` `absolutelyContinuous_smul` `ENNReal.coe_ne_zero` `instOuterMeasureClass` `MeasureTheory.withDensity_eq_iff_of_sigmaFinite` `MeasureTheory.SMul.sigmaFinite` `Measurable.aemeasurable` `measurable_rnDeriv` `AEMeasurable.const_smul` `MeasurableSMul.toMeasurableConstSMul` `ENNReal.instMeasurableSMulNNReal` `MeasureTheory.withDensity_smul` `haveLebesgueDecomposition_add` `haveLebesgueDecompositionSMulRight` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `singularPart_smul_right` `ENNReal.smul_def` `MeasureTheory.withDensity_smul_measure` `smul_assoc` `instIsScalarTower` `IsScalarTower.left` `smul_eq_mul` `inv_mul_cancel₀` `one_smul` `singularPart.instSigmaFinite`
`rnDeriv_smul_right_of_ne_top` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Function.hasSMul` `ENNReal.instInv`	—	`instOuterMeasureClass` `IsScalarTower.right` `rnDeriv_smul_right` `ENNReal.toNNReal_eq_zero_iff` `ENNReal.coe_inv` `ENNReal.coe_toNNReal`
`rnDeriv_smul_right_of_ne_top'` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Function.hasSMul` `ENNReal.instInv`	—	`instOuterMeasureClass` `IsScalarTower.right` `rnDeriv_smul_right'` `ENNReal.toNNReal_eq_zero_iff` `ENNReal.coe_toNNReal` `ENNReal.inv_ne_top` `ENNReal.smul_def` `ENNReal.toNNReal_inv`
`rnDeriv_withDensity` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `withDensity`	—	`rnDeriv_withDensity₀` `Measurable.aemeasurable`
`rnDeriv_withDensity₀` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `withDensity`	—	`zero_add` `Filter.EventuallyEq.symm` `instOuterMeasureClass` `eq_rnDeriv₀` `MutuallySingular.zero_left`
`rnDeriv_zero` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instZero` `Pi.instZero` `instZeroENNReal`	—	`instOuterMeasureClass` `rnDeriv_eq_zero` `instHaveLebesgueDecompositionZeroLeft` `MutuallySingular.zero_left`
`singularPart_add` 📖	mathematical	—	`singularPart` `MeasureTheory.Measure` `instAdd`	—	`eq_singularPart` `Measurable.add` `ContinuousAdd.measurableMul₂` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `ENNReal.instContinuousAdd` `measurable_rnDeriv` `MutuallySingular.add_left` `mutuallySingular_singularPart` `Pi.add_def` `MeasureTheory.withDensity_add_left` `add_assoc` `add_comm` `haveLebesgueDecomposition_add`
`singularPart_add_rnDeriv` 📖	mathematical	—	`MeasureTheory.Measure` `instAdd` `singularPart` `withDensity` `rnDeriv`	—	`haveLebesgueDecomposition_add`
`singularPart_def` 📖	mathematical	—	`singularPart` `MeasureTheory.Measure` `HaveLebesgueDecomposition` `Measurable` `ENNReal` `ENNReal.measurableSpace` `MutuallySingular` `instAdd` `withDensity` `HaveLebesgueDecomposition.lebesgue_decomposition` `instZero`	—	`HaveLebesgueDecomposition.lebesgue_decomposition`
`singularPart_eq_restrict` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `singularPart` `Compl.compl` `Set.instCompl` `instZeroENNReal`	`restrict`	—	`singularPart_eq_restrict'` `MeasureTheory.withDensity_absolutelyContinuous`
`singularPart_eq_restrict'` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `singularPart` `Compl.compl` `Set.instCompl` `instZeroENNReal` `withDensity` `rnDeriv`	`restrict`	—	`singularPart_add_rnDeriv` `restrict_add` `restrict_eq_self_of_ae_mem` `restrict_eq_zero` `add_zero`
`singularPart_eq_self` 📖	mathematical	—	`singularPart` `MutuallySingular`	—	`mutuallySingular_singularPart` `MutuallySingular.haveLebesgueDecomposition` `singularPart_add_rnDeriv` `withDensity_rnDeriv_eq_zero` `add_zero`
`singularPart_eq_zero` 📖	mathematical	—	`singularPart` `MeasureTheory.Measure` `instZero` `AbsolutelyContinuous`	—	`haveLebesgueDecomposition_add` `zero_add` `MeasureTheory.withDensity_absolutelyContinuous` `singularPart_eq_zero_of_ac`
`singularPart_eq_zero_of_ac` 📖	mathematical	`AbsolutelyContinuous`	`singularPart` `MeasureTheory.Measure` `instZero`	—	`MutuallySingular.self_iff` `MutuallySingular.mono_ac` `mutuallySingular_singularPart` `AbsolutelyContinuous.rfl` `AbsolutelyContinuous.trans` `absolutelyContinuous_of_le` `singularPart_le`
`singularPart_le` 📖	mathematical	—	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `singularPart`	—	`haveLebesgueDecomposition_add` `le_add_right` `le_rfl` `HaveLebesgueDecomposition.lebesgue_decomposition` `singularPart_def` `zero_le`
`singularPart_of_not_haveLebesgueDecomposition` 📖	mathematical	`HaveLebesgueDecomposition`	`singularPart` `MeasureTheory.Measure` `instZero`	—	`HaveLebesgueDecomposition.lebesgue_decomposition` `singularPart_def`
`singularPart_restrict` 📖	mathematical	`MeasurableSet`	`singularPart` `restrict`	—	`eq_singularPart` `Measurable.indicator` `measurable_rnDeriv` `MutuallySingular.restrict` `mutuallySingular_singularPart` `ext` `MeasureTheory.withDensity_indicator` `MeasureTheory.restrict_withDensity` `restrict_add` `haveLebesgueDecomposition_add`
`singularPart_self` 📖	mathematical	—	`singularPart` `MeasureTheory.Measure` `instZero`	—	`singularPart_eq_zero_of_ac` `AbsolutelyContinuous.rfl`
`singularPart_singularPart` 📖	mathematical	—	`singularPart`	—	`singularPart_eq_self` `mutuallySingular_singularPart`
`singularPart_smul` 📖	mathematical	—	`singularPart` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `zero_smul` `singularPart_zero` `eq_singularPart` `Measurable.const_smul` `MeasurableSMul.toMeasurableConstSMul` `measurableSMul_of_mul` `MeasurableMul₂.toMeasurableMul` `ENNReal.instMeasurableMul₂` `measurable_rnDeriv` `MutuallySingular.smul` `mutuallySingular_singularPart` `MeasureTheory.withDensity_smul` `smul_add` `haveLebesgueDecomposition_add` `ENNReal.smul_def` `HaveLebesgueDecomposition.lebesgue_decomposition` `singularPart_def` `inv_smul_smul₀` `haveLebesgueDecompositionSMul` `smul_zero`
`singularPart_smul_right` 📖	mathematical	—	`singularPart` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `eq_singularPart` `Measurable.const_smul` `MeasurableSMul.toMeasurableConstSMul` `ENNReal.instMeasurableSMulNNReal` `measurable_rnDeriv` `MutuallySingular.mono_ac` `mutuallySingular_singularPart` `AbsolutelyContinuous.rfl` `smul_absolutelyContinuous` `ENNReal.smul_def` `MeasureTheory.withDensity_smul_measure` `MeasureTheory.withDensity_smul` `smul_inv_smul₀` `haveLebesgueDecomposition_add` `HaveLebesgueDecomposition.lebesgue_decomposition` `singularPart_def` `inv_smul_smul₀` `haveLebesgueDecompositionSMulRight`
`singularPart_withDensity` 📖	mathematical	—	`singularPart` `withDensity` `MeasureTheory.Measure` `instZero`	—	`singularPart_eq_zero_of_ac` `MeasureTheory.withDensity_absolutelyContinuous`
`singularPart_zero` 📖	mathematical	—	`singularPart` `MeasureTheory.Measure` `instZero`	—	`singularPart_eq_zero_of_ac` `AbsolutelyContinuous.zero`
`singularPart_zero_right` 📖	mathematical	—	`singularPart` `MeasureTheory.Measure` `instZero`	—	`haveLebesgueDecomposition_add` `instHaveLebesgueDecompositionZeroRight` `MeasureTheory.withDensity_zero_left` `add_zero`
`withDensity_rnDeriv_eq_zero` 📖	mathematical	—	`withDensity` `rnDeriv` `MeasureTheory.Measure` `instZero` `MutuallySingular`	—	`haveLebesgueDecomposition_add` `add_zero` `mutuallySingular_singularPart` `MutuallySingular.self_iff` `MutuallySingular.mono_ac` `MutuallySingular.add_left_iff` `AbsolutelyContinuous.rfl` `MeasureTheory.withDensity_absolutelyContinuous`
`withDensity_rnDeriv_le` 📖	mathematical	—	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `withDensity` `rnDeriv`	—	`haveLebesgueDecomposition_add` `le_add_left` `le_rfl` `HaveLebesgueDecomposition.lebesgue_decomposition` `rnDeriv_def` `MeasureTheory.withDensity_zero` `zero_le`

MeasureTheory.Measure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withDensity_rnDeriv` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.Measure.withDensity` `MeasureTheory.Measure.rnDeriv`	—	`MeasureTheory.Measure.absolutelyContinuous_of_add_of_mutuallySingular` `MeasureTheory.Measure.haveLebesgueDecomposition_add` `add_comm` `MeasureTheory.Measure.MutuallySingular.mono_ac` `MeasureTheory.Measure.MutuallySingular.symm` `MeasureTheory.Measure.mutuallySingular_singularPart` `rfl`

MeasureTheory.Measure.HaveLebesgueDecomposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_left` 📖	mathematical	—	`MeasureTheory.Measure.HaveLebesgueDecomposition` `MeasureTheory.Measure` `MeasureTheory.Measure.instAdd`	—	`MeasureTheory.Measure.sum_fintype` `Finset.sum_insert` `Finset.sum_singleton` `sum_left` `Bool.countable`
`lebesgue_decomposition` 📖	mathematical	—	`Measurable` `ENNReal` `ENNReal.measurableSpace` `MeasureTheory.Measure` `MeasureTheory.Measure.MutuallySingular` `MeasureTheory.Measure.instAdd` `MeasureTheory.Measure.withDensity`	—	—
`sfinite_of_isFiniteMeasure` 📖	—	`MeasureTheory.Measure.HaveLebesgueDecomposition`	—	—	`sum_left` `instCountableNat` `MeasureTheory.isFiniteMeasure_sfiniteSeq` `MeasureTheory.sum_sfiniteSeq`
`sum_left` 📖	mathematical	`MeasureTheory.Measure.HaveLebesgueDecomposition`	`MeasureTheory.Measure.sum`	—	`Measurable.ennreal_tsum'` `MeasureTheory.Measure.measurable_rnDeriv` `MeasureTheory.withDensity_tsum` `MeasureTheory.Measure.sum_add_sum` `MeasureTheory.Measure.singularPart_add_rnDeriv`

MeasureTheory.Measure.LebesgueDecomposition

Definitions

Name	Category	Theorems
`measurableLE` 📖	CompOp	1 math math: `zero_mem_measurableLE`
`measurableLEEval` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup_le_le` 📖	mathematical	—	`Pi.hasLe` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`le_iSup₂`
`iSup_mem_measurableLE` 📖	mathematical	`Set` `Set.instMembership` `measurableLE`	`iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`iSup_congr_Prop` `Nat.instCanonicallyOrderedAdd` `iSup_iSup_eq_left` `iSup_succ_eq_sup` `Measurable.iSup` `ENNReal.borelSpace` `ENNReal.instOrderTopology` `ENNReal.instSecondCountableTopology` `instCountableNat` `Measurable.iSup_Prop` `sup_mem_measurableLE`
`iSup_mem_measurableLE'` 📖	mathematical	`Set` `Set.instMembership` `measurableLE`	`iSup` `Pi.supSet` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`iSup_apply` `iSup_mem_measurableLE`
`iSup_monotone` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `Pi.preorder` `ENNReal` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`biSup_mono` `ge_trans`
`iSup_monotone'` 📖	mathematical	—	`Monotone` `ENNReal` `Nat.instPreorder` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`iSup_monotone`
`iSup_succ_eq_sup` 📖	mathematical	—	`iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `ENNReal.instMax`	—	`le_antisymm_iff` `iSup₂_le` `Nat.of_le_succ` `le_sup_of_le_right` `le_iSup₂` `le_sup_left` `sup_le` `le_rfl` `biSup_mono` `LE.le.trans`
`sup_mem_measurableLE` 📖	mathematical	`Set` `Set.instMembership` `measurableLE`	`ENNReal` `ENNReal.instMax`	—	`Measurable.max` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `MeasurableSet.inter` `measurableSet_le` `measurableSet_lt` `MeasureTheory.setLIntegral_max` `LE.le.trans_eq` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `MeasureTheory.measure_inter_add_diff`
`zero_mem_measurableLE` 📖	mathematical	—	`Set` `Set.instMembership` `measurableLE` `Pi.instZero` `ENNReal` `instZeroENNReal`	—	`measurable_zero` `MeasureTheory.lintegral_const` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `MulZeroClass.zero_mul` `ENNReal.instCanonicallyOrderedAdd`

MeasureTheory.Measure.MutuallySingular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`haveLebesgueDecomposition` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`MeasureTheory.Measure.HaveLebesgueDecomposition`	—	`measurable_zero` `MeasureTheory.withDensity_zero` `add_zero`
`rnDeriv_ae_eq_zero` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.rnDeriv` `Pi.instZero` `instZeroENNReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.rnDeriv_eq_zero` `MeasureTheory.Measure.rnDeriv_of_not_haveLebesgueDecomposition` `Filter.EventuallyEq.refl`
`singularPart` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`MeasureTheory.Measure.singularPart`	—	`mono` `MeasureTheory.Measure.singularPart_le` `le_rfl`

MeasureTheory.Measure.singularPart

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsFiniteMeasure` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `MeasureTheory.Measure.singularPart`	—	`MeasureTheory.isFiniteMeasure_of_le` `MeasureTheory.Measure.singularPart_le`
`instIsLocallyFiniteMeasure` 📖	mathematical	—	`MeasureTheory.IsLocallyFiniteMeasure` `MeasureTheory.Measure.singularPart`	—	`MeasureTheory.Measure.isLocallyFiniteMeasure_of_le` `MeasureTheory.Measure.singularPart_le`
`instSigmaFinite` 📖	mathematical	—	`MeasureTheory.SigmaFinite` `MeasureTheory.Measure.singularPart`	—	`MeasureTheory.Measure.sigmaFinite_of_le` `MeasureTheory.Measure.singularPart_le`

MeasureTheory.Measure.withDensity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsFiniteMeasure` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `MeasureTheory.Measure.withDensity` `MeasureTheory.Measure.rnDeriv`	—	`MeasureTheory.isFiniteMeasure_of_le` `MeasureTheory.Measure.withDensity_rnDeriv_le`
`instIsLocallyFiniteMeasure` 📖	mathematical	—	`MeasureTheory.IsLocallyFiniteMeasure` `MeasureTheory.Measure.withDensity` `MeasureTheory.Measure.rnDeriv`	—	`MeasureTheory.Measure.isLocallyFiniteMeasure_of_le` `MeasureTheory.Measure.withDensity_rnDeriv_le`
`instSigmaFinite` 📖	mathematical	—	`MeasureTheory.SigmaFinite` `MeasureTheory.Measure.withDensity` `MeasureTheory.Measure.rnDeriv`	—	`MeasureTheory.Measure.sigmaFinite_of_le` `MeasureTheory.Measure.withDensity_rnDeriv_le`

---

← Back to Index