diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean index 62ccde0ce0..1aed03282a 100644 --- a/LeanCamCombi.lean +++ b/LeanCamCombi.lean @@ -17,7 +17,6 @@ import LeanCamCombi.GrowthInGroups.ApproximateSubgroup import LeanCamCombi.GrowthInGroups.Chevalley import LeanCamCombi.GrowthInGroups.ChevalleyComplex import LeanCamCombi.GrowthInGroups.Constructible -import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum import LeanCamCombi.GrowthInGroups.ConstructibleSetData import LeanCamCombi.GrowthInGroups.Lecture1 import LeanCamCombi.GrowthInGroups.Lecture2 @@ -47,24 +46,18 @@ import LeanCamCombi.Mathlib.Analysis.Convex.Exposed import LeanCamCombi.Mathlib.Analysis.Convex.Extreme import LeanCamCombi.Mathlib.Analysis.Convex.Independence import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic -import LeanCamCombi.Mathlib.Analysis.Normed.Group.Basic import LeanCamCombi.Mathlib.Combinatorics.Additive.VerySmallDoubling import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Finite import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps -import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph -import LeanCamCombi.Mathlib.Data.Finset.Basic -import LeanCamCombi.Mathlib.Data.Finset.PosDiffs -import LeanCamCombi.Mathlib.Data.Finset.Powerset import LeanCamCombi.Mathlib.Data.List.DropRight import LeanCamCombi.Mathlib.Data.Multiset.Basic import LeanCamCombi.Mathlib.Data.Nat.Defs import LeanCamCombi.Mathlib.Data.Prod.Lex import LeanCamCombi.Mathlib.Data.Set.Basic -import LeanCamCombi.Mathlib.Data.Set.Pairwise.Lattice import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional @@ -76,16 +69,17 @@ import LeanCamCombi.Mathlib.Order.Partition.Finpartition import LeanCamCombi.Mathlib.Order.RelIso.Group import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions import LeanCamCombi.Mathlib.RingTheory.FinitePresentation -import LeanCamCombi.Mathlib.RingTheory.Ideal.Span import LeanCamCombi.Mathlib.RingTheory.LocalRing.ResidueField.Ideal import LeanCamCombi.Mathlib.RingTheory.Localization.Integral import LeanCamCombi.Mathlib.RingTheory.PrimeSpectrum import LeanCamCombi.MetricBetween import LeanCamCombi.MinkowskiCaratheodory +import LeanCamCombi.Multipartite import LeanCamCombi.PhD.VCDim.Basic import LeanCamCombi.PlainCombi.LittlewoodOfford import LeanCamCombi.PlainCombi.OrderShatter import LeanCamCombi.PlainCombi.VanDenBergKesten +import LeanCamCombi.PosDiffs import LeanCamCombi.SimplicialComplex.Basic import LeanCamCombi.SimplicialComplex.Finite import LeanCamCombi.SimplicialComplex.Pure diff --git a/LeanCamCombi/GrowthInGroups/Chevalley.lean b/LeanCamCombi/GrowthInGroups/Chevalley.lean index b3c820a3aa..c6ee27bfe7 100644 --- a/LeanCamCombi/GrowthInGroups/Chevalley.lean +++ b/LeanCamCombi/GrowthInGroups/Chevalley.lean @@ -3,7 +3,6 @@ import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import LeanCamCombi.Mathlib.Data.Prod.Lex import LeanCamCombi.Mathlib.RingTheory.FinitePresentation -import LeanCamCombi.Mathlib.RingTheory.Ideal.Span import LeanCamCombi.Mathlib.RingTheory.Localization.Integral import LeanCamCombi.GrowthInGroups.PrimeSpectrumPolynomial @@ -51,7 +50,7 @@ lemma foo_induction obtain ⟨n, e, rfl⟩ : ∃ (n : ℕ) (e : Fin (n + 1) → R[X]), I = Ideal.span (Set.range e) := by obtain ⟨s, rfl⟩ := hI exact ⟨s.card, Fin.cons 0 (Subtype.val ∘ s.equivFin.symm), - by simp [← Set.union_singleton, Ideal.span_union]⟩ + by simp [← Set.union_singleton, Ideal.span_union, Set.singleton_zero]⟩ clear hI set v : (Fin (n + 1) → WithBot ℕ) ×ₗ Prop := toLex (degree ∘ e, ¬ ∃ i, IsUnit (e i).leadingCoeff ∧ ∀ j, e j ≠ 0 → @@ -59,7 +58,7 @@ lemma foo_induction clear_value v induction' v using WellFoundedLT.induction with v H_IH generalizing R by_cases he0 : e = 0 - · rw [he0, Set.range_zero, Ideal.span_singleton_zero]; exact hP₁ R + · simpa [he0, Set.range_zero, Set.singleton_zero] using hP₁ R cases subsingleton_or_nontrivial R · rw [Subsingleton.elim (Ideal.span (Set.range e)) ⊥]; exact hP₁ R simp only [funext_iff, Pi.zero_apply, not_forall] at he0 diff --git a/LeanCamCombi/GrowthInGroups/ConstructiblePrimeSpectrum.lean b/LeanCamCombi/GrowthInGroups/ConstructiblePrimeSpectrum.lean deleted file mode 100644 index 178be75478..0000000000 --- a/LeanCamCombi/GrowthInGroups/ConstructiblePrimeSpectrum.lean +++ /dev/null @@ -1,44 +0,0 @@ -import Mathlib.Algebra.Polynomial.Degree.Definitions -import Mathlib.RingTheory.PrimeSpectrum - - -variable (R) {n : ℕ} [CommRing R] - -namespace PrimeSpectrum - -section ConstructibleComponent - -structure ConstructibleComponent (n : ℕ) where - f : R - g : Fin n → R - -variable {R} (S T : ConstructibleComponent R n) - -def ConstructibleComponent.toSet : Set (PrimeSpectrum R) := - zeroLocus (Set.range S.g) \ zeroLocus {S.f} - -end ConstructibleComponent - -section Polynomial - -open Polynomial Set - -variable {R} (S : ConstructibleComponent R[X] n) - -def ConstructibleComponent.coeffSubmodule : Submodule ℤ R := - Submodule.span ℤ (⋃ i, range (S.g i).coeff) - -variable (n) in -abbrev ConstructibleComponent.DegreeType := (Fin n → WithBot ℕ) ×ₗ Prop - -def ConstructibleComponent.degree : DegreeType n := - (Polynomial.degree ∘ S.g, - ¬ ∃ i, IsUnit (S.g i).leadingCoeff ∧ ∀ j, S.g j ≠ 0 → (S.g i).degree ≤ (S.g j).degree) - -def ConstructibleComponent.complexityBound : ℕ := ∑ i, (S.g i).natDegree - -def ConstructibleComponent.exponentBound : ℕ := S.complexityBound ^ S.complexityBound - -end Polynomial - -end PrimeSpectrum diff --git a/LeanCamCombi/Mathlib/Analysis/Normed/Group/Basic.lean b/LeanCamCombi/Mathlib/Analysis/Normed/Group/Basic.lean deleted file mode 100644 index 0ece992c43..0000000000 --- a/LeanCamCombi/Mathlib/Analysis/Normed/Group/Basic.lean +++ /dev/null @@ -1,13 +0,0 @@ -import Mathlib.Analysis.Normed.Group.Basic - -variable {E : Type} [SeminormedGroup E] - -@[to_additive norm_nsmul_le'] -theorem norm_pow_le_mul_norm' (n : ℕ) (a : E) : ‖a ^ n‖ ≤ n * ‖a‖ := by - induction' n with n ih; · simp - simpa only [pow_succ, Nat.cast_succ, add_mul, one_mul] using norm_mul_le_of_le' ih le_rfl - -@[to_additive nnnorm_nsmul_le'] -theorem nnnorm_pow_le_mul_norm' (n : ℕ) (a : E) : ‖a ^ n‖₊ ≤ n * ‖a‖₊ := by - simpa only [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_natCast] using - norm_pow_le_mul_norm' n a diff --git a/LeanCamCombi/Mathlib/Data/Finset/Basic.lean b/LeanCamCombi/Mathlib/Data/Finset/Basic.lean deleted file mode 100644 index 571e688b91..0000000000 --- a/LeanCamCombi/Mathlib/Data/Finset/Basic.lean +++ /dev/null @@ -1,18 +0,0 @@ -import Mathlib.Data.Finset.Basic - -namespace Finset -variable {α : Type*} {a : α} {s t : Finset α} - -lemma not_mem_subset (h : s ⊆ t) : a ∉ t → a ∉ s := Set.not_mem_subset h - -end Finset - -namespace Finset -variable {ι α : Type*} [DecidableEq α] {s : Set ι} {f : ι → Finset α} - -lemma pairwiseDisjoint_iff : - s.PairwiseDisjoint f ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j := by - simp [Set.PairwiseDisjoint, Set.Pairwise, Function.onFun, not_imp_comm (a := _ = _), - not_disjoint_iff_nonempty_inter] - -end Finset diff --git a/LeanCamCombi/Mathlib/Data/Finset/Powerset.lean b/LeanCamCombi/Mathlib/Data/Finset/Powerset.lean deleted file mode 100644 index 4ff20faa57..0000000000 --- a/LeanCamCombi/Mathlib/Data/Finset/Powerset.lean +++ /dev/null @@ -1,19 +0,0 @@ -import Mathlib.Data.Finset.Powerset -import LeanCamCombi.Mathlib.Data.Finset.Basic -import LeanCamCombi.Mathlib.Data.Set.Pairwise.Lattice - -namespace Finset -variable {α : Type*} [DecidableEq α] {s : Finset α} {a : α} - -lemma pairwiseDisjoint_pair_insert (ha : a ∉ s) : - (s.powerset : Set (Finset α)).PairwiseDisjoint - fun t ↦ ({t, insert a t} : Set (Finset α)) := by - simp_rw [Set.pairwiseDisjoint_iff, mem_coe, mem_powerset] - rintro i hi j hj - simp only [Set.Nonempty, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff, - exists_eq_or_imp, exists_eq_left, or_imp, imp_self, true_and] - refine ⟨?_, ?_, insert_erase_invOn.2.injOn (not_mem_mono hi ha) (not_mem_mono hj ha)⟩ <;> - rintro rfl <;> - cases Finset.not_mem_subset ‹_› ha (Finset.mem_insert_self _ _) - -end Finset diff --git a/LeanCamCombi/Mathlib/Data/Set/Basic.lean b/LeanCamCombi/Mathlib/Data/Set/Basic.lean index 4da20bdd46..1930465d63 100644 --- a/LeanCamCombi/Mathlib/Data/Set/Basic.lean +++ b/LeanCamCombi/Mathlib/Data/Set/Basic.lean @@ -6,12 +6,4 @@ variable {α : Type*} {s : Set α} {a : α} lemma diff_inter_right_comm (s t u : Set α) : s \ t ∩ u = (s ∩ u) \ t := by ext; simp [and_right_comm] -lemma insert_diff_self_of_mem (ha : a ∈ s) : insert a (s \ {a}) = s := by aesop - -lemma insert_erase_invOn : - InvOn (insert a) (fun s ↦ s \ {a}) {s : Set α | a ∈ s} {s : Set α | a ∉ s} := - ⟨fun _s ha ↦ insert_diff_self_of_mem ha, fun _s ↦ insert_diff_self_of_not_mem⟩ - -@[gcongr] protected alias ⟨_, GCongr.singleton_subset_singleton⟩ := singleton_subset_singleton - end Set diff --git a/LeanCamCombi/Mathlib/Data/Set/Pairwise/Lattice.lean b/LeanCamCombi/Mathlib/Data/Set/Pairwise/Lattice.lean deleted file mode 100644 index e2092c9490..0000000000 --- a/LeanCamCombi/Mathlib/Data/Set/Pairwise/Lattice.lean +++ /dev/null @@ -1,24 +0,0 @@ -import Mathlib.Data.Set.Pairwise.Lattice -import LeanCamCombi.Mathlib.Data.Set.Basic - -namespace Set -variable {ι α : Type*} {s : Set ι} {f : ι → Set α} - -lemma pairwiseDisjoint_iff : - s.PairwiseDisjoint f ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j := by - simp [Set.PairwiseDisjoint, Set.Pairwise, Function.onFun, not_imp_comm (a := _ = _), - not_disjoint_iff_nonempty_inter] - -end Set - -namespace Set -variable {α : Type*} {s : Set α} {a : α} - -lemma pairwiseDisjoint_pair_insert (ha : a ∉ s) : - s.powerset.PairwiseDisjoint fun t ↦ ({t, insert a t} : Set (Set α)) := by - rw [pairwiseDisjoint_iff] - rintro i hi j hj - have := insert_erase_invOn.2.injOn (not_mem_subset hi ha) (not_mem_subset hj ha) - aesop (add simp [Set.Nonempty, Set.subset_def]) - -end Set diff --git a/LeanCamCombi/Mathlib/RingTheory/Ideal/Span.lean b/LeanCamCombi/Mathlib/RingTheory/Ideal/Span.lean deleted file mode 100644 index f91d25eb85..0000000000 --- a/LeanCamCombi/Mathlib/RingTheory/Ideal/Span.lean +++ /dev/null @@ -1,5 +0,0 @@ -import Mathlib.RingTheory.Ideal.Span - -variable {R : Type*} [Semiring R] - -@[simp] lemma Ideal.span_singleton_zero : Ideal.span {0} = (⊥ : Ideal R) := by simp diff --git a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Multipartite.lean b/LeanCamCombi/Multipartite.lean similarity index 100% rename from LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Multipartite.lean rename to LeanCamCombi/Multipartite.lean diff --git a/LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean b/LeanCamCombi/PosDiffs.lean similarity index 100% rename from LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean rename to LeanCamCombi/PosDiffs.lean index a8a9713cb0..208269d0e8 100644 --- a/LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean +++ b/LeanCamCombi/PosDiffs.lean @@ -3,8 +3,8 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies -/ -import Mathlib.Combinatorics.SetFamily.Compression.Down import Mathlib.Algebra.Group.Pointwise.Finset.Basic +import Mathlib.Combinatorics.SetFamily.Compression.Down import Mathlib.Data.Finset.Sups import Mathlib.Order.Interval.Set.OrdConnected import Mathlib.Order.UpperLower.Basic