Instances

📁 Source: Mathlib/MeasureTheory/MeasurableSpace/Instances.lean

Statistics

Metric	Count
Definitions instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace	12
Theorems instMeasurableSingletonClass, instDiscreteMeasurableSpace, instMeasurableSingletonClass, instMeasurableSingletonClass, instMeasurableSingletonClass, instDiscreteMeasurableSpace, instDiscreteMeasurableSpace, instMeasurableSingletonClass, instMeasurableSingletonClass, instMeasurableSingletonClass, measurableSingletonClass, instMeasurableSingletonClass	12
Total	24

Bool

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	20 math math: ProbabilityTheory.Kernel.instIsMarkovKernelBoolBoolKernelOfIsProbabilityMeasure, PMF.bernoulli_expectation, ProbabilityTheory.boolKernel_comp_measure, ProbabilityTheory.posterior_boolKernel_apply_true, ProbabilityTheory.Kernel.boolKernel_apply, instMeasurableSingletonClass, ProbabilityTheory.Kernel.eq_boolKernel, ProbabilityTheory.Kernel.boolKernel_false, ProbabilityTheory.posterior_boolKernel_apply_false, MeasurableSpace.measurableEquiv_nat_bool_of_countablyGenerated, ProbabilityTheory.Kernel.boolKernel_true, ProbabilityTheory.absolutelyContinuous_boolKernel_comp_right, MeasurableSpace.measurable_mapNatBool, ProbabilityTheory.Kernel.instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure, MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated, ProbabilityTheory.absolutelyContinuous_boolKernel_comp_left, borelSpace, ProbabilityTheory.Kernel.comp_boolKernel, measurable_to_bool, ProbabilityTheory.Kernel.instIsSFiniteKernelBoolBoolKernelOfSFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass instMeasurableSpace	—	—

ENat

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	4 math math: measurable_iff, measurable_encard, instDiscreteMeasurableSpace, instMeasurableSingletonClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteMeasurableSpace 📖	mathematical	—	DiscreteMeasurableSpace ENat instMeasurableSpace	—	—
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass ENat instMeasurableSpace	—	DiscreteMeasurableSpace.toMeasurableSingletonClass instDiscreteMeasurableSpace

Empty

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	1 math math: borelSpace

Fin

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	1 math math: instMeasurableSingletonClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass instMeasurableSpace	—	—

Int

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	8 math math: borelSpace, SubNegMonoid.measurableSMul_int₂, Measurable.ceil, measurable_floor, DivInvMonoid.measurableZPow, instMeasurableSingletonClass, measurable_ceil, Measurable.floor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass instMeasurableSpace	—	—

IterateAddAct

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	4 math math: instDiscreteMeasurableSpace, measurableVAdd_iterateAddAct, Measurable.measurableSMul₂_iterateAddAct, measurableSMul₂_iterateAddAct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteMeasurableSpace 📖	mathematical	—	DiscreteMeasurableSpace IterateAddAct instMeasurableSpace	—	instDiscreteMeasurableSpace

IterateMulAct

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	4 math math: measurableSMul₂_iterateMulAct, measurableSMul_iterateMulAct, instDiscreteMeasurableSpace, Measurable.measurableSMul₂_iterateMulAct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteMeasurableSpace 📖	mathematical	—	DiscreteMeasurableSpace IterateMulAct instMeasurableSpace	—	instDiscreteMeasurableSpace

Nat

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	23 math math: measurable_to_nat, measurable_floor, measurable_from_nat, ProbabilityTheory.stronglyMeasurable_geometricPMFReal, ProbabilityTheory.isProbabilityMeasurePoisson, measurable_ceil, ProbabilityTheory.stronglyMeasurable_poissonPMFReal, ProbabilityTheory.isProbabilityMeasure_geometricMeasure, ProbabilityTheory.measurable_poissonPMFReal, ProbabilityTheory.measurable_geometricPMFReal, MeasureTheory.StronglyAdapted.measurable_upcrossingsBefore, Measurable.nat_floor, measurable_findGreatest, Monoid.measurablePow, measurable_findGreatest', instMeasurableSingletonClass, ProbabilityTheory.isProbabilityMeasureGeometric, Measurable.nat_ceil, measurable_find, AddMonoid.measurableSMul_nat₂, borelSpace, MeasureTheory.measurableSet_spanningSetsIndex, measurable_ncard

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass instMeasurableSpace	—	—

PUnit

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	30 math math: ProbabilityTheory.Kernel.condKernelUnitBorel.instIsCondKernel, ProbabilityTheory.HasSubgaussianMGF_iff_kernel, MeasureTheory.Measure.condKernel_def, MeasureTheory.Measure.discard_comp, ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitReal, Unit.borelSpace, ProbabilityTheory.stieltjesOfMeasurableRat_unit_prod, ProbabilityTheory.Kernel.isSFiniteKernel_prodMkRight_unit, ProbabilityTheory.isRatCondKernelCDF_preCDF, ProbabilityTheory.Kernel.discard_apply, MeasureTheory.volume_preserving_pi_empty, ProbabilityTheory.Kernel.comp_discard, ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_unit, MeasureTheory.Measure.comp_eq_comp_const_apply, ProbabilityTheory.Kernel.comp_discard', ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prod, MeasureTheory.Measure.dirac_unit_compProd_const, ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitBorel, ProbabilityTheory.Kernel.condKernelUnitReal.instIsCondKernel, ProbabilityTheory.isRatCondKernelCDFAux_preCDF, MeasureTheory.Measure.snd_dirac_unit_compProd_const, ProbabilityTheory.isCondKernelCDF_condCDF, ProbabilityTheory.bayesRisk_discard, MeasureTheory.Measure.dirac_unit_compProd, MeasureTheory.measurePreserving_pi_empty, ProbabilityTheory.Kernel.discard_eq_const, MeasureTheory.Measure.condKernel_apply, MeasureTheory.Measure.tprod_nil, ProbabilityTheory.Kernel.instIsMarkovKernelUnitDiscard, measurable_unit

Prop

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	24 math math: MeasurableSet.mem, measurableSet_setOf, measurable_lt, measurable_mem, Measurable.subset, Measurable.eq, ProbabilityTheory.setBernoulli_apply', Measurable.const_eq, measurable_setOf, measurable_set_iff, measurable_to_prop, measurable_le, measurable_set_mem, measurable_set_notMem, MeasurableEquiv.coe_setOf, MeasurableEquiv.setOf_symm_apply, Measurable.le', Measurable.eq_const, MeasurableEquiv.setOf_apply, ProbabilityTheory.setBernoulli_apply, instMeasurableSingletonClass, MeasurableSpace.comap_not, Measurable.lt, ProbabilityTheory.setBernoulli_eq_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass instMeasurableSpace	—	—

Rat

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	2 math math: borelSpace, instMeasurableSingletonClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass instMeasurableSpace	—	—

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass	—	MeasurableSet.univ

ZMod

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	2 math math: instMeasurableSingletonClass, dft_eq_fourier

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass ZMod instMeasurableSpace	—	—

---

← Back to Index