Theorems · Theorem · probability

ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem

∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.IndepFun (∑ j ∈ s, f j) (f i) μ

Defined in: Mathlib.Probability.Independence.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommMonoid MeasurableAdd₂

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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

Finsetstatement and proof · cited by 13,712
MeasurableSpacestatement and proof · cited by 13,106
AddCommMonoidstatement and proof · cited by 12,281
MeasureTheory.Measurestatement and proof · cited by 10,939
Finset.sumstatement · cited by 5,195
Measurablestatement and proof · cited by 1,499
ProbabilityTheory.IndepFunstatement · cited by 192
MeasurableAdd₂statement and proof · cited by 155
ProbabilityTheory.iIndepFunstatement and proof · cited by 138
ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetSum_of_notMemproof · cited by 5

Cited by2

Results whose statement or proof uses this declaration.

ProbabilityTheory.iIndepFun.indepFun_finset_sum_of_notMemproof · cited by 0
ProbabilityTheory.iIndepFun.integrable_exp_mul_sumproof · cited by 0