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
4 open pull requests (0 with relevant labels)
Other
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
6 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
- feat(Tactic): convert now discharges side goals at reducible transparency #39039
- experiment: have `LinearMap` extend `DistribMulActionHom` #40001
- refactor: rename `MulAction` to `MonoidAction` #43404
1 open pull request (0 with relevant labels)
4 open pull requests (0 with relevant labels)
Other
1 open pull request (0 with relevant labels)
1 open pull request (0 with relevant labels)
2 open pull requests (0 with relevant labels)
13 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
- feat: use `max`/`min` for `union`/`intersection` in `Set`, `Finset`, `ZFSet`, `Class` #42316
- refactor: replace `SemilatticeSup.sup` with `max` #43472
- feat: `@[gcongr]` for `eq_top_mono` and friends #44334
- chore: golf using new `@[gcongr]` lemmas #44335
- chore: adaptations for stronger `simpNF` - part 1 #44554
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
- 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(SimpleGraph/Connectivity/EdgeConnectivity): morphism lemmas for edge reachability/connectivity #43823
- feat(SetTheory/Cardinal/Finite): simp lemmas for `[E]Nat.card` #44408
- feat(Linter/Style): lint against `∀ᵉ`/`∃ᵉ` #44544
10 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(Data/Set): add `Set.diag` #38380
- refactor: turn `Set` into a 1-field structure #39211
- feat: `Pi.map` rename to `Function.map` #39233
- chore(Data/Set): move lemmas from `Set.Disjoint` to `Disjoint` #41913
- refactor: rename the `diag` name token to `diagonal` #43494
No open pull requests.
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)
12 open pull requests (0 with relevant labels)
Other
- feat(Topology/MetricSpace/Pseudo/Defs): add easy lemma about opens in topological spaces #26994
- 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
- chore: remove backward.privateInPublic by wrapping proofs with private_decl% #44032
- chore(Topology): deprecate `UniformSpace.ball` in favor of `SetRel.ball` #44887
- WIP: Feat/positivity lemma #44923
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.