GiryMonad

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

Statistics

Metric	Count
Definitions bind, instMeasurableSpace, join	3
Theorems ae_of_bind, ae_of_join, measure_of_isPiSystem, measure_of_isPiSystem_of_isProbabilityMeasure, smul_measure, ae_ae_of_ae_bind, ae_ae_of_ae_join, aemeasurable_bind, aemeasurable_lintegral, bind_apply, bind_apply_le, bind_bind, bind_congr_right, bind_const, bind_dirac, bind_dirac_eq_map, bind_smul, bind_sum, bind_zero_left, bind_zero_right, bind_zero_right', dirac_bind, instMeasurableAdd₂, join_apply, join_dirac, join_eq_bind, join_map_dirac, join_map_join, join_map_map, join_smul, join_sum, join_zero, le_ae_join, le_join_apply, lintegral_bind, lintegral_bind_le, lintegral_join, lintegral_join_le, measurable_bind', measurable_coe, measurable_dirac, measurable_join, measurable_lintegral, measurable_map, measurable_measure, measurable_of_measurable_coe	46
Total	49

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_of_bind 📖	mathematical	AEMeasurable MeasureTheory.Measure MeasureTheory.Measure.instMeasurableSpace MeasureTheory.Measure.bind	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.ae_of_ae_map ae_of_join
ae_of_join 📖	mathematical	AEMeasurable MeasureTheory.Measure.join	Filter.Eventually MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instMeasurableSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass Filter.Eventually.mono MeasureTheory.Measure.ae_ae_of_ae_join

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_of_isPiSystem 📖	mathematical	MeasureTheory.IsFiniteMeasure MeasurableSpace.generateFrom IsPiSystem Measurable ENNReal ENNReal.measurableSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.univ	MeasureTheory.Measure.instMeasurableSpace	—	MeasureTheory.Measure.measurable_measure MeasurableSpace.induction_on_inter MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.measure_compl MeasureTheory.measure_ne_top sub ENNReal.instMeasurableSub₂ MeasureTheory.measure_iUnion instCountableNat ennreal_tsum
measure_of_isPiSystem_of_isProbabilityMeasure 📖	mathematical	MeasureTheory.IsProbabilityMeasure MeasurableSpace.generateFrom IsPiSystem Measurable ENNReal ENNReal.measurableSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike	MeasureTheory.Measure.instMeasurableSpace	—	measure_of_isPiSystem MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.IsProbabilityMeasure.measure_univ
smul_measure 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.Measure MeasureTheory.Measure.instMeasurableSpace MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	MeasureTheory.Measure.measurable_of_measurable_coe IsScalarTower.right mul_const MeasurableMul₂.toMeasurableMul ENNReal.instMeasurableMul₂

MeasureTheory.Measure

Definitions

Name	Category	Theorems
bind 📖	CompOp	87 math math: bind_apply, ProbabilityTheory.absolutelyContinuous_posterior_iff, swap_comp, dirac_bind, comp_apply_univ, comp_add, ProbabilityTheory.boolKernel_comp_measure, bind_congr_right, comp_compProd_comm, ProbabilityTheory.compProd_posterior_eq_map_swap, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim, ProbabilityTheory.condExpKernel_comp_trim, map_comp, const_comp, ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_add_compProd, ProbabilityTheory.Kernel.HasSubgaussianMGF.memLp_exp_mul, AbsolutelyContinuous.comp_left, ProbabilityTheory.posterior_boolKernel_apply_true, add_comp, comp_eq_sum_of_countable, discard_comp, snd_compProd, AbsolutelyContinuous.comp_right, AbsolutelyContinuous.comp, ProbabilityTheory.Kernel.Invariant.def, ProbabilityTheory.Kernel.absolutelyContinuous_comp_of_absolutelyContinuous, instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel, ProbabilityTheory.condDistrib_comp_map, absolutelyContinuous_comp_of_countable, ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul, add_comp', bind_apply_le, ProbabilityTheory.posterior_prod_id_comp, compProd_id_eq_copy_comp, ProbabilityTheory.Kernel.comp_apply, parallelComp_comp_compProd, bind_zero_right, comp_eq_comp_const_apply, ProbabilityTheory.Kernel.comp_const, comp_congr, compProd_eq_comp_prod, measurable_bind', bind_dirac_eq_map, ae_comp_iff, join_eq_bind, bind_smul, deterministic_comp_eq_map, bind_sum, lintegral_bind_le, bind_dirac, ProbabilityTheory.parallelProd_posterior_comp_copy_comp, MeasureTheory.isProbabilityMeasure_bind, ProbabilityTheory.posterior_boolKernel_apply_false, ae_comp_of_ae_ae, ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_comp, ProbabilityTheory.swap_compProd_posterior, ProbabilityTheory.avgRisk_const_left, comp_assoc, instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel, ProbabilityTheory.avgRisk_const_left', id_comp, prod_comp_left, comp_smul, ProbabilityTheory.absolutelyContinuous_boolKernel_comp_right, ProbabilityTheory.posterior_posterior, prod_comp_right, ProbabilityTheory.posterior_comp_self, ProbabilityTheory.posterior_eq_withDensity_of_countable, copy_comp_map, ProbabilityTheory.absolutelyContinuous_posterior, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero', instSFiniteBindCoeKernelOfIsSFiniteKernel, bind_zero_right', prod_def, ProbabilityTheory.absolutelyContinuous_boolKernel_comp_left, ProbabilityTheory.compProd_posterior_eq_swap_comp, prodMkLeft_comp_compProd, bind_zero_left, instIsZeroOrProbabilityMeasureBindCoeKernelOfIsZeroOrMarkovKernel, ProbabilityTheory.Kernel.HasSubgaussianMGF.aestronglyMeasurable, compProd_eq_parallelComp_comp_copy_comp, ProbabilityTheory.Kernel.comp_boolKernel, aemeasurable_bind, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable, bind_const, ProbabilityTheory.posterior_comp, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib
instMeasurableSpace 📖	CompOp	42 math math: join_smul, measurable_measure, le_ae_join, instMeasurableAdd₂, measurable_coe, aemeasurable_lintegral, MeasureTheory.ProbabilityMeasure.measurable_fun_prod, measurable_map, join_sum, join_map_map, StieltjesFunction.measurable_measure, ProbabilityTheory.Kernel.aemeasurable, AEMeasurable.ae_of_join, ProbabilityTheory.Kernel.measurable_trajFun, ProbabilityTheory.measurable_measure_stieltjesOfMeasurableRat, join_dirac, join_eq_bind, join_map_dirac, measurable_dirac, Measurable.smul_measure, Measurable.measure_of_isPiSystem, lintegral_join_le, Measurable.map_prodMk_right, le_join_apply, ProbabilityTheory.Kernel.measurable, ProbabilityTheory.measurable_measure_condCDF, ae_ae_of_ae_join, measurable_lintegral, join_apply, ProbabilityTheory.IsMeasurableRatCDF.measurable_measure_stieltjesFunction, lintegral_join, ProbabilityTheory.Kernel.measurable_singularPart, measurable_of_measurable_coe, ProbabilityTheory.Kernel.measurable', MeasureTheory.ProbabilityMeasure.measurableSet_isProbabilityMeasure, join_zero, MeasureTheory.FiniteMeasure.measurableSet_isFiniteMeasure, MeasureTheory.FiniteMeasure.measurable_fun_prod, Measurable.measure_of_isPiSystem_of_isProbabilityMeasure, Measurable.map_prodMk_left, join_map_join, measurable_join
join 📖	CompOp	14 math math: join_smul, le_ae_join, join_sum, join_map_map, join_dirac, join_eq_bind, join_map_dirac, lintegral_join_le, le_join_apply, join_apply, MeasureTheory.isProbabilityMeasure_join, join_zero, join_map_join, measurable_join

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_ae_of_ae_bind 📖	—	AEMeasurable MeasureTheory.Measure instMeasurableSpace Filter.Eventually MeasureTheory.ae instFunLike instOuterMeasureClass bind	—	—	instOuterMeasureClass MeasureTheory.ae_of_ae_map ae_ae_of_ae_join
ae_ae_of_ae_join 📖	mathematical	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass join	instMeasurableSpace	—	instOuterMeasureClass le_ae_join
aemeasurable_bind 📖	mathematical	AEMeasurable MeasureTheory.Measure instMeasurableSpace join	bind	—	instOuterMeasureClass measurable_bind' Filter.Eventually.mono ae_ae_of_ae_join bind_congr_right
aemeasurable_lintegral 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace join	MeasureTheory.Measure instMeasurableSpace MeasureTheory.lintegral	—	instOuterMeasureClass measurable_lintegral Filter.Eventually.mono ae_ae_of_ae_join MeasureTheory.lintegral_congr_ae
bind_apply 📖	mathematical	MeasurableSet AEMeasurable MeasureTheory.Measure instMeasurableSpace	DFunLike.coe Set ENNReal instFunLike bind MeasureTheory.lintegral	—	bind.eq_1 join_apply MeasureTheory.lintegral_map' Measurable.aemeasurable measurable_coe
bind_apply_le 📖	mathematical	MeasurableSet	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike bind MeasureTheory.lintegral	—	bind.eq_1 join_apply MeasureTheory.lintegral_map_le
bind_bind 📖	—	AEMeasurable MeasureTheory.Measure instMeasurableSpace bind	—	—	ext bind_apply lintegral_bind Measurable.comp_aemeasurable measurable_coe AEMeasurable.comp_aemeasurable aemeasurable_bind MeasureTheory.lintegral_congr_ae Filter.Eventually.mono instOuterMeasureClass AEMeasurable.ae_of_bind
bind_congr_right 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae instFunLike instOuterMeasureClass	bind	—	instOuterMeasureClass map_congr
bind_const 📖	mathematical	—	bind ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set instFunLike Set.univ	—	IsScalarTower.right map_const join_smul join_dirac
bind_dirac 📖	mathematical	—	bind dirac	—	ext bind_apply Measurable.aemeasurable measurable_dirac dirac_apply' MeasureTheory.lintegral_indicator MeasureTheory.lintegral_one restrict_apply Set.univ_inter
bind_dirac_eq_map 📖	mathematical	Measurable	bind dirac map	—	bind_dirac bind.eq_1 map_map measurable_dirac
bind_smul 📖	mathematical	—	bind MeasureTheory.Measure instSMul	—	map_smul join_smul
bind_sum 📖	mathematical	AEMeasurable MeasureTheory.Measure instMeasurableSpace sum	bind	—	map_sum join_sum
bind_zero_left 📖	mathematical	—	bind MeasureTheory.Measure instZero	—	map_zero join_zero
bind_zero_right 📖	mathematical	—	bind Pi.instZero MeasureTheory.Measure instZero	—	bind_zero_right'
bind_zero_right' 📖	mathematical	—	bind MeasureTheory.Measure instZero	—	IsScalarTower.right bind_const smul_zero
dirac_bind 📖	mathematical	Measurable MeasureTheory.Measure instMeasurableSpace	bind dirac	—	map_dirac join_dirac
instMeasurableAdd₂ 📖	mathematical	—	MeasurableAdd₂ MeasureTheory.Measure instMeasurableSpace instAdd	—	measurable_of_measurable_coe Measurable.add ContinuousAdd.measurableMul₂ ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instContinuousAdd Measurable.comp measurable_coe measurable_fst measurable_snd
join_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike join MeasureTheory.lintegral instMeasurableSpace	—	ofMeasurable_apply
join_dirac 📖	mathematical	—	join dirac MeasureTheory.Measure instMeasurableSpace	—	ext join_apply MeasureTheory.lintegral_dirac'
join_eq_bind 📖	mathematical	—	join bind MeasureTheory.Measure instMeasurableSpace	—	bind.eq_1 map_id
join_map_dirac 📖	mathematical	—	join map MeasureTheory.Measure instMeasurableSpace dirac	—	bind_dirac
join_map_join 📖	mathematical	—	join map MeasureTheory.Measure instMeasurableSpace	—	join_eq_bind bind_bind aemeasurable_id
join_map_map 📖	mathematical	Measurable	join map MeasureTheory.Measure instMeasurableSpace	—	ext join_apply map_apply MeasureTheory.lintegral_map measurable_coe measurable_map
join_smul 📖	mathematical	—	join MeasureTheory.Measure instMeasurableSpace instSMul	—	ext join_apply MeasureTheory.lintegral_smul_measure
join_sum 📖	mathematical	—	join sum MeasureTheory.Measure instMeasurableSpace	—	ext sum_apply join_apply MeasureTheory.lintegral_sum_measure
join_zero 📖	mathematical	—	join MeasureTheory.Measure instMeasurableSpace instZero	—	ext join_apply MeasureTheory.lintegral_zero_measure
le_ae_join 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.bind MeasureTheory.Measure MeasureTheory.ae instMeasurableSpace instFunLike instOuterMeasureClass join	—	instOuterMeasureClass MeasureTheory.exists_measurable_superset_of_null Filter.mem_bind' Filter.Eventually.mono MeasureTheory.lintegral_eq_zero_iff measurable_coe join_apply MeasureTheory.measure_mono_null
le_join_apply 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral MeasureTheory.Measure instMeasurableSpace DFunLike.coe Set instFunLike join	—	MeasureTheory.measure_eq_iInf le_iInf₂ le_iInf MeasureTheory.lintegral_mono_fn' le_refl MeasureTheory.measure_mono instOuterMeasureClass join_apply
lintegral_bind 📖	mathematical	AEMeasurable MeasureTheory.Measure instMeasurableSpace ENNReal ENNReal.measurableSpace bind	MeasureTheory.lintegral	—	lintegral_join MeasureTheory.lintegral_map' aemeasurable_lintegral
lintegral_bind_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral bind	—	LE.le.trans lintegral_join_le MeasureTheory.lintegral_map_le
lintegral_join 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace join	MeasureTheory.lintegral MeasureTheory.Measure instMeasurableSpace	—	MeasureTheory.lintegral_eq_iSup_eapprox_lintegral Finset.sum_congr join_apply MeasureTheory.SimpleFunc.measurableSet_preimage MeasureTheory.lintegral_iSup Finset.measurable_sum ContinuousAdd.measurableMul₂ ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instContinuousAdd Measurable.const_mul MeasurableMul₂.toMeasurableMul ENNReal.instMeasurableMul₂ MeasureTheory.lintegral_finset_sum MeasureTheory.lintegral_const_mul measurable_coe MeasureTheory.SimpleFunc.lintegral_mono MeasureTheory.SimpleFunc.monotone_eapprox le_rfl instOuterMeasureClass MeasureTheory.lintegral_congr_ae Measurable.aemeasurable Filter.Eventually.mono ae_ae_of_ae_join
lintegral_join_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral join MeasureTheory.Measure instMeasurableSpace	—	MeasureTheory.exists_measurable_le_lintegral_eq lintegral_join Measurable.aemeasurable MeasureTheory.lintegral_mono_fn' le_refl
measurable_bind' 📖	mathematical	Measurable MeasureTheory.Measure instMeasurableSpace	bind	—	Measurable.comp measurable_join measurable_map
measurable_coe 📖	mathematical	MeasurableSet	Measurable MeasureTheory.Measure ENNReal instMeasurableSpace ENNReal.measurableSpace DFunLike.coe Set instFunLike	—	Measurable.of_comap_le le_iSup_of_le le_rfl
measurable_dirac 📖	mathematical	—	Measurable MeasureTheory.Measure instMeasurableSpace dirac	—	measurable_of_measurable_coe dirac_apply' Measurable.indicator measurable_one
measurable_join 📖	mathematical	—	Measurable MeasureTheory.Measure instMeasurableSpace join	—	measurable_of_measurable_coe join_apply measurable_lintegral measurable_coe
measurable_lintegral 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.Measure instMeasurableSpace MeasureTheory.lintegral	—	MeasureTheory.lintegral_eq_iSup_eapprox_lintegral Measurable.iSup ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology instCountableNat Finset.measurable_fun_sum ContinuousAdd.measurableMul₂ ENNReal.instContinuousAdd Measurable.const_mul MeasurableMul₂.toMeasurableMul ENNReal.instMeasurableMul₂ measurable_coe MeasureTheory.SimpleFunc.measurableSet_preimage
measurable_map 📖	mathematical	Measurable	MeasureTheory.Measure instMeasurableSpace map	—	measurable_of_measurable_coe map_apply measurable_coe
measurable_measure 📖	mathematical	—	Measurable MeasureTheory.Measure instMeasurableSpace ENNReal ENNReal.measurableSpace DFunLike.coe Set instFunLike	—	Measurable.comp measurable_coe measurable_of_measurable_coe
measurable_of_measurable_coe 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace DFunLike.coe MeasureTheory.Measure Set instFunLike	instMeasurableSpace	—	Measurable.of_le_map iSup₂_le MeasurableSpace.comap_le_iff_le_map MeasurableSpace.map_comp

---

← Back to Index