[CONFLICT] Sync upstream mathlib4 (2026-05-13)#7
Merged
Conversation
…measures (#39103) We show that the variation of vector measures satisfies the triangle inequality. As an application, we show that integrals are additive in vector measures and bilinear forms in #30230. Coauthored by @yoh-tanimoto. Created with the help of Codex.
…orm` (#38646) - rewrites `spectralValue_eq_zero_iff` via `eq_X_pow_iff_natDegree_le_natTrailingDegree` and `spectralValueTerms_of_lt_natDegree` - rewrites `spectralNorm.eq_of_normalClosure'` as two applications of `spectralNorm.eq_of_tower` - tidies `spectralNorm_unique` by switching the local transported structures to `set`/`letI`/`haveI` with `inferInstanceAs` Extracted from #37968 [](https://gitpod.io/from-referrer/)
… (#38884) - shortens `tendstoUniformlyOn_diff_iUnionNotConvergentSeq` by extracting the needed distance bound from `hx` with a single `not_lt.mp` argument, instead of unpacking `hx` via a long `simp`/`push Not` chain Extracted from #38104 [](https://gitpod.io/from-referrer/)
…CharacteristicFunction` (#39182) - moves the additive lemmas next to the finite-sum version they now reuse - shortens `characteristic_add_top_le` to a one-line `simpa` from `characteristic_sum_top_le` Extracted from #37968 [](https://gitpod.io/from-referrer/)
…… (#28546)
This PR adds a **group-generic** foundation for symbolic dynamics over an arbitrary group `G`, together with convenient specializations for `ℤ` and `ℤ^d`.
Summary of additions:
- **Full shift and shift action**
- `abbrev FullShift (A G) := G → A` (inherits product topology from the Π-type).
- Right shift `shift g x` with convention `(shift g x) h = x (h * g)`.
- **Cylinders and topology**
- `cylinder U x : Set (G → A)` for finite `U : Finset G`.
- Cylinders are open under `[DiscreteTopology A]`; with a finite alphabet they are also closed.
- Equality with dependent products:
`cylinder U x = Set.pi (↑U) (fun i => ({x i} : Set A))`, enabling use of the `Set.pi` API.
- **Patterns, occurrences, and subshifts**
- `Pattern A G` with finite `support : Finset G` and `data : support → A`.
- `Pattern.occursIn p x g` (occurrence at translate `g`) and the expected shift law.
- `forbids F` and `Subshift A G` (closed, shift-invariant subsets).
- `FixedSupport A G U` with an equivalence to `(U → A)` to obtain finiteness.
- **Language on finite shapes and counting**
- `languageOn X U`, `languageCardOn X U`, and `patternCountOn Y U`.
- **Entropy along a shape sequence**
- `limsupAtTop` (as an `sInf` of eventual upper bounds).
- `entropyAlong X F hF := limsup (log (patternCountOn X (F n) + 1) / |F n|)`
for any nonempty finite shapes `F : ℕ → Finset G` (the `+ 1` avoids `log 0`).
- **Specializations**
- `IntShapes`: segments `[-n,n]` on `Multiplicative ℤ`, with `entropy_Z`.
- `ZdShapes`: boxes `[-n,n]^d` on `ℤ^d` (as functions `Fin d → ℤ`), with `entropy_Zd`.
Mathematical remarks:
- The API is **shape-parametric**: entropy is defined along user-provided finite shapes.
- On **amenable** groups, using a **Følner** sequence yields a canonical value (Ornstein–Weiss).
This PR does not assume amenability; the family of shapes is an explicit input.
Motivation:
Provide a clean, reusable base for symbolic dynamics on groups in mathlib.
Future work:
- Add a Følner predicate and prove shape-independence / limit existence on amenable groups.
- Expand the `ℤ`/`ℤ^d` toolkit (alternative shapes, mixing, factors).
- Develop 1D theory and, longer-term, multidimensional SFT results (e.g. along the lines of Hochman–Meyerovitch).
Co-authored-by: Sfgangloff <silvere.gangloff@gmx.com>
Co-authored-by: Sfgangloff <37847888+Sfgangloff@users.noreply.github.com>
We also remove a redundant `ZeroLEOneClass Ordinal` instance (which can now be inferred via `CanonicallyOrderedAdd` → `IsBotZeroClass` → `ZeroLEOneClass`).
…#39238) This PR was automatically created from PR #28013 by @astrainfinita via a [review comment](leanprover-community/mathlib4#28013 (comment)) by @jcommelin. Co-authored-by: astrainfinita <19634778+astrainfinita@users.noreply.github.com>
This PR allows the use of `⊆` notation while the underlying constant is `≤`. Similarly for `⊂`/`<`, `⊇`/`≥` and `⊃`/`>`. - The idea is to later extend this feature to other set notation constants, such as union/intersection. - There are some types for which we cannot use `LE.le` as the underlying constant, such as `List` and `Multiset`. So, the elaborator for the `⊆` notation needs to make a decision which underlying constant to elaborate to, depending on the type. Sometimes the type is not known yet, which makes things awkward. Most of these cases are solved by delaying the elaboration until later when the type is known. - However, in some cases this doesn't work either, such as `simp_rw [and_comm (_ ⊆ _)]`, where it is impossible to tell the type when elaborating the term. So, some such cases need to be fixed by making it `simp_rw [and_comm ((_ : Set _) ⊆ _)]`. This is because `simp_rw`, unlike `rw`, fully elaborates the rewrite rules before using them. A linter warns you whever there is such an ambiguity. See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629
…egeneracy are "contractible" (#38346)
Remove the TODO list, since the have already been implemented on an instance. Co-authored-by: abeldonate <abeldm3108@gmail.com>
…#39038) In this PR, we construct Guitart exact squares which involve quotient categories.
…ra.IsIntegral` (#39070) Several results in `GoingUp.lean` assumed `IsIntegralClosure` when they only used `Algebra.IsIntegral`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…tion (#39237) This PR was automatically created from PR #28013 by @astrainfinita via a [review comment](leanprover-community/mathlib4#28013 (comment)) by @jcommelin. Co-authored-by: astrainfinita <19634778+astrainfinita@users.noreply.github.com>
…ing nondegenerate simplices (#38552) Given a simplicial set `X` and an object `R` in a preadditive category `C` (with coproducts), we introduce the chain complex `X.normalizedChainComplex R` which is a direct factor of `X.chainComplex R`, and is homotopy equivalent to it. The `n`-chains are coproducts indexed by nondegenerate `n`-simplices of `X` instead of all `n`-simplices. It follows that if `X` has dimension `< d`, then the homology of `X` vanishes in degrees `≥ d`. (This is an application of results previously obtained as part of the formalization of the Dold-Kan equivalence.)
…ne files (#38991) Follow-up to #38806: re-adds deprecation shims at the old paths for files moved into `LevelOne/` (so git rename detection in #38806 preserved blame). - [x] depends on: #38806 This PR was done with the help of Claude Code.
As required in our style guide; the linter was just not compliant.
The `fun_prop.lean` test file is rather meant to be literate documentation of fun_prop. One last addition to the file should moved to the main test file instead. While at it, document the main test file as being that. Developed at the ICERM workshop, in-person approved by `lecopivo`.
From Proetale.
…`comap (algebraMap R S)` (#37840) This PR switches over from `comap (algebraMap R S)` to `under`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
The implementation notes section references the Lean 3 namespace \`real.contfrac_legendre\`, but this was renamed to \`Real.ContfracLegendre\` during the port. This fixes the reference.
The new file is heavily based on `Hom.lean`, with some theorems removed for now.
Found by the linter in #27897, but I expect the move to Verso would also have discovered this.
There is no reason for this, and this makes it easier to lint them. Found by the linter in #27897.
This PR moves StacksAttribute.lean to CrossRefAttribute.lean both in Mathlib/Tactic/ and in MathlibTest/. In the future, we can refactor the file to abstract over the type of cross-references. Currently, cross-reference attributes are implemented for the Stacks Project and Kerodon. A good candidate for a future PR is to add an attribute for Wikidata identifiers.
Commenting `+LLM-generated` or `-LLM-generated` adds or removes the label.
From Sobolev spaces. Written by (some unspecified subset of) Floris, Filippo and me.
… `ContMDiffSection` (#39272) Its subject of study, bundled `C^n` sections, were generalised to `C^n` sections and renamed as `ContMDiffSection` a while ago. Rename the module to match.
They mostly were introduced in #39266; also fix the same grammar typo 'an homeomorphism' in the rest of mathlib.
…cAbove` for `i ≤ j` (#39170) - proves `(cycleIcc i j) ∘ j.succAbove = i.succAbove` for `i ≤ j`, giving the expected `succAbove` compatibility for `cycleIcc`
These are strictly speaking, required by markdown, and make it more clear to the reader that a new paragraph begins. This corrects some generated documentation entries to have proper paragraph breaks. Found by the linter in #27897.
From the Riemann mapping theorem project.
](https://gitpod.io/from-referrer/){kind=link}
2 tasks
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
20 participants
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.
Automated daily sync from
leanprover-community/mathlib4@master.1c1dadbc28517bb148fc05b9abc8659ce110d217The merge commit on this branch contains conflict markers, so CI will fail
and auto-merge will not run. Resolve manually:
Files with conflict markers
Note
Medium Risk
Medium risk due to a large upstream sync that adds new modules and modifies core algebra/category theory simp/
dsimpbehavior, which can cause non-local proof breakages and tactic loops.Overview
Automated upstream sync that adds several new modules (e.g.
SSet.normalizedChainComplexvia nondegenerate simplices, fixed-point classification forGL(2,ℝ)acting onℍwithPGL/PSLaction results, symbolic dynamics basics, chosen coends/explicit coends inType, and Guitart-exact quotient criteria) and wires them intoMathlib.lean.Also refactors/extends core APIs: new/updated simp lemmas around
symm_mkfor various equivs (Ring/Alg/Linear/Star), new injective/surjective facts forMonoidAlgebra.map, extra lemmas for uniform convergence and integrability, updates to localization/"under" API in algebraic geometry and Dedekind domain code, and multiple small doc/import cleanups plus a new GitHub workflow to apply labels from PR/issue comments.Reviewed by Cursor Bugbot for commit 34686d5. Bugbot is set up for automated code reviews on this repo. Configure here.