Beta marginals of the real Dirichlet distribution

@[simp]

theorem ProbabilityTheory.mem_mvRealBetaDomain_fin_two (α β : ℝ) : ![α, β] ∈ mvRealBetaDomain ↔ 0 < α ∧ 0 < β

For two parameters, mvRealBetaDomain is just positivity of both parameters.

@[simp]

theorem ProbabilityTheory.mvRealBeta_fin_two (α β : ℝ) : mvRealBeta ![α, β] = beta α β

In the two-variable case, mvRealBeta is the ordinary beta function.

@[simp]

theorem ProbabilityTheory.mem_stdSimplexInterior_fin_two (x : ℝ) : ![x, 1 - x] ∈ stdSimplexInterior ↔ 0 < x ∧ x < 1

Under x ↦ ![x, 1 - x], the relative interior of the two-coordinate simplex corresponds to the open unit interval.

@[simp]

theorem ProbabilityTheory.dirichletPdfReal_fin_two (α β x : ℝ) : dirichletPdfReal ![α, β] ![x, 1 - x] = betaPDFReal α β x

The two-variable real Dirichlet density is the beta density under the parametrization x ↦ ![x, 1 - x].

@[simp]

theorem ProbabilityTheory.dirichletPdf_fin_two (α β x : ℝ) : dirichletPdf ![α, β] ![x, 1 - x] = betaPDF α β x

The two-variable ENNReal-valued Dirichlet density is the beta density.

theorem ProbabilityTheory.betaMarginal {ι : Type u_1} [Fintype ι] [Nontrivial ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (i : ι) : MeasureTheory.Measure.map (fun (u : ι → ℝ) => u i) (dirichletMeasure b) = betaMeasure (b i) (∑ j ∈ Finset.univ.erase i, b j)

Marginalization of the Dirichlet density with respect to the i coordinate.

theorem ProbabilityTheory.map_dirichletMeasure_fin_two {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) : MeasureTheory.Measure.map (fun (u : Fin 2 → ℝ) => u 0) (dirichletMeasure ![α, β]) = betaMeasure α β

The push-forward of the two-variable Dirichlet measure under the first coordinate is the beta measure.