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
3 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
- refactor: rename `MulAction` to `MonoidAction` #32737
- 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
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` #32737
10 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: 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
- feat(LinearAlgebra): dual of tensor is tensor of duals for finite projective modules #41479
2 open pull requests (0 with relevant labels)
13 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: replace terminal `convert` with `exact` #41762
- style: eta reduce in proofs #41875
- chore: rename Directed to Predirected #42290
- feat: add diagonal iSup and iInf lemmas #42339
1 open pull request (0 with relevant labels)
1 open pull request (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
1 open pull request (0 with relevant labels)
4 open pull requests (0 with relevant labels)
Other
12 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
- refactor(Data): make `Set` a one-field structure #41506
- feat: `IsLocallyClosedAt` predicate #42196
- feat: use `max`/`min` for `union`/`intersection` in `Set`, `Finset`, `ZFSet`, `Class` #42316
14 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
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
- 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
- refactor(Data): make `Set` a one-field structure #41506
- chore(Data/Set): move lemmas from `Set.Disjoint` to `Disjoint` #41913
2 open pull requests (0 with relevant labels)
15 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(Analysis/InnerProductSpace/TensorProduct): add TensorProduct.congrL #40846
- feat(Topology): use `FComp` in `ContinuousLinearMap` #41224
- feat: constructions of Fredholm operators #41602
- feat: add a wrapper around `fun_prop` that calls `simp` on the function #42398
- feat: characterize Fredholm projections #42689
- feat: a continuous linear map is invertible iff it is an homeomorphism #42698
- feat: the set of Fredholm operators between two Banach spaces is open #42742
- 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)
9 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
- wip header cleanup #42582
- chore: use `private` proof elaborator to remove `set_option backward.privateInPublic` #42755
- chore: linters for identifying `backward.privateInPublic` removal opportunities #42756
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.