Dirac

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

Statistics

Metric	Count
Definitions dirac, instMeasureSpacePUnit	2
Theorems ae_eq_or_eq_iff_eq_dirac_add_dirac, ae_eq_or_eq_iff_map_eq_dirac_add_dirac, ae_mem_finset_iff, ae_mem_finset_iff_map_eq_sum_dirac, instIsFiniteMeasure, instSigmaFinite, isProbabilityMeasure, dirac_apply, dirac_apply', dirac_apply_eq_zero_or_one, dirac_apply_ne_one_iff_eq_zero, dirac_apply_ne_zero_iff_eq_one, dirac_apply_of_mem, dirac_ne_zero, exists_sum_smul_dirac, ext_iff_singleton, ext_of_singleton, le_dirac_apply, map_const, map_dirac, map_eq_sum, restrict_singleton, sum_smul_dirac, tsum_indicator_apply_singleton, ae_dirac_eq, ae_dirac_iff, ae_eq_dirac, ae_eq_dirac', aemeasurable_dirac, dirac_eq_dirac_iff, dirac_eq_dirac_iff_forall_mem_iff_mem, dirac_eq_one_iff_mem, dirac_eq_zero_iff_not_mem, dirac_ne_dirac, dirac_ne_dirac_iff, dirac_ne_dirac_iff_exists_measurableSet, ext_iff_measureReal_singleton, injective_dirac, instNonemptySubtypeMeasureIsProbabilityMeasure, mem_ae_dirac_iff, mutuallySingular_dirac, restrict_dirac, restrict_dirac'	43
Total	45

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_dirac_eq 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.dirac Filter Filter.instPure	—	Filter.ext Measure.instOuterMeasureClass Measure.dirac_apply NeZero.charZero_one ENNReal.instCharZero
ae_dirac_iff 📖	mathematical	MeasurableSet setOf	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.dirac	—	mem_ae_dirac_iff
ae_eq_dirac 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.dirac	—	Measure.instOuterMeasureClass ae_dirac_eq
ae_eq_dirac' 📖	mathematical	Measurable	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.dirac	—	Measure.instOuterMeasureClass ae_dirac_iff MeasurableSingletonClass.measurableSet_singleton
aemeasurable_dirac 📖	mathematical	—	AEMeasurable Measure.dirac	—	Measure.instOuterMeasureClass measurable_const ae_eq_dirac
dirac_eq_dirac_iff 📖	mathematical	—	Measure.dirac	—	not_iff_not dirac_ne_dirac_iff
dirac_eq_dirac_iff_forall_mem_iff_mem 📖	mathematical	—	Measure.dirac Set Set.instMembership	—	Set.indicator_of_mem Measure.dirac_apply' Set.indicator_of_notMem NeZero.charZero_one ENNReal.instCharZero Measure.ext
dirac_eq_one_iff_mem 📖	mathematical	MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.dirac AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Set.instMembership	—	prob_compl_eq_zero_iff Measure.dirac.isProbabilityMeasure Measure.instOuterMeasureClass mem_ae_iff mem_ae_dirac_iff
dirac_eq_zero_iff_not_mem 📖	mathematical	MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.dirac instZeroENNReal Set.instMembership	—	compl_compl Measure.instOuterMeasureClass mem_ae_iff Set.notMem_compl_iff mem_ae_dirac_iff MeasurableSet.compl_iff
dirac_ne_dirac 📖	—	—	—	—	MeasurableSpace.exists_measurableSet_of_ne dirac_ne_dirac_iff_exists_measurableSet
dirac_ne_dirac_iff 📖	—	—	—	—	dirac_ne_dirac
dirac_ne_dirac_iff_exists_measurableSet 📖	mathematical	—	MeasurableSet Set Set.instMembership	—	not_iff_not MeasurableSet.compl_iff
ext_iff_measureReal_singleton 📖	mathematical	—	Measure.real Set Set.instSingletonSet	—	Measure.ext_iff_singleton measureReal_def ENNReal.toReal_eq_toReal_iff
injective_dirac 📖	mathematical	—	Measure Measure.dirac	—	dirac_eq_dirac_iff
instNonemptySubtypeMeasureIsProbabilityMeasure 📖	mathematical	—	Measure IsProbabilityMeasure	—	Measure.dirac.isProbabilityMeasure
mem_ae_dirac_iff 📖	mathematical	MeasurableSet	Set Filter Filter.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.dirac Set.instMembership	—	Measure.instOuterMeasureClass Measure.dirac_apply' MeasurableSet.compl Set.indicator_of_notMem Set.indicator_of_mem NeZero.charZero_one ENNReal.instCharZero
mutuallySingular_dirac 📖	mathematical	—	Measure.MutuallySingular Measure.dirac	—	MeasurableSet.compl MeasurableSet.singleton Measure.dirac_apply' Set.indicator_of_notMem compl_compl NoAtoms.measure_singleton
restrict_dirac 📖	mathematical	—	Measure.restrict Measure.dirac Measure Set Set.instMembership Measure.instZero	—	Measure.restrict_eq_self_of_ae_mem Measure.instOuterMeasureClass ae_dirac_eq Measure.restrict_eq_zero Measure.dirac_apply Set.indicator_of_notMem
restrict_dirac' 📖	mathematical	MeasurableSet	Measure.restrict Measure.dirac Measure Set Set.instMembership Measure.instZero	—	Measure.restrict_eq_self_of_ae_mem Measure.instOuterMeasureClass ae_dirac_iff Measure.restrict_eq_zero Measure.dirac_apply' Set.indicator_of_notMem

MeasureTheory.Measure

Definitions

Name	Category	Theorems
dirac 📖	CompOp	105 math math: MeasureTheory.mutuallySingular_dirac, restrict_singleton, MeasureTheory.restrict_dirac', dirac_bind, MeasureTheory.integrable_dirac', ae_mem_finset_iff, dirac_conv_dirac, ProbabilityTheory.HasSubgaussianMGF_iff_kernel, pi_of_empty, sum_smul_dirac, ae_mem_finset_iff_map_eq_sum_dirac, ProbabilityTheory.gaussianReal_zero_var, MeasureTheory.setIntegral_dirac, dirac_conv, ProbabilityTheory.Kernel.swap_apply, discard_comp, ProbabilityTheory.setBernoulli_one, MeasureTheory.injective_dirac, PMF.toPMF_dirac, MeasureTheory.lintegral_dirac', MeasureTheory.restrict_dirac, ProbabilityTheory.setBernoulli_apply', MeasureTheory.mem_ae_dirac_iff, dirac_apply', ProbabilityTheory.Kernel.deterministic_apply, ae_eq_or_eq_iff_map_eq_dirac_add_dirac, ProbabilityTheory.Kernel.copy_apply, MeasureTheory.lintegral_dirac, mconv_dirac_one, ProbabilityTheory.Kernel.discard_apply, map_eq_sum, dirac_mconv_dirac, MeasureTheory.dirac_eq_zero_iff_not_mem, ProbabilityTheory.instIsGaussianDirac, MeasureTheory.dirac_eq_one_iff_mem, MeasureTheory.ae_dirac_iff, ProbabilityTheory.IsGaussian.eq_dirac_of_variance_eq_zero, ae_eq_or_eq_iff_eq_dirac_add_dirac, ProbabilityTheory.Kernel.comp_discard', MeasureTheory.integral_dirac, volume_pi_eq_dirac, MeasureTheory.ae_eq_dirac', MeasureTheory.dirac_eq_dirac_iff, dirac_prod_dirac, ProbabilityTheory.setBernoulli_zero, dirac_unit_compProd_const, Probability.cauchyMeasure_zero_scale, bind_dirac_eq_map, dirac.isProbabilityMeasure, join_dirac, MeasureTheory.count_withDensity, infinitePi_dirac, exists_sum_smul_dirac, dirac_prod, dirac_one_mconv, dirac_apply_ne_zero_iff_eq_one, join_map_dirac, MeasureTheory.ae_eq_dirac, MeasureTheory.count_withDensity', dirac_apply_eq_zero_or_one, MeasureTheory.setLIntegral_dirac', dirac_apply_ne_one_iff_eq_zero, measurable_dirac, prod_dirac, dirac_apply_of_mem, bind_dirac, MeasureTheory.setIntegral_dirac', PMF.toMeasure_pure, MeasureTheory.setLIntegral_dirac, SchwartzMap.integralCLM_dirac_eq_delta, MeasureTheory.ae_dirac_eq, map_dirac, conv_dirac, MeasureTheory.integral_dirac', ProbabilityTheory.Kernel.id_apply, dirac.instIsFiniteMeasure, aestronglyMeasurable_dirac, snd_dirac_unit_compProd_const, ProbabilityTheory.variance_dirac, ProbabilityTheory.Kernel.borelMarkovFromReal_apply, TemperedDistribution.toTemperedDistribution_dirac_eq_delta, dirac.instSigmaFinite, MeasureTheory.dirac_eq_dirac_iff_forall_mem_iff_mem, ProbabilityTheory.mgf_dirac', map_const, MeasureTheory.charFunDual_dirac, MeasureTheory.dirac_withDensity', dirac_apply, volume_euclideanSpace_eq_dirac, dirac_compProd_apply, MeasureTheory.charFun_dirac, mconv_dirac, le_dirac_apply, MeasureTheory.integrable_dirac, dirac_mconv, dirac_unit_compProd, MeasureTheory.measurePreserving_pi_empty, ProbabilityTheory.Kernel.discard_eq_const, ProbabilityTheory.setBernoulli_apply, MeasureTheory.aemeasurable_dirac, tprod_nil, conv_dirac_zero, dirac_zero_conv, ProbabilityTheory.setBernoulli_eq_map, MeasureTheory.dirac_withDensity
instMeasureSpacePUnit 📖	CompOp	1 math math: MeasureTheory.volume_preserving_pi_empty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_or_eq_iff_eq_dirac_add_dirac 📖	mathematical	—	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass instAdd ENNReal instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set Set.instSingletonSet dirac	—	instOuterMeasureClass IsScalarTower.right Finset.sum_cons Finset.sum_singleton ae_mem_finset_iff
ae_eq_or_eq_iff_map_eq_dirac_add_dirac 📖	mathematical	AEMeasurable	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass map instAdd ENNReal instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set Set.preimage Set.instSingletonSet dirac	—	instOuterMeasureClass IsScalarTower.right Finset.sum_cons Finset.sum_singleton ae_mem_finset_iff_map_eq_sum_dirac
ae_mem_finset_iff 📖	mathematical	—	Filter.Eventually Finset Finset.instMembership MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass Finset.sum instAddCommMonoid ENNReal instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set Set.instSingletonSet dirac	—	instOuterMeasureClass IsScalarTower.right ext MeasureTheory.measure_diff_null Set.diff_compl Set.biUnion_of_singleton Set.iUnion_congr_Prop Set.inter_iUnion MeasureTheory.measure_biUnion_finset Disjoint.inter_left' Disjoint.inter_right' coe_finset_sum Finset.sum_apply Finset.sum_congr Set.inter_singleton_of_mem dirac_apply' Set.indicator_of_mem mul_one Set.inter_singleton_of_notMem MeasureTheory.measure_empty Set.indicator_of_notMem MulZeroClass.mul_zero MeasureTheory.ae_finsetSum_measure_iff ae_smul_measure MeasureTheory.ae_dirac_eq
ae_mem_finset_iff_map_eq_sum_dirac 📖	mathematical	AEMeasurable	Filter.Eventually Finset Finset.instMembership MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass map Finset.sum instAddCommMonoid ENNReal instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set Set.preimage Set.instSingletonSet dirac	—	instOuterMeasureClass IsScalarTower.right MeasureTheory.ae_map_iff Finset.measurableSet ae_mem_finset_iff Finset.sum_congr map_apply₀
dirac_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike dirac Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	dirac_apply_of_mem Set.indicator_of_mem Pi.one_apply Set.indicator_of_notMem nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd MeasureTheory.measure_mono instOuterMeasureClass Set.subset_compl_comm Set.singleton_subset_iff dirac_apply' MeasurableSet.compl MeasurableSingletonClass.measurableSet_singleton
dirac_apply' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike dirac Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	MeasureTheory.toMeasure_apply
dirac_apply_eq_zero_or_one 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike dirac instZeroENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	MeasureTheory.measure_toMeasurable dirac_apply' MeasureTheory.measurableSet_toMeasurable Set.indicator.eq_1 NeZero.charZero_one ENNReal.instCharZero
dirac_apply_ne_one_iff_eq_zero 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike dirac instZeroENNReal	—	dirac_apply_eq_zero_or_one zero_ne_one NeZero.charZero_one ENNReal.instCharZero
dirac_apply_ne_zero_iff_eq_one 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike dirac AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	dirac_apply_eq_zero_or_one ne_zero_of_eq_one NeZero.charZero_one ENNReal.instCharZero
dirac_apply_of_mem 📖	mathematical	Set Set.instMembership	DFunLike.coe MeasureTheory.Measure ENNReal instFunLike dirac AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Set.indicator_of_mem le_antisymm dirac_apply' MeasurableSet.univ MeasureTheory.measure_mono instOuterMeasureClass Set.subset_univ le_dirac_apply
dirac_ne_zero 📖	—	—	—	—	NeZero.charZero_one ENNReal.instCharZero dirac_apply_of_mem Set.mem_univ
exists_sum_smul_dirac 📖	mathematical	—	sum Set.Elem ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set instFunLike measurableAtom Set.instMembership dirac	—	mem_measurableAtom_self Set.Nonempty.some_mem IsScalarTower.right MeasureTheory.ext_of_measurableAtoms sum_apply MeasurableSet.measurableAtom_of_countable dirac_apply' Set.image_univ tsum_eq_single SummationFilter.instLeAtTopUnconditional ENNReal.instNoZeroDivisors NeZero.charZero_one ENNReal.instCharZero measurableAtom_eq_of_mem Set.indicator_of_mem mul_one
ext_iff_singleton 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.instSingletonSet	—	ext_of_singleton
ext_of_singleton 📖	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.instSingletonSet	—	—	ext_of_sUnion_eq_univ Set.countable_range Set.ext IsScalarTower.right restrict_singleton
le_dirac_apply 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike dirac	—	MeasureTheory.le_toMeasure_apply MeasureTheory.OuterMeasure.dirac_apply
map_const 📖	mathematical	—	map ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set instFunLike Set.univ dirac	—	ext IsScalarTower.right dirac_apply' map_apply measurable_const Set.preimage_const Set.indicator_eq_one_iff_mem mul_one Set.indicator_eq_zero_iff_notMem MeasureTheory.measure_empty instOuterMeasureClass MulZeroClass.mul_zero
map_dirac 📖	mathematical	Measurable	map dirac	—	ext map_apply dirac_apply' Set.indicator_apply
map_eq_sum 📖	mathematical	Measurable	map sum ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set instFunLike Set.preimage Set.instSingletonSet dirac	—	ext IsScalarTower.right MeasurableSingletonClass.measurableSet_singleton map_apply MeasureTheory.tsum_measure_preimage_singleton Set.to_countable SetCoe.countable tsum_subtype sum_apply dirac_apply' Set.indicator_mul_right mul_one
restrict_singleton 📖	mathematical	—	restrict Set Set.instSingletonSet ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe instFunLike dirac	—	ext IsScalarTower.right restrict_apply dirac_apply' Set.indicator_of_mem mul_one Set.inter_singleton_eq_empty MeasureTheory.measure_empty instOuterMeasureClass Set.indicator_of_notMem MulZeroClass.mul_zero
sum_smul_dirac 📖	mathematical	—	sum ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set instFunLike Set.instSingletonSet dirac	—	IsScalarTower.right map_id map_eq_sum measurable_id
tsum_indicator_apply_singleton 📖	mathematical	MeasurableSet	tsum ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Set.indicator instZeroENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instSingletonSet SummationFilter.unconditional	—	IsScalarTower.right Set.indicator_apply sum_apply dirac_apply mul_ite mul_one MulZeroClass.mul_zero sum_smul_dirac

MeasureTheory.Measure.dirac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsFiniteMeasure 📖	mathematical	—	MeasureTheory.IsFiniteMeasure MeasureTheory.Measure.dirac	—	MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure isProbabilityMeasure
instSigmaFinite 📖	mathematical	—	MeasureTheory.SigmaFinite MeasureTheory.Measure.dirac	—	MeasureTheory.IsFiniteMeasure.toSigmaFinite instIsFiniteMeasure
isProbabilityMeasure 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure MeasureTheory.Measure.dirac	—	MeasureTheory.Measure.dirac_apply_of_mem Set.mem_univ

---

← Back to Index