Theorems · Theorem · probability

MeasureTheory.pdf.IsUniform.mul_pdf_integrable

∀ {Ω : Type u_2} {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {s : Set ℝ},
  IsCompact s →
    MeasureTheory.pdf.IsUniform X s ℙ MeasureTheory.volume →
      MeasureTheory.Integrable (fun x_1 => x_1 * (MeasureTheory.pdf X ℙ MeasureTheory.volume x_1).toReal)
        MeasureTheory.volume

Defined in: Mathlib.Probability.Distributions.Uniform
Cited by: 0 results in Mathlib
Foundations: Depth 244 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites45

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Setstatement and proof · cited by 53,352
Realstatement and proof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealproof · cited by 9,879
Top.topproof · cited by 9,680
mul_oneproof · cited by 3,885
MulZeroClass.mul_zeroproof · cited by 2,091
Filter.univ_mem'proof · cited by 1,672
Filter.mp_memproof · cited by 1,537
MeasureTheory.Integrablestatement and proof · cited by 1,367

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.