Mathlib upstreaming drafts — CI-guarded copies #
Compiles the contents of planning/mathlib_upstream_drafts/PR1_CDF.lean (generic cdf
lemmas, target Mathlib/Probability/CDF.lean) and
planning/mathlib_upstream_drafts/PR2_GaussianReal.lean (Gaussian cdf facts and the
1-D Cameron–Martin formula, target Mathlib/Probability/Distributions/Gaussian/Real.lean) and
planning/mathlib_upstream_drafts/PR3_GaussianMultivariate.lean
(full support of stdGaussian, target Mathlib/Probability/Distributions/Gaussian/Multivariate.lean)
against this repo's pinned Mathlib, inside the namespace MathlibUpstream so nothing clashes with
Mathlib or with LeanMlir.Proofs. Keep in sync with those three files.
A Certs root (audited in tests/AuditAxioms.lean) so the drafts can't rot between
Mathlib pin bumps while the PRs are in flight. GaussianQuantile derives its Φ facts from
the PR2 lemmas, Smoothing.Gaussian its Neyman–Pearson shift from the Cameron–Martin one.
Once a PR merges and the pin catches up, delete the corresponding section here and repoint those
uses at Mathlib.
Fast check: lake env lean LeanMlir/Proofs/Foundation/UpstreamDraft.lean
If a probability measure on ℝ gives positive mass to every nonempty open set, then its
cdf is strictly monotone.
If a probability measure on ℝ gives positive mass to every nonempty open set, then its
cdf is everywhere positive: there is mass below every point.
If a probability measure on ℝ gives positive mass to every nonempty open set, then its
cdf is everywhere less than 1: there is mass above every point.
If a probability measure on ℝ gives positive mass to every nonempty open set, then its
cdf maps into the open unit interval.
If the cdf of a probability measure on ℝ is strictly monotone, the measure gives positive
mass to every nonempty open set. Converse of strictMono_cdf.
The cdf of a probability measure on ℝ is strictly monotone iff the measure gives positive
mass to every nonempty open set.
The cdf of a probability measure on ℝ without atoms has no jumps: its left limit at every
point equals its value there.
The cdf of a probability measure on ℝ without atoms is continuous: it is monotone and
right-continuous, and by leftLim_cdf it has no jumps.
If the cdf of a probability measure on ℝ is continuous, the measure has no atoms.
Converse of continuous_cdf.
The cdf of a probability measure on ℝ is continuous iff the measure has no atoms.
The integral of the indicator of Iic t against a probability measure on ℝ is its cdf
at t.
A real Gaussian measure with nonzero variance gives positive mass to every nonempty open set: its density is everywhere positive, so it dominates the Lebesgue measure.
The cdf of a real Gaussian measure with nonzero variance is strictly monotone.
The cdf of a real Gaussian measure with nonzero variance is continuous.
The cdf of a real Gaussian measure with nonzero variance is everywhere positive.
The cdf of a real Gaussian measure with nonzero variance is everywhere less than 1.
The cdf of a real Gaussian measure with nonzero variance maps into the open unit interval.
Symmetry of the centered Gaussian cdf: Φ_v (-x) = 1 - Φ_v x. The centered Gaussian is
invariant under negation, so the mass of Iic (-x) is the mass of Ici x, which (no atoms)
is the mass of the complement of Iic x.
Shifting the mean of a Gaussian shifts its cdf: cdf (gaussianReal (μ + δ) v) x = cdf (gaussianReal μ v) (x - δ). Holds for v = 0 as well (both sides are Dirac cdfs).
Shifting the mean of a Gaussian multiplies its density by an exponential likelihood ratio:
gaussianPDFReal (μ + δ) v x = exp ((δ (x - μ) - δ² / 2) / v) * gaussianPDFReal μ v x. Holds
for v = 0 as well (both densities are 0).
The one-dimensional Cameron–Martin formula: translating the argument of a function by δ
under a Gaussian measure with nonzero variance is integrating it against the exponential
likelihood ratio of gaussianPDFReal_add_mean.
The standard Gaussian on a finite-dimensional inner-product space gives positive mass to
every nonempty open set: it is the pushforward of the product of standard real Gaussians (open-pos
by instIsOpenPosMeasureGaussianReal and Measure.pi.isOpenPosMeasure) under the surjective
continuous basis sum.