Beta Distribution

Stream: mathlib4

[Alvan Arulandu]

@Rémy Degenne I'm also working on formalizing the Beta distribution in branch arulandu/beta, if that sounds good

[Alvan Arulandu]

One question I have is that the UniformPDF, despite having bounded support, is defined on the extended non-negative reals. I'm confused why this is / should I do it for this bounded support distribution as well. Perhaps @Josha Dekker has thoughts as well

[Alvan Arulandu]

I'm also running into an issue in that the complex gamma function isn't proven to have no zeros, so I can't prove that the beta pdf integrates to 1. Would love to hear any advice as to how to go about resolving this.

[Alvan Arulandu]

The rest of the formalization is done. What remains are the following proofs:

lemma betaReal_Integral {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
Beta a b = ∫ (x : ℝ) in Ioc 0 1, x ^ (a - 1) * (1 - x) ^ (b - 1) := by
  rw [Beta, Complex.betaIntegral]
  -- type casting weirdness
  sorry

lemma Gamma_mul_Gamma_div_Gamma_eq_betaIntegralReal {a b : ℝ} :
Beta a b = Gamma a * Gamma b / Gamma (a+b) := by sorry --  doable w ha/hb + real?

I'm still new to lean so working through the casts in the first is proving difficult. I think the second poses the more fundamental challenge

[Alvan Arulandu]

the only workaround I can think of is to prove Beta a b > 0 directly from the integral instead of routing through Gamma

[Josha Dekker]

Alvan Arulandu said:

One question I have is that the UniformPDF, despite having bounded support, is defined on the extended non-negative reals. I'm confused why this is / should I do it for this bounded support distribution as well. Perhaps Josha Dekker has thoughts as well

I made the API by mimicking that of other distributions, so this is a matter of consistency. I prefer that FooPDF always takes similar arguments regardless of what Foo is, but my personal taste shouldn’t be leading on this, in particular if it proves prohibitive. It also depends on @Rémy Degenne’s thoughts on this!

for what it is worth, you may also begin by defining things the nonnegative reals, and then casting to ENNReal. Starting on an interval is not preferred if I understood correctly (in the past).

[Kexing Ying]

Defining the pdf this way also allows for the degenerate cases (i.e. the zero measure and the infinite measure). Note that a pdf does not a priori need to integrate to one but is rather a property we prove later.

[Jeremy Tan]

Don't formalise just the beta, formalise the Dirichlet distribution for any number of real variables

[Jeremy Tan]

Then not only do you get the beta as the two-variable case, but taking the average over the Dirichlet gives you Carlson's R-function, which leads to elliptic integrals

[Alvan Arulandu]

Will consider working on the Dirichlet after, just because I don't see as much special function support for that required for the latter.

[Alvan Arulandu]

I'm having some trouble converting between Bochner / interval integrals and proving positivity by lower bounding integrands.

[Josha Dekker]

Alvan Arulandu said:

Will consider working on the Dirichlet after, just because I don't see as much special function support for that required for the latter.

If the special function support is lacking, you may consider PR’ing that in another PR (or nerdsniping someone into doing it). I guess that it is reasonable to do Beta first and extend (or let someone else extend) to Dirichlet later, although there’ll probably be some double work. (Similar to how we first had exponential distributions, then added gamma distributions and rewrote exponential distributions to be a special case).

[Alvan Arulandu]

Haha yes nerd sniping is real. My problem at the moment is converting between typecasts of R -> C and interval integral (special functions) to bochner integral in PDF. If you have any advice, that'd be greatly appreciated. Here are the last three claims I need:

lemma betaIntegral_real_eq {a b : ℝ} (ha : 0 < a) (hb : 0 < b):
Complex.re (∫ (x : ℝ) in (0)..1, ↑x ^ (↑a - 1:ℂ) * (1 - ↑x) ^ (↑b - 1:ℂ)) =
∫ (x : ℝ) in (0)..1, x ^ (a - 1) * (1 - x) ^ (b - 1) := by
  sorry

lemma betaPDF_integrable_cast {a b : ℝ} :
@IntervalIntegrable ℂ Complex.instNormedAddCommGroup
(fun x ↦ ↑x ^ (↑a - 1:ℂ) * (1 - ↑x) ^ (↑b - 1:ℂ)) ℙ 0 1
= @IntervalIntegrable ℝ normedAddCommGroup
(fun x ↦ x ^ (a - 1) * (1 - x) ^ (b - 1)) ℙ 0 1 := by
sorry

lemma betaReal_integral_eq {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
∫ (x : ℝ) in (0)..1, x ^ (a - 1) * (1 - x) ^ (b - 1)
= ∫ (x : ℝ) in Ioc 0 1, x ^ (a - 1) * (1 - x) ^ (b - 1) := by
sorry

[Alvan Arulandu]

Honestly, I feel like the Beta special function definition should be rewritten with MeasureTheory.integral (bochner) instead of interval. Yes, it would make my life a lot easier, but on top of this, Gamma function uses this type as well

[Alvan Arulandu]

Plus, the Beta.lean isn't being used by any other part of mathlib so I feel like this is safe

[Alvan Arulandu]

@Rémy Degenne formalized #16773

[Alvan Arulandu]

Unsure how to organize lemmas between Distributions/Beta.lean SpecialFunctions/Gamma/Beta.lean + where to place the integral complex<->real casting lemmas from Etienne

[Rémy Degenne]

If you want reviewers to notice your PR, make sure to add a topic label (in this case t-measure-probability). Sorry that I have not yet reviewed your other PR, but I have little time these days. I may find time over the week end.

Let me use that occasion to recall that anybody is welcome to leave a review, and that helps us a lot. So if for example @Etienne Marion has things to say about #16713 or #16773 that would be helpful. You don't need to be a Mathlib reviewer to leave a review!
Pinging also @Jason KY. (who is a Mathlib reviewer). If you could help on those that would be great!

[Alvan Arulandu]

No worries, I will be sure to tag with the topic in the future; I apologize for the inconvenience.