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 (1 with relevant labels)
Relevant
Other
2 open pull requests (0 with relevant labels)
No open pull requests.
No open pull requests.
10 open pull requests (2 with relevant labels)
Relevant
Other
- chore: make `finiteness` a default tactic #26090
- refactor: unbundle algebra from `ENormed*` #28803
- feat(MeasureTheory): add `MemLp.Const` class and instances to unify `p = ∞` and `μ.IsFiniteMeasure` cases #30030
- feat: define Sobolev Spaces #32305
- perf: unbundle algebra from `ENormed*`, April 2026 version #38032
- refactor(Order): make completeness typeclasses mixins #38537
- feat: fun_prop for integrability #39323
- feat(FunProp): tag integrableOn #39325
11 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(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas #38193
- wip, chore: rename Directed -> Predirected [please-adopt] #38792
- feat(MeasureTheory): use `IsApply` for `SimpleFunc` #40918
- feat(MeasureTheory): use `IsApply` for `Measure` #41177
- chore: remove redudant haveI/letI in defs #41680
- chore: rename Directed to Predirected #42290
- chore: split too long file Measure.MeasureSpace #42943
- chore: deprecate Measure.MeasureSpace #42944
5 open pull requests (1 with relevant labels)
Relevant
Other
8 open pull requests (0 with relevant labels)
Other
- refactor: unbundle algebra from `ENormed*` #28803
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- feat(Topology/Compactness/CompactSystem): set system of countable intersections of sets in a compact system is again a compact system #36225
- perf: unbundle algebra from `ENormed*`, April 2026 version #38032
- refactor(Order): make completeness typeclasses mixins #38537
- feat(IntervalIntegrable): add `fun_prop` support #38822
- feat: define contour integrals #39254
- chore: remove redudant `nonrec`'s #41259
1 open pull request (0 with relevant labels)
7 open pull requests (0 with relevant labels)
Other
- chore: make `finiteness` a default tactic #26090
- bench: review #39049
- chore: add missing `to_additive` docstrings #41628
- chore: rename Directed to Predirected #42290
- feat: use `max`/`min` for `union`/`intersection` in `Set`, `Finset`, `ZFSet`, `Class` #42316
- chore: split too long file Measure.MeasureSpace #42943
- chore: deprecate Measure.MeasureSpace #42944
7 open pull requests (0 with relevant labels)
Other
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore(MeasureTheory): remove all `erw` in `MeasureTheory` #40348
- chore(MeasureTheory/Measure/Prod): remove an `erw` #40409
- feat(MeasureTheory): use `IsApply` for `Measure` #41177
- chore: split too long file Measure.MeasureSpace #42943
- chore: deprecate Measure.MeasureSpace #42944
- feat(MeasureTheory): generalize `QuasiMeasurePreserving` to `AEMeasurable` #43191
No open pull requests.
12 open pull requests (0 with relevant labels)
Other
- feat: `gconvert` tactic #27135
- feat: map a seminorm along a surjective linear map #34106
- refactor: use `OrderSupInfSet` #35263
- refactor: use `OrderSupSet` in `ConditionallyCompleteLattice` #35674
- feat(Order/ConditionallyCompleteLattice): ConditionallyCompleteSemiLatticeInf #38192
- refactor(Order/(Conditionally)CompletePartialOrder): extends `OrderSupSet` #38444
- refactor(Order): make completeness typeclasses mixins #38537
- feat: holder continuity of suprema and infima #40585
- feat(Order/ConditionallyCompleteLattice): antitone versions of `sSup (f '' s)` lemmas #41273
- chore: unexpose public sections with no defs #41564
- refactor: rename Function.swap #42282
- chore: rename Directed to Predirected #42290
No open pull requests.
3 open pull requests (1 with relevant labels)
Relevant
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.