Theorems · Theorem · probability

ProbabilityTheory.stieltjesOfMeasurableRat_unit_prod

∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (a : α),
  ProbabilityTheory.stieltjesOfMeasurableRat (fun p => f p.2) ⋯ ((), a) =
    ProbabilityTheory.stieltjesOfMeasurableRat f hf a

Defined in: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Cited by: 1 results in Mathlib
Foundations: Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites20

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

Realstatement and proof · cited by 25,697
TopologicalSpaceproof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
LinearOrderproof · cited by 8,572
Measurablestatement and proof · cited by 1,499
Monotoneproof · cited by 1,397
Set.Iciproof · cited by 1,070
ContinuousWithinAtproof · cited by 512
Measurable.compstatement and proof · cited by 234
measurable_sndstatement and proof · cited by 94
StieltjesFunctionstatement · cited by 85
ProbabilityTheory.stieltjesOfMeasurableRatstatement · cited by 22

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prodproof · cited by 2