Revision #2924 → #3983 · back to history
modifiedChi-squared distribution (lead)d70f4612c4e3
| Field | From #2924 | To #3983 |
|---|
| note | Mathlib has no chi-squared distribution declaration; grep for chi/ChiSquared in Mathlib/Probability returns nothing relevant. | No chi-squared distribution is defined in Mathlib; grep for chi/ChiSquared under Mathlib/ returns no probability decls. |
modifiedChi-squared as special case of gamma/Wishart6bbd256ef800
| Field | From #2924 | To #3983 |
|---|
| note | Gamma distribution exists (ProbabilityTheory.gammaMeasure) but no chi-squared definition or Wishart distribution is present in Mathlib. | gammaMeasure exists in Mathlib.Probability.Distributions.Gamma, but neither chi-squared nor Wishart distributions are defined. |
modifiedCumulative distribution function of chi-squareda29f7cb280b5
| Field | From #2924 | To #3983 |
|---|
| note | No chi-squared CDF is defined; Mathlib has a general cdf and cdf_gammaMeasure_eq_integral but no chi-squared specialization. | No chi-squared CDF is defined; Mathlib has a general cdf and gamma-CDF integrals but no chi-squared specialization. |
modifiedChernoff tail bounds for chi-squared CDF221a841a16d0
| Field | From #2924 | To #3983 |
|---|
| note | Mathlib has generic subgaussian/moment machinery in Mathlib.Probability.Moments but no Chernoff tail bound stated for chi-squared. | Mathlib has generic subgaussian/moment machinery but no Chernoff tail bound stated for chi-squared. |
modifiedDifferential entropy of chi-squared29c7e76fe536
| Field | From #2924 | To #3983 |
|---|
| note | No chi-squared distribution and no computed differential entropy formula for it appears in Mathlib. | No chi-squared distribution and no differential entropy formula for it appears in Mathlib. |
modifiedNoncentral chi-squared distribution2b31225f0fb4
| Field | From #2924 | To #3983 |
|---|
| note | Noncentral chi-squared distribution is not defined in Mathlib (grep for 'noncentral' finds only Mathlib/LinearAlgebra/Center.lean). | Noncentral chi-squared distribution is not defined in Mathlib. |
modifiedChi-squared as special case of gamma distribution1c4a0b67437b
| Field | From #2924 | To #3983 |
|---|
| note | Mathlib defines the general gamma measure but does not identify chi-squared as its specialization at shape k/2, rate 1/2. | Mathlib defines the general gammaMeasure but does not identify chi-squared as its specialization at shape k/2, rate 1/2. |
modifiedChi-squared and Rayleigh distribution relation25ed075b1b43
| Field | From #2924 | To #3983 |
|---|
| note | The Rayleigh distribution is not defined in Mathlib. | The Rayleigh distribution is not defined in Mathlib.Probability.Distributions. |
addedStudent's t-distribution as transformation of chi-squared3512bf23826a
addedChi-squared as transformation of Pareto distributionbbefa7eb6bbd
addedChi-squared with 2 degrees of freedom is exponential5c188d29fdce
addedChi-squared arises from multivariate normal approximation to multinomial9c0ac03928ae