PlainCombi: Upper bound on intersecting families #41
Conversation
YaelDillies
changed the title
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
Great work! Here's a style review. I will review the proof later
There was a problem hiding this comment.
Can you follow the UpperCamelCase convention for file names?
| Eq.symm (Nat.le_antisymm (inter A₁ A₁_in_𝒜 A₂ A₂_in_𝒜) (Nat.lt_succ.mp card_x₁_x₂)) | ||
| by_cases s_eq_inter_all : ∃ s , (k ≤ s.card) ∧ (∀a∈𝒜, s ⊆ a) | ||
| . obtain ⟨s,_,s_inter_a⟩ := s_eq_inter_all | ||
| let mp : (Finset α) → Finset α := fun a' ↦ (a'\s) |
There was a problem hiding this comment.
Instead of defining it with a let, you can write this function (\. \ s) wherever you need it (sorry, can't type unicode right now)
| have k_le_inter := inter A₁ A₁_in_𝒜 A₂ A₂_in_𝒜 | ||
| have inter_eq_k : #(A₁ ∩ A₂) = k := | ||
| Eq.symm (Nat.le_antisymm (inter A₁ A₁_in_𝒜 A₂ A₂_in_𝒜) (Nat.lt_succ.mp card_x₁_x₂)) | ||
| by_cases s_eq_inter_all : ∃ s , (k ≤ s.card) ∧ (∀a∈𝒜, s ⊆ a) |
There was a problem hiding this comment.
You tend to write too many brackets
| by_cases s_eq_inter_all : ∃ s , (k ≤ s.card) ∧ (∀a∈𝒜, s ⊆ a) | |
| by_cases s_eq_inter_all : ∃ s, k ≤ #s ∧ ∀a∈𝒜, s ⊆ a |
and can you make sure to use the # notation wherever possible?
YaelDillies
force-pushed
the
master
branch
2 times, most recently
from
0bf4401 to
1183dde
Compare
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
I think I figured out the argument you were missing. cf Zulip because typesetting on github seems a bit broken
| def IsIntersectingFamily (l : ℕ) (𝒜 : Finset (Finset α)) : Prop := | ||
| ∀ a ∈ 𝒜, ∀ b ∈ 𝒜, l ≤ (a ∩ b).card |
There was a problem hiding this comment.
Can you move this out of the Finset namespace and generalise to
| def IsIntersectingFamily (l : ℕ) (𝒜 : Finset (Finset α)) : Prop := | |
| ∀ a ∈ 𝒜, ∀ b ∈ 𝒜, l ≤ (a ∩ b).card | |
| def IsIntersectingFamilyWith (l : ℕ) (𝒜 : Set (Finset α)) : Prop := | |
| ∀ a ∈ 𝒜, ∀ b ∈ 𝒜, l ≤ #(a ∩ b) |
| _ = (Fintype.card α - (k + 1)).choose (Fintype.card α - (k + 1) - (r - (k + 1))) := by | ||
| rw [Nat.choose_symm];omega | ||
| _ = (Fintype.card α - (k + 1)).choose (Fintype.card α - r) := by congr 1;omega | ||
| _ = (Fintype.card α - k - 1).choose (Fintype.card α - r) := by congr 1 |
There was a problem hiding this comment.
I would expect something like the following to work
| _ = (Fintype.card α - (k + 1)).choose (Fintype.card α - (k + 1) - (r - (k + 1))) := by | |
| rw [Nat.choose_symm];omega | |
| _ = (Fintype.card α - (k + 1)).choose (Fintype.card α - r) := by congr 1;omega | |
| _ = (Fintype.card α - k - 1).choose (Fintype.card α - r) := by congr 1 | |
| _ = (Fintype.card α - k - 1).choose (Fintype.card α - r) := by | |
| rw [Nat.choose_symm]; omega |
| mul_assoc,←Nat.choose_succ_right_eq,mul_assoc] | ||
| omega | ||
| _ = (2 ^ (3*r) * (r * (Fintype.card α - k).choose (r-k) * (r-k)) / (Fintype.card α - k - (r - (k + 1)))) := by congr<;>omega | ||
| _ ≤ ( (Fintype.card α - k).choose (r-k) * (r-k) * (2 ^ (3*r) * r) / (Fintype.card α - k - (r - (k + 1)))) := by simp [←mul_assoc,Nat.le_of_eq,Nat.div_le_div_right,mul_comm] |
There was a problem hiding this comment.
Can you make sure not to exceed 100 characters per line?
| theorem IsIntersectingFamily.card_le_of_sized {l r:ℕ} {𝒜 : Finset (Finset α)} (sized𝒜 : @Set.Sized α r 𝒜) | ||
| (inter : IsIntersectingFamily l 𝒜) (n_much_bigger_r :2 ^ (3 * r) * r * r+ 5 * r ≤ Fintype.card α): | ||
| #𝒜 ≤ ((Fintype.card α)-l).choose (r-l) := by |
There was a problem hiding this comment.
| theorem IsIntersectingFamily.card_le_of_sized {l r:ℕ} {𝒜 : Finset (Finset α)} (sized𝒜 : @Set.Sized α r 𝒜) | |
| (inter : IsIntersectingFamily l 𝒜) (n_much_bigger_r :2 ^ (3 * r) * r * r+ 5 * r ≤ Fintype.card α): | |
| #𝒜 ≤ ((Fintype.card α)-l).choose (r-l) := by | |
| theorem IsIntersectingFamily.card_le_of_sized {l r : ℕ} {𝒜 : Finset (Finset α)} | |
| (sized𝒜 : 𝒜.toSet.Sized r) (inter : IsIntersectingFamily l 𝒜) | |
| (n_much_bigger_r : 2 ^ (3 * r) * r * r + 5 * r ≤ Fintype.card α) : | |
| #𝒜 ≤ (Fintype.card α - l).choose (r - l) := by |
| rw [card_sdiff] | ||
| exact congrFun (congrArg HSub.hSub (sized𝒜 x_in_𝒜)) #s | ||
| exact s_inter_a x x_in_𝒜 | ||
| rw [←card𝒜_eq_cardℬ] |
There was a problem hiding this comment.
| rw [←card𝒜_eq_cardℬ] | |
| rw [← card𝒜_eq_cardℬ] |
and below
|
Can you please merge master? I've turned on the mathlib linters in the project, so you will need to fix a few things. |
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
|
Can you make sure to resolve the conversations you've dealt with? Also don't forget https://github.com/YaelDillies/LeanCamCombi/pull/41/files#r1938239953 |
|
Hey, coming back to this: Are you planning on working on this further? If not, I'll gladly take over 😄 |
2 participants
Proof of theorem 1.17 from the the lecture notes. Closes #38.
The proof is slightly different for the lecture notes. As far as i understand, the original proof claims that given that
#U ≤ 3 * rand∀ a ∈ 𝒜, l + 1 ≤ #(a ∩ U)then#𝒜 ≤(3 * r).choose (l+1) * n.choose (r - (l+1)). I think this might be wrong as the bound should be something like the sum over i from 1 to r-l of(3 * r).choose (l+i) * (n-(l+i)).choose (r - (l+i)), and it is not clear to me how to recover the original bound from that. Instead i just bound this by the simpler bound of2 ^ (3*r) * ((n - k).choose (r-(k+1)) * r).