Theorems · Theorem · measure theory
MeasureTheory.laverage_eq
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
⨍⁻ (x : α), f x ∂μ = (∫⁻ (x : α), f x ∂μ) / μ Set.univ- Defined in
- Mathlib.MeasureTheory.Integral.Average
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement and proof · cited by 9,879
- Set.univstatement and proof · cited by 3,945
- MeasureTheory.lintegralstatement and proof · cited by 1,152
- smul_eq_mulproof · cited by 357
- MeasureTheory.laveragestatement · cited by 44
- MeasureTheory.lintegral_smul_measureproof · cited by 20
- ENNReal.div_eq_inv_mulproof · cited by 18
- MeasureTheory.laverage_eq'proof · cited by 1
Cited by12
Results whose statement or proof uses this declaration.
- MeasureTheory.setLAverage_eqproof · cited by 3
- MeasureTheory.toReal_laverageproof · cited by 3
- MeasureTheory.measure_mul_laverageproof · cited by 2
- MeasureTheory.measure_setLAverage_le_posproof · cited by 2
- MeasureTheory.laverage_mul_measure_univproof · cited by 1
- bergelson'proof · cited by 1
- MeasureTheory.laverage_add_measureproof · cited by 1
- MeasureTheory.laverage_lt_topproof · cited by 1
- MeasureTheory.toReal_setLAverageproof · cited by 0
- MeasureTheory.setLAverage_congr_funproof · cited by 0
- MeasureTheory.setLAverage_congr_fun_aeproof · cited by 0
- MeasureTheory.laverage_congrproof · cited by 0