Theorems · Theorem · probability

ProbabilityTheory.Kernel.withDensity_rnDeriv_eq

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

Defined in: Mathlib.Probability.Kernel.RadonNikodym
Cited by: 1 results in Mathlib
Foundations: Depth 334 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.

Cites17

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
MeasureTheory.aeproof · cited by 2,352
Filter.EventuallyEqproof · cited by 1,912
ProbabilityTheory.Kernelstatement and proof · cited by 1,281
MeasureTheory.Measure.AbsolutelyContinuousstatement and proof · cited by 325
MeasureTheory.Measure.rnDerivproof · cited by 234
ProbabilityTheory.IsFiniteKernelstatement and proof · cited by 178
MeasurableSpace.CountableOrCountablyGeneratedstatement and proof · cited by 97
ProbabilityTheory.Kernel.rnDerivstatement and proof · cited by 45
ProbabilityTheory.Kernel.withDensitystatement · cited by 45

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.Kernel.ae_eq_of_compProd_eqproof · cited by 3