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)
8 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
- chore(Algebra/Group/Action/Pointwise/Set): generalize smul_mem_smul_set_iff to IsLeftCancelSMul #42614
- feat(Algebra/Group/Action/Pointwise/Set/Basic): `mul_mem_smul_set` #42646
- refactor: rename `MulAction` to `MonoidAction` #43404
- chore: use `congr()` much more widely #43408
- feat(Pointwise/Finset): generalise smul_finset lemmas #43455
8 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
- chore: use `congr()` much more widely #43408
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.
2 open pull requests (0 with relevant labels)
1 open pull request (0 with relevant labels)
1 open pull request (0 with relevant labels)
2 open pull requests (0 with relevant labels)
9 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
- chore: use simp instead of norm_num where simp suffices #43035
2 open pull requests (0 with relevant labels)
11 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
17 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(Data/Set/Card): characterize finite lower bounds on encard #42024
- 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(Combinatorics/SimpleGraph/Connectivity): change IsEdgeReachable and IsEdgeConnected to accept ENat instead of Nat #43346
- feat(Data/Set/Card): cardinality of complement and difference #43424
- style: omit `<|` before `fun` #43522
13 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
- chore(Basic): move `FunLike` from Data #43253
- refactor: rename the `diag` name token to `diagonal` #43494
2 open pull requests (0 with relevant labels)
11 open pull requests (0 with relevant labels)
Other
- fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) #27403
- refactor: deprecate `ContinuousLinearMapClass` #33448
- refactor: deprecate `LinearIsometryClass` #33450
- feat: add instances of `LawfulInv` #33810
- fix(Tactic/FunProp): do not unfold semireducible definitions in the presence of projections #35548
- feat: flip arguments for continuous linear maps under finite dimension assumptions #36775
- chore(Topology/Algebra): rename .equivOfInverse to .ofContinuousLinearMap #40841
- feat(Topology): use `FComp` in `ContinuousLinearMap` #41224
- fix(Tactic/FunProp): apply theorems at reducible transparency #42330
- feat: add a wrapper around `fun_prop` that calls `simp` on the function #42398
- chore(Algebra/Module/Equiv): add deprecated module for `/Equiv.lean` #42822
1 open pull request (0 with relevant labels)
2 open pull requests (0 with relevant labels)
1 open pull request (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
- 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(Tactic): general tactic to translate `(E)NNReal`, `ENat`, `PNat` goals to `Real` and `Nat` #43254
- feat: tag `Metric.closedBall_subset_ball` with `@[gcongr strict]` #43419
- chore(Tactic): deprecate `pnat_to_nat` and `enat_to_nat` in favor of `basify` #43422
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.