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)
5 open pull requests (0 with relevant labels)
Other
8 open pull requests (0 with relevant labels)
Other
- ignore this: Lean pr testing 9124 #26581
- 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` #32737
12 open pull requests (0 with relevant labels)
Other
- refactor(*): migrate from `Matrix.toLin'` to `Matrix.mulVecLin` #25012
- feat(Algebra/Module/Equiv/Basic): Restriction of scalars from a semilinear equivalence to a linear equivalence #25034
- WIP: experiments with vertex algebras #25822
- fix: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) #27403
- refactor: rename `MulAction` to `MonoidAction` #32737
- refactor(Algebra): add type-classes for algebraic properties of `FunLike` #33477
- chore(misc): fix typos #35896
- feat: @[simps] warns when generating defeq abusing lemmas #37528
- feat(Tactic): convert now discharges side goals at reducible transparency #39039
- experiment: have `LinearMap` extend `DistribMulActionHom` #40001
- refactor(Algebra/Module/Equiv): update name and refactor API ofLinearEquiv #40865
- feat(LinearAlgebra): dual of tensor is tensor of duals for finite projective modules #41479
2 open pull requests (0 with relevant labels)
12 open pull requests (0 with relevant labels)
Other
- chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. #14598
- refactor: Make ENNReal an abbrev #23509
- chore: make `finiteness` a default tactic #26090
- chore: fix naming of `mono` and `monotone` #26911
- feat: `GroupWithZero` versions of `le` lemmas #34120
- feat(Algebra/Order/Ring): replace ENNReal lemmas with WithTop versions #34674
- test(Tactic/Algebra): try to replace `ring` with algebra in many places #38637
- chore(MeasureTheory): remove all `erw` in `MeasureTheory` #40348
- chore(MeasureTheory/Integral/Lebesgue/Basic): fix an `erw` #40392
- chore(MulLECancellable): rename lemmas #41467
- chore: replace terminal `convert` with `exact` #41762
- style: eta reduce in proofs #41875
13 open pull requests (0 with relevant labels)
Other
- chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. #14598
- feat: Add type class for ENat-valued floor functions #15773
- feat(RingTheory/Valuation/PrimeMultiplicity): define `WithTop ℤ`-valued prime multiplicity on a fraction field #19596
- feat: Multiplicity and prime-adic valuation of derivations #19621
- feat(Topology/Instances/ENat): ENat and tsum #23503
- feat: replace `IsWellFounded` with `WellFounded` #35602
- refactor(Order): make completeness typeclasses mixins #38537
- chore(MeasureTheory/MeasurableSpace/Constructions): remove defEq abuse #40425
- chore: remove declarations deprecated between 2021-06-15 and 2025-12-15 #40618
- feat(RingTheory): characterizing lemma for rings of infinite Krull dimension #41073
- feat(RingTheory): a ring is nontrivial iff it has nontrivial Krull dimension #41074
- feat(RingTheory): krull dimension of a polynomial ring in an infinite number of variables #41098
- feat(Data/{ENat,ENNReal,EReal}): missing coercion lemmas #41101
No open pull requests.
9 open pull requests (0 with relevant labels)
Other
- chore: make `finiteness` a default tactic #26090
- feat(Dynamics/BirkhoffSum): add the maximal ergodic theorem #34031
- feat: Dedekind completion of rationals is isomorphic to EReal #37071
- refactor(Order): make completeness typeclasses mixins #38537
- feat(EReal): simplify nat + ⊤ #38979
- feat(Dynamics): pointwise ergodic theorem (via maximal inequality) #40178
- feat(Data/{ENat,ENNReal,EReal}): missing coercion lemmas #41101
- feat: integral of EReal-valued functions #41549
- style: eta reduce in proofs #41875
1 open pull request (0 with relevant labels)
4 open pull requests (0 with relevant labels)
Other
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
- chore(Data/Set): reduce defeq abuse of `Set α = α → Prop` #39110
- refactor: turn `Set` into a 1-field structure #39211
- chore: remove declarations deprecated between 2021-06-15 and 2025-12-15 #40618
- refactor(Data): make `Set` a one-field structure #41506
12 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
- chore(Order): infer `toDecidable*` in `*LinearOrder`s when possible #39908
- refactor(Data): make `Set` a one-field structure #41506
- style: add missing spaces #41942
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
- chore(Data/Set): reduce defeq abuse of `Set α = α → Prop` #39110
- refactor: turn `Set` into a 1-field structure #39211
- feat: `Pi.map` rename to `Function.map` #39233
- feat(Logic/Function/Defs): add `Function.diag` #41082
- refactor(Data): make `Set` a one-field structure #41506
- chore(Data/Set): move lemmas from `Set.Disjoint` to `Disjoint` #41913
No open pull requests.
3 open pull requests (0 with relevant labels)
9 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(fun_prop): 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(Analysis/InnerProductSpace/TensorProduct): add TensorProduct.congrL #40846
- feat(Topology): use `FComp` in `ContinuousLinearMap` #41224
1 open pull request (0 with relevant labels)
1 open pull request (0 with relevant labels)
1 open pull request (0 with relevant labels)
6 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
- refactor: reorganize Topology/EMetricSpace/Defs to generalise basic results #40510
- feat(Tactic): automatic positivity attribute #41895
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.