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
5 open pull requests (0 with relevant labels)
Other
12 open pull requests (0 with relevant labels)
Other
- refactor(Analysis/Normed*): use `RingHomIsometric` for `*.norm_cast` #6931
- chore: migrate to `tfae` block tactic #11003
- feat: more linting of cdots #12411
- feat: a norm_num extension for complex numbers #26975
- chore: reduce `Topology` imports in `Data` #29012
- refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` #29354
- chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` #31607
- feat(RCLike): add `Continuous.re` and similar #34419
- feat(Tactic/Linter): linter for comments that should become docstrings #36636
- fix(Tactic/Continuity): mark Continuous.comp' as unsafe #36806
- perf(Algebra/Ring): faster Ring.toAddGroupWithOne instance #38017
- chore(Data/Real): encapsulate real numbers #38702
3 open pull requests (0 with relevant labels)
Other
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
- feat: use `to_dual` for `HeytingAlgebra` #33543
- chore: do not use `inf` `sup` in `LinearOrder` lemmas #35881
- feat(Translate): copy `alias` and `deprecated` attributes #40503
No open pull requests.
1 open pull request (0 with relevant labels)
3 open pull requests (0 with relevant labels)
6 open pull requests (0 with relevant labels)
Other
- feat: port ge_or_gt linter from mathlib3 #12879
- chore: replace some use of > or ≥ by < or ≤ #12933
- feat(Tactic/Push): add basic tags and tests #29000
- feat(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas #38193
- chore: deprecate duplicate theorems about `IsBotZeroClass` #38663
- chore: replace `by calc` by `calc` whenever possible #40292
3 open pull requests (1 with relevant labels)
Relevant
3 open pull requests (0 with relevant labels)
Other
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(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas #38193
- wip, chore: rename Directed -> Predirected [please-adopt] #38792
- feat(MeasureTheory): use `IsApply` for `SimpleFunc` #40918
- refactor: use `Function.prod` instead of anonymous version #41147
- feat(MeasureTheory): use `IsApply` for `Measure` #41177
1 open pull request (0 with relevant labels)
8 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: fun_prop for integrability #39323
- feat(FunProp): tag integrableOn #39325
9 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
- feat(MeasureTheory): weaken hypotheses on the continuity-multiplication and xˢ·exp(-xᵖ) integrability lemmas #40587
- chore: remove redudant `nonrec`'s #41259
1 open pull request (0 with relevant labels)
2 open pull requests (0 with relevant labels)
5 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
- refactor: use `Function.prod` instead of anonymous version #41147
- feat(MeasureTheory): use `IsApply` for `Measure` #41177
No open pull requests.
14 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/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): ConditionallyCompleteSemiLatticeInf #38192
- refactor(Order/(Conditionally)CompletePartialOrder): extends `OrderSupSet` #38444
- refactor(Order): make completeness typeclasses mixins #38537
- chore(ConditionallyCompleteLattice/Indexed): dualize #38938
- chore: remove @[expose] from def-free public sections #39388
- feat(Topology/Order): convergence of suprema and infima #40578
- chore(Order): add to_dual tags in Mathlib/Order/ConditionallyCompleteLattice/Indexed #40584
- feat: holder continuity of suprema and infima #40585
- feat(Order/ConditionallyCompleteLattice): antitone versions of `sSup (f '' s)` lemmas #41273
14 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(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
- feat(Topology/Order): convergence of suprema and infima #40578
- chore(Order): add to_dual tags in Mathlib/Order/ConditionallyCompleteLattice/Indexed #40584
- feat: holder continuity of suprema and infima #40585
1 open pull request (0 with relevant labels)
No open pull requests.
No open pull requests.
1 open pull request (0 with relevant labels)
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.
1 sorry