Binomial distribution

TheoremSecond factorial moment of the binomial law#✓fully proved

E[X (X - 1)] = n (n - 1) p².

theorem integral_mul_sub_one_map_cast_binomial :
    ∫ x, x * (x - 1) ∂Bin(ℝ, n, p) = (n : ℝ) * ((n : ℝ) - 1) * (p : ℝ) ^ 2

Used by 2

Used bySecond factorial moment of a binomial random variable · Second moment of the binomial law

TheoremSecond moment of the binomial law#✓fully proved

E[X²] = n p (1 - p) + (n p)².

theorem integral_sq_map_cast_binomial :
    ∫ x, x ^ 2 ∂Bin(ℝ, n, p) = (n : ℝ) * p * (1 - (p : ℝ)) + ((n : ℝ) * p) ^ 2

Uses 1 · Used by 4

Proof usesSecond factorial moment of the binomial law

Used byDrift of the Wright–Fisher chain with mutation (Ewens 2004, ch. 4) · Infinitesimal variance of the Wright–Fisher chain with mutation · Second moment of a binomial random variable · Variance of the binomial law

TheoremVariance of the binomial law#✓fully proved

Var X = n p (1 - p).

theorem variance_id_map_cast_binomial :
    Var[id; Bin(ℝ, n, p)] = (n : ℝ) * p * (1 - (p : ℝ))

Uses 1 · Used by 1

Proof usesSecond moment of the binomial law

Used byVariance of a binomial random variable

TheoremSecond factorial moment of a binomial random variable#✓fully proved

If X has law Bin(ℝ, n, p) then E[X (X - 1)] = n (n - 1) p².

theorem integral_mul_sub_one_of_hasLaw_binomial (hX : HasLaw X Bin(ℝ, n, p) P) :
    P[fun ω => X ω * (X ω - 1)] = (n : ℝ) * ((n : ℝ) - 1) * (p : ℝ) ^ 2

Uses 1 · Used by 3

Proof usesSecond factorial moment of the binomial law

Used byUnbiased f2 · Unbiased f3 · Unbiased heterozygosity

TheoremSecond moment of a binomial random variable#✓fully proved

If X has law Bin(ℝ, n, p) then E[X²] = n p (1 - p) + (n p)².

theorem integral_sq_of_hasLaw_binomial (hX : HasLaw X Bin(ℝ, n, p) P) :
    P[X ^ 2] = (n : ℝ) * p * (1 - (p : ℝ)) + ((n : ℝ) * p) ^ 2

Uses 1

Proof usesSecond moment of the binomial law

TheoremVariance of a binomial random variable#✓fully proved

If X has law Bin(ℝ, n, p) then Var X = n p (1 - p).

theorem variance_of_hasLaw_binomial (hX : HasLaw X Bin(ℝ, n, p) P) :
    Var[X; P] = (n : ℝ) * p * (1 - (p : ℝ))

Uses 1

Proof usesVariance of the binomial law

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.