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, target
Mathlib/Probability/Distributions/Gaussian/Real.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 two 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. Once a PR merges and the pin catches up,
delete the corresponding section here and cite Mathlib directly.
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.
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).