feat(Probability/Quantile): the lower quantile function of a real cdf - #42461
feat(Probability/Quantile): the lower quantile function of a real cdf#42461Ganton23 wants to merge 5 commits into
Conversation
… core
Define `ProbabilityTheory.quantileSet F p = {x | p <= F x}` and
`ProbabilityTheory.lowerQuantile F p = sInf (quantileSet F p)`, the lower
generalized inverse of a cdf-like function on the reals, together with the
order-theoretic lemmas that need no topology.
`sInf` of an empty or unbounded-below set is the junk value `0`, so each lemma
carries exactly the side conditions its proof consumes, which is not always
both of `Set.Nonempty` and `BddBelow`. A later commit discharges both for the
cdf of a probability measure at a level in `(0, 1)`.
Prior art: `Mathlib/Order/SemiconjSup.lean` defines `IsOrderRightAdjoint` as a
supremum over a sub-level set. That is the order dual, the upper generalized
inverse, and neither definition unfolds to the other.
…ug-in identity Add the adjunction `lowerQuantile F p <= x <-> p <= F x` for `F` monotone and right continuous at the quantile, its strict form, attainment `p <= F (lowerQuantile F p)`, and the plug-in identity `F (lowerQuantile F p) = p` under continuity. Add the witness `jumpAtZero` and three lemmas refuting the weakened forms of attainment, the forward half of the adjunction, and the plug-in identity. They are stated as `not (forall ...)` rather than as existentials, so each records that the weakened lemma is false rather than that a bad case exists.
…junction Specialize to the cdf of a measure: the quantile set is nonempty at every level below one and bounded below at every level above zero, so the adjunction holds at `0 < p < 1` with no remaining side condition. Add three lemmas recording that the bundled `GaloisConnection` packaging is not reachable here. The quantile set of a cdf is unbounded below at level zero and empty at level two, so the bundled conclusion is false. Five of these lemmas take a general measure rather than a probability measure. Their proofs consume only `tendsto_cdf_atBot` and `tendsto_cdf_atTop`, both of which hold without `IsProbabilityMeasure`. The three probability-measure-facing lemmas keep the instance under `@[nolint unusedArguments]`, so that the API a user reaches for still says what it is about. The docstring at `lowerQuantile_cdf_le_iff` states the choice and invites the reviewer to ask for the general form instead.
…iance Add left continuity of the lower quantile in the level, uniqueness under strict monotonicity, existence on an interval via the intermediate value theorem, and equivariance under an `OrderIso` of the reals in both functional and pushforward form. The cdf specialization of left continuity keeps `IsProbabilityMeasure` under `@[nolint unusedArguments]`, matching the probability-measure-facing lemmas of the previous commit. The equivariance lemmas keep it because their proofs do consume it, through `Measure.isProbabilityMeasure_map`.
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
|
LLM-generated |
github-actions
Bot
added
the
LLM-generated
PR summary 1bfd2e2ec4Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (weak) |
|---|---|---|
| 5048 | 1 | exposed public sections |
Current commit 1bfd2e2ec4
Reference commit 4d6f98930f
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).
github-actions
Bot
added
the
t-measure-probability
1 participant
This adds
ProbabilityTheory.lowerQuantile, the lower quantile function(the generalized inverse of a cdf-like monotone function on ℝ), with the
order core, the Galois connection under right-continuity, the plug-in
identity, left-continuity in the level, uniqueness, equivariance under
order isomorphisms, and the specialization to
cdf μwhere both standingside conditions become theorems.
This adds the LOWER QUANTILE FUNCTION, that is the generalized inverse of a cdf-like
monotone function on
ℝ, in a new fileMathlib/Probability/Quantile.leanbesideMathlib/Probability/CDF.lean.What it adds
ProbabilityTheory.quantileSet F p = {x | p ≤ F x}andProbabilityTheory.lowerQuantile F p = sInf (quantileSet F p), with:csInfbounds;p ≤ F (lowerQuantile F p)under monotonicity and right continuity;lowerQuantile F p ≤ x ↔ p ≤ F x, and its strict form;F (lowerQuantile F p) = punder continuity;OrderIso ℝ ℝ, in both functional and pushforward form;cdf μfor a probability measure at0 < p < 1, where bothstanding side conditions become theorems.
Why
sInfof an empty or unbounded-below set is Lean's junk value0. A quantile lemmastated without
Set.NonemptyandBddBelowis therefore either false or accidentallytrue of the junk value, and a reader cannot tell which. Every general lemma here carries
both by name, and the cdf section discharges both from the limits of the cdf at
atBotand
atTop. That discharge is what makes the general statements non-vacuous.Three lemmas record that the continuity hypotheses are load bearing, stated as
¬ ∀ ...rather than as existentials. An existential says a bad case exists; the negateduniversal says the weakened lemma is FALSE, which is what a reader asking "is this
hypothesis decorative" actually wants. The witness is a monotone step function that is
left continuous at its jump: monotone, bounded, well behaved quantile set, and not right
continuous, which alone breaks attainment, the forward half of the adjunction, and the
plug-in identity.
not_galoisConnection_lowerQuantile_cdfis included deliberately as a NEGATIVE result.The bundled
GaloisConnectionpackaging quantifies over all levels, and a cdf has anunbounded quantile set at level
0and an empty one at level2, so the bundledconclusion is false for every probability measure. Reaching the cdf case would need the
level indexed by the open unit interval as a subtype. I would rather state that boundary
than let a reader discover it.
What it depends on
Mathlib.Probability.CDFfor the cdf and its monotonicity and limits;Mathlib.Topology.Order.IntermediateValue;Mathlib.Topology.Order.MonotoneContinuity;Mathlib.Order.ConditionallyCompleteLattice.Indexed. No new axioms: every declarationreports exactly
propext,Classical.choice,Quot.sound.Prior art, named because a reviewer will find it
Mathlib/Order/SemiconjSup.leandefinesIsOrderRightAdjoint f g := ∀ y, IsLUB {x | f x ≤ y} (g y), built byisOrderRightAdjoint_csSupas a supremum over aSUB-level set. That is the order-dual construction, the UPPER generalized inverse; the
two functions are different and neither definition unfolds to the other. Its file is
about circle homeomorphisms, which is why searching for "quantile" does not find it.
GaloisConnectionis used rather than reinvented.There is no existing
quantilein mathlib: zero case-insensitive hits across the tree.medianexists but is the median of a simplex in affine geometry, a different word in adifferent subject.
Generality, stated rather than left to review
Everything is at
F : ℝ → ℝ. Running mathlib's environment linters locally flagged[IsProbabilityMeasure μ]as unused in nine cdf-facing declarations. Five (the twoside-condition dischargers and the three negative results) are generalized: they now
hold for the cdf of any measure, since the cdf's limit lemmas hold unconditionally.
Four convenience wrappers (
lowerQuantile_cdf_le_iff,lowerQuantile_cdf_mono,le_cdf_lowerQuantile,continuousWithinAt_lowerQuantile_cdf_Iic) KEEP the instanceunder
@[nolint unusedArguments], deliberately: for a non-probability measure,cdf μis a normalizing construction, so the generalized statements would beaccidentally true of the construction rather than of the object the name suggests,
which is the failure mode the Why section above exists to avoid. If reviewers prefer
the fully general forms, I am happy to drop the instances; the proofs do not use
them. Two declarations (
cdf_map_orderIso,lowerQuantile_cdf_map) consume theinstance and keep it.
The ORDER CORE generalizes to a
ConditionallyCompleteLinearOrderdomain with aPreordercodomain with proof terms UNCHANGED, and I have checked that rather thanassumed it. Two caveats found while checking, which is why I would rather do it as a
follow-up than fold it in here:
apply_lt_of_lt_lowerQuantileneeds a LINEAR codomain, since it goes from¬ (p ≤ F x)toF x < p.exists_apply_lt_of_bddBelowis FALSE withoutNoMinOrderon the domain. Overℝitis proved by exhibiting
b - 1; on a domain with a least element, a constantFatlevel
phas a quantile set that is everything, is bounded below, and has no pointwith
F a < p.The TOPOLOGICAL layer does not transcribe:
tendsto_lowerQuantile_nhdsLTtakes themidpoint
(c + q) / 2, which uses the field structure, and a general version needsDenselyOrdered. Happy to do the generalization in a follow-up, or in this PR if areviewer prefers it landed general the first time.
Open, and not claimed
The UPPER quantile and the lemmas relating the two; the probability integral transform;
Measure.mapalong a general measurable monotone function rather than an orderisomorphism; and a
GaloisConnectionpackaging indexed by the open unit interval thatwould reach the cdf case.
AI disclosure
-Ran aggressive adversarial review process on each agents work with a separate agent; A hostile-reviewer pass, refutation lemmas proving the hypotheses are load bearing, and a certified negative result for the packaging that does not work. The corrections forced by this process are in the file and history.