Comp

📁 Source: Mathlib/Probability/Kernel/Composition/Comp.lean

Statistics

Metric	Count
Definitions Comp, Comp, Comp, comp, instMonoid, «term_∘ₖ_», Comp	7
Theorems comp, comp, comp, comp, ae_ae_of_ae_comp, ae_comp_iff, ae_comp_of_ae_ae, ae_lt_top_of_comp_ne_top, ae_null_of_comp_null, comp_add_left, comp_add_right, comp_apply, comp_apply', comp_apply_univ_le, comp_assoc, comp_discard, comp_discard', comp_id, comp_null, comp_restrict, comp_sum_left, comp_sum_right, comp_zero, const_comp, const_comp', id_comp, lintegral_comp, pow_add, pow_add_apply_eq_lintegral, pow_succ_apply_eq_lintegral, swap_copy, zero_comp	32
Total	39

Functor

Definitions

Name	Category	Theorems
Comp 📖	CompOp	32 math math: Comp.run_seq, LawfulBitraversable.comp_bitraverse, Bitraversable.tfst_comp_tfst, LawfulTraversable.comp_traverse, Comp.map_pure, Comp.seq_pure, Bitraversable.tsnd_comp_tfst, Bitraversable.tfst_tsnd, Multiset.comp_traverse, Bitraversable.comp_tsnd, Comp.pure_seq_eq_map, Equiv.comp_traverse, Traversable.comp_sequence, Sum.comp_traverse, Comp.instCommApplicative, Bitraversable.tsnd_comp_tsnd, Option.comp_traverse, LawfulBitraversable.bitraverse_comp, Bitraversable.tfst_comp_tsnd, List.comp_traverse, Comp.run_pure, Bitraversable.tsnd_tfst, Comp.run_map, Traversable.traverse_comp, Comp.seq_assoc, List.Vector.comp_traverse, Bitraversable.comp_tfst, Comp.instLawfulApplicativeComp, Comp.seq_mk, Comp.map_mk, Comp.lawfulFunctor, Tree.comp_traverse

Mathlib.Tactic.Linarith

Definitions

Name	Category	Theorems
Comp 📖	CompData	—

MvQPF

Definitions

Name	Category	Theorems
Comp 📖	CompOp	2 math math: Comp.get_map, Comp.map_mk

ProbabilityTheory

Definitions

Name	Category	Theorems
«term_∘ₖ_» 📖	CompOp	—

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
comp 📖	CompOp	73 math math: parallelComp_comp_parallelComp, parallelComp_comp_prod, partialTraj_succ_of_le, comp_assoc, swap_swap, partialTraj_comp_partialTraj', parallelComp_comm, deterministic_comp_eq_map, const_comp', fst_comp, pow_add, snd_comp, IsSFiniteKernel.comp, partialTraj_comp_partialTraj'', swap_prod, comp_eq_snd_compProd, zero_comp, ProbabilityTheory.avgRisk_le_iSup_risk, prod_const_comp, snd_compProd_prodMkLeft, prod_prodMkRight_comp_deterministic_prod, deterministic_comp_deterministic, comp_zero, partialTraj_succ_eq_comp, partialTraj_le_def, ae_comp_iff, comp_discard, traj_comp_partialTraj, comp_sum_left, compProd_prodMkLeft_eq_comp, comp_apply, MeasureTheory.Measure.parallelComp_comp_compProd, parallelComp_id_right_comp_parallelComp, MeasureTheory.Measure.comp_eq_comp_const_apply, comp_discard', swap_copy, IsMarkovKernel.comp, comp_const, parallelComp_comp_copy, swap_comp_eq_map, deterministic_comp_copy, ProbabilityTheory.hasFiniteIntegral_comp_iff, partialTraj_comp_partialTraj, ProbabilityTheory.bayesRisk_le_bayesRisk_comp, const_prod_comp, continuous_integral_integral_comp, map_comp, comp_restrict, comp_map, MeasureTheory.Measure.comp_assoc, comp_sum_right, prod_prodMkLeft_comp_prod_deterministic, IsZeroOrMarkovKernel.comp, compProd_def, id_comp, lintegral_comp, ae_comp_of_ae_ae, Invariant.comp, comp_apply', comp_add_right, IsFiniteKernel.comp, comp_id, comp_deterministic_eq_comap, comp_apply_univ_le, comp_add_left, swap_parallelComp, const_comp, comp_boolKernel, Invariant.comp_const, comp_null, parallelComp_id_left_comp_parallelComp, ProbabilityTheory.deterministic_comp_posterior, ProbabilityTheory.posterior_comp
instMonoid 📖	CompOp	5 math math: pow_add, isIrreducible_iff, pow_add_apply_eq_lintegral, IsIrreducible.irreducible, pow_succ_apply_eq_lintegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_ae_of_ae_comp 📖	—	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike comp	—	—	MeasureTheory.Measure.instOuterMeasureClass ae_null_of_comp_null
ae_comp_iff 📖	mathematical	MeasurableSet setOf	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike comp	—	MeasureTheory.Measure.instOuterMeasureClass ae_ae_of_ae_comp ae_comp_of_ae_ae
ae_comp_of_ae_ae 📖	mathematical	MeasurableSet setOf Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	comp	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_iff comp_null MeasurableSet.compl
ae_lt_top_of_comp_ne_top 📖	mathematical	—	Filter.Eventually ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Top.top instTopENNReal MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_lt_top measurable_coe MeasureTheory.measurableSet_toMeasurable comp_apply' MeasureTheory.measure_toMeasurable Filter.mp_mem Filter.univ_mem' LE.le.trans_lt MeasureTheory.measure_mono MeasureTheory.subset_toMeasurable
ae_null_of_comp_null 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike comp instZeroENNReal	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass Pi.instZero	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.exists_measurable_superset_of_null Filter.eventuallyLE_antisymm_iff Filter.EventuallyLE.trans_eq MeasureTheory.ae_of_all MeasureTheory.measure_mono comp_null zero_le ENNReal.instCanonicallyOrderedAdd
comp_add_left 📖	mathematical	—	comp ProbabilityTheory.Kernel instAdd	—	ext MeasureTheory.Measure.ext comp_apply' MeasureTheory.lintegral_add_left measurable_coe
comp_add_right 📖	mathematical	—	comp ProbabilityTheory.Kernel instAdd	—	ext MeasureTheory.Measure.ext comp_apply' MeasureTheory.lintegral_add_measure
comp_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike comp MeasureTheory.Measure.bind	—	—
comp_apply' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike comp MeasureTheory.lintegral	—	comp_apply MeasureTheory.Measure.bind_apply aemeasurable
comp_apply_univ_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike comp Set.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring bound	—	comp_apply' MeasurableSet.univ MeasureTheory.lintegral_mono measure_le_bound MeasureTheory.lintegral_const mul_comm
comp_assoc 📖	mathematical	—	comp	—	ext_fun lintegral_comp Measurable.lintegral_kernel
comp_discard 📖	mathematical	—	comp PUnit.instMeasurableSpace discard	—	ext MeasureTheory.Measure.ext IsScalarTower.right Measurable.smul_measure measurable_coe MeasurableSet.univ MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' one_smul comp_discard' MeasureTheory.Measure.dirac_apply' discard_apply
comp_discard' 📖	mathematical	—	comp PUnit.instMeasurableSpace discard ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Set.univ MeasureTheory.Measure.dirac Measurable.smul_measure measurable_coe MeasurableSet.univ	—	ext IsScalarTower.right Measurable.smul_measure measurable_coe MeasurableSet.univ MeasureTheory.Measure.ext comp_apply' discard_apply MeasureTheory.Measure.dirac_apply' MeasureTheory.lintegral_const mul_comm
comp_id 📖	mathematical	—	comp id	—	ext MeasureTheory.Measure.ext comp_apply' id_apply MeasureTheory.lintegral_dirac' measurable_coe
comp_null 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike comp instZeroENNReal Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass Pi.instZero	—	MeasureTheory.Measure.instOuterMeasureClass comp_apply' MeasureTheory.lintegral_eq_zero_iff measurable_coe
comp_restrict 📖	mathematical	MeasurableSet	comp restrict	—	ext MeasureTheory.Measure.ext comp_apply' restrict_apply' MeasurableSet.inter
comp_sum_left 📖	mathematical	—	comp sum	—	ext MeasureTheory.Measure.ext comp_apply' MeasureTheory.Measure.sum_apply MeasureTheory.lintegral_tsum Measurable.aemeasurable measurable_coe
comp_sum_right 📖	mathematical	—	comp sum	—	ext MeasureTheory.Measure.ext comp_apply' MeasureTheory.Measure.sum_apply MeasureTheory.lintegral_sum_measure
comp_zero 📖	mathematical	—	comp ProbabilityTheory.Kernel instZero	—	ext MeasureTheory.Measure.ext MeasureTheory.Measure.bind_zero_left
const_comp 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike comp const ENNReal MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Set MeasureTheory.Measure.instFunLike Set.univ	—	IsScalarTower.right MeasureTheory.Measure.ext comp_apply' MeasureTheory.lintegral_const mul_comm
const_comp' 📖	mathematical	—	comp const	—	ext MeasureTheory.Measure.ext IsScalarTower.right const_comp MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' one_smul
id_comp 📖	mathematical	—	comp id	—	ext MeasureTheory.Measure.ext comp_apply' id_apply MeasureTheory.Measure.dirac_apply' MeasureTheory.lintegral_indicator_one
lintegral_comp 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike comp	—	comp_apply MeasureTheory.Measure.lintegral_bind aemeasurable Measurable.aemeasurable
pow_add 📖	mathematical	—	ProbabilityTheory.Kernel Monoid.toNatPow instMonoid comp	—	pow_add
pow_add_apply_eq_lintegral 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Monoid.toNatPow instMonoid MeasureTheory.lintegral	—	add_comm pow_add comp_apply'
pow_succ_apply_eq_lintegral 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Monoid.toNatPow instMonoid MeasureTheory.lintegral	—	pow_one pow_add_apply_eq_lintegral
swap_copy 📖	mathematical	—	comp Prod.instMeasurableSpace swap copy	—	ext MeasureTheory.Measure.ext comp_apply copy_apply MeasureTheory.Measure.dirac_bind measurable swap_apply' MeasureTheory.Measure.dirac_apply'
zero_comp 📖	mathematical	—	comp ProbabilityTheory.Kernel instZero	—	ext MeasureTheory.Measure.ext MeasureTheory.Measure.bind_zero_right

ProbabilityTheory.Kernel.IsFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel.comp	—	ENNReal.mul_lt_top ProbabilityTheory.Kernel.bound_lt_top ProbabilityTheory.Kernel.comp_apply_univ_le mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid ProbabilityTheory.Kernel.measure_le_bound

ProbabilityTheory.Kernel.IsMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel.comp	—	ProbabilityTheory.Kernel.comp_apply MeasureTheory.Measure.bind_apply MeasurableSet.univ ProbabilityTheory.Kernel.aemeasurable MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' MeasureTheory.lintegral_const mul_one

ProbabilityTheory.Kernel.IsSFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel.comp	—	instCountableNat ProbabilityTheory.Kernel.kernel_sum_seq ProbabilityTheory.Kernel.comp_sum_left ProbabilityTheory.Kernel.sum.congr_simp ProbabilityTheory.Kernel.comp_sum_right ProbabilityTheory.Kernel.isSFiniteKernel_sum ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.Kernel.IsFiniteKernel.comp ProbabilityTheory.Kernel.isFiniteKernel_seq

ProbabilityTheory.Kernel.IsZeroOrMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.comp	—	ProbabilityTheory.eq_zero_or_isMarkovKernel ProbabilityTheory.Kernel.comp_zero ProbabilityTheory.instIsZeroOrMarkovKernelOfNatKernel ProbabilityTheory.Kernel.zero_comp ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.IsMarkovKernel.comp

Relation

Definitions

Name	Category	Theorems
Comp 📖	MathDef	12 math math: List.perm_comp_perm, comp_iff, eq_comp, List.perm_comp_forall₂, flip_comp, comp_eq, List.forall₂_comp_perm_eq_perm_comp_forall₂, fun_eq_comp, List.eq_map_comp_perm, comp_eq_fun, iff_comp, comp_assoc

---

← Back to Index