Theorems · Theorem · probability

ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero

∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [inst : ProbabilityTheory.IsFiniteKernel η] (a : α),
  (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Defined in: Mathlib.Probability.Kernel.RadonNikodym
Cited by: 1 results in Mathlib
Foundations: Depth 333 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace.CountableOrCountablyGenerated ProbabilityTheory.IsFiniteKernel ProbabilityTheory.IsFiniteKernel

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.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Compl.complstatement and proof · cited by 2,925
add_zeroproof · cited by 2,707
ProbabilityTheory.Kernelstatement and proof · cited by 1,281
ProbabilityTheory.IsFiniteKernelstatement and proof · cited by 178
MeasurableSet.complproof · cited by 172
MeasurableSpace.CountableOrCountablyGeneratedstatement and proof · cited by 97
ProbabilityTheory.Kernel.rnDerivstatement and proof · cited by 45

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.Measure.MutuallySingular.compProd_of_rightproof · cited by 3