Marginal

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

Statistics

Metric	Count
Definitions lmarginal, «term∫⋯∫⁻__,_», «term∫⋯∫⁻__,_∂_»	3
Theorems lmarginal, lintegral_eq_lmarginal_univ, lintegral_eq_of_lmarginal_eq, lintegral_le_of_lmarginal_le, lmarginal_congr, lmarginal_empty, lmarginal_eq_of_subset, lmarginal_erase, lmarginal_erase', lmarginal_image, lmarginal_insert, lmarginal_insert', lmarginal_le_of_subset, lmarginal_mono, lmarginal_singleton, lmarginal_union, lmarginal_union', lmarginal_univ, lmarginal_update_of_mem, lmarginal_update_of_notMem	20
Total	23

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lmarginal 📖	mathematical	MeasureTheory.SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace	MeasureTheory.lmarginal	—	lintegral_prod_right MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.pi.sigmaFinite comp measurable_pi_iff measurable_snd measurable_fst

MeasureTheory

Definitions

Name	Category	Theorems
lmarginal 📖	CompOp	19 math math: lmarginal_univ, GridLines.T_lmarginal_antitone, lintegral_eq_lmarginal_univ, lintegral_infinitePi_of_piFinset, lmarginal_union, lmarginal_erase, lmarginal_insert, lmarginal_singleton, lmarginal_erase', Measurable.lmarginal, lmarginal_update_of_notMem, lmarginal_image, lmarginal_congr, lmarginal_empty, lmarginal_update_of_mem, lmarginal_union', GridLines.T_insert_le_T_lmarginal_singleton, lmarginal_mono, lmarginal_insert'
«term∫⋯∫⁻__,_» 📖	CompOp	—
«term∫⋯∫⁻__,_∂_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lintegral_eq_lmarginal_univ 📖	mathematical	SigmaFinite	lintegral MeasurableSpace.pi Measure.pi lmarginal Finset.univ	—	lmarginal_univ
lintegral_eq_of_lmarginal_eq 📖	mathematical	SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace lmarginal	lintegral Measure.pi	—	isEmpty_or_nonempty lintegral_of_isEmpty lintegral_eq_lmarginal_univ lmarginal_eq_of_subset Finset.subset_univ
lintegral_le_of_lmarginal_le 📖	mathematical	SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace Pi.hasLe Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lmarginal	lintegral Measure.pi	—	isEmpty_or_nonempty lintegral_of_isEmpty lintegral_eq_lmarginal_univ lmarginal_le_of_subset Finset.subset_univ
lmarginal_congr 📖	mathematical	—	lmarginal	—	—
lmarginal_empty 📖	mathematical	—	lmarginal Finset Finset.instEmptyCollection	—	Finset.instIsEmpty Measure.pi_of_empty lintegral_dirac' Subsingleton.measurable Unique.instSubsingleton
lmarginal_eq_of_subset 📖	—	SigmaFinite Finset Finset.instHasSubset Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace lmarginal	—	—	Finset.union_sdiff_of_subset lmarginal_union' Finset.disjoint_sdiff
lmarginal_erase 📖	mathematical	SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace Finset Finset.instMembership	lmarginal lintegral Finset.erase Function.update	—	lmarginal.congr_simp Finset.insert_erase lmarginal_insert Finset.notMem_erase
lmarginal_erase' 📖	mathematical	SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace Finset Finset.instMembership	lmarginal Finset.erase lintegral Function.update	—	Finset.insert_erase lmarginal_insert' Finset.notMem_erase
lmarginal_image 📖	mathematical	SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace	lmarginal Finset.image Function.dcomp Measure	—	measurable_pi_iff measurable_pi_apply Finset.induction lmarginal_empty Finset.image_insert lmarginal_insert Measurable.comp Iff.not Function.Injective.mem_finset_image lmarginal.congr_simp Function.update_comp_eq_of_injective'
lmarginal_insert 📖	mathematical	SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace Finset Finset.instMembership	lmarginal Finset.instInsert lintegral Function.update	—	Finset.insert_eq lmarginal_union Finset.disjoint_singleton_left lmarginal_singleton
lmarginal_insert' 📖	mathematical	SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace Finset Finset.instMembership	lmarginal Finset.instInsert lintegral Function.update	—	Finset.insert_eq Finset.union_comm lmarginal_union Finset.disjoint_singleton_right lmarginal_singleton
lmarginal_le_of_subset 📖	—	SigmaFinite Finset Finset.instHasSubset Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace Pi.hasLe Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lmarginal	—	—	Finset.union_sdiff_of_subset lmarginal_union' Finset.disjoint_sdiff lmarginal_mono
lmarginal_mono 📖	mathematical	Pi.hasLe ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	lmarginal	—	lintegral_mono
lmarginal_singleton 📖	mathematical	—	lmarginal Finset Finset.instSingleton lintegral Function.update	—	MeasurePreserving.lintegral_map_equiv MeasurePreserving.symm measurePreserving_piUnique Function.update_eq_updateFinset
lmarginal_union 📖	mathematical	SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace Disjoint Finset Finset.partialOrder Finset.instOrderBot	lmarginal Finset.instUnion	—	MeasurePreserving.lintegral_map_equiv measurePreserving_piFinsetUnion lintegral_prod instSFiniteOfSigmaFinite Measure.pi.sigmaFinite Measurable.aemeasurable Measurable.comp measurable_updateFinset MeasurableEquiv.measurable Function.updateFinset_updateFinset
lmarginal_union' 📖	mathematical	SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace Disjoint Finset Finset.partialOrder Finset.instOrderBot	lmarginal Finset.instUnion	—	Finset.union_comm lmarginal_union Disjoint.symm
lmarginal_univ 📖	mathematical	SigmaFinite	lmarginal Finset.univ lintegral MeasurableSpace.pi Measure.pi	—	Finset.mem_univ MeasurePreserving.lintegral_map_equiv measurePreserving_piCongrLeft
lmarginal_update_of_mem 📖	mathematical	Finset Finset.instMembership	lmarginal Function.update	—	—
lmarginal_update_of_notMem 📖	mathematical	SigmaFinite Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace Finset Finset.instMembership	lmarginal Function.update	—	Finset.induction lmarginal_empty lmarginal_insert Measurable.comp measurable_update_left Finset.mem_insert_self lmarginal.congr_simp Function.update_comm Finset.mem_insert_of_mem

---

← Back to Index