Theorems · Definition · measure theory
MeasureTheory.ProbabilityMeasure.toWeakDualBCNN
{Ω : Type u_1} →
[inst : MeasurableSpace Ω] →
[inst_1 : TopologicalSpace Ω] →
[OpensMeasurableSpace Ω] →
MeasureTheory.ProbabilityMeasure Ω → WeakDual NNReal (BoundedContinuousFunction Ω NNReal)Probability measures yield elements of the WeakDual of bounded continuous nonnegative
functions via MeasureTheory.FiniteMeasure.testAgainstNN, i.e., integration.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 210 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- NNRealstatement · cited by 4,310
- OpensMeasurableSpacestatement and proof · cited by 636
- BoundedContinuousFunctionstatement · cited by 511
- MeasureTheory.ProbabilityMeasurestatement · cited by 127
- WeakDualstatement · cited by 103
- MeasureTheory.ProbabilityMeasure.toFiniteMeasureproof · cited by 26
- MeasureTheory.FiniteMeasure.toWeakDualBCNNproof · cited by 8
Cited by3
Results whose statement or proof uses this declaration.
- MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_applystatement · cited by 0
- MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuousstatement · cited by 0
- MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNNstatement · cited by 0