Revision #2038 → #2796 · back to history
modifiedBox–Muller transform791e1786dfe0
| Field | From #2038 | To #2796 |
|---|
| note | No Box–Muller transform construction exists in Mathlib; grepping `Mathlib` for `Box.?Muller` returns no files. | Confirmed: grep for `Box.?Muller` under `Mathlib/` returns no files, so the transform is not formalized. |
modifiedBasic form setupedd161932876
| Field | From #2038 | To #2796 |
|---|
| note | Mathlib has uniform distributions and independence of random variables, but does not formalize this specific Box–Muller setup. | Verified `MeasureTheory.pdf.IsUniform` at Uniform.lean:63; general uniform-distribution infra exists but the Box–Muller setup itself is not formalized. |
modifiedZ0 and Z1 are independent standard normalddb3154004da
| Field | From #2038 | To #2796 |
|---|
| note | The Box–Muller output theorem is absent from Mathlib, although `gaussianReal` (in `Mathlib.Probability.Distributions.Gaussian.Real`) defines the standard normal. | `ProbabilityTheory.gaussianReal` (Real.lean:222) defines the normal law, but no Box–Muller output theorem was found. |
modifiedPolar coordinate derivation8ddb0cfdbe2c
| Field | From #2038 | To #2796 |
|---|
| note | No statement about polar-coordinate transformation of a 2D Gaussian giving independent radial-squared and angular components is present in Mathlib. | No statement about polar-coordinate decomposition of a 2D standard Gaussian yielding independent radial-squared and angular components is present in Mathlib. |
modifiedR^2 chi-squared / exponentialde9168c6b2c1
| Field | From #2038 | To #2796 |
|---|
| note | Mathlib defines `exponentialPDF`/`expMeasure` but has no chi-squared distribution and no theorem identifying the squared norm of a 2D standard Gaussian with an exponential law. | Verified `ProbabilityTheory.exponentialPDF` (Exponential.lean:46) and `expMeasure`; no chi-squared and no theorem identifying ‖(Z₀,Z₁)‖² with an exponential law were found. |
addedAffine transform of a standard normal is normal12f219629af7