Theorems · Theorem · probability

IndepFun.singleton_indepSets_of_indicator

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : Type u_4} [mX : MeasurableSpace 𝓧]
  {A : Set Ω} {X : Ω → 𝓧},
  ProbabilityTheory.IndepFun (A.indicator 1) X P → ProbabilityTheory.IndepSets {A} {s | MeasurableSet s} P

If the indicator of a set A is independent from a variable X, then the set A is independent from the sigma algebra generated by X.

Defined in: Mathlib.Probability.Independence.BoundedContinuousFunction
Cited by: 5 results in Mathlib
Foundations: Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Setstatement and proof · cited by 53,352
Realstatement · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Set.ofPredstatement and proof · cited by 6,101
Set.preimageproof · cited by 4,946
MeasurableSetstatement and proof · cited by 3,075
Set.extproof · cited by 2,266
Set.indicatorstatement and proof · cited by 723
ProbabilityTheory.IndepFunstatement and proof · cited by 192
Set.mem_singleton_iffproof · cited by 172

Cited by5

Results whose statement or proof uses this declaration.

indepSets_comap_of_bcfproof · cited by 1
indepSets_comap_pi_of_bcfproof · cited by 1
indepSets_comap_pi_of_prod_bcfproof · cited by 1
indepSets_comap_process_of_bcfproof · cited by 1
indepSets_comap_process_of_prod_bcfproof · cited by 1