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
- feat: try using grind as gcongr discharger #37688
- test: insert `@[informal]` attributes from overview #38195
No open pull requests.
No open pull requests.
8 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(Analysis/TemperedDistribution): polynomially bounded locally integrable functions define tempered distributions #36595
- refactor(Order): make completeness typeclasses mixins #38537
- feat: fun_prop for integrability #39323
13 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
- refactor: change the definition of stoppedValue #43185
- feat: strong measurability of a path-valued random variable #43358
- refactor: replace `SemilatticeSup.sup` with `max` #43472
- chore: more filter generalizations in tsum/tprod lemmas #44511
2 open pull requests (1 with relevant labels)
Relevant
10 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
1 open pull request (0 with relevant labels)
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`/`intersection` in `Set`, `Finset`, `ZFSet`, `Class` #42316
- feat(MeasureTheory): generalize `MeasurePreserving` to `AEMeasurable` #43489
- chore: rename `nonzero` to `ne_zero` in theorem names #44824
No open pull requests.
11 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
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.