Upstreaming dashboard
The eventual goal of the MeanFourier project is to be fully upstreamed to Mathlib.
As such, it is crucial to continuously organise upstreaming from MeanFourier to Mathlib.
The way we organise this is with the following two lists,
showing files with no MeanFourier dependencies depending on whether they contain sorry or not.
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: mean-fourier
2 open pull requests (0 with relevant labels)
6 open pull requests (0 with relevant labels)
Other
- feat(Tactic/Push): add basic tags and tests #29000
- feat(Combinatorics/Schnirelmann): prove Mann's theorem #38077
- chore: remove trailing semicolons #41695
- feat(Algebra/Group/Action/Pointwise/Set/Basic): `mul_mem_smul_set` #42646
- refactor: rename `MulAction` to `MonoidAction` #43404
- refactor(Logic/Pairwise): define more general pairwise based on mem, change old pairwise into pairwise' #43635
7 open pull requests (0 with relevant labels)
Other
- chore: fix naming of `mono` and `monotone` #26911
- chore: dedent `to_additive` docstrings #28298
- feat(Tactic/Push): add basic tags and tests #29000
- refactor (Algebra.Group.Defs): add npow/zpow/nsmul/zsmul as fields of new parents classes #29482
- experiment(Algebra): unbundle npow/zpow from Monoid/InvDivMonoid #29605
- feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` #30042
- refactor: rename `MulAction` to `MonoidAction` #43404
7 open pull requests (0 with relevant labels)
Other
- refactor(*): migrate from `Matrix.toLin'` to `Matrix.mulVecLin` #25012
- WIP: experiments with vertex algebras #25822
- fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) #27403
- refactor(Algebra): add type-classes for algebraic properties of `FunLike` #33477
- feat(Tactic): convert now discharges side goals at reducible transparency #39039
- experiment: have `LinearMap` extend `DistribMulActionHom` #40001
- refactor: rename `MulAction` to `MonoidAction` #43404
No open pull requests.
5 open pull requests (0 with relevant labels)
Other
- chore(MeasureTheory/Integral/Lebesgue/Basic): fix an `erw` #40392
- chore: replace terminal `convert` with `exact` #41762
- feat(Data/Set/Card): cardinality of complement and difference #43424
- chore: lake shake --add-public --keep-implied --keep-prefix --fix #43782
- chore: rename `ENNReal.toReal_mono'` #43856
1 open pull request (0 with relevant labels)
1 open pull request (0 with relevant labels)
2 open pull requests (0 with relevant labels)
8 open pull requests (0 with relevant labels)
Other
- chore: make `finiteness` a default tactic #26090
- feat: Dedekind completion of rationals is isomorphic to EReal #37071
- refactor(Order): make completeness typeclasses mixins #38537
- feat(EReal): simplify nat + ⊤ #38979
- feat(Data/{ENat,ENNReal,EReal}): missing coercion lemmas #41101
- feat: integral of EReal-valued functions #41549
- style: eta reduce in proofs #41875
- refactor: remove `DecidableEq` and `DecidableLT` from `LinearOrder` #42577
2 open pull requests (0 with relevant labels)
14 open pull requests (0 with relevant labels)
Other
- feat: grind tags for set operations #27683
- feat(Tactic/Push): add basic tags and tests #29000
- feat(push): `@[push]` attributes for `∈` in `Set`, `Finset` and `Multiset` #30042
- bench: lean4#10832 #30642
- bench: before lean4#10832 #30643
- (WIP) Separation axioms #32865
- chore: tag set lemmas with @[push] #38853
- refactor: turn `Set` into a 1-field structure #39211
- refactor(Data): make `Set` a one-field structure #41506
- feat: use `max`/`min` for `union`/`intersection` in `Set`, `Finset`, `ZFSet`, `Class` #42316
- refactor: replace `SemilatticeSup.sup` with `max` #43472
- chore: delete deprecated declarations to March 2026 #44240
- feat: `@[gcongr]` for `eq_top_mono` and friends #44334
- chore: golf using new `@[gcongr]` lemmas #44335
15 open pull requests (0 with relevant labels)
Other
- feat: more linting of cdots #12411
- feat(Topology/Instances/ENat): ENat and tsum #23503
- chore: fix links #27709
- chore(Data/Finset/Card): rename `pred_card_le_card_erase` to `sub_one_card_le_card_erase` #36832
- feat: integral of the binomial distribution #37531
- feat(NumberTheory/ArithmeticStatistics/Reducible): Counting reducible polynomials #37663
- chore(Data/Set/Finite/Basic): fix `Fintype ({a} : Set α)` instance #38870
- refactor: turn `Set` into a 1-field structure #39211
- chore(Data): refactor proofs where `grind?` fails #39808
- refactor(Data): make `Set` a one-field structure #41506
- feat(ModelTheory): add counting formulas #42025
- feat(ModelTheory/ElementaryMaps): preserve definable-set cardinality #42026
- feat(ModelTheory): construct a counterexample to the two-cardinal phenomenon #42190
- feat(Data/Set/Card): cardinality of complement and difference #43424
- feat(SimpleGraph/Connectivity/EdgeConnectivity): morphism lemmas for edge reachability/connectivity #43823
12 open pull requests (0 with relevant labels)
Other
- feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring. #25902
- feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring #25903
- chore: fix links #27709
- feat(Tactic/Push): add basic tags and tests #29000
- perf: remove some `aesop`s and `grind`s #35738
- feat(Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system #36160
- feat(Data/Set): add `Set.diag` #38380
- refactor: turn `Set` into a 1-field structure #39211
- feat: `Pi.map` rename to `Function.map` #39233
- refactor(Data): make `Set` a one-field structure #41506
- chore(Data/Set): move lemmas from `Set.Disjoint` to `Disjoint` #41913
- refactor: rename the `diag` name token to `diagonal` #43494
2 open pull requests (0 with relevant labels)
2 open pull requests (0 with relevant labels)
3 open pull requests (0 with relevant labels)
3 open pull requests (0 with relevant labels)
2 open pull requests (0 with relevant labels)
13 open pull requests (0 with relevant labels)
Other
- feat(Topology/MetricSpace/Pseudo/Defs): add easy lemma about opens in topological spaces #26994
- feat(Basic/Rel): balls #33077
- chore(EMetric/*): rename theorems #34096
- feat(Mathlib/Analysis/PDE/Quasilinear/Characteristics): the method of characteristics for first order quasilinear PDEs #34134
- chore(Topology): refactor proofs where `grind?` fails #39769
- feat(Tactic): automatic positivity attribute #41895
- refactor: rename Function.swap #42282
- chore: use `private` proof elaborator to remove `set_option backward.privateInPublic` #42755
- chore: linters for identifying `backward.privateInPublic` removal opportunities #42756
- feat: tag `Metric.closedBall_subset_ball` with `@[gcongr strict]` #43419
- doc(Topology): `wikidata` tags for some basics #43669
- chore: lake shake --add-public --keep-implied --keep-prefix --fix #43782
- chore: remove backward.privateInPublic by wrapping proofs with private_decl% #44032
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.