Theorems · Definition · measure theory
MeasureTheory.preVariationFun
{X : Type u_1} → [MeasurableSpace X] → (Set X → ENNReal) → Set X → ENNRealIf s is measurable then preVariationFun f s is the supremum over partitions P of s of
the quantity ∑ p ∈ P.parts, f p. If s is not measurable then it is set to 0.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- ENNRealstatement and proof · cited by 9,879
- Finset.sumproof · cited by 5,195
- MeasurableSetproof · cited by 3,075
- iSupproof · cited by 2,415
- Finpartitionproof · cited by 199
- Finpartition.partsproof · cited by 184
Cited by18
Results whose statement or proof uses this declaration.
- MeasureTheory.ennrealPreVariationproof · cited by 10
- MeasureTheory.preVariation.sum_lestatement · cited by 5
- MeasureTheory.VectorMeasure.exists_variation_le_add'proof · cited by 2
- MeasureTheory.preVariation.exists_Finpartition_sum_gestatement and proof · cited by 2
- MeasureTheory.preVariation.exists_Finpartition_sum_gtstatement and proof · cited by 2
- MeasureTheory.preVariationFun_applystatement · cited by 1
- MeasureTheory.preVariationFun_of_not_measurableSetstatement · cited by 1
- MeasureTheory.VectorMeasure.preVariationFun_apply_of_ennrealstatement · cited by 1
- MeasureTheory.preVariation.exists_Finpartition_sum_ge'statement and proof · cited by 1
- MeasureTheory.preVariation.monostatement and proof · cited by 1
- MeasureTheory.preVariation.sum_le'statement and proof · cited by 1
- MeasureTheory.preVariation.sum_le_preVariationFun_iUnionstatement and proof · cited by 1