Theorems · Theorem · probability
ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul
∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} (h𝓑𝓧 : 𝓑 ≤ 𝓧),
π.IsProper ↔ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x => 1) x • π x- Defined in
- Mathlib.Probability.Kernel.Proper
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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 and proof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
- ENNRealstatement · cited by 9,879
- MeasurableSetstatement and proof · cited by 3,075
- ProbabilityTheory.Kernelstatement and proof · cited by 1,281
- Set.indicatorstatement and proof · cited by 723
- inf_le_rightproof · cited by 238
- inf_eq_leftproof · cited by 41
- ProbabilityTheory.Kernel.restrictstatement and proof · cited by 19
- ProbabilityTheory.Kernel.IsProperstatement and proof · cited by 11
Cited by3
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mulproof · cited by 2
- ProbabilityTheory.Kernel.IsProper.of_restrict_eq_indicator_smulproof · cited by 0
- ProbabilityTheory.Kernel.IsProper.restrict_eq_indicator_smulproof · cited by 0