Move code to MiscYD

See https://github.com/YaelDillies/MiscYD.
YaelDillies · Feb 1, 2025 · b0ce14d · b0ce14d
1 parent 594b4b3
commit b0ce14d
Show file tree

Hide file tree

Showing 26 changed files with 2 additions and 3,143 deletions.
diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
@@ -1,7 +1,3 @@
-import LeanCamCombi.Archive.CauchyDavenportFromKneser
-import LeanCamCombi.ConvexityRefactor.Defs
-import LeanCamCombi.ConvexityRefactor.StdSimplex
-import LeanCamCombi.Corners.CombiDegen
 import LeanCamCombi.ExtrProbCombi.BernoulliSeq
 import LeanCamCombi.ExtrProbCombi.BinomialRandomGraph
 import LeanCamCombi.ExtrProbCombi.BollobasContainment
@@ -14,33 +10,14 @@ import LeanCamCombi.GrowthInGroups.Lecture1
 import LeanCamCombi.GrowthInGroups.Lecture2
 import LeanCamCombi.GrowthInGroups.Lecture3
 import LeanCamCombi.GrowthInGroups.Lecture4
-import LeanCamCombi.Impact
-import LeanCamCombi.Kneser.Kneser
-import LeanCamCombi.Kneser.KneserRuzsa
-import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup
-import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
-import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
-import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
-import LeanCamCombi.Mathlib.Order.Flag
-import LeanCamCombi.Mathlib.Order.RelIso.Group
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
-import LeanCamCombi.Mathlib.Topology.MetricSpace.MetricSeparated
-import LeanCamCombi.MetricBetween
-import LeanCamCombi.MinkowskiCaratheodory
-import LeanCamCombi.Multipartite
-import LeanCamCombi.PhD.VCDim.AddVCDim
-import LeanCamCombi.PhD.VCDim.HausslerPacking
-import LeanCamCombi.PhD.VCDim.HypercubeEdges
 import LeanCamCombi.PlainCombi.LittlewoodOfford
 import LeanCamCombi.PlainCombi.OrderShatter
 import LeanCamCombi.PlainCombi.VanDenBergKesten
-import LeanCamCombi.PosDiffs
-import LeanCamCombi.SliceRank
 import LeanCamCombi.StableCombi.AddSet
 import LeanCamCombi.StableCombi.Formula
 import LeanCamCombi.StableCombi.Rel
-import LeanCamCombi.SylvesterChvatal
 import LeanCamCombi.Util
diff --git a/LeanCamCombi/Archive/CauchyDavenportFromKneser.lean b/LeanCamCombi/Archive/CauchyDavenportFromKneser.lean
diff --git a/LeanCamCombi/ConvexityRefactor/Defs.lean b/LeanCamCombi/ConvexityRefactor/Defs.lean
diff --git a/LeanCamCombi/ConvexityRefactor/StdSimplex.lean b/LeanCamCombi/ConvexityRefactor/StdSimplex.lean