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
No open pull requests.
No open pull requests.
7 open pull requests (0 with relevant labels)
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(Analysis/TemperedDistribution): polynomially bounded locally integrable functions define tempered distributions #36595
- refactor(Order): make completeness typeclasses mixins #38537
- feat: fun_prop for integrability #39323
- chore: remove declarations deprecated between 2021-10-15 and 2026-04-15 #44886
10 open pull requests (0 with relevant labels)
Other
- 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
- chore: remove redudant haveI/letI in defs #41680
- chore: rename Directed to Predirected #42290
- refactor: change the definition of stoppedValue #43185
- refactor: replace `SemilatticeSup.sup` with `max` #43472
- chore: remove declarations deprecated between 2021-10-15 and 2026-04-15 #44886
- refactor(Algebra/Order/Archimedean/Basic): change `nat` → `natCast` in theorem statements #45003
- feat: use `IsApply` for `Measure` #45225
3 open pull requests (1 with relevant labels)
Relevant
12 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
- refactor(Order): make completeness typeclasses mixins #38537
- feat(IntervalIntegrable): add `fun_prop` support #38822
- feat: define contour integrals #39254
- chore: replace `by exact` occurences #40223
- chore: remove redudant `nonrec`'s #41259
- perf: remove `simp` from `sup_of_le_left` and friends #43436
- chore: tag definitions with `fun_prop` #44064
- perf(Linter/Multigoal): use `InfoTree.foldInfo` #44247
- chore: remove declarations deprecated between 2021-10-15 and 2026-04-15 #44886
- chore: rename `notation3` to `notation +delab` #45028
No open pull requests.
8 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: replace terminal `convert` with `exact` #41762
- chore: rename Directed to Predirected #42290
- feat: use `max`/`min` for `union`/`inter` in `Set`, `Finset`, `ZFSet`, `Class` #42316
- feat(MeasureTheory): generalize `MeasurePreserving` to `AEMeasurable` #43489
- refactor: deprecate `DivisibleBy` in favor of a `Prop`-valued typeclass #45297
No open pull requests.
15 open pull requests (0 with relevant labels)
Other
- 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
- chore: unexpose public sections with no defs #41564
- refactor: rename Function.swap #42282
- chore: rename Directed to Predirected #42290
- chore: remove superfluous `@[expose]` modifiers from public sections #43817
- feat(RingTheory): the associates of a UFD form a complete lattice #45020
- feat(Order): transfer instances for complete lattices #45249
- refactor(Order): generalise the `CompleteLattice` instance on `WithTop` #45250
- chore(Order/CompleteLattice): use `@[to_dual]` more #45253
No open pull requests.
5 open pull requests (1 with relevant labels)
Relevant
Other
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.