Upstreaming dashboard
Files ready to upstream
The following files are sorry-free and do not depend on any other file, meaning they can be readily PRed to Mathlib.
PRs are grouped as 'relevant' if they contain the following label: carleson
6 open pull requests (0 with relevant labels)
Other
- lint also `let` vs `have` #12181
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- feat: add convolution_comp_add_right #32169
- chore: golf using .ne and friends #37553
- test: insert `@[informal]` attributes from overview #38195
- feat: use `Is*Apply` classes for continuous linear maps #38561
No open pull requests.
No open pull requests.
No open pull requests.
5 open pull requests (0 with relevant labels)
Other
- feat: use ` binderNameHint` in sum_congr #24957
- feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` #30042
- chore: make OrderDual a structure #35125
- chore: do not use `inf` `sup` in `LinearOrder` lemmas #35881
- chore(Data/Finset/Lattice/Fold): rename `comp_sup_*` to `apply_sup_*` #37185
No open pull requests.
1 open pull request (0 with relevant labels)
2 open pull requests (0 with relevant labels)
8 open pull requests (0 with relevant labels)
Other
- chore: attribute [induction_eliminator] #12605
- chore(MeasureTheory): use `0` instead of `const _ 0` #24060
- feat(Tactic/Push): add basic tags and tests #29000
- feat: generalize argument of `IsOrderedMonoid` from `CommMonoid` to `CommSemigroup` #36824
- feat(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas #38193
- feat(GRewrite): new `grw` implementation #38318
- wip, chore: rename Directed -> Predirected [please-adopt] #38792
- feat(GRewrite): strict rewriting #38868
No open pull requests.
7 open pull requests (2 with relevant labels)
Relevant
Other
- feat: integrals and integrability with .re #17176
- refactor: unbundle algebra from `ENormed*` #28803
- feat(MeasureTheory): add `MemLp.Const` class and instances to unify `p = ∞` and `μ.IsFiniteMeasure` cases #30030
- perf: unbundle algebra from `ENormed*`, April 2026 version #38032
- feat: `locallyIntegrableOn_smul_iff` #39217
1 open pull request (0 with relevant labels)
3 open pull requests (0 with relevant labels)
1 open pull request (0 with relevant labels)
No open pull requests.
15 open pull requests (0 with relevant labels)
Other
- chore: refactor WithBot/WithTop as structures #27918
- feat: map a seminorm along a surjective linear map #34106
- refactor: use `OrderSupInfSet` #35263
- feat(Mathlib/Data/Finset/Mex): `sInf sᶜ ≤ s.encard` #35669
- refactor: use `OrderSupSet` in `ConditionallyCompleteLattice` #35674
- feat(Order/ConditionallyCompleteLattice): `sSup (f '' s) ≤ f (sSup s)` #35822
- feat(Order/OrdContinuous): every map between complete lattices that preserves sSup is a left adjoint of some Galois connection #37683
- feat(Topology/Order): provide lemmas linking topological continuity to order continuity #37684
- feat(Order/ConditionallyCompleteLattice/Basic): `ConditionallyCompleteLinearOrderBot (WithBot α)` #37784
- feat(Order/SuccPred/CompleteLinearOrder): generalize `csSup_mem_of_not_isSuccLimit` #38142
- feat(Order/ConditionallyCompleteLattice): ConditionallyCompleteSemiLatticeInf #38192
- refactor(Order/(Conditionally)CompletePartialOrder): extends `OrderSupSet` #38444
- refactor(Order): make completeness typeclasses mixins #38537
- feat(Order/ConditionallyCompleteLattice/Basic): more `WithTop` instances #38890
- chore(ConditionallyCompleteLattice/Indexed): dualize #38938
12 open pull requests (1 with relevant labels)
Relevant
Other
- refactor: use `OrderSupInfSet` #35263
- refactor: use `OrderSupSet` in `ConditionallyCompleteLattice` #35674
- chore: do not use `inf` `sup` in `LinearOrder` lemmas #35881
- feat(Order/ConditionallyCompleteLattice/Indexed): `iSup` of `sup`s vs `sup` of `iSup`s #36169
- feat(Tactic/Linter): lint against `simpa ... using by tactic` #36496
- refactor(Order/(Conditionally)CompletePartialOrder): extends `OrderSupSet` #38444
- refactor(Order): make completeness typeclasses mixins #38537
- feat(Order/ConditionallyCompleteLattice/Indexed): `≤` version of `ciSup_or'` for `ConditionallyCompleteLattice` #38855
- feat(Order/ConditionallyCompleteLattice/Indexed): `iSup_iSup_eq_{left/right}` for `ConditionallyCompleteLinearOrderBot` #38856
- feat(Order/CompleteLattice/Basic): tag `iSup_of_empty'` with `@[simp]` #38859
- chore(ConditionallyCompleteLattice/Indexed): dualize #38938
No open pull requests.
No open pull requests.
Files easy to unlock
The following files do not depend on any other file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.