Theorems · Theorem · probability

ProbabilityTheory.setBernoulli_real_singleton

∀ {ι : Type u_1} {s u : Set ι} [Countable ι] (p : ↑unitInterval),
  s ⊆ u → u.Finite → (ProbabilityTheory.setBernoulli u p).real {s} = ↑p ^ s.ncard * (1 - ↑p) ^ (u \ s).ncard

Defined in: Mathlib.Probability.Distributions.SetBernoulli
Cited by: 1 results in Mathlib
Foundations: Depth 288 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Countable

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.

Setstatement and proof · cited by 53,352
Realstatement · cited by 25,697
Set.Elemstatement and proof · cited by 7,166
Set.Finitestatement and proof · cited by 1,814
ENNReal.ofNNRealproof · cited by 1,279
ENNReal.toRealproof · cited by 859
Countablestatement and proof · cited by 633
unitIntervalstatement and proof · cited by 607
MeasureTheory.Measure.realstatement · cited by 530
Set.ncardstatement and proof · cited by 344
unitInterval.symmproof · cited by 69
ENNReal.toReal_mulproof · cited by 57

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.map_ncard_setBernoulli_real_singletonproof · cited by 2