Theorems · Theorem · probability

ProbabilityTheory.Kernel.densityProcess_nonneg

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) (a : α) (x : γ) (s : Set β), 0 ≤ κ.densityProcess ν n a x s

Defined in: Mathlib.Probability.Kernel.Disintegration.Density
Cited by: 5 results in Mathlib
Foundations: Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace.CountablyGenerated

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites7

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
Realstatement · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
ProbabilityTheory.Kernelstatement and proof · cited by 1,281
MeasurableSpace.CountablyGeneratedstatement and proof · cited by 124
ENNReal.toReal_nonnegproof · cited by 86
ProbabilityTheory.Kernel.densityProcessstatement · cited by 37

Cited by5

Results whose statement or proof uses this declaration.

ProbabilityTheory.Kernel.density_nonnegproof · cited by 5
ProbabilityTheory.Kernel.density_le_oneproof · cited by 4
ProbabilityTheory.Kernel.eLpNorm_densityProcess_leproof · cited by 3
ProbabilityTheory.Kernel.density_mono_setproof · cited by 3
ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcessproof · cited by 2