AbsolutelyContinuous

📁 Source: Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean

Statistics

Metric	Count
Definitions AbsolutelyContinuous, AbsolutelyContinuous, «term_≪_»	3
Theorems absolutelyContinuous, absolutelyContinuous, absolutelyContinuous_of_ae, absolutelyContinuous_map, of_absolutelyContinuous, of_le, add, add_left, add_left_iff, add_right, add_right', ae_eq, ae_le, instRefl, map, mk, null_mono, pos_mono, refl, rfl, smul, smul_left, smul_right, trans, zero, absolutelyContinuous_of_eq, absolutelyContinuous_of_le, absolutelyContinuous_of_le_smul, absolutelyContinuous_refl, absolutelyContinuous_rfl, absolutelyContinuous_smul, absolutelyContinuous_sum_left, absolutelyContinuous_sum_right, absolutelyContinuous_zero_iff, ae_le_iff_absolutelyContinuous, ae_mono', smul_absolutelyContinuous, ae_mono	38
Total	41

Eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous	—	MeasureTheory.Measure.absolutelyContinuous_of_eq

LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder	MeasureTheory.Measure.AbsolutelyContinuous	—	MeasureTheory.Measure.absolutelyContinuous_of_le
absolutelyContinuous_of_ae 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Measure.AbsolutelyContinuous	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_le_iff_absolutelyContinuous

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_map 📖	mathematical	MeasurableEmbedding MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.map	—	map_apply

MeasureTheory

Definitions

Name	Category	Theorems
«term_≪_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_mono 📖	mathematical	Measure Preorder.toLE PartialOrder.toPreorder Measure.instPartialOrder	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.AbsolutelyContinuous.ae_le LE.le.absolutelyContinuous

MeasureTheory.AEDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_absolutelyContinuous 📖	mathematical	MeasureTheory.AEDisjoint MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.AEDisjoint	—	—
of_le 📖	mathematical	MeasureTheory.AEDisjoint MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder	MeasureTheory.AEDisjoint	—	of_absolutelyContinuous MeasureTheory.Measure.absolutelyContinuous_of_le

MeasureTheory.Measure

Definitions

Name	Category	Theorems
AbsolutelyContinuous 📖	MathDef	107 math math: absolutelyContinuous_isAddHaarMeasure, ProbabilityTheory.absolutelyContinuous_posterior_iff, MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map, MeasureTheory.absolutelyContinuous_toFinite, AbsolutelyContinuous.smul_left, MeasureTheory.absolutelyContinuous_of_isMulLeftInvariant, AbsolutelyContinuous.kernel_of_compProd, AbsolutelyContinuous.prod, AbsolutelyContinuous.add_left, MeasureTheory.withDensity_absolutelyContinuous', singularPart_eq_zero, MeasureTheory.inv_absolutelyContinuous, MeasureTheory.absolutelyContinuous_map_add_right, MeasureTheory.absolutelyContinuous_of_isAddLeftInvariant, AbsolutelyContinuous.smul_right, AbsolutelyContinuous.zero, MeasureTheory.hasPDF_iff, ProbabilityTheory.absolutelyContinuous_of_posterior, AbsolutelyContinuous.comp_left, AbsolutelyContinuous.add_left_iff, AbsolutelyContinuous.comp_right, AbsolutelyContinuous.comp, ProbabilityTheory.Kernel.absolutelyContinuous_comp_of_absolutelyContinuous, LE.le.absolutelyContinuous_of_ae, MeasureTheory.absolutelyContinuous_map_div_left, AbsolutelyContinuous.mk, AbsolutelyContinuous.add_right', MeasureTheory.SignedMeasure.absolutelyContinuous_ennreal_iff, ProbabilityTheory.Kernel.withDensity_absolutelyContinuous, absolutelyContinuous_comp_of_countable, AbsolutelyContinuous.compProd_right, absolutelyContinuous_isHaarMeasure, absolutelyContinuous_of_compProd, absolutelyContinuous_restrict, AbsolutelyContinuous.compProd, AbsolutelyContinuous.compProd_of_compProd, InformationTheory.klDiv_def, InformationTheory.klDiv_eq_lintegral_klFun, absolutelyContinuous_of_eq, MeasureTheory.absolutelyContinuous_inv, conv_absolutelyContinuous, AbsolutelyContinuous.add_right, AbsolutelyContinuous.trans, InformationTheory.klDiv_ne_top_iff, MeasureTheory.absolutelyContinuous_neg, smul_absolutelyContinuous, InformationTheory.klDiv_eq_integral_klFun, MeasureTheory.toFinite_absolutelyContinuous, ProbabilityTheory.Kernel.measurableSet_absolutelyContinuous, absolutelyContinuous_compProd_left_iff, absolutelyContinuous_smul, LE.le.absolutelyContinuous, Real.hasPDF_iff, absolutelyContinuous_withDensity_rnDeriv_swap, absolutelyContinuous_of_le_smul, absolutelyContinuous_compProd_of_compProd, absolutelyContinuous_rfl, Real.hasPDF_iff_of_aemeasurable, ae_le_iff_absolutelyContinuous, mconv_absolutelyContinuous, AbsolutelyContinuous.restrict, ProbabilityTheory.cond_absolutelyContinuous, Eq.absolutelyContinuous, MeasurableEmbedding.absolutelyContinuous_map, absolutelyContinuous_refl, ProbabilityTheory.Kernel.singularPart_eq_zero_iff_absolutelyContinuous, AbsolutelyContinuous.withDensity_rnDeriv, MeasureTheory.neg_absolutelyContinuous, absolutelyContinuous_of_le, QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.absolutelyContinuous_tilted, AbsolutelyContinuous.add, AbsolutelyContinuous.rfl, absolutelyContinuous_compProd_iff', ProbabilityTheory.absolutelyContinuous_cond_univ, absolutelyContinuous_zero_iff, ProbabilityTheory.absolutelyContinuous_boolKernel_comp_right, ProbabilityTheory.gaussianReal_absolutelyContinuous', AbsolutelyContinuous.smul, AbsolutelyContinuous.refl, MeasureTheory.tilted_absolutelyContinuous, ProbabilityTheory.absolutelyContinuous_posterior, AbsolutelyContinuous.trim, MeasureTheory.absolutelyContinuous_map_mul_right, IicSnd_ac_fst, absolutelyContinuous_compProd_right_iff, ProbabilityTheory.absolutelyContinuous_boolKernel_comp_left, absolutelyContinuous_iff_withDensity_rnDeriv_eq, AbsolutelyContinuous.map, absolutelyContinuous_of_add_of_mutuallySingular, absolutelyContinuous_sum_left, MeasureTheory.hasPDF_iff_of_aemeasurable, MeasureTheory.IsAddFundamentalDomain.absolutelyContinuous_map, absolutelyContinuous_withDensity_rnDeriv, absolutelyContinuous_sum_right, MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff, AbsolutelyContinuous.compProd_left, MeasureTheory.pdf.IsUniform.absolutelyContinuous, MeasureTheory.HasPDF.absolutelyContinuous', MeasureTheory.sfiniteSeq_absolutelyContinuous_toFinite, absolutelyContinuous_compProd_iff, AbsolutelyContinuous.instRefl, MeasureTheory.absolutelyContinuous_map_sub_left, MeasureTheory.HasPDF.absolutelyContinuous, MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous, ProbabilityTheory.gaussianReal_absolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_of_eq 📖	mathematical	—	AbsolutelyContinuous	—	LE.le.absolutelyContinuous Eq.le
absolutelyContinuous_of_le 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder	AbsolutelyContinuous	—	nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd le_iff'
absolutelyContinuous_of_le_smul 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder ENNReal instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	AbsolutelyContinuous	—	IsScalarTower.right AbsolutelyContinuous.trans absolutelyContinuous_of_le smul_absolutelyContinuous
absolutelyContinuous_refl 📖	mathematical	—	AbsolutelyContinuous	—	AbsolutelyContinuous.refl
absolutelyContinuous_rfl 📖	mathematical	—	AbsolutelyContinuous	—	AbsolutelyContinuous.rfl
absolutelyContinuous_smul 📖	mathematical	—	AbsolutelyContinuous ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	ENNReal.instNoZeroDivisors
absolutelyContinuous_sum_left 📖	mathematical	AbsolutelyContinuous	AbsolutelyContinuous sum	—	sum_apply tsum_zero
absolutelyContinuous_sum_right 📖	mathematical	AbsolutelyContinuous	AbsolutelyContinuous sum	—	sum_apply
absolutelyContinuous_zero_iff 📖	mathematical	—	AbsolutelyContinuous MeasureTheory.Measure instZero	—	measure_univ_eq_zero AbsolutelyContinuous.zero
ae_le_iff_absolutelyContinuous 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass AbsolutelyContinuous	—	instOuterMeasureClass MeasureTheory.measure_eq_zero_iff_ae_notMem
ae_mono' 📖	mathematical	AbsolutelyContinuous	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	—	AbsolutelyContinuous.ae_le
smul_absolutelyContinuous 📖	mathematical	—	AbsolutelyContinuous ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	AbsolutelyContinuous.smul_left IsScalarTower.right AbsolutelyContinuous.rfl

MeasureTheory.Measure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	Unique.instSubsingleton
add_left 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	add_left_iff
add_left_iff 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	Unique.instSubsingleton trans add IsScalarTower.right Nat.instAtLeastTwoHAddOfNat two_smul smul_left rfl
add_right 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	Unique.instSubsingleton
add_right' 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	add_comm add_right
ae_eq 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass ae_le
ae_le 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_le_iff_absolutelyContinuous
instRefl 📖	mathematical	—	MeasureTheory.Measure MeasureTheory.Measure.AbsolutelyContinuous	—	rfl
map 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous Measurable	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.map	—	MeasureTheory.Measure.map_apply
mk 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal	MeasureTheory.Measure.AbsolutelyContinuous	—	MeasureTheory.exists_measurable_superset_of_null MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass
null_mono 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal	—	—
pos_mono 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike	—	Mathlib.Tactic.Contrapose.contrapose₁ null_mono ENNReal.instCanonicallyOrderedAdd instReflLe
refl 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous	—	Eq.absolutelyContinuous
rfl 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous	—	—
smul 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure MeasureTheory.Measure.instSMul	—	MeasureTheory.Measure.smul_apply smul_one_smul smul_eq_mul mul_eq_zero ENNReal.instNoZeroDivisors
smul_left 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure MeasureTheory.Measure.instSMul	—	smul_one_smul smul_zero
smul_right 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.AbsolutelyContinuous ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	trans IsScalarTower.right MeasureTheory.Measure.absolutelyContinuous_smul smul
trans 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.AbsolutelyContinuous	—	—
zero 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure MeasureTheory.Measure.instZero	—	—

MeasureTheory.VectorMeasure

Definitions

Name	Category	Theorems
AbsolutelyContinuous 📖	MathDef	17 math math: AbsolutelyContinuous.eq, MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq, AbsolutelyContinuous.trans, MeasureTheory.SignedMeasure.absolutelyContinuous_ennreal_iff, AbsolutelyContinuous.neg_right, AbsolutelyContinuous.add, AbsolutelyContinuous.neg_left, AbsolutelyContinuous.map, AbsolutelyContinuous.sub, AbsolutelyContinuous.zero, MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous, AbsolutelyContinuous.ennrealToMeasure, MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous, AbsolutelyContinuous.mk, AbsolutelyContinuous.refl, MeasureTheory.ComplexMeasure.absolutelyContinuous_ennreal_iff, AbsolutelyContinuous.smul

---

← Back to Index