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
2 open pull requests (0 with relevant labels)
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
- refactor(Order): make completeness typeclasses mixins #38537
- feat: fun_prop for integrability #39323
- feat(FunProp): tag integrableOn #39325
15 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
- refactor: change the definition of stoppedValue #43185
- feat: strong measurability of a path-valued random variable #43358
- refactor: replace `SemilatticeSup.sup` with `max` #43472
- feat(Tactic/Linter/Multigoal): lint on superfluous focusing dots #43992
5 open pull requests (1 with relevant labels)
Relevant
Other
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
- feat(Topology/Compactness/CompactSystem): set system of countable intersections of sets in a compact system is again a compact system #36225
- 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
1 open pull request (0 with relevant labels)
9 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
- chore: split too long file Measure.MeasureSpace #42943
- chore: deprecate Measure.MeasureSpace #42944
- feat(MeasureTheory): generalize `MeasurePreserving` to `AEMeasurable` #43489
10 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: replace terminal `convert` with `exact` #41762
- chore: split too long file Measure.MeasureSpace #42943
- chore: deprecate Measure.MeasureSpace #42944
- feat(MeasureTheory): generalize `QuasiMeasurePreserving` to `AEMeasurable` #43191
- feat(Measure/Prod): add map_prod_map_of_aemeasurable #43485
- feat(MeasureTheory): generalize `MeasurePreserving` to `AEMeasurable` #43489
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.
2 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.