Repository navigation
Conversation
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 Zulip and join the Lean community. |
PR summary ee8119aacaImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (weak) |
|---|---|---|
| 5081 | 1 | exposed public sections |
Current commit ee8119aaca
Reference commit 850e737494
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.py 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).
…ecaying sequences
For a real sequence a with |a k| <= C * r ^ k and 0 <= r < 1, the Cesaro
means n^-1 * sum_{k < n} a k tend to zero. The file gives the explicit
rate bound first,
abs_sum_range_div_le_of_abs_le_geometric:
|n^-1 * sum_{k in range n} a k| <= (C / (1 - r)) * n^-1 for 1 <= n,
which is independently useful in error estimates, and obtains the limit
statement tendsto_sum_range_div_nhds_zero_of_abs_le_geometric as an
immediate squeeze.
The statements are a port of a lemma from a separate kernel-verified
formalization (Lean v4.33.1 + pinned Mathlib, 0 sorry / 0 warnings),
split there from a Markov-chain ergodic theorem for geometrically
contracting kernels - which is the motivation for the general shape:
Mathlib carries only specific instances (Probability/StrongLaw.lean,
Asymptotics/SpecificAsymptotics.lean).
Validated on this branch: lake build Mathlib.Analysis.SpecificLimits.Cesaro
completes with no errors, no warnings and no lint suggestions; downstream
usability probes for both lemmas compile.
…ueeze_zero_norm' proof, usage tests Extends the real-valued Cesaro bounds to their upstream-worthy shape: - norm_sum_range_smul_le_of_norm_le_geometric (PRIMARY, E-valued): for a : Nat -> E with ||a k|| <= C * r ^ k, 0 <= r < 1, the n-th Cesaro mean satisfies ||n^-1 * sum a k|| <= (C / (1 - r)) * n^-1; - tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric (PRIMARY): the Cesaro means tend to 0, via squeeze_zero_norm' on the explicit rate; - abs_sum_range_div_le_of_abs_le_geometric and tendsto_sum_range_div_nhds_zero_of_abs_le_geometric (R-corollaries, the previous commit's statements kept under their original names). MathlibTest/Cesaro.lean adds five worked usage examples (geometric sequence over R: bound + limit; the zero sequence; scaled-geometric sequences in a general normed space: bound + limit). Built against current master with the mathlib cache: 0 errors, 0 warnings (both files). Module-system notes: the norm notation needs Mathlib.Analysis.Normed.Group.Basic (and Continuity for squeeze_zero_norm') in the file's own public imports; Real's norm/abs instances are module-sealed, so the R corollaries bridge via an explicit Real.norm_eq_abs rewrite.
…add literature citations and the orbit-tile example Per review discussion: the two R-corollary theorems leave the module (the normed-space primaries specialize in one line) and re-enter the test file as full worked examples, keeping their classical statements available to users without adding upstream API surface. The test docstring now carries the literature references (Cesaro 1889; Hardy 1949, ch. I; Tserunyan, arXiv:1805.07365 - the orbit-tiling proof of the pointwise ergodic theorem consuming orbit-average measurability [Birkhoff 1931, PNAS 17]), and a constant-observable orbit example illustrates the uniform-tile case of the tiling lemma. Built against current master: 0 errors, 0 warnings (both files).
r-irbe
changed the title
…a Try-this suggestion that trips --iofail)
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adding this because the Cesaro-mean step appears inside ergodic and mixing arguments constantly + mathlib's
SpecificLimitsfiles do not carry it.It proves that a sequence has convergent Cesaro means with an explicit rate via the following four lemmas:
norm_sum_range_smul_le_of_norm_le_geometric:‖a k‖ ≤ C * r ^ k → ‖n⁻¹ • ∑ a k‖ ≤ (C / (1 - r)) * n⁻¹in any normed space;tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric: the means tend to zero, viasqueeze_zero_norm';The real-valued forms are worked out as full examples in
MathlibTest/Cesaro.lean, alongside further usage examples including the orbit-average case and serve as documentation for users :)Disclaimer: I used AI for proof golfing. Every proof is kernel-checked and I take full responsibility for the mathematics.