From c5d8d7a082131623af8f42436104a1ccbc08294b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 17 Oct 2023 21:41:33 +0000 Subject: [PATCH] bump mathlib --- LeanCamCombi.lean | 1 - LeanCamCombi/KruskalKatona.lean | 34 +- .../SetFamily/Compression/UV.lean | 386 ------------------ .../Combinatorics/SimpleGraph/Subgraph.lean | 2 +- lake-manifest.json | 44 +- lean-toolchain | 2 +- 6 files changed, 25 insertions(+), 444 deletions(-) delete mode 100644 LeanCamCombi/Mathlib/Combinatorics/SetFamily/Compression/UV.lean diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean index 66d17be091..e6979604fd 100644 --- a/LeanCamCombi.lean +++ b/LeanCamCombi.lean @@ -19,7 +19,6 @@ import LeanCamCombi.Mathlib.Analysis.Convex.Mul import LeanCamCombi.Mathlib.Analysis.Convex.Strong import LeanCamCombi.Mathlib.Combinatorics.Colex import LeanCamCombi.Mathlib.Combinatorics.SetFamily.AhlswedeZhang -import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Compression.UV import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shadow import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic diff --git a/LeanCamCombi/KruskalKatona.lean b/LeanCamCombi/KruskalKatona.lean index 395c987f00..f4b9341f69 100644 --- a/LeanCamCombi/KruskalKatona.lean +++ b/LeanCamCombi/KruskalKatona.lean @@ -7,10 +7,10 @@ import Mathlib.Algebra.GeomSum import Mathlib.Combinatorics.SetFamily.Intersecting import Mathlib.Data.Finset.Fin import Mathlib.Data.Finset.Sort +import Mathlib.Combinatorics.SetFamily.Compression.UV import LeanCamCombi.Mathlib.Combinatorics.Colex import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shadow import LeanCamCombi.Mathlib.Data.Finset.Sups -import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Compression.UV import LeanCamCombi.Mathlib.Order.RelClasses /-! @@ -185,12 +185,12 @@ protected lemma IsInitSeg.shadow [Finite α] (h₁ : IsInitSeg 𝒜 r) : IsInitS end Wolex -open Finset Wolex Nat UW +open Finset Wolex Nat UV open scoped BigOperators FinsetFamily variable {α : Type*} [LinearOrder α] {s U V : Finset α} {n : ℕ} -namespace UW +namespace UV /-- Applying the compression makes the set smaller in wolex. This is intuitive since a portion of the set is being "shifted 'down" as `max U < max V`. -/ @@ -216,8 +216,8 @@ shadow. In particular, 'good' means it's useful, and every smaller compression w difference. -/ lemma compression_improved (𝒜 : Finset (Finset α)) (h₁ : UsefulCompression U V) (h₂ : ∀ ⦃U₁ V₁⦄, UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜) : - (∂ (𝓔 U V 𝒜)).card ≤ (∂ 𝒜).card := by - obtain ⟨UWd, same_size, hU, hV, max_lt⟩ := h₁ + (∂ (𝓒 U V 𝒜)).card ≤ (∂ 𝒜).card := by + obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁ refine' card_shadow_compression_le _ _ fun x Hx ↦ ⟨min' V hV, min'_mem _ _, _⟩ obtain hU' | hU' := eq_or_lt_of_le (succ_le_iff.2 hU.card_pos) · rw [←hU'] at same_size @@ -226,7 +226,7 @@ lemma compression_improved (𝒜 : Finset (Finset α)) (h₁ : UsefulCompression rw [←Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ←same_size] rw [‹erase U x = ∅›, ‹erase V (min' V hV) = ∅›] exact isCompressed_self _ _ - refine' h₂ ⟨UWd.mono (erase_subset _ _) (erase_subset _ _), _, _, _, _⟩ (card_erase_lt_of_mem Hx) + refine' h₂ ⟨UVd.mono (erase_subset _ _) (erase_subset _ _), _, _, _, _⟩ (card_erase_lt_of_mem Hx) · rw [card_erase_of_mem (min'_mem _ _), card_erase_of_mem Hx, same_size] · rwa [←card_pos, card_erase_of_mem Hx, tsub_pos_iff_lt] · rwa [←Finset.card_pos, card_erase_of_mem (min'_mem _ _), ←same_size, tsub_pos_iff_lt] @@ -271,8 +271,8 @@ private def familyMeasure (𝒜 : Finset (Finset (Fin n))) : ℕ := ∑ A in /-- Applying a compression strictly decreases the measure. This helps show that "compress until we can't any more" is a terminating process. -/ lemma familyMeasure_compression_lt_familyMeasure {U V : Finset (Fin n)} {hU : U.Nonempty} - {hV : V.Nonempty} (h : max' U hU < max' V hV) {𝒜 : Finset (Finset (Fin n))} (a : 𝓔 U V 𝒜 ≠ 𝒜) : - familyMeasure (𝓔 U V 𝒜) < familyMeasure 𝒜 := by + {hV : V.Nonempty} (h : max' U hU < max' V hV) {𝒜 : Finset (Finset (Fin n))} (a : 𝓒 U V 𝒜 ≠ 𝒜) : + familyMeasure (𝓒 U V 𝒜) < familyMeasure 𝒜 := by rw [compression] at a ⊢ have q : ∀ Q ∈ 𝒜.filter fun A ↦ compress U V A ∉ 𝒜, compress U V Q ≠ Q := by simp_rw [mem_filter] @@ -311,10 +311,10 @@ private lemma kruskal_katona_helper {r : ℕ} (𝒜 : Finset (Finset (Fin n))) univ.filter fun t ↦ UsefulCompression t.1 t.2 ∧ ¬ IsCompressed t.1 t.2 A obtain husable | husable := usable.eq_empty_or_nonempty -- No. Then where we are is the required set family. - · refine' ⟨A, le_rfl, rfl, h, fun U V hUW ↦ _⟩ + · refine' ⟨A, le_rfl, rfl, h, fun U V hUV ↦ _⟩ rw [eq_empty_iff_forall_not_mem] at husable by_contra h - exact husable ⟨U, V⟩ $ mem_filter.2 ⟨mem_univ _, hUW, h⟩ + exact husable ⟨U, V⟩ $ mem_filter.2 ⟨mem_univ _, hUV, h⟩ -- Yes. Then apply the compression, then keep going obtain ⟨⟨U, V⟩, hUV, t⟩ := exists_min_image usable (fun t ↦ t.1.card) husable rw [mem_filter] at hUV @@ -322,14 +322,14 @@ private lemma kruskal_katona_helper {r : ℕ} (𝒜 : Finset (Finset (Fin n))) rintro U₁ V₁ huseful hUcard by_contra h exact hUcard.not_le $ t ⟨U₁, V₁⟩ $ mem_filter.2 ⟨mem_univ _, huseful, h⟩ - have p1 : (∂ (𝓔 U V A)).card ≤ (∂ A).card := compression_improved _ hUV.2.1 h₂ + have p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card := compression_improved _ hUV.2.1 h₂ obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1 unfold InvImage at ih - obtain ⟨t, q1, q2, q3, q4⟩ := ih (𝓔 U V A) - (familyMeasure_compression_lt_familyMeasure hmax hUV.2.2) (h.uwCompression hUV') + obtain ⟨t, q1, q2, q3, q4⟩ := ih (𝓒 U V A) + (familyMeasure_compression_lt_familyMeasure hmax hUV.2.2) (h.uvCompression hUV') exact ⟨t, q1.trans p1, (card_compression _ _ _).symm.trans q2, q3, q4⟩ -end UW +end UV -- Finally we can prove Kruskal-Katona. section KK @@ -345,11 +345,11 @@ Proof notes: Most of the work was done in Kruskal-Katona helper; it gives a `ℬ compressed, and so we know it's an initial segment, which by uniqueness is the same as `𝒞`. -/ lemma kruskal_katona (h₁ : (𝒜 : Set (Finset (Fin n))).Sized r) (h₂ : 𝒜.card = 𝒞.card) (h₃ : IsInitSeg 𝒞 r) : (∂ 𝒞).card ≤ (∂ 𝒜).card := by - obtain ⟨ℬ, card_le, t, hℬ, fully_comp⟩ := UW.kruskal_katona_helper 𝒜 h₁ + obtain ⟨ℬ, card_le, t, hℬ, fully_comp⟩ := UV.kruskal_katona_helper 𝒜 h₁ convert card_le have hcard : card ℬ = card 𝒞 := t.symm.trans h₂ obtain CB | BC := - h₃.total (UW.isInitSeg_of_compressed hℬ fun U V hUW ↦ by convert fully_comp U V hUW) + h₃.total (UV.isInitSeg_of_compressed hℬ fun U V hUV ↦ by convert fully_comp U V hUV) · exact eq_of_subset_of_card_le CB hcard.le · exact (eq_of_subset_of_card_le BC hcard.ge).symm @@ -457,7 +457,7 @@ lemma EKR {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (𝒜 : Set (Finse have kk := lovasz_form ‹n - 2 * r ≤ n - r› ((tsub_le_tsub_iff_left ‹1 ≤ n›).2 h1r) tsub_le_self h𝒜bar z.le have q : n - r - (n - 2 * r) = r := by - rw [Nat.sub.right_comm, Nat.sub_sub_self, two_mul] + rw [tsub_right_comm, Nat.sub_sub_self, two_mul] apply Nat.add_sub_cancel rw [mul_comm, ←Nat.le_div_iff_mul_le' zero_lt_two] exact h₃ diff --git a/LeanCamCombi/Mathlib/Combinatorics/SetFamily/Compression/UV.lean b/LeanCamCombi/Mathlib/Combinatorics/SetFamily/Compression/UV.lean deleted file mode 100644 index da72511b82..0000000000 --- a/LeanCamCombi/Mathlib/Combinatorics/SetFamily/Compression/UV.lean +++ /dev/null @@ -1,386 +0,0 @@ -import Mathlib.Combinatorics.SetFamily.Compression.UV - -/-! -# UW-compressions - -This file defines UW-compression. It is an operation on a set family that reduces its shadow. - -UW-compressing `a : α` along `u v : α` means replacing `a` by `(a ⊔ u) \ v` if `a` and `u` are -disjoint and `v ≤ a`. In some sense, it's moving `a` from `v` to `u`. - -UW-compressions are immensely useful to prove the Kruskal-Katona theorem. The idea is that -compressing a set family might decrease the size of its shadow, so iterated compressions hopefully -minimise the shadow. - -## Main declarations - -* `UW.compress`: `compress u v a` is `a` compressed along `u` and `v`. -* `UW.compression`: `compression u v s` is the compression of the set family `s` along `u` and `v`. - It is the compressions of the elements of `s` whose compression is not already in `s` along with - the element whose compression is already in `s`. This way of splitting into what moves and what - does not ensures the compression doesn't squash the set family, which is proved by - `UW.card_compression`. -* `UW.card_shadow_compression_le`: Compressing reduces the size of the shadow. This is a key fact in - the proof of Kruskal-Katona. - -## Notation - -`𝓔` (typed with `\MCC`) is notation for `UW.compression` in locale `FinsetFamily`. - -## Notes - -Even though our emphasis is on `Finset α`, we define UW-compressions more generally in a generalized -boolean algebra, so that one can use it for `Set α`. - -## References - -* https://github.com/b-mehta/maths-notes/blob/master/iii/mich/combinatorics.pdf - -## Tags - -compression, UW-compression, shadow --/ - -open Finset - -variable {α : Type*} - --- The namespace is here to distinguish from other compressions. -namespace UW - -/-! ### UW-compression in generalized boolean algebras -/ - - -section GeneralizedBooleanAlgebra - -variable [GeneralizedBooleanAlgebra α] [DecidableRel (@Disjoint α _ _)] - [DecidableRel ((· ≤ ·) : α → α → Prop)] {s : Finset α} {u v a b : α} - -/-- UW-compressing `a` means removing `v` from it and adding `u` if `a` and `u` are disjoint and -`v ≤ a` (it replaces the `v` part of `a` by the `u` part). Else, UW-compressing `a` doesn't do -anything. This is most useful when `u` and `v` are disjoint finsets of the same size. -/ -def compress (u v a : α) : α := - if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a - -theorem compress_of_disjoint_of_le (hua : Disjoint u a) (hva : v ≤ a) : - compress u v a = (a ⊔ u) \ v := - if_pos ⟨hua, hva⟩ - -theorem compress_of_disjoint_of_le' (hva : Disjoint v a) (hua : u ≤ a) : - compress u v ((a ⊔ v) \ u) = a := by - rw [compress_of_disjoint_of_le disjoint_sdiff_self_right - (le_sdiff.2 ⟨(le_sup_right : v ≤ a ⊔ v), hva.mono_right hua⟩), - sdiff_sup_cancel (le_sup_of_le_left hua), hva.symm.sup_sdiff_cancel_right] - -@[simp] -theorem compress_self (u a : α) : compress u u a = a := by - unfold compress - split_ifs with h - · exact h.1.symm.sup_sdiff_cancel_right - · rfl - -/-- An element can be compressed to any other element by removing/adding the differences. -/ -@[simp] -theorem compress_sdiff_sdiff (a b : α) : compress (a \ b) (b \ a) b = a := by - refine' (compress_of_disjoint_of_le disjoint_sdiff_self_left sdiff_le).trans _ - rw [sup_sdiff_self_right, sup_sdiff, disjoint_sdiff_self_right.sdiff_eq_left, sup_eq_right] - exact sdiff_sdiff_le - -/-- Compressing an element is idempotent. -/ -@[simp] -theorem compress_idem (u v a : α) : compress u v (compress u v a) = compress u v a := by - unfold compress - split_ifs with h h' - · rw [le_sdiff_iff.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem] - · rfl - · rfl - -variable [DecidableEq α] - -/-- To UW-compress a set family, we compress each of its elements, except that we don't want to -reduce the cardinality, so we keep all elements whose compression is already present. -/ -def compression (u v : α) (s : Finset α) := - (s.filter fun a => compress u v a ∈ s) ∪ (s.image $ compress u v).filter fun a ↦ a ∉ s - -scoped[FinsetFamily] notation "𝓔 " => UW.compression - -open scoped FinsetFamily - -/-- `IsCompressed u v s` expresses that `s` is UW-compressed. -/ -def IsCompressed (u v : α) (s : Finset α) := - 𝓔 u v s = s - -/-- UW-compression is injective on the sets that are not UW-compressed. -/ -theorem compress_injOn : Set.InjOn (compress u v) ↑(s.filter fun a ↦ compress u v a ∉ s) := by - intro a ha b hb hab - rw [mem_coe, mem_filter] at ha hb - rw [compress] at ha hab - split_ifs at ha hab with has - · rw [compress] at hb hab - split_ifs at hb hab with hbs - · exact sup_sdiff_injOn u v has hbs hab - · exact (hb.2 hb.1).elim - · exact (ha.2 ha.1).elim - -/-- `a` is in the UW-compressed family iff it's in the original and its compression is in the -original, or it's not in the original but it's the compression of something in the original. -/ -theorem mem_compression : - a ∈ 𝓔 u v s ↔ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a := by - simp_rw [compression, mem_union, mem_filter, mem_image, @and_comm (a ∉ s)] - -protected theorem IsCompressed.eq (h : IsCompressed u v s) : 𝓔 u v s = s := h - -@[simp] -theorem compression_self (u : α) (s : Finset α) : 𝓔 u u s = s := by - unfold compression - convert union_empty s - · ext a - rw [mem_filter, compress_self, and_self_iff] - · refine' eq_empty_of_forall_not_mem fun a ha ↦ _ - simp_rw [mem_filter, mem_image, compress_self] at ha - obtain ⟨⟨b, hb, rfl⟩, hb'⟩ := ha - exact hb' hb - -/-- Any family is compressed along two identical elements. -/ -theorem isCompressed_self (u : α) (s : Finset α) : IsCompressed u u s := compression_self u s - -theorem compress_disjoint : - Disjoint (s.filter fun a ↦ compress u v a ∈ s) ((s.image $ compress u v).filter (· ∉ s)) := - disjoint_left.2 fun _a ha₁ ha₂ ↦ (mem_filter.1 ha₂).2 (mem_filter.1 ha₁).1 - -theorem compress_mem_compression (ha : a ∈ s) : compress u v a ∈ 𝓔 u v s := by - rw [mem_compression] - by_cases compress u v a ∈ s - · rw [compress_idem] - exact Or.inl ⟨h, h⟩ - · exact Or.inr ⟨h, a, ha, rfl⟩ - --- This is a special case of `compress_mem_compression` once we have `compression_idem`. -theorem compress_mem_compression_of_mem_compression (ha : a ∈ 𝓔 u v s) : - compress u v a ∈ 𝓔 u v s := by - rw [mem_compression] at ha ⊢ - simp only [compress_idem, exists_prop] - obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha - · exact Or.inl ⟨ha, ha⟩ - · exact Or.inr ⟨by rwa [compress_idem], b, hb, (compress_idem _ _ _).symm⟩ - -/-- Compressing a family is idempotent. -/ -@[simp] -theorem compression_idem (u v : α) (s : Finset α) : 𝓔 u v (𝓔 u v s) = 𝓔 u v s := by - have h : filter (fun a ↦ compress u v a ∉ 𝓔 u v s) (𝓔 u v s) = ∅ := - filter_false_of_mem fun a ha h ↦ h $ compress_mem_compression_of_mem_compression ha - rw [compression, image_filter, h, image_empty, ←h] - exact filter_union_filter_neg_eq _ (compression u v s) - -/-- Compressing a family doesn't change its size. -/ -@[simp] -theorem card_compression (u v : α) (s : Finset α) : (𝓔 u v s).card = s.card := by - rw [compression, card_disjoint_union compress_disjoint, image_filter, - card_image_of_injOn compress_injOn, ←card_disjoint_union (disjoint_filter_filter_neg s _ _), - filter_union_filter_neg_eq] - -theorem le_of_mem_compression_of_not_mem (h : a ∈ 𝓔 u v s) (ha : a ∉ s) : u ≤ a := by - rw [mem_compression] at h - obtain h | ⟨-, b, hb, hba⟩ := h - · cases ha h.1 - unfold compress at hba - split_ifs at hba with h - · rw [←hba, le_sdiff] - exact ⟨le_sup_right, h.1.mono_right h.2⟩ - · cases ne_of_mem_of_not_mem hb ha hba - -theorem disjoint_of_mem_compression_of_not_mem (h : a ∈ 𝓔 u v s) (ha : a ∉ s) : Disjoint v a := by - rw [mem_compression] at h - obtain h | ⟨-, b, hb, hba⟩ := h - · cases ha h.1 - unfold compress at hba - split_ifs at hba with h - · rw [←hba] - exact disjoint_sdiff_self_right - · cases ne_of_mem_of_not_mem hb ha hba - -theorem sup_sdiff_mem_of_mem_compression_of_not_mem (h : a ∈ 𝓔 u v s) (ha : a ∉ s) : - (a ⊔ v) \ u ∈ s := by - rw [mem_compression] at h - obtain h | ⟨-, b, hb, hba⟩ := h - · cases ha h.1 - unfold compress at hba - split_ifs at hba with h - · rwa [←hba, sdiff_sup_cancel (le_sup_of_le_left h.2), sup_sdiff_right_self, - h.1.symm.sdiff_eq_left] - · cases ne_of_mem_of_not_mem hb ha hba - -/-- If `a` is in the family compression and can be compressed, then its compression is in the -original family. -/ -theorem sup_sdiff_mem_of_mem_compression (ha : a ∈ 𝓔 u v s) (hva : v ≤ a) (hua : Disjoint u a) : - (a ⊔ u) \ v ∈ s := by - rw [mem_compression, compress_of_disjoint_of_le hua hva] at ha - obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha - · exact ha - have hu : u = ⊥ := by - suffices Disjoint u (u \ v) by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this - refine' hua.mono_right _ - rw [←compress_idem, compress_of_disjoint_of_le hua hva] - exact sdiff_le_sdiff_right le_sup_right - have hv : v = ⊥ := by - rw [←disjoint_self] - apply Disjoint.mono_right hva - rw [←compress_idem, compress_of_disjoint_of_le hua hva] - exact disjoint_sdiff_self_right - rwa [hu, hv, compress_self, sup_bot_eq, sdiff_bot] - -/-- If `a` is in the `u, v`-compression but `v ≤ a`, then `a` must have been in the original -family. -/ -theorem mem_of_mem_compression (ha : a ∈ 𝓔 u v s) (hva : v ≤ a) (hvu : v = ⊥ → u = ⊥) : a ∈ s := by - rw [mem_compression] at ha - obtain ha | ⟨_, b, hb, h⟩ := ha - · exact ha.1 - unfold compress at h - split_ifs at h - · rw [←h, le_sdiff_iff] at hva - rwa [←h, hvu hva, hva, sup_bot_eq, sdiff_bot] - · rwa [←h] - -end GeneralizedBooleanAlgebra - -/-! ### UW-compression on finsets -/ - -open scoped FinsetFamily - -variable [DecidableEq α] {𝒜 : Finset (Finset α)} {u v a : Finset α} {r : ℕ} - -/-- Compressing a finset doesn't change its size. -/ -theorem card_compress (hUV : u.card = v.card) (A : Finset α) : (compress u v A).card = A.card := by - unfold compress - split_ifs with h - · rw [card_sdiff (h.2.trans le_sup_left), sup_eq_union, card_disjoint_union h.1.symm, hUV, - add_tsub_cancel_right] - · rfl - -lemma _root_.Set.Sized.uwCompression (huv : u.card = v.card) (h𝒜 : (𝒜 : Set (Finset α)).Sized r) : - (𝓔 u v 𝒜 : Set (Finset α)).Sized r := by - simp_rw [Set.Sized, mem_coe, mem_compression] - rintro s (hs | ⟨huvt, t, ht, rfl⟩) - · exact h𝒜 hs.1 - · rw [card_compress huv, h𝒜 ht] - -private theorem aux (huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜) : - v = ∅ → u = ∅ := by - rintro rfl; refine' eq_empty_of_forall_not_mem fun a ha ↦ _; obtain ⟨_, ⟨⟩, -⟩ := huv a ha - -/-- UW-compression reduces the size of the shadow of `𝒜` if, for all `x ∈ u` there is `y ∈ v` such -that `𝒜` is `(u.erase x, v.erase y)`-compressed. This is the key fact about compression for -Kruskal-Katona. -/ -theorem shadow_compression_subset_compression_shadow (u v : Finset α) - (huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜) : - ∂ (𝓔 u v 𝒜) ⊆ 𝓔 u v (∂ 𝒜) := by - set 𝒜' := 𝓔 u v 𝒜 - suffices H : ∀ s, s ∈ ∂ 𝒜' → s ∉ ∂ 𝒜 → - u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜' - · rintro s hs' - rw [mem_compression] - by_cases hs : s ∈ 𝒜.shadow; swap - · obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs - exact Or.inr ⟨hs, _, h, compress_of_disjoint_of_le' hvs hus⟩ - refine' Or.inl ⟨hs, _⟩ - rw [compress] - split_ifs with huvs; swap - · exact hs - rw [mem_shadow_iff] at hs' - obtain ⟨t, Ht, a, hat, rfl⟩ := hs' - have hav : a ∉ v := not_mem_mono huvs.2 (not_mem_erase a t) - have hvt : v ≤ t := huvs.2.trans (erase_subset _ t) - have ht : t ∈ 𝒜 := mem_of_mem_compression Ht hvt (aux huv) - by_cases hau : a ∈ u - · obtain ⟨b, hbv, Hcomp⟩ := huv a hau - refine' mem_shadow_iff_insert_mem.2 ⟨b, not_mem_sdiff_of_mem_right hbv, _⟩ - rw [←Hcomp.eq] at ht - have hsb := - sup_sdiff_mem_of_mem_compression ht ((erase_subset _ _).trans hvt) - (disjoint_erase_comm.2 huvs.1) - rwa [sup_eq_union, sdiff_erase (mem_union_left _ $ hvt hbv), union_erase_of_mem hat, ← - erase_union_of_mem hau] at hsb - · refine' - mem_shadow_iff.2 - ⟨(t ⊔ u) \ v, - sup_sdiff_mem_of_mem_compression Ht hvt $ disjoint_of_erase_right hau huvs.1, a, _, _⟩ - · rw [sup_eq_union, mem_sdiff, mem_union] - exact ⟨Or.inl hat, hav⟩ - · rw [←erase_sdiff_comm, sup_eq_union, erase_union_distrib, erase_eq_of_not_mem hau] - intro s hs𝒜' hs𝒜 - -- This is gonna be useful a couple of times so let's name it. - have m : ∀ (y) (_ : y ∉ s), insert y s ∉ 𝒜 := fun y h a ↦ - hs𝒜 (mem_shadow_iff_insert_mem.2 ⟨y, h, a⟩) - obtain ⟨x, _, _⟩ := mem_shadow_iff_insert_mem.1 hs𝒜' - have hus : u ⊆ insert x s := le_of_mem_compression_of_not_mem ‹_ ∈ 𝒜'› (m _ ‹x ∉ s›) - have hvs : Disjoint v (insert x s) := disjoint_of_mem_compression_of_not_mem ‹_› (m _ ‹x ∉ s›) - have : (insert x s ∪ v) \ u ∈ 𝒜 := sup_sdiff_mem_of_mem_compression_of_not_mem ‹_› (m _ ‹x ∉ s›) - have hsv : Disjoint s v := hvs.symm.mono_left (subset_insert _ _) - have hvu : Disjoint v u := disjoint_of_subset_right hus hvs - have hxv : x ∉ v := disjoint_right.1 hvs (mem_insert_self _ _) - have : v \ u = v := ‹Disjoint v u›.sdiff_eq_left - -- The first key part is that `x ∉ u` - have : x ∉ u := by - intro hxu - obtain ⟨y, hyv, hxy⟩ := huv x hxu - -- If `x ∈ u`, we can get `y ∈ v` so that `𝒜` is `(u.erase x, v.erase y)`-compressed - apply m y (disjoint_right.1 hsv hyv) - -- and we will use this `y` to contradict `m`, so we would like to show `insert y s ∈ 𝒜`. - -- We do this by showing the below - have : ((insert x s ∪ v) \ u ∪ erase u x) \ erase v y ∈ 𝒜 := by - refine' - sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) _ - (disjoint_of_subset_left (erase_subset _ _) disjoint_sdiff) - rw [union_sdiff_distrib, ‹v \ u = v›] - exact (erase_subset _ _).trans (subset_union_right _ _) - -- and then arguing that it's the same - convert this using 1 - rw [sdiff_union_erase_cancel (hus.trans $ subset_union_left _ _) ‹x ∈ u›, erase_union_distrib, - erase_insert ‹x ∉ s›, erase_eq_of_not_mem ‹x ∉ v›, sdiff_erase (mem_union_right _ hyv), - union_sdiff_cancel_right hsv] - -- Now that this is done, it's immediate that `u ⊆ s` - have hus : u ⊆ s := by rwa [←erase_eq_of_not_mem ‹x ∉ u›, ←subset_insert_iff] - -- and we already had that `v` and `s` are disjoint, - -- so it only remains to get `(s ∪ v) \ u ∈ ∂ 𝒜 \ ∂ 𝒜'` - simp_rw [mem_shadow_iff_insert_mem] - refine' ⟨hus, hsv.symm, ⟨x, _, _⟩, _⟩ - -- `(s ∪ v) \ u ∈ ∂ 𝒜` is pretty direct: - · exact not_mem_sdiff_of_not_mem_left (not_mem_union.2 ⟨‹x ∉ s›, ‹x ∉ v›⟩) - · rwa [←insert_sdiff_of_not_mem _ ‹x ∉ u›, ←insert_union] - -- For (s ∪ v) \ u ∉ ∂ 𝒜', we split up based on w ∈ u - rintro ⟨w, hwB, hw𝒜'⟩ - have : v ⊆ insert w ((s ∪ v) \ u) := - (subset_sdiff.2 ⟨subset_union_right _ _, hvu⟩).trans (subset_insert _ _) - by_cases hwu : w ∈ u - -- If `w ∈ u`, we find `z ∈ v`, and contradict `m` again - · obtain ⟨z, hz, hxy⟩ := huv w hwu - apply m z (disjoint_right.1 hsv hz) - have : insert w ((s ∪ v) \ u) ∈ 𝒜 := mem_of_mem_compression hw𝒜' ‹_› (aux huv) - have : (insert w ((s ∪ v) \ u) ∪ erase u w) \ erase v z ∈ 𝒜 := by - refine' sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ((erase_subset _ _).trans ‹_›) _ - rw [←sdiff_erase (mem_union_left _ $ hus hwu)] - exact disjoint_sdiff - convert this using 1 - rw [insert_union_comm, insert_erase ‹w ∈ u›, - sdiff_union_of_subset (hus.trans $ subset_union_left _ _), - sdiff_erase (mem_union_right _ ‹z ∈ v›), union_sdiff_cancel_right hsv] - -- If `w ∉ u`, we contradict `m` again - rw [mem_sdiff, ←not_imp, Classical.not_not] at hwB - apply m w (hwu ∘ hwB ∘ mem_union_left _) - have : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜 := - sup_sdiff_mem_of_mem_compression ‹insert w ((s ∪ v) \ u) ∈ 𝒜'› ‹_› - (disjoint_insert_right.2 ⟨‹_›, disjoint_sdiff⟩) - convert this using 1 - rw [insert_union, sdiff_union_of_subset (hus.trans $ subset_union_left _ _), - insert_sdiff_of_not_mem _ (hwu ∘ hwB ∘ mem_union_right _), union_sdiff_cancel_right hsv] - -/-- UW-compression reduces the size of the shadow of `𝒜` if, for all `x ∈ u` there is `y ∈ v` -such that `𝒜` is `(u.erase x, v.erase y)`-compressed. This is the key UW-compression fact needed for -Kruskal-Katona. -/ -theorem card_shadow_compression_le (u v : Finset α) - (huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜) : - (∂ (𝓔 u v 𝒜)).card ≤ (∂ 𝒜).card := - (card_le_of_subset $ shadow_compression_subset_compression_shadow _ _ huv).trans - (card_compression _ _ _).le - -end UW diff --git a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean index 34033072c6..fd0b420752 100644 --- a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean +++ b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean @@ -70,7 +70,7 @@ def topIso : (⊤ : G.Subgraph).coe ≃g G where @[simps] noncomputable def isoMap {H : SimpleGraph β} (f : G →g H) (hf : Injective f) (G' : G.Subgraph) : G'.coe ≃g (G'.map f).coe := - { Equiv.Set.image f G'.verts hf with map_rel_iff' := by simp [hf] } + { Equiv.Set.image f G'.verts hf with map_rel_iff' := by dsimp; simp [hf] } open scoped Classical diff --git a/lake-manifest.json b/lake-manifest.json index a24f6b7e23..26021fc740 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,19 +4,11 @@ [{"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "39796d114b0eb24b437387e237a3b4fb26ef61d5", + "rev": "b940be208b0720c3acc6f89b25360dd812054166", "opts": {}, "name": "mathlib", "inputRev?": null, "inherited": false}}, - {"git": - {"url": "https://github.com/leanprover/doc-gen4", - "subDir?": null, - "rev": "f9d987567129f422ebd8cfac6a1e6233a06c720b", - "opts": {}, - "name": "«doc-gen4»", - "inputRev?": "main", - "inherited": false}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, @@ -25,14 +17,6 @@ "name": "Qq", "inputRev?": "master", "inherited": true}}, - {"git": - {"url": "https://github.com/JLimperg/aesop", - "subDir?": null, - "rev": "41c6370eb2f0c9052bee6af0e0a017b9ba8da2b8", - "opts": {}, - "name": "aesop", - "inputRev?": "master", - "inherited": true}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli.git", "subDir?": null, @@ -52,33 +36,17 @@ {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "a093d7a6ac721071d8ba3774b0318063928cd3e2", + "rev": "85a0d4891518518edfccee16cbceac139efa460c", "opts": {}, "name": "std", "inputRev?": "main", "inherited": true}}, {"git": - {"url": "https://github.com/xubaiw/CMark.lean", - "subDir?": null, - "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", - "opts": {}, - "name": "CMark", - "inputRev?": "main", - "inherited": true}}, - {"git": - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "subDir?": null, - "rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32", - "opts": {}, - "name": "«lean4-unicode-basic»", - "inputRev?": "main", - "inherited": true}}, - {"git": - {"url": "https://github.com/hargonix/LeanInk", + {"url": "https://github.com/JLimperg/aesop", "subDir?": null, - "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1", + "rev": "0bd8465d8a5cfdd53c1ff0fd57ca5eaa53eb455c", "opts": {}, - "name": "leanInk", - "inputRev?": "doc-gen", + "name": "aesop", + "inputRev?": "master", "inherited": true}}], "name": "LeanCamCombi"} diff --git a/lean-toolchain b/lean-toolchain index 400394aaf2..a61d282854 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0-rc1 +leanprover/lean4:v4.2.0-rc3