Diff — Box–Muller transform

Revision #2796 → #3271 · back to history

modifiedBasic form setupedd161932876

Field	From #2796	To #3271
note	Verified `MeasureTheory.pdf.IsUniform` at Uniform.lean:63; general uniform-distribution infra exists but the Box–Muller setup itself is not formalized.	Verified `MeasureTheory.pdf.IsUniform` in Mathlib.Probability.Distributions.Uniform; general uniform-distribution infra exists but the Box–Muller setup itself is not formalized.

modifiedZ0 and Z1 are independent standard normalddb3154004da

Field	From #2796	To #3271
note	`ProbabilityTheory.gaussianReal` (Real.lean:222) defines the normal law, but no Box–Muller output theorem was found.	`ProbabilityTheory.gaussianReal` defines the normal law, but no Box–Muller output theorem was found.

modifiedR^2 chi-squared / exponentialde9168c6b2c1

Field	From #2796	To #3271
note	Verified `ProbabilityTheory.exponentialPDF` (Exponential.lean:46) and `expMeasure`; no chi-squared and no theorem identifying ‖(Z₀,Z₁)‖² with an exponential law were found.	Verified `ProbabilityTheory.exponentialPDF` in Mathlib.Probability.Distributions.Exponential; no chi-squared and no theorem identifying ‖(Z₀,Z₁)‖² with an exponential law were found.

addedChi-squared with two DoF equals exponential19fbfcb05c7d

addedRejection samplinge10d45cfa8f3

modifiedAffine transform of a standard normal is normal12f219629af7

Field	From #2796	To #3271
anchor.snippet	If	will have a normal distribution with mean
note	Verified `gaussianReal_map_mul_const` (Real.lean:356) and `gaussianReal_map_add_const` (line 309), whose composition gives σ·Z + μ ∼ N(μ,σ²), though no single-named lemma states the affine case directly.	Verified `gaussianReal_map_mul_const` and `gaussianReal_map_add_const` in Mathlib.Probability.Distributions.Gaussian.Real, whose composition gives σ·Z + μ ∼ N(μ,σ²), though no single-named lemma states the affine case directly. Anchor tightened from bare 'If' during moderation.
provenance	ai	ai-moderated