Upstreaming dashboard
The eventual goal of the MiscYD project is to not contain any significant new formalisation, but instead to act as a shallow layer over Mathlib showing concretely how to turn paper-combinatorics into Lean-combinatorics.
As such, it is crucial to continuously upstream code from MiscYD to Mathlib. The way we organise this is with the following two lists, showing files with no MiscYD dependencies depending on whether they contain the keyword sorry or not.
Files ready to upstream
The following files are sorry-free and do not depend on any other MiscYD, meaning they can be readily PRed to Mathlib.
MiscYD.Book.MetricBetweenMiscYD.PhD.VCDim.AddVCDimMiscYD.PhD.VCDim.NetMiscYD.Convexity.Refactor.StdSimplexMiscYD.Mathlib.Probability.CondVarMiscYD.Mathlib.MeasureTheory.MeasurableSpace.BasicMiscYD.Mathlib.MeasureTheory.Integral.Bochner.SetMiscYD.Mathlib.Combinatorics.SetFamily.ShatterMiscYD.AddCombi.Kneser.MulStabMiscYD.AddCombi.Corner.CombiDegen
Files easy to unlock
The following files do not depend on any other MiscYD file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.
MiscYD.Convexity.MinkowskiCaratheodory2 sorriesMiscYD.SetFamily.PosDiffs2 sorriesMiscYD.AddCombi.SliceRank2 sorriesMiscYD.AddCombi.Impact5 sorriesMiscYD.PhD.VCDim.Convex5 sorriesMiscYD.PhD.VCDim.UnifAP.Defs3 sorriesMiscYD.Convexity.Sperner.Sperner1 sorryMiscYD.Mathlib.GroupTheory.OrderOfElement1 sorryMiscYD.Mathlib.LinearAlgebra.AffineSpace.Combination2 sorriesMiscYD.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional1 sorryMiscYD.Mathlib.Analysis.Convex.Combination1 sorry