diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean index 67592adab9..678ffa0215 100644 --- a/LeanCamCombi.lean +++ b/LeanCamCombi.lean @@ -16,18 +16,19 @@ import LeanCamCombi.Kneser.MulStab import LeanCamCombi.KruskalKatona import LeanCamCombi.LittlewoodOfford import LeanCamCombi.Mathlib.Algebra.BigOperators.LocallyFinite -import LeanCamCombi.Mathlib.Analysis.Convex.Combination +import LeanCamCombi.Mathlib.Algebra.BigOperators.Ring +import LeanCamCombi.Mathlib.Algebra.Order.Sub.Canonical 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.Combinatorics.Colex -import LeanCamCombi.Mathlib.Combinatorics.SetFamily.AhlswedeZhang import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Containment import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Degree import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density +import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph import LeanCamCombi.Mathlib.Data.Finset.Card diff --git a/LeanCamCombi/Incidence.lean b/LeanCamCombi/Incidence.lean index b71258ece8..f8414d70c0 100644 --- a/LeanCamCombi/Incidence.lean +++ b/LeanCamCombi/Incidence.lean @@ -218,16 +218,8 @@ instance instNonAssocSemiring [Preorder α] [LocallyFiniteOrder α] [DecidableEq mul := (· * ·) zero := 0 one := 1 - one_mul := fun f ↦ by - ext a b - simp_rw [mul_apply, one_apply, sum_boole_mul] - exact ite_eq_left_iff.2 (not_imp_comm.1 fun h ↦ left_mem_Icc.2 <| le_of_ne_zero <| Ne.symm h) - mul_one := fun f ↦ by - ext a b - simp_rw [mul_apply, one_apply, eq_comm, sum_mul_boole] - convert - (ite_eq_left_iff.2 <| - not_imp_comm.1 fun h ↦ right_mem_Icc.2 <| le_of_ne_zero <| Ne.symm h).symm + one_mul := fun f ↦ by ext; simp [*] + mul_one := fun f ↦ by ext; simp [*] instance instSemiring [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Semiring 𝕜] : Semiring (IncidenceAlgebra 𝕜 α) where diff --git a/LeanCamCombi/Kneser/Kneser.lean b/LeanCamCombi/Kneser/Kneser.lean index 944dbfa7ac..5773761aeb 100644 --- a/LeanCamCombi/Kneser/Kneser.lean +++ b/LeanCamCombi/Kneser/Kneser.lean @@ -202,7 +202,7 @@ lemma disjoint_mul_sub_card_le {a : α} (b : α) {s t C : Finset α} (has : a · apply smul_finset_subset_smul (mem_union_left t has) (mem_sdiff.mp hx).1 have hx' := (mem_sdiff.mp hx).2 contrapose! hx' - obtain ⟨y, d, hyst, hd, hxyd⟩ := mem_mul.mp hx' + obtain ⟨y, hyst, d, hd, hxyd⟩ := mem_mul.mp hx' obtain ⟨c, hc, hcx⟩ := mem_smul_finset.mp (mem_sdiff.mp hx).1 rw [← hcx, ← eq_mul_inv_iff_mul_eq] at hxyd have hyC : y ∈ a • C.mulStab := by @@ -255,7 +255,7 @@ lemma inter_mul_sub_card_le {a : α} {s t C : Finset α} (has : a ∈ s) have hx' := (mem_sdiff.mp hx).2 contrapose! hx' rw [← inter_distrib_right] - obtain ⟨y, d, hyst, hd, hxyd⟩ := mem_mul.mp hx' + obtain ⟨y, hyst, d, hd, hxyd⟩ := mem_mul.mp hx' obtain ⟨c, hc, hcx⟩ := mem_smul_finset.mp (mem_sdiff.mp hx).1 rw [← hcx, ← eq_mul_inv_iff_mul_eq] at hxyd have hyC : y ∈ a • C.mulStab := by @@ -380,7 +380,7 @@ theorem mul_kneser : rw [mul_subset_left_iff (hs.mul ht), hstab, ← coe_subset, coe_one] exact hCstab.not_subset_singleton simp_rw [mul_subset_iff_left, Classical.not_forall, mem_mul] at this - obtain ⟨_, ⟨a, b, ha, hb, rfl⟩, hab⟩ := this + obtain ⟨_, ⟨a, ha, b, hb, rfl⟩, hab⟩ := this set s₁ := s ∩ a • H with hs₁ set s₂ := s ∩ b • H with hs₂ set t₁ := t ∩ b • H with ht₁ diff --git a/LeanCamCombi/Kneser/KneserRuzsa.lean b/LeanCamCombi/Kneser/KneserRuzsa.lean index 5f65082385..1f9061406b 100644 --- a/LeanCamCombi/Kneser/KneserRuzsa.lean +++ b/LeanCamCombi/Kneser/KneserRuzsa.lean @@ -58,7 +58,7 @@ lemma le_card_union_add_card_mulStab_union : mulStab (image QuotientGroup.mk t) = 1 := by ext x constructor - · simp only [Nonempty.image_iff, mem_one, and_imp, ← QuotientGroup.mk_one] + · simp only [image_nonempty, mem_one, and_imp, ← QuotientGroup.mk_one] intro hx rw [← mulStab_quotient_commute_subgroup N s, ← mulStab_quotient_commute_subgroup N t] at hx simp only [mem_inter, mem_image] at hx @@ -66,7 +66,7 @@ lemma le_card_union_add_card_mulStab_union : obtain ⟨w, hwx⟩ := Quotient.exists_rep x have : ⟦w⟧ = QuotientGroup.mk (s := N) w := by exact rfl rw [← hwx, this, QuotientGroup.eq] at hyx hzx ⊢ - simp only [mul_one, inv_mem_iff, mem_inf, mem_stabilizer_iff] at hyx hzx ⊢ + simp only [mul_one, inv_mem_iff, Subgroup.mem_inf, mem_stabilizer_iff] at hyx hzx ⊢ constructor · convert hyx.1 using 1 rw [mul_comm, mul_smul] @@ -79,7 +79,7 @@ lemma le_card_union_add_card_mulStab_union : all_goals { aesop } · aesop specialize this (α := α ⧸ N) (s := s.image (↑)) (t := t.image (↑)) - simp only [Nonempty.image_iff, mulStab_nonempty, mul_nonempty, and_imp, + simp only [image_nonempty, mulStab_nonempty, mul_nonempty, and_imp, forall_true_left, hs, ht, h1] at this calc min (card s + card Hs) (card t + card Ht) = diff --git a/LeanCamCombi/Kneser/MulStab.lean b/LeanCamCombi/Kneser/MulStab.lean index d855eae3fc..930e57c597 100644 --- a/LeanCamCombi/Kneser/MulStab.lean +++ b/LeanCamCombi/Kneser/MulStab.lean @@ -38,14 +38,14 @@ def mulStab (s : Finset α) : Finset α := (s / s).filter fun a ↦ a • s = s lemma mem_mulStab (hs : s.Nonempty) : a ∈ s.mulStab ↔ a • s = s := by rw [mulStab, mem_filter, mem_div, and_iff_right_of_imp] obtain ⟨b, hb⟩ := hs - exact fun h ↦ ⟨_, _, by rw [← h]; exact smul_mem_smul_finset hb, hb, mul_div_cancel'' _ _⟩ + exact fun h ↦ ⟨_, by rw [← h]; exact smul_mem_smul_finset hb, _, hb, mul_div_cancel'' _ _⟩ @[to_additive] lemma mulStab_subset_div : s.mulStab ⊆ s / s := filter_subset _ _ @[to_additive] lemma mulStab_subset_div_right (ha : a ∈ s) : s.mulStab ⊆ s / {a} := by - refine fun b hb ↦ mem_div.2 ⟨_, _, ?_, mem_singleton_self _, mul_div_cancel'' _ _⟩ + refine fun b hb ↦ mem_div.2 ⟨_, ?_, _, mem_singleton_self _, mul_div_cancel'' _ _⟩ rw [mem_mulStab ⟨a, ha⟩] at hb rw [← hb] exact smul_mem_smul_finset ha @@ -157,7 +157,7 @@ variable [CommGroup α] [DecidableEq α] {s t : Finset α} {a : α} @[to_additive] lemma mulStab_subset_div_left (ha : a ∈ s) : s.mulStab ⊆ {a} / s := by - refine fun b hb ↦ mem_div.2 ⟨_, _, mem_singleton_self _, ?_, div_div_cancel _ _⟩ + refine fun b hb ↦ mem_div.2 ⟨_, mem_singleton_self _, _, ?_, div_div_cancel _ _⟩ rw [mem_mulStab ⟨a, ha⟩] at hb rwa [← hb, ← inv_smul_mem_iff, smul_eq_mul, inv_mul_eq_div] at ha @@ -357,7 +357,7 @@ lemma mulStab_quotient_commute_subgroup (s : Subgroup α) (t : Finset α) · simp have hti : (image (QuotientGroup.mk (s := s)) t).Nonempty := by aesop ext x; - simp only [mem_image, Nonempty.image_iff, mem_mulStab hti] + simp only [mem_image, image_nonempty, mem_mulStab hti] constructor · rintro ⟨a, hax⟩ rw [← hax.2] diff --git a/LeanCamCombi/KruskalKatona.lean b/LeanCamCombi/KruskalKatona.lean index b5d4217fd6..2f07fbdd91 100644 --- a/LeanCamCombi/KruskalKatona.lean +++ b/LeanCamCombi/KruskalKatona.lean @@ -412,7 +412,7 @@ lemma EKR {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (𝒜 : Set (Finse have h𝒜bar : (𝒜ᶜˢ : Set (Finset (Fin n))).Sized (n - r) := by simpa using h₂.compls have : n - 2 * r ≤ n - r := by rw [tsub_le_tsub_iff_left ‹r ≤ n›] - exact Nat.le_mul_of_pos_left zero_lt_two + exact Nat.le_mul_of_pos_left _ zero_lt_two -- We can use the Lovasz form of Kruskal-Katona to get |∂^[n-2k] 𝒜ᶜˢ| ≥ (n-1) choose r 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 diff --git a/LeanCamCombi/Mathlib/Algebra/BigOperators/Ring.lean b/LeanCamCombi/Mathlib/Algebra/BigOperators/Ring.lean new file mode 100644 index 0000000000..e217694c27 --- /dev/null +++ b/LeanCamCombi/Mathlib/Algebra/BigOperators/Ring.lean @@ -0,0 +1,16 @@ +import Mathlib.Algebra.BigOperators.Ring + +open scoped BigOperators + +namespace Finset +variable {ι α : Type*} + +section NonAssocSemiring +variable [NonAssocSemiring α] [DecidableEq ι] + +-- TODO: Replace `sum_boole_mul` +lemma sum_boole_mul' (s : Finset ι) (f : ι → α) (i : ι) : + ∑ j in s, ite (i = j) 1 0 * f j = ite (i ∈ s) (f i) 0 := by simp + +end NonAssocSemiring +end Finset diff --git a/LeanCamCombi/Mathlib/Algebra/Order/Sub/Canonical.lean b/LeanCamCombi/Mathlib/Algebra/Order/Sub/Canonical.lean new file mode 100644 index 0000000000..62d2d65c2a --- /dev/null +++ b/LeanCamCombi/Mathlib/Algebra/Order/Sub/Canonical.lean @@ -0,0 +1,3 @@ +import Mathlib.Algebra.Order.Sub.Canonical + +attribute [simp] tsub_lt_self_iff diff --git a/LeanCamCombi/Mathlib/Analysis/Convex/Combination.lean b/LeanCamCombi/Mathlib/Analysis/Convex/Combination.lean deleted file mode 100644 index a2aa235564..0000000000 --- a/LeanCamCombi/Mathlib/Analysis/Convex/Combination.lean +++ /dev/null @@ -1,82 +0,0 @@ -import Mathlib.Analysis.Convex.Combination -import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional - -open Finset -open scoped BigOperators - -variable {𝕜 E ι : Type*} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {m n : ℕ} - -lemma AffineIndependent.subset_convexHull_inter {X : Finset E} - (hX : AffineIndependent 𝕜 ((↑) : X → E)) {Y₁ Y₂ : Finset E} (hY₁ : Y₁ ⊆ X) - (hY₂ : Y₂ ⊆ X) : - convexHull 𝕜 (Y₁ : Set E) ∩ convexHull 𝕜 (Y₂ : Set E) ⊆ convexHull 𝕜 (Y₁ ∩ Y₂ : Set E) := by - classical - rintro x ⟨hx₁, hx₂⟩ - rw [← coe_inter] - rw [Finset.convexHull_eq] at hx₁ hx₂ - rcases hx₁ with ⟨w₁, h₁w₁, h₂w₁, h₃w₁⟩ - rcases hx₂ with ⟨w₂, h₁w₂, h₂w₂, h₃w₂⟩ - rw [centerMass_eq_of_sum_1 _ _ h₂w₁] at h₃w₁ - rw [centerMass_eq_of_sum_1 _ _ h₂w₂] at h₃w₂ - dsimp at h₃w₁ h₃w₂ - let w : E → 𝕜 := by - intro x - apply (if x ∈ Y₁ then w₁ x else 0) - if x ∈ Y₂ then w₂ x else 0 - have h₁w : ∑ i in X, w i = 0 := by - rw [Finset.sum_sub_distrib, ← sum_filter, filter_mem_eq_inter, ← sum_filter, - filter_mem_eq_inter, Finset.inter_eq_right.2 hY₁, Finset.inter_eq_right.2 hY₂, - h₂w₁, h₂w₂] - simp only [sub_self] - have : ∑ i : E in X, w i • i = 0 := by - simp only [sub_smul, zero_smul, ite_smul, Finset.sum_sub_distrib, ← Finset.sum_filter, h₃w₁, - Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 hY₁, Finset.inter_eq_right.2 hY₂, h₃w₂, - sub_self] - have hX' := hX.eq_zero_of_sum_eq_zero_subtype h₁w this - have t₁ : ∀ x, x ∈ Y₁ → x ∉ Y₂ → w₁ x = 0 := by - intro x hx₁ hx₂ - have : ite (x ∈ Y₁) (w₁ x) 0 - ite (x ∈ Y₂) (w₂ x) 0 = 0 := hX' _ (hY₁ hx₁) - simpa [hx₁, hx₂] using this - have h₄w₁ : ∑ y : E in Y₁ ∩ Y₂, w₁ y = 1 := by - rw [Finset.sum_subset (Finset.inter_subset_left Y₁ Y₂), h₂w₁] - rintro x - simp_intro hx₁ hx₂ - exact t₁ x hx₁ hx₂ - rw [Finset.convexHull_eq] - refine' ⟨w₁, _, h₄w₁, _⟩ - · simp only [and_imp, Finset.mem_inter] - exact fun y hy₁ _ ↦ h₁w₁ y hy₁ - · rw [Finset.centerMass_eq_of_sum_1 _ _ h₄w₁] - dsimp only [id.def] - rw [Finset.sum_subset (Finset.inter_subset_left Y₁ Y₂), h₃w₁] - rintro x - simp_intro hx₁ hx₂ - exact Or.inl $ t₁ x hx₁ hx₂ - -/-- If an affine independent finset is contained in the convex hull of another finset, then it is -smaller than that finset. -/ -lemma AffineIndependent.card_le_card_of_subset_convexHull {X Y : Finset E} - (hX : AffineIndependent 𝕜 ((↑) : X → E)) (hXY : (X : Set E) ⊆ convexHull 𝕜 ↑Y) : - X.card ≤ Y.card := by - obtain rfl | h₁ := X.eq_empty_or_nonempty - · simp - obtain rfl | h₂ := Y.eq_empty_or_nonempty - · simp only [Finset.coe_empty, convexHull_empty, Set.subset_empty_iff, Finset.coe_eq_empty] at hXY - subst hXY - rfl - have X_card_pos : 1 ≤ X.card := h₁.card_pos - have X_eq_succ : Fintype.card (X : Set E) = X.card - 1 + 1 := by - simp [Nat.sub_add_cancel ‹1 ≤ X.card›] - have Y_card_pos : 1 ≤ Y.card := h₂.card_pos - have Y_eq_succ : Fintype.card (Y : Set E) = Y.card - 1 + 1 := by - simp [Nat.sub_add_cancel ‹1 ≤ Y.card›] - have direction_le := AffineSubspace.direction_le (affineSpan_mono 𝕜 hXY) - rw [affineSpan_convexHull] at direction_le - letI : FiniteDimensional 𝕜 (vectorSpan 𝕜 (Y : Set E)) := - finiteDimensional_vectorSpan_of_finite _ Y.finite_toSet - rw [direction_affineSpan, direction_affineSpan] at direction_le - have finrank_le := Submodule.finrank_le_finrank_of_le direction_le - erw [← @Subtype.range_coe _ (X : Set E), ← @Subtype.range_coe _ (Y : Set E), - hX.finrank_vectorSpan X_eq_succ] at finrank_le - have := le_trans finrank_le (finrank_vectorSpan_range_le 𝕜 ((↑) : Y → E) Y_eq_succ) - rwa [tsub_le_tsub_iff_right] at this - exact Y_card_pos diff --git a/LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean index 525c00cc85..4772815b6f 100644 --- a/LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean +++ b/LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean @@ -1,5 +1,4 @@ import Mathlib.Analysis.Convex.SimplicialComplex.Basic -import LeanCamCombi.Mathlib.Analysis.Convex.Combination import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional open Finset Geometry diff --git a/LeanCamCombi/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean b/LeanCamCombi/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean deleted file mode 100644 index 89e287f6ad..0000000000 --- a/LeanCamCombi/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean +++ /dev/null @@ -1,426 +0,0 @@ -/- -Copyright (c) 2023 Yaël Dillies, Vladimir Ivanov. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Yaël Dillies, Vladimir Ivanov --/ -import Mathlib.Algebra.BigOperators.Intervals -import Mathlib.Algebra.BigOperators.Order -import Mathlib.Algebra.BigOperators.Ring -import Mathlib.Data.Finset.Sups -import Mathlib.Order.Hom.Lattice -import Mathlib.Tactic.FieldSimp -import Mathlib.Tactic.Ring - -/-! -# The Ahlswede-Zhang identity - -This file proves the Ahlswede-Zhang identity, which is a nontrivial relation between the size of the -"truncated unions" of a set family. It sharpens the Lubell-Yamamoto-Meshalkin inequality -`Finset.sum_card_slice_div_choose_le_one`, by making explicit the correction term. - -For a set family `𝒜`, the Ahlswede-Zhang identity states that the sum of -`|⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|)` is exactly `1`. This implies the LYM inequality since -for an antichain `𝒜` and every `B ∈ 𝒜` we have -`|⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|) = 1 / n.choose |A|`. - -## Main declarations - -* `Finset.truncatedSup`: `s.truncatedSup a` is the supremum of all `b ≤ a` in `𝒜` if there are - some, or `⊤` if there are none. -* `Finset.truncatedInf` `s.truncatedInf a` is the infimum of all `b ≥ a` in `𝒜` if there are - some, or `⊥` if there are none. -* `AhlswedeZhang.infSum`: RHS of the Ahlswede-Zhang identity. -* `AhlswedeZhang.le_infSum`: The sum of `1 / n.choose |A|` over an antichain is less than the RHS of - the Ahlswede-Zhang identity. -* `AhlswedeZhang.infSum_eq_one`: Ahlswede-Zhang identity. - -## References - -* [R. Ahlswede, Z. Zhang, *An identity in combinatorial extremal theory*](https://doi.org/10.1016/0001-8708(90)90023-G) -* [D. T. Tru, *An AZ-style identity and Bollobás deficiency*](https://doi.org/10.1016/j.jcta.2007.03.005) --/ - -section -variable (α : Type*) [Fintype α] [Nonempty α] {m n : ℕ} - -open Finset Fintype Nat -open scoped BigOperators - -private lemma binomial_sum_eq (h : n < m) : - ∑ i in range (n + 1), (n.choose i * (m - n) / ((m - i) * m.choose i) : ℚ) = 1 := by - set f : ℕ → ℚ := fun i ↦ n.choose i * (m.choose i : ℚ)⁻¹ with hf - suffices : ∀ i ∈ range (n + 1), f i - f (i + 1) = n.choose i * (m - n) / ((m - i) * m.choose i) - · rw [← sum_congr rfl this, sum_range_sub', hf] - simp [choose_self, choose_zero_right, choose_eq_zero_of_lt h] - intro i h₁ - rw [mem_range] at h₁ - have h₁ := le_of_lt_succ h₁ - have h₂ := h₁.trans_lt h - have h₃ := h₂.le - have hi₄ : (i + 1 : ℚ) ≠ 0 := by - have := (@cast_ne_zero ℚ _ _ _).mpr (succ_ne_zero i) - push_cast at this - exact this - have := congr_arg ((↑) : ℕ → ℚ) (choose_succ_right_eq m i) - push_cast at this - dsimp [hf] - rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this] - have := congr_arg ((↑) : ℕ → ℚ) (choose_succ_right_eq n i) - push_cast at this - rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this] - have : (m - i : ℚ) ≠ 0 := sub_ne_zero_of_ne (cast_lt.mpr h₂).ne' - have : (m.choose i : ℚ) ≠ 0 := cast_ne_zero.2 (choose_pos h₂.le).ne' - field_simp - ring - -private lemma Fintype.sum_div_mul_card_choose_card : - ∑ s : Finset α, (card α / ((card α - s.card) * (card α).choose s.card) : ℚ) = - card α * ∑ k in range (card α), (↑k)⁻¹ + 1 := by - rw [← powerset_univ, powerset_card_disjiUnion, sum_disjiUnion] - have : ∀ {x : ℕ}, ∀ s ∈ powersetCard x (univ : Finset α), - (card α / ((card α - Finset.card s) * (card α).choose (Finset.card s)) : ℚ) = - card α / ((card α - x) * (card α).choose x) - · intros n s hs - rw [mem_powersetCard_univ.1 hs] - simp_rw [sum_congr rfl this, sum_const, card_powersetCard, card_univ] - simp - simp_rw [mul_div, mul_comm, ← mul_div] - rw [← mul_sum, ← mul_inv_cancel (cast_ne_zero.mpr card_ne_zero : (card α : ℚ) ≠ 0), ← mul_add, - add_comm _ ((card α)⁻¹ : ℚ), ← sum_insert (f := fun x : ℕ ↦ (x⁻¹ : ℚ)) not_mem_range_self, - ← range_succ] - have : ∀ x ∈ range (card α + 1), - ((card α).choose x / ((card α - x) * (card α).choose x) : ℚ) = (card α - x : ℚ)⁻¹ - · intros n hn - rw [div_mul_left] - · simp - · exact cast_ne_zero.2 (choose_pos $ mem_range_succ_iff.1 hn).ne' - simp only [sum_congr rfl this, mul_eq_mul_left_iff] - convert Or.inl $ Finset.sum_range_reflect _ _ with x hx - rw [tsub_right_comm, ← tsub_add_eq_tsub_tsub, cast_sub (mem_range.1 hx)] - simp - -end - -open scoped FinsetFamily - -namespace Finset -variable {α β : Type*} - -/-! ### Truncated supremum, truncated infimum -/ - -section SemilatticeSup -variable [SemilatticeSup α] [OrderTop α] [@DecidableRel α (· ≤ ·)] [SemilatticeSup β] - [BoundedOrder β] [@DecidableRel β (· ≤ ·)] {s t : Finset α} {a b : α} - -private lemma sup_aux : a ∈ lowerClosure s → (s.filter fun b ↦ a ≤ b).Nonempty := - fun ⟨b, hb, hab⟩ ↦ ⟨b, mem_filter.2 ⟨hb, hab⟩⟩ - -/-- The infimum of the elements of `s` less than `a` if there are some, otherwise `⊤`. -/ -def truncatedSup (s : Finset α) (a : α) : α := - if h : a ∈ lowerClosure s then (s.filter fun b ↦ a ≤ b).sup' (sup_aux h) id else ⊤ - -lemma truncatedSup_of_mem (h : a ∈ lowerClosure s) : - truncatedSup s a = (s.filter fun b ↦ a ≤ b).sup' (sup_aux h) id := dif_pos h - -lemma truncatedSup_of_not_mem (h : a ∉ lowerClosure s) : truncatedSup s a = ⊤ := dif_neg h - -@[simp] lemma truncatedSup_empty (a : α) : truncatedSup ∅ a = ⊤ := truncatedSup_of_not_mem $ by simp - -@[simp] lemma truncatedSup_singleton (b a : α) : truncatedSup {b} a = if a ≤ b then b else ⊤ := by - simp [truncatedSup]; split_ifs <;> simp [*] - -lemma le_truncatedSup : a ≤ truncatedSup s a := by - rw [truncatedSup] - split_ifs with h - · obtain ⟨ℬ, hb, h⟩ := h - exact h.trans $ le_sup' id $ mem_filter.2 ⟨hb, h⟩ - · exact le_top - -lemma map_truncatedSup (e : α ≃o β) (s : Finset α) (a : α) : - e (truncatedSup s a) = truncatedSup (s.map e.toEquiv.toEmbedding) (e a) := by - have : e a ∈ lowerClosure (s.map e.toEquiv.toEmbedding : Set β) ↔ a ∈ lowerClosure s - · simp - simp_rw [truncatedSup, apply_dite e, map_finset_sup', map_top, this] - congr with h - simp only [filter_map, Function.comp, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv, - OrderIso.le_iff_le, id.def] - rw [sup'_map] - -- TODO: Why can't `simp` use `Finset.sup'_map`? - simp only [sup'_map, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv, Function.comp_apply] - -variable [DecidableEq α] - -private lemma lower_aux : a ∈ lowerClosure ↑(s ∪ t) ↔ a ∈ lowerClosure s ∨ a ∈ lowerClosure t := by rw [coe_union, lowerClosure_union, LowerSet.mem_sup_iff] - -lemma truncatedSup_union (hs : a ∈ lowerClosure s) (ht : a ∈ lowerClosure t) : - truncatedSup (s ∪ t) a = truncatedSup s a ⊔ truncatedSup t a := by - simpa only [truncatedSup_of_mem, hs, ht, lower_aux.2 (Or.inl hs), filter_union] using - sup'_union _ _ _ - -lemma truncatedSup_union_left (hs : a ∈ lowerClosure s) (ht : a ∉ lowerClosure t) : - truncatedSup (s ∪ t) a = truncatedSup s a := by - simp only [mem_lowerClosure, mem_coe, exists_prop, not_exists, not_and] at ht - simp only [truncatedSup_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty, - lower_aux.2 (Or.inl hs), ht] - -lemma truncatedSup_union_right (hs : a ∉ lowerClosure s) (ht : a ∈ lowerClosure t) : - truncatedSup (s ∪ t) a = truncatedSup t a := by rw [union_comm, truncatedSup_union_left ht hs] - -lemma truncatedSup_union_of_not_mem (hs : a ∉ lowerClosure s) (ht : a ∉ lowerClosure t) : - truncatedSup (s ∪ t) a = ⊤ := truncatedSup_of_not_mem fun h ↦ (lower_aux.1 h).elim hs ht - -lemma truncatedSup_of_isAntichain (hs : IsAntichain (· ≤ ·) (s : Set α)) (ha : a ∈ s) : - truncatedSup s a = a := by - refine' le_antisymm _ le_truncatedSup - simp_rw [truncatedSup_of_mem (subset_lowerClosure ha), sup'_le_iff, mem_filter] - rintro b ⟨hb, hab⟩ - exact (hs.eq ha hb hab).ge - -end SemilatticeSup - -section SemilatticeInf -variable [SemilatticeInf α] [BoundedOrder α] [@DecidableRel α (· ≤ ·)] [SemilatticeInf β] - [BoundedOrder β] [@DecidableRel β (· ≤ ·)] {s t : Finset α} {a : α} - -private lemma inf_aux : a ∈ upperClosure s → (s.filter (· ≤ a)).Nonempty := - fun ⟨b, hb, hab⟩ ↦ ⟨b, mem_filter.2 ⟨hb, hab⟩⟩ - -/-- The infimum of the elements of `s` less than `a` if there are some, otherwise `⊥`. -/ -def truncatedInf (s : Finset α) (a : α) : α := - if h : a ∈ upperClosure s then (s.filter (· ≤ a)).inf' (inf_aux h) id else ⊥ - -lemma truncatedInf_of_mem (h : a ∈ upperClosure s) : - truncatedInf s a = (s.filter (· ≤ a)).inf' (inf_aux h) id := dif_pos h - -lemma truncatedInf_of_not_mem (h : a ∉ upperClosure s) : truncatedInf s a = ⊥ := dif_neg h - -lemma truncatedInf_le : truncatedInf s a ≤ a := by - unfold truncatedInf - split_ifs with h - · obtain ⟨b, hb, hba⟩ := h - exact hba.trans' $ inf'_le id $ mem_filter.2 ⟨hb, ‹_›⟩ - · exact bot_le - -@[simp] lemma truncatedInf_empty (a : α) : truncatedInf ∅ a = ⊥ := truncatedInf_of_not_mem $ by simp - -@[simp] lemma truncatedInf_singleton (b a : α) : truncatedInf {b} a = if b ≤ a then b else ⊥ := by - simp [truncatedInf]; split_ifs <;> simp [*] - -lemma map_truncatedInf (e : α ≃o β) (s : Finset α) (a : α) : - e (truncatedInf s a) = truncatedInf (s.map e.toEquiv.toEmbedding) (e a) := by - have : e a ∈ upperClosure (s.map e.toEquiv.toEmbedding) ↔ a ∈ upperClosure s := by simp - simp_rw [truncatedInf, apply_dite e, map_finset_inf', map_bot, this] - congr with h - simp only [filter_map, Function.comp, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv, - OrderIso.le_iff_le, id.def] - rw [inf'_map] - -- TODO: Why can't `simp` use `Finset.inf'_map`? - simp only [Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv, Function.comp_apply] - -variable [DecidableEq α] - -private lemma upper_aux : a ∈ upperClosure ↑(s ∪ t) ↔ a ∈ upperClosure s ∨ a ∈ upperClosure t := by - rw [coe_union, upperClosure_union, UpperSet.mem_inf_iff] - -lemma truncatedInf_union (hs : a ∈ upperClosure s) (ht : a ∈ upperClosure t) : - truncatedInf (s ∪ t) a = truncatedInf s a ⊓ truncatedInf t a := by - simpa only [truncatedInf_of_mem, hs, ht, upper_aux.2 (Or.inl hs), filter_union] using - inf'_union _ _ _ - -lemma truncatedInf_union_left (hs : a ∈ upperClosure s) (ht : a ∉ upperClosure t) : - truncatedInf (s ∪ t) a = truncatedInf s a := by - simp only [mem_upperClosure, mem_coe, exists_prop, not_exists, not_and] at ht - simp only [truncatedInf_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty, - upper_aux.2 (Or.inl hs), ht] - -lemma truncatedInf_union_right (hs : a ∉ upperClosure s) (ht : a ∈ upperClosure t) : - truncatedInf (s ∪ t) a = truncatedInf t a := by - rw [union_comm, truncatedInf_union_left ht hs] - -lemma truncatedInf_union_of_not_mem (hs : a ∉ upperClosure s) (ht : a ∉ upperClosure t) : - truncatedInf (s ∪ t) a = ⊥ := - truncatedInf_of_not_mem $ by rw [coe_union, upperClosure_union]; exact fun h ↦ h.elim hs ht - -lemma truncatedInf_of_isAntichain (hs : IsAntichain (· ≤ ·) (s : Set α)) (ha : a ∈ s) : - truncatedInf s a = a := by - refine' le_antisymm truncatedInf_le _ - simp_rw [truncatedInf_of_mem (subset_upperClosure ha), le_inf'_iff, mem_filter] - rintro b ⟨hb, hba⟩ - exact (hs.eq hb ha hba).ge - -end SemilatticeInf - -section DistribLattice -variable [DistribLattice α] [BoundedOrder α] [DecidableEq α] [@DecidableRel α (· ≤ ·)] - {s t : Finset α} {a : α} - -private lemma infs_aux : a ∈ lowerClosure ↑(s ⊼ t) ↔ a ∈ lowerClosure s ∧ a ∈ lowerClosure t := by - rw [coe_infs, lowerClosure_infs, LowerSet.mem_inf_iff] - -private lemma sups_aux : a ∈ upperClosure ↑(s ⊻ t) ↔ a ∈ upperClosure s ∧ a ∈ upperClosure t := by - rw [coe_sups, upperClosure_sups, UpperSet.mem_sup_iff] - -lemma truncatedSup_infs (hs : a ∈ lowerClosure s) (ht : a ∈ lowerClosure t) : - truncatedSup (s ⊼ t) a = truncatedSup s a ⊓ truncatedSup t a := by - simp only [truncatedSup_of_mem, hs, ht, infs_aux.2 ⟨hs, ht⟩, sup'_inf_sup', filter_infs_le] - simp_rw [← image_inf_product] - rw [sup'_image] - rfl - -lemma truncatedInf_sups (hs : a ∈ upperClosure s) (ht : a ∈ upperClosure t) : - truncatedInf (s ⊻ t) a = truncatedInf s a ⊔ truncatedInf t a := by - simp only [truncatedInf_of_mem, hs, ht, sups_aux.2 ⟨hs, ht⟩, inf'_sup_inf', filter_sups_le] - simp_rw [← image_sup_product] - rw [inf'_image] - rfl - -lemma truncatedSup_infs_of_not_mem (ha : a ∉ lowerClosure s ⊓ lowerClosure t) : - truncatedSup (s ⊼ t) a = ⊤ := - truncatedSup_of_not_mem $ by rwa [coe_infs, lowerClosure_infs] - -lemma truncatedInf_sups_of_not_mem (ha : a ∉ upperClosure s ⊔ upperClosure t) : - truncatedInf (s ⊻ t) a = ⊥ := - truncatedInf_of_not_mem $ by rwa [coe_sups, upperClosure_sups] - -end DistribLattice - -section BooleanAlgebra -variable [BooleanAlgebra α] [@DecidableRel α (· ≤ ·)] {s : Finset α} {a : α} - -@[simp] lemma compl_truncatedSup (s : Finset α) (a : α) : - (truncatedSup s a)ᶜ = truncatedInf sᶜˢ aᶜ := map_truncatedSup (OrderIso.compl α) _ _ - -@[simp] lemma compl_truncatedInf (s : Finset α) (a : α) : - (truncatedInf s a)ᶜ = truncatedSup sᶜˢ aᶜ := map_truncatedInf (OrderIso.compl α) _ _ - -end BooleanAlgebra - -variable [DecidableEq α] [Fintype α] - -lemma card_truncatedSup_union_add_card_truncatedSup_infs (𝒜 ℬ : Finset (Finset α)) (s : Finset α) : - (truncatedSup (𝒜 ∪ ℬ) s).card + (truncatedSup (𝒜 ⊼ ℬ) s).card = - (truncatedSup 𝒜 s).card + (truncatedSup ℬ s).card := by - by_cases h𝒜 : s ∈ lowerClosure (𝒜 : Set $ Finset α) <;> - by_cases hℬ : s ∈ lowerClosure (ℬ : Set $ Finset α) - · rw [truncatedSup_union h𝒜 hℬ, truncatedSup_infs h𝒜 hℬ] - exact card_union_add_card_inter _ _ - · rw [truncatedSup_union_left h𝒜 hℬ, truncatedSup_of_not_mem hℬ, - truncatedSup_infs_of_not_mem fun h ↦ hℬ h.2] - · rw [truncatedSup_union_right h𝒜 hℬ, truncatedSup_of_not_mem h𝒜, - truncatedSup_infs_of_not_mem fun h ↦ h𝒜 h.1, add_comm] - · rw [truncatedSup_of_not_mem h𝒜, truncatedSup_of_not_mem hℬ, - truncatedSup_union_of_not_mem h𝒜 hℬ, truncatedSup_infs_of_not_mem fun h ↦ h𝒜 h.1] - -lemma card_truncatedInf_union_add_card_truncatedInf_sups (𝒜 ℬ : Finset (Finset α)) (s : Finset α) : - (truncatedInf (𝒜 ∪ ℬ) s).card + (truncatedInf (𝒜 ⊻ ℬ) s).card = - (truncatedInf 𝒜 s).card + (truncatedInf ℬ s).card := by - by_cases h𝒜 : s ∈ upperClosure (𝒜 : Set $ Finset α) <;> - by_cases hℬ : s ∈ upperClosure (ℬ : Set $ Finset α) - · rw [truncatedInf_union h𝒜 hℬ, truncatedInf_sups h𝒜 hℬ] - exact card_inter_add_card_union _ _ - · rw [truncatedInf_union_left h𝒜 hℬ, truncatedInf_of_not_mem hℬ, - truncatedInf_sups_of_not_mem fun h ↦ hℬ h.2] - · rw [truncatedInf_union_right h𝒜 hℬ, truncatedInf_of_not_mem h𝒜, - truncatedInf_sups_of_not_mem fun h ↦ h𝒜 h.1, add_comm] - · rw [truncatedInf_of_not_mem h𝒜, truncatedInf_of_not_mem hℬ, - truncatedInf_union_of_not_mem h𝒜 hℬ, truncatedInf_sups_of_not_mem fun h ↦ h𝒜 h.1] - -end Finset - -open Finset hiding card -open Fintype Nat -open scoped BigOperators - -namespace AhlswedeZhang -variable {α : Type*} [Fintype α] [DecidableEq α] {𝒜 ℬ : Finset (Finset α)} {s : Finset α} - -/-- Weighted sum of the size of the truncated infima of a set family. Relevant to the -Ahlswede-Zhang identity. -/ -def infSum (𝒜 : Finset (Finset α)) : ℚ := - ∑ s, (truncatedInf 𝒜 s).card / (s.card * (card α).choose s.card) - -/-- Weighted sum of the size of the truncated suprema of a set family. Relevant to the -Ahlswede-Zhang identity. -/ -def supSum (𝒜 : Finset (Finset α)) : ℚ := - ∑ s, (truncatedSup 𝒜 s).card / ((card α - s.card) * (card α).choose s.card) - -lemma supSum_union_add_supSum_infs (𝒜 ℬ : Finset (Finset α)) : - supSum (𝒜 ∪ ℬ) + supSum (𝒜 ⊼ ℬ) = supSum 𝒜 + supSum ℬ := by - unfold supSum - rw [← sum_add_distrib, ← sum_add_distrib, sum_congr rfl fun s _ ↦ _] - simp_rw [div_add_div_same, ← Nat.cast_add, card_truncatedSup_union_add_card_truncatedSup_infs] - simp - -lemma infSum_union_add_infSum_sups (𝒜 ℬ : Finset (Finset α)) : - infSum (𝒜 ∪ ℬ) + infSum (𝒜 ⊻ ℬ) = infSum 𝒜 + infSum ℬ := by - unfold infSum - rw [← sum_add_distrib, ← sum_add_distrib, sum_congr rfl fun s _ ↦ _] - simp_rw [div_add_div_same, ← Nat.cast_add, card_truncatedInf_union_add_card_truncatedInf_sups] - simp - -lemma IsAntichain.le_infSum (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) (h𝒜₀ : ∅ ∉ 𝒜) : - ∑ s in 𝒜, ((card α).choose s.card : ℚ)⁻¹ ≤ infSum 𝒜 := by - calc - _ = ∑ s in 𝒜, (truncatedInf 𝒜 s).card / (s.card * (card α).choose s.card : ℚ) := ?_ - _ ≤ _ := sum_le_univ_sum_of_nonneg fun s ↦ by positivity - refine' sum_congr rfl fun s hs ↦ _ - rw [truncatedInf_of_isAntichain h𝒜 hs, div_mul_right, one_div] - have := (nonempty_iff_ne_empty.2 $ ne_of_mem_of_not_mem hs h𝒜₀).card_pos - positivity - -variable [Nonempty α] - -@[simp] lemma supSum_singleton (hs : s ≠ univ) : - supSum ({s} : Finset (Finset α)) = card α * ∑ k in range (card α), (k : ℚ)⁻¹ := by - have : ∀ t : Finset α, - (card α - (truncatedSup {s} t).card : ℚ) / ((card α - t.card) * (card α).choose t.card) = - if t ⊆ s then (card α - s.card : ℚ) / ((card α - t.card) * (card α).choose t.card) else 0 - · rintro t - simp_rw [truncatedSup_singleton, le_iff_subset] - split_ifs <;> simp [card_univ] - simp_rw [← sub_eq_of_eq_add (Fintype.sum_div_mul_card_choose_card α), eq_sub_iff_add_eq, ← - eq_sub_iff_add_eq', supSum, ← sum_sub_distrib, ← sub_div] - rw [sum_congr rfl fun t _ ↦ this t, sum_ite, sum_const_zero, add_zero, filter_subset_univ, - sum_powerset, ← binomial_sum_eq ((card_lt_iff_ne_univ _).2 hs), eq_comm] - refine' sum_congr rfl fun n _ ↦ _ - rw [mul_div_assoc, ← nsmul_eq_mul] - exact sum_powersetCard n s fun m ↦ (card α - s.card : ℚ) / ((card α - m) * (card α).choose m) - -/-- The **Ahlswede-Zhang Identity**. -/ -lemma infSum_compls_add_supSum (𝒜 : Finset (Finset α)) : - infSum 𝒜ᶜˢ + supSum 𝒜 = card α * ∑ k in range (card α), (k : ℚ)⁻¹ + 1 := by - unfold infSum supSum - rw [← @map_univ_of_surjective (Finset α) _ _ _ ⟨compl, compl_injective⟩ compl_surjective, sum_map] - simp only [Function.Embedding.coeFn_mk, univ_map_embedding, ← compl_truncatedSup, ← - sum_add_distrib, card_compl, cast_sub (card_le_univ _), choose_symm (card_le_univ _), - div_add_div_same, sub_add_cancel, Fintype.sum_div_mul_card_choose_card] - -lemma supSum_of_not_univ_mem (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜) : - supSum 𝒜 = card α * ∑ k in range (card α), (k : ℚ)⁻¹ := by - set m := 𝒜.card with hm - clear_value m - induction' m using Nat.strong_induction_on with m ih generalizing 𝒜 - replace ih := fun 𝒜 h𝒜 h𝒜₁ h𝒜₂ ↦ @ih _ h𝒜 𝒜 h𝒜₁ h𝒜₂ rfl - obtain ⟨a, rfl⟩ | h𝒜₃ := h𝒜₁.exists_eq_singleton_or_nontrivial - · refine' supSum_singleton _ - simpa [eq_comm] using h𝒜₂ - cases m - · cases h𝒜₁.card_pos.ne hm - obtain ⟨s, 𝒜, hs, rfl, rfl⟩ := card_eq_succ.1 hm.symm - have h𝒜 : 𝒜.Nonempty := nonempty_iff_ne_empty.2 (by rintro rfl; simp at h𝒜₃) - rw [insert_eq, eq_sub_of_add_eq (supSum_union_add_supSum_infs _ _), singleton_infs, - supSum_singleton (ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂), ih, ih, add_sub_cancel] - · exact card_image_le.trans_lt (lt_add_one _) - · exact h𝒜.image _ - · simpa using fun _ ↦ ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂ - · exact lt_add_one _ - · exact h𝒜 - · exact fun h ↦ h𝒜₂ (mem_insert_of_mem h) - -/-- The **Ahlswede-Zhang Identity**. -/ -lemma infSum_eq_one (h𝒜₁ : 𝒜.Nonempty) (h𝒜₀ : ∅ ∉ 𝒜) : infSum 𝒜 = 1 := by - rw [← compls_compls 𝒜, eq_sub_of_add_eq (infSum_compls_add_supSum _), - supSum_of_not_univ_mem h𝒜₁.compls, add_sub_cancel'] - simpa - -end AhlswedeZhang diff --git a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Basic.lean index fa0bdb7969..c0efd33e5c 100644 --- a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -49,10 +49,6 @@ lemma ind_singleton (G : SimpleGraph α) (a : α) : G.ind {a} = ⊥ := by lemma ind_inter (G : SimpleGraph α) (s t : Set α) : G.ind (s ∩ t) = G.ind s ⊓ G.ind t := by ext; simp; tauto -@[simp] -lemma spanningCoe_induce (G : SimpleGraph α) (s : Set α) : - spanningCoe (induce (s : Set α) G) = G.ind s := by ext; simp [← and_assoc] - /-- Induced subgraphs on disjoint sets meet in the empty graph. -/ lemma disjoint_ind (h : Disjoint s t) : Disjoint (G.ind s) (G.ind t) := by rw [disjoint_iff, ← ind_inter, disjoint_iff_inter_eq_empty.1 h, ind_empty] diff --git a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Maps.lean b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Maps.lean new file mode 100644 index 0000000000..57193a747c --- /dev/null +++ b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Maps.lean @@ -0,0 +1,13 @@ +import Mathlib.Combinatorics.SimpleGraph.Maps +import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic + +variable {α : Type*} + +namespace SimpleGraph +section Ind + +@[simp] lemma spanningCoe_induce (G : SimpleGraph α) (s : Set α) : + spanningCoe (induce (s : Set α) G) = G.ind s := by ext; simp [← and_assoc] + +end Ind +end SimpleGraph diff --git a/LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean b/LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean index b8c04a9e91..e2b39b7cd5 100644 --- a/LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean +++ b/LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean @@ -46,7 +46,7 @@ variable [GeneralizedBooleanAlgebra α] [@DecidableRel α (· ≤ ·)] [Decidabl /-- The positive set difference of finsets `s` and `t` is the set of `a \ b` for `a ∈ s`, `b ∈ t`, `b ≤ a`. -/ def posDiffs (s t : Finset α) : Finset α := - ((s ×ˢ t).filter fun x ↦ x.2 ≤ x.1).image fun x ↦ x.1 \ x.2 + ((s ×ˢ t).filter fun (a, b) ↦ b ≤ a).image fun (a, b) ↦ a \ b scoped[FinsetFamily] infixl:70 " \\₊ " => Finset.posDiffs @@ -102,7 +102,7 @@ variable [Sub α] [Preorder α] [@DecidableRel α (· ≤ ·)] [DecidableEq α] /-- The positive subtraction of finsets `s` and `t` is the set of `a - b` for `a ∈ s`, `b ∈ t`, `b ≤ a`. -/ def posSub (s t : Finset α) : Finset α := - ((s ×ˢ t).filter fun x ↦ x.2 ≤ x.1).image fun x ↦ x.1 - x.2 + ((s ×ˢ t).filter fun (a, b) ↦ b ≤ a).image fun (a, b) ↦ a - b scoped[FinsetFamily] infixl:70 " -₊ " => Finset.posSub @@ -112,10 +112,9 @@ lemma mem_posSub : a ∈ s -₊ t ↔ ∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b - simp_rw [posSub, mem_image, mem_filter, mem_product, Prod.exists, and_assoc, exists_and_left] lemma posSub_subset_sub : s -₊ t ⊆ s - t := fun x ↦ by - rw [mem_posSub, mem_sub]; exact fun ⟨b, hb, c, hc, _, h⟩ ↦ ⟨b, c, hb, hc, h⟩ + rw [mem_posSub, mem_sub]; exact fun ⟨b, hb, c, hc, _, h⟩ ↦ ⟨b, hb, c, hc, h⟩ -lemma card_posSub_self_le (hs : (s : Set α).OrdConnected) : (s -₊ s).card ≤ s.card := - sorry +lemma card_posSub_self_le (hs : (s : Set α).OrdConnected) : (s -₊ s).card ≤ s.card := sorry end posSub end Finset diff --git a/LeanCamCombi/Schnirelmann.lean b/LeanCamCombi/Schnirelmann.lean index 06d9f8f689..5eede64766 100644 --- a/LeanCamCombi/Schnirelmann.lean +++ b/LeanCamCombi/Schnirelmann.lean @@ -7,405 +7,107 @@ import Mathlib.Data.Nat.Prime import Mathlib.Data.Real.Basic import Mathlib.Data.Set.Pointwise.SMul import Mathlib.GroupTheory.Submonoid.Operations +import LeanCamCombi.Mathlib.Algebra.Order.Sub.Canonical open Finset open scoped Classical Pointwise open Function +variable {A B : Set ℕ} {n : ℕ} + +/-- The Schnirelmann density of `A` is `1` if and only if `A` contains all the positive naturals. -/ +lemma one_le_schnirelmannDensity_iff : 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A := by + rw [schnirelmannDensity_le_one.ge_iff_eq, schnirelmannDensity_eq_one_iff] + +/-- The Schnirelmann density of `A` containing `0` is `1` if and only if `A` is the naturals. -/ +lemma one_le_schnirelmannDensity_iff_of_zero_mem (hA : 0 ∈ A) : + 1 ≤ schnirelmannDensity A ↔ A = Set.univ := by + rw [schnirelmannDensity_le_one.ge_iff_eq, schnirelmannDensity_eq_one_iff_of_zero_mem hA] + noncomputable def countelements (A : Set ℕ) (n : ℕ) : ℕ := -- for teaching purposes, Finset.card ((Icc 1 n).filter (· ∈ A)) -- writing this is better lemma countelements_nonneg (A : Set ℕ) (n : ℕ) : (0 ≤ countelements A n) := by positivity - -- -- ∧ (countelements A n ≤ n) := - -- -- have B := (Icc 1 n).filter (· ∈ A) - -- rw [countelements] - -- rw [← card_empty] - -- -- rw [← u] - -- apply card_le_of_subset - -- exact empty_subset ((Icc 1 n).filter (· ∈ A)) lemma card_Icc_one_n_n (n : ℕ) : card (Icc 1 n) = n := by rw [Nat.card_Icc 1 n, add_tsub_cancel_right] lemma countelements_le_n (A : Set ℕ) (n : ℕ) : countelements A n ≤ n := by - -- have u := filter_subset (· ∈ A) (Icc 1 n) - rw [countelements] - --have h := card_I - rw [← card_Icc_one_n_n n] - apply card_le_of_subset - rw [card_Icc_one_n_n n] - exact filter_subset (· ∈ A) (Icc 1 n) - -lemma sumset_contains_n (A B : Set ℕ) (n : ℕ) (ha : 0 ∈ A) (hb : 0 ∈ B) - (hc : n ≤ countelements A n + countelements B n) : n ∈ A + B := by - by_contra! h - have hna : n ∉ A := by - by_contra! - apply h - use n, 0 - simp only [add_zero, and_true] - exact { left := this, right := hb } - have hnb : n ∉ B := by - by_contra! - apply h - use 0, n - simp only [zero_add, and_true] - exact { left := ha, right := this} - have hca : countelements A (n - 1) = countelements A n := by - repeat rw [countelements] - apply le_antisymm - · refine card_le_of_subset ?_ - refine filter_subset_filter (· ∈ A) ?_ - refine Icc_subset_Icc_right ?_ - simp only [tsub_le_iff_right, le_add_iff_nonneg_right, zero_le_one] - · refine card_le_of_subset ?_ - refine Iff.mpr subset_iff ?_ - intro x hx - rw [mem_filter] - rw [mem_filter] at hx - constructor - · refine Iff.mpr mem_Icc ?_ - rw [mem_Icc] at hx - constructor - · exact hx.1.1 - · have hhx : x < n := by - have hxx : x ≠ n := by - by_contra! - apply hna - rw [← this] - exact hx.2 - refine Nat.lt_of_le_of_ne ?h₁ hxx - exact hx.1.2 - exact Nat.le_pred_of_lt hhx - · exact hx.2 - have hcb : countelements B (n - 1) = countelements B n := by - repeat rw [countelements] - apply le_antisymm - · refine card_le_of_subset ?_ - refine filter_subset_filter _ ?_ - refine Icc_subset_Icc_right ?_ - simp only [tsub_le_iff_right, le_add_iff_nonneg_right, zero_le_one] - · refine card_le_of_subset ?_ - refine Iff.mpr subset_iff ?_ - intro x hx - rw [mem_filter] - rw [mem_filter] at hx - constructor - · refine Iff.mpr mem_Icc ?_ - rw [mem_Icc] at hx - constructor - · exact hx.1.1 - · have hhx : x < n := by - have hxx : x ≠ n := by - by_contra! - apply hnb - rw [← this] - exact hx.2 - refine Nat.lt_of_le_of_ne ?hh hxx - exact hx.1.2 - exact Nat.le_pred_of_lt hhx - · exact hx.2 - rcases n.eq_zero_or_pos with hn0 | hn1 - · rw [hn0] at hna - rw [hn0] at hnb - contradiction - · have main : ∃ a b, a ∈ A ∧ b ∈ B ∧ (a : ℤ) = n - b := by - have lem1 : Finset.card (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1))) = countelements B (n-1) := by - rw [countelements] - set f := fun x ↦ n - x - have hfinj : Set.InjOn f (filter (fun x ↦ x ∈ B) (Icc 1 (n - 1))) := by -- (filter (fun x ↦ x ∈ B) (Icc 1 (n - 1))) - intro xx hxx yy hyy hfxy - simp only [ge_iff_le] at hfxy - simp only [ge_iff_le, gt_iff_lt, Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Icc, and_imp, - coe_filter, Set.mem_setOf_eq] at hxx - simp only [ge_iff_le, gt_iff_lt, Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Icc, and_imp, - coe_filter, Set.mem_setOf_eq] at hyy - have hnx : 0 < n - xx := by - obtain ⟨hx1, hx2⟩ := hxx - obtain ⟨hx11, hx12⟩ := hx1 - rw [← Nat.lt_add_one_iff] at hx12 - have : n - 1 + 1 = n := by - zify - aesop - rw [this] at hx12 - rwa [tsub_pos_iff_lt] - have hny : 0 < n - yy := by - obtain ⟨hy1, hy2⟩ := hyy - obtain ⟨hy11, hy12⟩ := hy1 - rw [← Nat.lt_add_one_iff] at hy12 - have : n - 1 + 1 = n := by - zify - aesop - rw [this] at hy12 - rwa [tsub_pos_iff_lt] - zify at hfxy - rw [Nat.cast_sub, Nat.cast_sub] at hfxy - · simp at hfxy - exact hfxy - · by_contra! hny0 - have : n - yy = 0 := by - have hhle : n ≤ yy := Nat.le_of_lt hny0 - rw [Nat.sub_eq_zero_of_le hhle] - rw [this] at hny - absurd hny - trivial - · by_contra! hnx0 - have : n - xx = 0 := by - have hhle : n ≤ xx := Nat.le_of_lt hnx0 - rw [Nat.sub_eq_zero_of_le hhle] - rw [this] at hnx - absurd hnx - trivial - have hfim : Finset.image f (filter (fun x ↦ x ∈ B) (Icc 1 (n - 1))) = (filter (fun x ↦ x ∈ {n} - B) (Icc 1 (n - 1))) := by - ext y - constructor - · intro hy - simp only [ge_iff_le, gt_iff_lt, Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Icc, and_imp, - mem_image, mem_filter] at hy - simp only [Set.singleton_sub, ge_iff_le, Set.mem_image, gt_iff_lt, Nat.lt_one_iff, - tsub_eq_zero_iff_le, mem_Icc, and_imp, not_exists, not_and, mem_filter] - obtain ⟨a, hya, hnay⟩ := hy - obtain ⟨hya1, hya2⟩ := hya - obtain ⟨hya11, hya12⟩ := hya1 - constructor - · constructor - · rw [← hnay] - rw [← Nat.lt_add_one_iff] at hya12 - have : n - 1 + 1 = n := by - zify - aesop - rw [this] at hya12 - -- zify - rw [Nat.one_le_iff_ne_zero] - exact Nat.sub_ne_zero_of_lt hya12 - · rw [← hnay, ← Nat.lt_add_one_iff] - have : n - 1 + 1 = n := by - zify - aesop - rw [this, tsub_lt_iff_right] - zify - · simp only [lt_add_iff_pos_right, Nat.cast_pos] - exact hya11 - · rw [← Nat.lt_add_one_iff, this] at hya12 - exact Nat.le_of_lt hya12 - · use a - · intro hy - simp only [Set.singleton_sub, ge_iff_le, Set.mem_image, gt_iff_lt, Nat.lt_one_iff, - tsub_eq_zero_iff_le, mem_Icc, and_imp, not_exists, not_and, mem_filter] at hy - simp only [ge_iff_le, gt_iff_lt, Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Icc, and_imp, - mem_image, mem_filter] - obtain ⟨hy1, x, hnxy⟩ := hy - obtain ⟨hy11, hy12⟩ := hy1 - obtain ⟨hx, hnxy1⟩ := hnxy - use x - constructor - · constructor - · constructor - · rw [← hnxy1, ← Nat.lt_add_one_iff] at hy12 - have : n - 1 + 1 = n := by - zify - aesop - rw [this, tsub_lt_iff_right] at hy12 - zify at hy12 - · simp only [lt_add_iff_pos_right, Nat.cast_pos] at hy12 - exact hy12 - · rw [← hnxy1] at hy11 - by_contra! hnx - have last : n - x = 0 := by - have hhle : n ≤ x := Nat.le_of_lt hnx - rw [Nat.sub_eq_zero_of_le hhle] - rw [last] at hy11 - absurd hy11 - trivial - · rw [← hnxy1] at hy11 - by_contra! hnx - have last : n - x ≤ 0 := by - rw [← Nat.add_one_le_iff] at hnx - have : n - 1 + 1 = n := by - zify - aesop - rw [this] at hnx - rw [Nat.sub_eq_zero_of_le hnx] - have abs : 1 ≤ 0 := le_trans hy11 last - absurd abs - trivial - · exact hx - · exact hnxy1 - rw [← hfim] - exact card_image_iff.mpr hfinj - have lem2 : (Icc 1 (n-1)).filter (· ∈ A) ∪ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1))) ⊆ Icc 1 (n-1) := by - intro x hx - simp only [ge_iff_le, gt_iff_lt, Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Icc, and_imp, - Set.singleton_sub, Set.mem_image, not_exists, not_and, mem_union, mem_filter] at hx - simp only [ge_iff_le, gt_iff_lt, Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Icc] - rcases hx with hx1 | hx2 - · exact hx1.1 - · exact hx2.1 - have lem3 : (Icc 1 (n-1)).filter (· ∈ A) ∩ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1))) ≠ ∅ := by - rw [← hca, ← hcb] at hc - have hun : Finset.card ((Icc 1 (n-1)).filter (· ∈ A) ∪ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1)))) ≤ n - 1 := by - nth_rewrite 3 [← card_Icc_one_n_n (n - 1)] - exact card_le_of_subset lem2 - have hui : Finset.card ((Icc 1 (n-1)).filter (· ∈ A) ∪ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1)))) - + Finset.card ((Icc 1 (n-1)).filter (· ∈ A) ∩ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1)))) = countelements A (n-1) + countelements B (n-1) := by - rw [card_union_add_card_inter, ← lem1, countelements] - have hin : 0 < Finset.card ((Icc 1 (n-1)).filter (· ∈ A) ∩ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1)))) := by - rw [← hui] at hc - -- have hip : 0 ≤ Finset.card ((Icc 1 (n-1)).filter (· ∈ A) ∩ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1)))) := by positivity - have hun1 : Finset.card ((Icc 1 (n-1)).filter (· ∈ A) ∪ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1)))) - + Finset.card ((Icc 1 (n-1)).filter (· ∈ A) ∩ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1)))) ≤ (n - 1) - + Finset.card ((Icc 1 (n-1)).filter (· ∈ A) ∩ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1)))) := add_le_add hun le_rfl - have hip0 : n ≤ (n - 1) + Finset.card ((Icc 1 (n-1)).filter (· ∈ A) ∩ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1)))) := le_trans hc hun1 - by_contra! hip - have hip1 : (n - 1) + Finset.card ((Icc 1 (n-1)).filter (· ∈ A) ∩ (Finset.filter (· ∈ {n} - B) (Icc 1 (n-1)))) ≤ (n - 1) := add_le_add le_rfl hip - have hnn : n ≤ (n - 1) := le_trans hip0 hip1 - rw [← not_lt] at hnn - apply hnn - rw [propext (Nat.lt_iff_le_pred hn1)] - rwa [← Finset.nonempty_iff_ne_empty, ← Finset.card_pos] - simp only [Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Icc, and_imp, Set.singleton_sub, Set.mem_image, ne_eq] at lem3 -- set is nonempty iff ? - have lem31 : A ∩ ({n} - B) ∩ Icc 1 (n-1) ≠ ∅ := by - intro hyp - apply lem3 - rw [← filter_and, filter_eq_empty_iff] - intro xx hxx - push_neg - intro hxa yy hyb - intro main - have : xx ∈ A ∩ ({n} - B) ∩ Icc 1 (n-1) := by - constructor - · constructor - · exact hxa - · rw [Set.mem_sub] - use n, yy - constructor - · rfl - · constructor - · exact hyb - · exact main - · exact hxx - rw [hyp] at this - contradiction - rw [← Set.nonempty_iff_ne_empty, Set.nonempty_def] at lem31 - obtain ⟨x, hx⟩ := lem31 - rw [Set.inter_def] at hx - obtain ⟨hx1, hx2⟩ := hx - use x, n - x - have hnx : x < n := by - simp only [Nat.lt_one_iff, tsub_eq_zero_iff_le, coe_Icc, not_le, Set.mem_Icc] at hx2 - zify - zify at hx2 - rw [Int.coe_pred_of_pos hn1] at hx2 - rw [← @Int.le_sub_one_iff] - exact hx2.2 - constructor - · simp_all only [Set.singleton_sub, Set.mem_image, Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Icc, and_imp, Set.mem_inter_iff, coe_Icc, not_le, Set.mem_Icc] - · constructor - · obtain ⟨hx11, hx12⟩ := hx1 - rw [Set.mem_sub] at hx12 - obtain ⟨xx, yy, hxx, hyy, hxy⟩ := hx12 - rw [Set.mem_singleton_iff] at hxx - rw [hxx] at hxy - zify at hxy - have : yy = n - x := by - zify - rw [Nat.cast_sub, eq_sub_iff_add_eq', ← eq_sub_iff_add_eq, ← Nat.cast_sub] - · exact id hxy.symm - · simp only [ge_iff_le, Nat.cast_inj] at hxy - rw [← hxy] at hx2 - simp only [ge_iff_le, gt_iff_lt, Nat.lt_one_iff, tsub_eq_zero_iff_le, coe_Icc, not_le, - Set.mem_Icc, tsub_le_iff_right] at hx2 - zify at hx2 - by_contra! hh - have : n - yy = 0 := by - have hhle : n ≤ yy := Nat.le_of_lt hh - rw [Nat.sub_eq_zero_of_le hhle] - rw [this] at hx2 - obtain ⟨hx21, hx22⟩ := hx2 - rw [← Int.not_lt] at hx21 - apply hx21 - simp only [Nat.cast_zero, zero_lt_one] - · exact Nat.le_of_lt hnx - rwa [← this] - aesop - apply h - obtain ⟨aa, bb, haa, hbb, hnn⟩ := main - rw [eq_sub_iff_add_eq] at hnn - rw [Set.mem_add] - use aa, bb - constructor - · exact haa - · constructor - · exact hbb - · zify - exact hnn + simpa [countelements] using card_filter_le (Icc 1 n) _ +lemma countelements_pred (hn : n ∉ A) : countelements A (n - 1) = countelements A n := by + repeat rw [countelements] + refine (card_le_card $ filter_subset_filter (· ∈ A) $ Icc_subset_Icc_right ?_).antisymm ?_ + · simp only [tsub_le_iff_right, le_add_iff_nonneg_right, zero_le_one] + refine card_le_card fun x hx ↦ ?_ + rw [mem_filter] + rw [mem_filter, mem_Icc] at hx + refine ⟨mem_Icc.2 ⟨hx.1.1, Nat.le_pred_of_lt $ hx.1.2.lt_of_ne ?_⟩, hx.2⟩ + rintro rfl + exact hn hx.2 +lemma sumset_contains_n (hA : 0 ∈ A) (hB : 0 ∈ B) (hc : n ≤ countelements A n + countelements B n) : + n ∈ A + B := by + by_contra! h + have hnA : n ∉ A := Set.not_mem_subset (Set.subset_add_left _ hB) h + have hnB : n ∉ B := Set.not_mem_subset (Set.subset_add_right _ hA) h + have hca : countelements A (n - 1) = countelements A n := countelements_pred hnA + have hcb : countelements B (n - 1) = countelements B n := countelements_pred hnB + obtain rfl | hn1 := n.eq_zero_or_pos + · contradiction + apply h + have lem1 : ((Ioo 0 n).filter (· ∈ {n} - B)).card = countelements B (n - 1) := by + rw [countelements] + have hfim : Finset.image (n - ·) (filter (fun x ↦ x ∈ B) (Ioo 0 n)) = (filter (fun x ↦ x ∈ {n} - B) (Ioo 0 n)) := by ext; aesop + rw [← hfim, card_image_of_injOn] + congr + exact (tsub_add_cancel_of_le $ Nat.succ_le_iff.2 hn1).symm + · exact Set.InjOn.mono (fun x hx ↦ (mem_Ioo.1 (mem_filter.1 hx).1).2.le) $ + fun x hx y hy ↦ tsub_inj_right hx hy + have lem3 : ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)).Nonempty := by + rw [← hca, ← hcb] at hc + have hun : Finset.card ((Ioo 0 n).filter (· ∈ A) ∪ (Ioo 0 n).filter (· ∈ {n} - B)) ≤ n - 1 := by + rw [← filter_or, ← tsub_zero n, ← Nat.card_Ioo] + exact card_filter_le _ _ + have hui : ((Ioo 0 n).filter (· ∈ A) ∪ (Ioo 0 n).filter (· ∈ {n} - B)).card + + ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)).card = + countelements A (n - 1) + countelements B (n - 1) := by + rw [card_union_add_card_inter, ← lem1, countelements] + congr + exact (tsub_add_cancel_of_le $ Nat.succ_le_iff.2 hn1).symm + have hin : 0 < Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) := by + rw [← hui] at hc + -- have hip : 0 ≤ Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) := by positivity + have hun1 : Finset.card ((Ioo 0 n).filter (· ∈ A) ∪ (Ioo 0 n).filter (· ∈ {n} - B)) + + Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) ≤ (n - 1) + + Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) := add_le_add hun le_rfl + have hip0 : n ≤ (n - 1) + Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) := le_trans hc hun1 + by_contra! hip + have hip1 : (n - 1) + Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) ≤ (n - 1) := add_le_add le_rfl hip + have hnn : n ≤ (n - 1) := le_trans hip0 hip1 + rw [← not_lt] at hnn + apply hnn + rw [propext (Nat.lt_iff_le_pred hn1)] + rwa [← Finset.card_pos] + simp only [Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Ioo, and_imp, Set.singleton_sub, Set.mem_image, ne_eq] at lem3 -- set is nonempty iff ? + have lem31 : (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty := by + rw [← filter_and, ← coe_nonempty, coe_filter, Set.setOf_and, Set.setOf_and, Set.setOf_mem_eq, + Set.inter_comm] at lem3 + convert lem3 using 3 <;> ext <;> simp + obtain ⟨_, ⟨hxA, n, rfl, x, hxB, rfl⟩, hx⟩ := lem31 + simp only [Set.mem_Ioo, Nat.succ_le_iff, tsub_pos_iff_lt, tsub_le_iff_right] at hx + exact ⟨_, hxA, x, hxB, tsub_add_cancel_of_le hx.1.le⟩ -theorem sum_schnirelmannDensity_ge_one_sumset_nat (A B : Set ℕ) : - 0 ∈ A → 0 ∈ B → 1 ≤ schnirelmannDensity A + schnirelmannDensity B → Set.univ = A + B := by - intro hA hB h - have l := lt_trichotomy (schnirelmannDensity A) 0 - rcases l with l1 | l2 | l3 - · have ulb := schnirelmannDensity_nonneg (A := A) - have v : schnirelmannDensity A ≠ schnirelmannDensity A := by - refine LT.lt.ne ?h - exact lt_of_lt_of_le l1 ulb - -- simp only [ne_eq, not_true] - contradiction - · rw [l2] at h - simp only [zero_add, ge_iff_le] at h - have uub := schnirelmannDensity_le_one (A := B) - have hb : schnirelmannDensity B = 1 := le_antisymm uub h - have v := schnirelmannDensity_eq_one_iff (A := B) - have hsub : B ⊆ A + B := by - intro b hb - rw [Set.mem_add] - use 0 - use b - simp only [zero_add, and_true] - constructor - · exact hA - · exact hb - rw [v] at hb - rw [Set.Subset.antisymm_iff] - constructor - · have u : {0}ᶜ ⊆ A + B := le_trans hb hsub - intro x - rcases x.eq_zero_or_pos with rfl | hxek - · intro hzero - rw [Set.mem_add] - use 0, 0 - · intro hx - exact hsub (hb $ Nat.pos_iff_ne_zero.1 hxek) - · exact Set.subset_univ (A + B) - · rw [Set.Subset.antisymm_iff] - constructor - · have u : ∀ n : ℕ, n ≤ countelements A n + countelements B n := by - intro n - rcases n.eq_zero_or_pos with rfl | hnge₀ - · exact countelements_nonneg A 0 - · have ha : schnirelmannDensity A ≤ countelements A n / n := by - rw [countelements] - apply schnirelmannDensity_le_div - positivity - have hb : schnirelmannDensity B ≤ countelements B n / n := by - rw [countelements] - apply schnirelmannDensity_le_div - positivity - have hsum : schnirelmannDensity A + schnirelmannDensity B ≤ (countelements A n + countelements B n) / n := by - rw [add_div] - exact add_le_add ha hb - have hf : (1 : ℝ) ≤ (countelements A n + countelements B n) / n := le_trans h hsum - zify at hf - zify - rw [le_div_iff, one_mul] at hf - · norm_cast at hf - norm_cast - · positivity - intro n hn - refine sumset_contains_n _ _ _ hA hB $ u n - · exact Set.subset_univ (A + B) +theorem sum_schnirelmannDensity_ge_one_sumset_nat (hA : 0 ∈ A) (hB : 0 ∈ B) + (hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B) : A + B = Set.univ := by + refine Set.eq_univ_of_forall $ fun n ↦ sumset_contains_n hA hB ?_ + obtain rfl | hn := eq_or_ne n 0 + · exact countelements_nonneg A 0 + rw [← Nat.cast_le (α := ℝ), ← one_le_div (by positivity)] + calc + _ ≤ _ := hAB + _ ≤ _ := add_le_add (schnirelmannDensity_le_div hn) (schnirelmannDensity_le_div hn) + _ = _ := by push_cast; rw [add_div]; rfl noncomputable def next_elm (A : Set ℕ) (a : A) (n : ℕ) : ℕ := if h : ((Ioc ↑a n).filter (· ∈ A)).Nonempty then ((Ioc ↑a n).filter (· ∈ A)).min' h else n @@ -439,7 +141,7 @@ theorem le_schnirelmannDensity_add (A B : Set ℕ) (hA : 0 ∈ A) (hB : 0 ∈ B) constructor · intro i hi x hx rw [Set.mem_inter_iff] at hx - simp only [Set.mem_setOf_eq, ge_iff_le] at hx + simp only [Set.mem_setOf_eq] at hx exact hx.1.1 intro i hi x hx simp only [Set.mem_inter_iff, Set.mem_setOf_eq] at hx @@ -461,7 +163,7 @@ theorem le_schnirelmannDensity_add (A B : Set ℕ) (hA : 0 ∈ A) (hB : 0 ∈ B) have aux : countelements (⋃ a : A, {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)}) n ≤ countelements (A + B) n := by rw [countelements, countelements] - apply card_le_of_subset + apply card_le_card intro y repeat rw [mem_filter] intro hy @@ -497,7 +199,7 @@ theorem le_schnirelmannDensity_add (A B : Set ℕ) (hA : 0 ∈ A) (hB : 0 ∈ B) rw [hbeta] at hbo rw [lt_sub_iff_add_lt, zero_add, lt_iff_le_and_ne] exact ⟨schnirelmannDensity_le_one, hbo⟩ - simp only [add_le_add_iff_right, sub_pos, sub_neg, ge_iff_le] + simp only [add_le_add_iff_right, sub_pos, sub_neg] rw [← le_div_iff (hbn)] rw [mul_div_assoc] have hun : (1 - schnirelmannDensity B) / (1 - schnirelmannDensity B) = 1 := by diff --git a/README.md b/README.md index 606b92890c..562e43b65f 100644 --- a/README.md +++ b/README.md @@ -54,7 +54,6 @@ The following topics are covered in LeanCamCombi and could be upstreamed to math * Kneser's addition theorem * The Sylvester-Chvatal theorem -* The Ahlswede-Zhang inequality * Containment of graphs * Incidence algebras @@ -65,6 +64,7 @@ The following topics are archived because they are already covered by mathlib, b The following topics have been upstreamed to mathlib and no longer live in LeanCamCombi. +* The Ahlswede-Zhang inequality * The four functions theorem and related discrete correlation inequalities: FKG inequality, Holley inequality, Daykin inequality, Marica-Schönheim inequality * The Birkhoff representation theorem, non-categorical version * The Cauchy-Davenport theorem for general groups, and also for linearly ordered cancellative semigroup diff --git a/docs/index.md b/docs/index.md index 123e147fb4..cbf48b45e1 100644 --- a/docs/index.md +++ b/docs/index.md @@ -65,7 +65,6 @@ The following topics are covered in LeanCamCombi and could be upstreamed to math * Kneser's addition theorem * The Sylvester-Chvatal theorem -* The Ahlswede-Zhang inequality * Containment of graphs * Incidence algebras @@ -80,6 +79,7 @@ The following topics are archived because they are already covered by mathlib, b The following topics have been upstreamed to mathlib and no longer live in LeanCamCombi. +* The Ahlswede-Zhang inequality * The four functions theorem and related discrete correlation inequalities: FKG inequality, Holley inequality, Daykin inequality, Marica-Schönheim inequality * The Birkhoff representation theorem, non-categorical version * The Cauchy-Davenport theorem for general groups, and also for linearly ordered cancellative semigroup diff --git a/lake-manifest.json b/lake-manifest.json index 77fa137569..7f80eea5aa 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "ee49cf8fada1bf5a15592c399a925c401848227f", + "rev": "ca91956e8d5c311e00d6a69eb93d5eb5eef9b37d", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c", + "rev": "1c88406514a636d241903e2e288d21dc6d861e01", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a", + "rev": "2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,10 +31,10 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "31d41415d5782a196999d4fd8eeaef3cae386a5f", + "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.24", + "inputRev": "v0.0.25", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -46,10 +46,19 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/import-graph.git", + "type": "git", + "subDir": null, + "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "fb3fd7cd7a0004f3d9bc0daf99c3d767cf6e7600", + "rev": "18eeff5e177341cf18c792a07c8d85173ea06f12", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -85,7 +94,7 @@ {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "rev": "86d5c219a9ad7aa686c9e0e704af030e203c63a1", + "rev": "b7fad51b87a5f8fb3a238dc820ec40ebfa2a636e", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main",