WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Chi-squared distribution

Revision #1078 → #2470 · back to history

modifiedChi-squared distribution (lead)d70f4612c4e3
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no chi-squared distribution declaration; grep for chi/ChiSquared in Mathlib/Probability returns nothing relevant.
status—not_formalized
modifiedChi-squared as special case of gamma/Wishart6bbd256ef800
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Gamma distribution exists (ProbabilityTheory.gammaMeasure) but no chi-squared definition or Wishart distribution is present in Mathlib.
status—not_formalized
modifiedScaled chi-squared reparametrizationb23d887dd90b
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No chi-squared or Wishart distribution is present in Mathlib to state the reparametrization.
status—not_formalized
modifiedChi-squared distribution formal definition90a68497814f
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No chi-squared measure or PDF definition appears in Mathlib.
status—not_formalized
modifiedSquare of standard normal has chi-squared distributionf762b3eb5026
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No lemma identifies the pushforward of a standard Gaussian under squaring as a chi-squared/gamma measure in Mathlib.
status—not_formalized
modifiedProbability density function of chi-squared2f05fbf8340a
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No chi-squared PDF is defined in Mathlib; only the general gammaPDFReal exists in Mathlib.Probability.Distributions.Gamma.
status—not_formalized
modifiedCumulative distribution function of chi-squareda29f7cb280b5
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No chi-squared CDF is defined; Mathlib has a general cdf and cdf_gammaMeasure_eq_integral but no chi-squared specialization.
status—not_formalized
modifiedChernoff tail bounds for chi-squared CDF221a841a16d0
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has generic subgaussian/moment machinery in Mathlib.Probability.Moments but no Chernoff tail bound stated for chi-squared.
status—not_formalized
modifiedCochran's theorem (chi-squared special case)94473cbe9071
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Cochran's theorem is not in Mathlib; no chi-squared statement to specialize it to.
status—not_formalized
modifiedAdditivity of chi-squared variablese83daf414d70
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No chi-squared additivity or gamma-convolution-of-independents lemma appears in Mathlib.Probability.Distributions.
status—not_formalized
modifiedSample mean of chi-squared is gamma9f575d886e87
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Requires chi-squared and rescaling lemmas for gammaMeasure, neither of which is present in Mathlib.
status—not_formalized
modifiedDifferential entropy of chi-squared29c7e76fe536
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No chi-squared distribution and no computed differential entropy formula for it appears in Mathlib.
status—not_formalized
modifiedChi-squared as maximum entropy distributionbf1c841cd906
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No maximum-entropy characterization for chi-squared is present in Mathlib.
status—not_formalized
modifiedNoncentral (raw) moments of chi-squared0ee3c13d59ae
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no chi-squared distribution to which such a moment formula could be attached.
status—not_formalized
modifiedCumulants of chi-squared9b395e058ff4
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No cumulants of the chi-squared distribution are computed in Mathlib.
status—not_formalized
modifiedLaurent-Massart concentration bounds48508320b298
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Laurent–Massart chi-squared concentration bounds are not stated in Mathlib.
status—not_formalized
modifiedChernoff bound and union bound for chi-squareda7797dc1028c
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Chernoff bound specialized to a chi-squared random variable appears in Mathlib.
status—not_formalized
modifiedAsymptotic normality of chi-squared9e215f49513b
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No CLT specialization to the chi-squared distribution exists in Mathlib (no chi-squared object to converge).
status—not_formalized
modifiedWilson-Hilferty transformation733dbbdea3f4
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Wilson–Hilferty cube-root normal approximation is not in Mathlib.
status—not_formalized
modifiedSquared norm of k standard normals is chi-squaredf55314543b1e
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No lemma links the squared Euclidean norm of iid standard Gaussians to a chi-squared/gamma distribution in Mathlib.
status—not_formalized
modifiedChi-squared via sum of squares of standard normalse1a81a219b5d
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no such definition of the chi-squared distribution.
status—not_formalized
modifiedQuadratic form of Gaussian vector is chi-squareddaaf66168ec6
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No distributional result about Gaussian quadratic forms being chi-squared is present in Mathlib.
status—not_formalized
modifiedNoncentral chi-squared distribution2b31225f0fb4
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Noncentral chi-squared distribution is not defined in Mathlib (grep for 'noncentral' finds only Mathlib/LinearAlgebra/Center.lean).
status—not_formalized
modifiedQuadratic form with idempotent matrix is chi-square2864fce27f48
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This special case of Cochran's theorem is not formalized in Mathlib.
status—not_formalized
modifiedRatio of chi-squared variables is F-distributed78be8d41cf1f
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither the chi-squared nor the F-distribution is defined in Mathlib.
status—not_formalized
modifiedLinear combination as generalized chi-squared7326447c0e54
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The generalized chi-squared distribution is not defined in Mathlib.
status—not_formalized
modifiedNoncentral chi-squared distribution91de1b1e9269
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No noncentral chi-squared distribution is defined in Mathlib.
status—not_formalized
modifiedGeneralized chi-squared distribution52470939c7b5
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No generalized chi-squared distribution is defined in Mathlib.
status—not_formalized
modifiedChi-squared as special case of gamma distribution1c4a0b67437b
FieldFrom #1078To #2470
mathlib.decl—ProbabilityTheory.gammaMeasure
mathlib.match_kind—generalization
mathlib.module—Mathlib.Probability.Distributions.Gamma
note—Mathlib defines the general gamma measure but does not identify chi-squared as its specialization at shape k/2, rate 1/2.
status—partial
modifiedExponential as special case7e577be3b45b
FieldFrom #1078To #2470
mathlib.decl—ProbabilityTheory.exponentialPDF
mathlib.match_kind—generalization
mathlib.module—Mathlib.Probability.Distributions.Exponential
note—Exponential and gamma measures both exist in Mathlib but their identification as gamma with shape 1 is not proven as a lemma.
status—partial
modifiedErlang as special case3ff48db02551
FieldFrom #1078To #2470
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Erlang distribution is not defined in Mathlib.
status—not_formalized
addedConcentration of squared Gaussian vector lengthd0eb2d3d65d6
addedFisher's square-root normal approximation0819b2bd66c6
addedChi-squared relates to chi distribution via square root8d506044aaf0
addedChi-squared and Rayleigh distribution relation25ed075b1b43
addedChi-squared and Maxwell distribution relatione29d6953d684
addedInverse-chi-squared distribution relation7822aa5a11b9
addedChi-squared as type III Pearson distribution77a933a29e62
addedRatio of independent chi-squared gives beta distribution7f79759662e7