Theorems · Theorem · probability

ProbabilityTheory.isCondKernelCDF_condCDF

∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ],
  ProbabilityTheory.IsCondKernelCDF (fun p => ProbabilityTheory.condCDF ρ p.2) (ProbabilityTheory.Kernel.const Unit ρ)
    (ProbabilityTheory.Kernel.const Unit ρ.fst)

Defined in: Mathlib.Probability.Kernel.Disintegration.CondCDF
Cited by: 5 results in Mathlib
Foundations: Depth 267 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasureTheory.IsFiniteMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
ProbabilityTheory.Kernel.conststatement and proof · cited by 93
MeasureTheory.Measure.fststatement and proof · cited by 70
ProbabilityTheory.IsCondKernelCDFstatement and proof · cited by 22
ProbabilityTheory.condCDFstatement · cited by 20
ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prodproof · cited by 2
ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRatproof · cited by 2
ProbabilityTheory.isRatCondKernelCDF_preCDFproof · cited by 2

Cited by5

Results whose statement or proof uses this declaration.

ProbabilityTheory.lintegral_condCDFproof · cited by 1
ProbabilityTheory.setLIntegral_condCDFproof · cited by 0
ProbabilityTheory.integrable_condCDFproof · cited by 0
ProbabilityTheory.integral_condCDFproof · cited by 0
ProbabilityTheory.setIntegral_condCDFproof · cited by 0