[Merged by Bors] - feat: multivariate Gaussian distributions#36143
[Merged by Bors] - feat: multivariate Gaussian distributions#36143EtienneC30 wants to merge 40 commits intoleanprover-community:masterfrom
Conversation
PR summary 4644b1dc05
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.InnerProductSpace.Dual | 2182 | 2222 | +40 (+1.83%) |
Import changes for all files
| Files | Import difference |
|---|---|
4 filesMathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology |
40 |
Mathlib.Probability.Distributions.Gaussian.Multivariate (new file) |
2838 |
Declarations diff
+ OrthonormalBasis.norm_dual
+ charFunDual_stdGaussian
+ charFun_multivariateGaussian
+ charFun_stdGaussian
+ covarianceBilin_multivariateGaussian
+ covarianceBilin_stdGaussian
+ covariance_eval_multivariateGaussian
+ integral_id_multivariateGaussian
+ integral_id_multivariateGaussian'
+ integral_id_stdGaussian
+ integral_strongDual_stdGaussian
+ isGaussian_multivariateGaussian
+ isGaussian_stdGaussian
+ isProbabilityMeasure_stdGaussian
+ map_pi_eq_stdGaussian
+ measurePreserving_eval_multivariateGaussian
+ measurePreserving_restrict₂_multivariateGaussian
+ multivariateGaussian
+ multivariateGaussian_of_not_posSemidef
+ multivariateGaussian_zero_one
+ restrict₂
+ restrict₂_apply
+ stdGaussian
+ stdGaussian_eq_map_pi_orthonormalBasis
+ stdGaussian_map
+ variance_dual_stdGaussian
+ variance_eval_multivariateGaussian
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
Increase in tech debt: (relative, absolute) = (11.00, 0.00)
| Current number | Change | Type |
|---|---|---|
| 10171 | 11 | backward.isDefEq |
Current commit dc52315cc4
Reference commit 4644b1dc05
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
EtienneC30
changed the title
mathlib-dependent-issues
bot
added
the
blocked-by-other-PR
RemyDegenne
added
the
brownian
This reverts commit 290fe09.
sgouezel
added
the
awaiting-author
EtienneC30
removed
the
awaiting-author
|
✌️ EtienneC30 can now approve this pull request. To approve and merge a pull request, simply reply with |
mathlib-triage
bot
added
the
delegated
|
Thanks! |
Define the standard Gaussian distribution over a Euclidean space and multivariate Gaussian distributions over `EuclideanSpace ℝ ι`. Co-authored-by: @RemyDegenne
|
Pull request successfully merged into master. Build succeeded:
|
mathlib-bors
bot
changed the title
3 participants
Define the standard Gaussian distribution over a Euclidean space and multivariate Gaussian distributions over
EuclideanSpace ℝ ι.Co-authored-by: @RemyDegenne