← Mathematical handbook

noncomputable def Verification.betaMoment (a b : ℕ) : ℝ

Equations

• Verification.betaMoment a b = ↑a.factorial * ↑b.factorial / ↑(a + b + 1).factorial

theorem Verification.integral_beta_monomial (a b : ℕ) : ∫ (u : ↑unitInterval), ↑u ^ a * (1 - ↑u) ^ b = betaMoment a b

theorem Verification.betaMoment_binomial (a b : ℕ) : betaMoment a b = 1 / ((↑a + ↑b + 1) * ↑((a + b).choose a))

theorem Verification.betaMoment_succ (a b : ℕ) : betaMoment (a + 1) b = (↑a + 1) / (↑a + ↑b + 2) * betaMoment a b

theorem Verification.betaMoment_succ_succ (a b : ℕ) : betaMoment (a + 2) b = (↑a + 1) * (↑a + 2) / ((↑a + ↑b + 2) * (↑a + ↑b + 3)) * betaMoment a b