Theorems · Theorem · probability

ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular

∀ {α : 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).MutuallySingular (η a)

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.

Cites19

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
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
zero_addproof · cited by 2,366
ProbabilityTheory.Kernelstatement and proof · cited by 1,281
ProbabilityTheory.IsFiniteKernelstatement and proof · cited by 178
add_applyproof · cited by 154
MeasurableSpace.CountableOrCountablyGeneratedstatement and proof · cited by 97
MeasureTheory.Measure.MutuallySingularstatement and proof · cited by 91
ProbabilityTheory.Kernel.rnDerivstatement and proof · cited by 45
ProbabilityTheory.Kernel.withDensitystatement and proof · cited by 45
MeasureTheory.Measure.AbsolutelyContinuous.rflproof · cited by 30

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.Measure.MutuallySingular.compProd_of_rightproof · cited by 3