From e65ca70b2160088feed9ad645876f72ce3f01346 Mon Sep 17 00:00:00 2001 From: xbb Date: Tue, 7 Jan 2025 13:52:48 +0800 Subject: [PATCH 1/9] Chapter 2.3 --- .../Combinations.lean | 42 +++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 Combinatorics/PermutationsCombinations/Combinations.lean diff --git a/Combinatorics/PermutationsCombinations/Combinations.lean b/Combinatorics/PermutationsCombinations/Combinations.lean new file mode 100644 index 0000000..fd26274 --- /dev/null +++ b/Combinatorics/PermutationsCombinations/Combinations.lean @@ -0,0 +1,42 @@ +import Mathlib +import Combinatorics.PermutationsCombinations.permutation + + +open Nat Finset BigOperators + + +/- +Theorem 2.3.1 For 0 ≤ r ≤ n, P(n, r) = r! × C(n, r). Hence, C(n, r) = n! / (r! × (n - r)!). +-/ +theorem permutations_choose_Factorial (r : ℕ) (n : Finset α) (h : r ≤ n.card) (hp: (permutationsLength r n).card = n.card.factorial / (n.card - r).factorial) : + n.card.choose r = n.card.factorial / (r.factorial * (n.card - r).factorial) := by sorry + +-- theorem permutations_choose_Factorial' {n k : ℕ} (hk : k ≤ n) : +-- choose n k = n ! / (k ! * (n - k)!) := +-- choose_eq_factorial_div_factorial hk + + +/- + Corollary 2.3.2 For 0 ≤ r ≤ n, C(n, n - k) = C(n, k) +-/ +lemma choose_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k := + Nat.choose_symm hk + + +/- + Theorem 2.3.3 (Pascal's formula) For all integers n and k with 1 ≤ k ≤ n - 1, C(n, k) = C(n - 1, k - 1) + C(n - 1, k). +-/ + +theorem Pascal_formula {n k : ℕ} (hk1 : 1 ≤ k)(hkn : k ≤ n - 1) : + choose n k = choose (n - 1) (k - 1) + choose (n - 1) k := by + + have hn : 0 < n := by omega + have hk : 0 < k := by omega + rw [Nat.choose_eq_choose_pred_add hn hk] + +/- + Theorem 2.3.4 For n ≥ 0, C(n, 0) + C(n, 1) + ... + C(n, n) = 2^n. +-/ + +theorem sum_range_choose {n : ℕ} : ∑ k in range (n + 1), choose n k = 2 ^ n := + Nat.sum_range_choose n From 0c7a7501dbbb3c508f4baa8decb746d9adf3de16 Mon Sep 17 00:00:00 2001 From: xbb Date: Tue, 7 Jan 2025 13:55:18 +0800 Subject: [PATCH 2/9] update --- Combinatorics/PermutationsCombinations/Combinations.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Combinatorics/PermutationsCombinations/Combinations.lean b/Combinatorics/PermutationsCombinations/Combinations.lean index fd26274..429241f 100644 --- a/Combinatorics/PermutationsCombinations/Combinations.lean +++ b/Combinatorics/PermutationsCombinations/Combinations.lean @@ -11,9 +11,9 @@ Theorem 2.3.1 For 0 ≤ r ≤ n, P(n, r) = r! × C(n, r). Hence, C(n, r) = n! / theorem permutations_choose_Factorial (r : ℕ) (n : Finset α) (h : r ≤ n.card) (hp: (permutationsLength r n).card = n.card.factorial / (n.card - r).factorial) : n.card.choose r = n.card.factorial / (r.factorial * (n.card - r).factorial) := by sorry --- theorem permutations_choose_Factorial' {n k : ℕ} (hk : k ≤ n) : --- choose n k = n ! / (k ! * (n - k)!) := --- choose_eq_factorial_div_factorial hk +theorem permutations_choose_Factorial' {n k : ℕ} (hk : k ≤ n) : + choose n k = n ! / (k ! * (n - k)!) := + choose_eq_factorial_div_factorial hk /- From 5a2a6ecf7a553efaed93dc1b0e112cb1c18c0a76 Mon Sep 17 00:00:00 2001 From: xbb Date: Tue, 7 Jan 2025 13:58:29 +0800 Subject: [PATCH 3/9] update --- Combinatorics/PermutationsCombinations/Combinations.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Combinatorics/PermutationsCombinations/Combinations.lean b/Combinatorics/PermutationsCombinations/Combinations.lean index 429241f..d472a56 100644 --- a/Combinatorics/PermutationsCombinations/Combinations.lean +++ b/Combinatorics/PermutationsCombinations/Combinations.lean @@ -4,7 +4,7 @@ import Combinatorics.PermutationsCombinations.permutation open Nat Finset BigOperators - + /- Theorem 2.3.1 For 0 ≤ r ≤ n, P(n, r) = r! × C(n, r). Hence, C(n, r) = n! / (r! × (n - r)!). -/ From 36f9d43ea89d38d103ec95f4b2eabcedb746d451 Mon Sep 17 00:00:00 2001 From: xbb Date: Tue, 7 Jan 2025 14:07:02 +0800 Subject: [PATCH 4/9] Basic --- .../PermutationsCombinations/permutation.lean | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 Combinatorics/PermutationsCombinations/permutation.lean diff --git a/Combinatorics/PermutationsCombinations/permutation.lean b/Combinatorics/PermutationsCombinations/permutation.lean new file mode 100644 index 0000000..71b28ba --- /dev/null +++ b/Combinatorics/PermutationsCombinations/permutation.lean @@ -0,0 +1,55 @@ +import Mathlib.Data.List.Perm.Basic +import Mathlib.Data.Nat.Factorial.Basic +import Mathlib.Data.Finset.Card + +namespace List + +/-- +For each element x of the list l returns it and the remaining part. +-/ +def permutationsLengthAux : List α → List (α × List α) + | [] => [] + | x :: xs => (x, xs) :: (permutationsLengthAux xs).map (fun ⟨y, ys⟩ => ⟨y, x :: ys⟩) + +/-- +List of all r-permutations of the list l +-/ +def permutationsLength : ℕ → List α → List (List α) + | 0, _ => [[]] + | r + 1, l => List.flatten ((permutationsLengthAux l).map (fun ⟨x, xs⟩ => (permutationsLength r xs).map (List.cons x))) + +end List + +#eval List.permutationsLength 2 [1, 2, 3] + +namespace Multiset + +open List + +theorem permutationsLength_perm {r : ℕ} {l₁ l₂ : List α} (h : l₁ ~ l₂) : + permutationsLength r l₁ ~ permutationsLength r l₂ := by sorry + +def permutationsLength (r : ℕ) (s : Multiset α) : Multiset (List α) := + Quot.liftOn s (fun l => List.permutationsLength r l) (fun _ _ h => Quot.sound (permutationsLength_perm h)) + +namespace Nodup + +def permutationsLength {r : ℕ} {s : Multiset α} (h : s.Nodup) : + (permutationsLength r s).Nodup := by sorry + +end Nodup + +end Multiset + +namespace Finset + +def permutationsLength (r : ℕ) (s : Finset α) : Finset (List α) := + ⟨s.1.permutationsLength r, s.2.permutationsLength⟩ + +/-- +Theorem 2.2.1 For n and r positive integers with r ≤ s, P(n, r) = n × (n - 1) × … × (n - r + 1) +-/ +theorem permutationsLength_card (r : ℕ) (s : Finset α) (h : r ≤ s.card) : + (permutationsLength r s).card = s.card.factorial / (s.card - r).factorial := by sorry + +end Finset From ca2e02e66985666ae33b9c0365e0f972dc1a51dd Mon Sep 17 00:00:00 2001 From: xbb Date: Tue, 7 Jan 2025 15:19:23 +0800 Subject: [PATCH 5/9] example --- .../PermutationsCombinations/example.lean | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 Combinatorics/PermutationsCombinations/example.lean diff --git a/Combinatorics/PermutationsCombinations/example.lean b/Combinatorics/PermutationsCombinations/example.lean new file mode 100644 index 0000000..0fdf8de --- /dev/null +++ b/Combinatorics/PermutationsCombinations/example.lean @@ -0,0 +1,23 @@ +import Mathlib + + +open Nat + +open Finset + +open BigOperators + + +example {m n : ℕ} : + ∑ k in range (m + 1), choose (n + k) k = choose (n + m + 1) m := by + induction m with + | zero => + simp only [zero_add, range_one, sum_singleton, + add_zero, choose_zero_right] + + | succ m IH => + rw [sum_range_succ] + simp only [IH] + rw [choose_succ_succ] + simp only [succ_eq_add_one, add_left_inj] + ring_nf From 68a11cf225fa89b646a5ca6a131ab794ea6411da Mon Sep 17 00:00:00 2001 From: xbb Date: Wed, 8 Jan 2025 10:58:04 +0800 Subject: [PATCH 6/9] rename --- Combinatorics/PermutationsCombinations/Combinations.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Combinatorics/PermutationsCombinations/Combinations.lean b/Combinatorics/PermutationsCombinations/Combinations.lean index d472a56..04cea60 100644 --- a/Combinatorics/PermutationsCombinations/Combinations.lean +++ b/Combinatorics/PermutationsCombinations/Combinations.lean @@ -4,7 +4,7 @@ import Combinatorics.PermutationsCombinations.permutation open Nat Finset BigOperators - + /- Theorem 2.3.1 For 0 ≤ r ≤ n, P(n, r) = r! × C(n, r). Hence, C(n, r) = n! / (r! × (n - r)!). -/ @@ -19,7 +19,7 @@ theorem permutations_choose_Factorial' {n k : ℕ} (hk : k ≤ n) : /- Corollary 2.3.2 For 0 ≤ r ≤ n, C(n, n - k) = C(n, k) -/ -lemma choose_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k := +lemma choose_sub_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k := Nat.choose_symm hk @@ -29,7 +29,6 @@ lemma choose_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k := theorem Pascal_formula {n k : ℕ} (hk1 : 1 ≤ k)(hkn : k ≤ n - 1) : choose n k = choose (n - 1) (k - 1) + choose (n - 1) k := by - have hn : 0 < n := by omega have hk : 0 < k := by omega rw [Nat.choose_eq_choose_pred_add hn hk] @@ -38,5 +37,5 @@ theorem Pascal_formula {n k : ℕ} (hk1 : 1 ≤ k)(hkn : k ≤ n - 1) : Theorem 2.3.4 For n ≥ 0, C(n, 0) + C(n, 1) + ... + C(n, n) = 2^n. -/ -theorem sum_range_choose {n : ℕ} : ∑ k in range (n + 1), choose n k = 2 ^ n := +theorem sum_range_choose_two {n : ℕ} : ∑ k in range (n + 1), choose n k = 2 ^ n := Nat.sum_range_choose n From ec15bf9a2b120b269f1623b973b64810c41894f9 Mon Sep 17 00:00:00 2001 From: xbb Date: Wed, 8 Jan 2025 11:09:24 +0800 Subject: [PATCH 7/9] adjust import --- Combinatorics/PermutationsCombinations/Combinations.lean | 2 +- Combinatorics/PermutationsCombinations/example.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Combinatorics/PermutationsCombinations/Combinations.lean b/Combinatorics/PermutationsCombinations/Combinations.lean index 04cea60..24cec51 100644 --- a/Combinatorics/PermutationsCombinations/Combinations.lean +++ b/Combinatorics/PermutationsCombinations/Combinations.lean @@ -1,5 +1,5 @@ -import Mathlib import Combinatorics.PermutationsCombinations.permutation +import Mathlib.Data.Nat.Choose.Sum open Nat Finset BigOperators diff --git a/Combinatorics/PermutationsCombinations/example.lean b/Combinatorics/PermutationsCombinations/example.lean index 0fdf8de..bd40b01 100644 --- a/Combinatorics/PermutationsCombinations/example.lean +++ b/Combinatorics/PermutationsCombinations/example.lean @@ -1,4 +1,4 @@ -import Mathlib +import Mathlib.Data.Nat.Choose.Sum open Nat From d02692c671f7e75aa979b69bc055efbadb05a497 Mon Sep 17 00:00:00 2001 From: xbb Date: Thu, 9 Jan 2025 00:46:55 +0800 Subject: [PATCH 8/9] fix --- .../PermutationsCombinations/Combinations.lean | 16 +++++++--------- .../PermutationsCombinations/example.lean | 15 ++++++--------- 2 files changed, 13 insertions(+), 18 deletions(-) diff --git a/Combinatorics/PermutationsCombinations/Combinations.lean b/Combinatorics/PermutationsCombinations/Combinations.lean index 24cec51..050d1f6 100644 --- a/Combinatorics/PermutationsCombinations/Combinations.lean +++ b/Combinatorics/PermutationsCombinations/Combinations.lean @@ -5,37 +5,35 @@ import Mathlib.Data.Nat.Choose.Sum open Nat Finset BigOperators -/- +/-- Theorem 2.3.1 For 0 ≤ r ≤ n, P(n, r) = r! × C(n, r). Hence, C(n, r) = n! / (r! × (n - r)!). -/ -theorem permutations_choose_Factorial (r : ℕ) (n : Finset α) (h : r ≤ n.card) (hp: (permutationsLength r n).card = n.card.factorial / (n.card - r).factorial) : - n.card.choose r = n.card.factorial / (r.factorial * (n.card - r).factorial) := by sorry +theorem permutations_choose_Factorial (r : ℕ) (s : Finset α) (hp: (permutationsLength r s).card = s.card.factorial / (s.card - r).factorial) : + s.card.choose r = s.card.factorial / (r.factorial * (s.card - r).factorial) := by sorry theorem permutations_choose_Factorial' {n k : ℕ} (hk : k ≤ n) : choose n k = n ! / (k ! * (n - k)!) := choose_eq_factorial_div_factorial hk -/- +/-- Corollary 2.3.2 For 0 ≤ r ≤ n, C(n, n - k) = C(n, k) -/ lemma choose_sub_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k := Nat.choose_symm hk -/- +/-- Theorem 2.3.3 (Pascal's formula) For all integers n and k with 1 ≤ k ≤ n - 1, C(n, k) = C(n - 1, k - 1) + C(n - 1, k). -/ - theorem Pascal_formula {n k : ℕ} (hk1 : 1 ≤ k)(hkn : k ≤ n - 1) : choose n k = choose (n - 1) (k - 1) + choose (n - 1) k := by have hn : 0 < n := by omega have hk : 0 < k := by omega rw [Nat.choose_eq_choose_pred_add hn hk] -/- +/-- Theorem 2.3.4 For n ≥ 0, C(n, 0) + C(n, 1) + ... + C(n, n) = 2^n. -/ - -theorem sum_range_choose_two {n : ℕ} : ∑ k in range (n + 1), choose n k = 2 ^ n := +theorem sum_range_choose_two {n : ℕ} : ∑ k ∈ range (n + 1), choose n k = 2 ^ n := Nat.sum_range_choose n diff --git a/Combinatorics/PermutationsCombinations/example.lean b/Combinatorics/PermutationsCombinations/example.lean index bd40b01..b46076e 100644 --- a/Combinatorics/PermutationsCombinations/example.lean +++ b/Combinatorics/PermutationsCombinations/example.lean @@ -1,20 +1,17 @@ import Mathlib.Data.Nat.Choose.Sum -open Nat +open Nat Finset BigOperators -open Finset - -open BigOperators - - -example {m n : ℕ} : - ∑ k in range (m + 1), choose (n + k) k = choose (n + m + 1) m := by +/-- +Example For 0 ≤ m and 0 ≤ n, ∑ k ∈ range (m + 1), choose (n + k) k = choose (n + m + 1) m. +-/ +theorem sum_choose_eq_choose {m n : ℕ} : + ∑ k ∈ range (m + 1), choose (n + k) k = choose (n + m + 1) m := by induction m with | zero => simp only [zero_add, range_one, sum_singleton, add_zero, choose_zero_right] - | succ m IH => rw [sum_range_succ] simp only [IH] From 1ade878d7f315025b7486607df141972fbebe997 Mon Sep 17 00:00:00 2001 From: xbb Date: Tue, 14 Jan 2025 14:59:27 +0800 Subject: [PATCH 9/9] update --- .../Combinations.lean | 38 +++++++------ .../PermutationsCombinations/permutation.lean | 55 ------------------- 2 files changed, 20 insertions(+), 73 deletions(-) delete mode 100644 Combinatorics/PermutationsCombinations/permutation.lean diff --git a/Combinatorics/PermutationsCombinations/Combinations.lean b/Combinatorics/PermutationsCombinations/Combinations.lean index 050d1f6..7a07b2b 100644 --- a/Combinatorics/PermutationsCombinations/Combinations.lean +++ b/Combinatorics/PermutationsCombinations/Combinations.lean @@ -1,26 +1,29 @@ -import Combinatorics.PermutationsCombinations.permutation -import Mathlib.Data.Nat.Choose.Sum +import Mathlib.Data.Finset.Powerset +import Combinatorics.PermutationsCombinations.Permutations +open Nat Finset -open Nat Finset BigOperators +/-- Generate all possible subsets of size k from a given finite set s . +-/ +def combinations (r : ℕ) (s : Finset α) : Finset (Finset α) := + s.powersetCard r +theorem combinations_card (r : ℕ) (s : Finset α) : + s.card.choose r = (combinations r s).card := by + rw [combinations] + exact (Finset.card_powersetCard r s).symm /-- Theorem 2.3.1 For 0 ≤ r ≤ n, P(n, r) = r! × C(n, r). Hence, C(n, r) = n! / (r! × (n - r)!). -/ -theorem permutations_choose_Factorial (r : ℕ) (s : Finset α) (hp: (permutationsLength r s).card = s.card.factorial / (s.card - r).factorial) : - s.card.choose r = s.card.factorial / (r.factorial * (s.card - r).factorial) := by sorry - -theorem permutations_choose_Factorial' {n k : ℕ} (hk : k ≤ n) : - choose n k = n ! / (k ! * (n - k)!) := - choose_eq_factorial_div_factorial hk +theorem combinations_Factorial (r : ℕ) (s : Finset α) (h : r ≤ s.card) (hp: (permutationsLength r s).card = r.factorial * (combinations r s).card) : + (combinations r s).card = (Finset.card s).factorial / (r.factorial * (Finset.card s - r).factorial) := by sorry -/-- +/- Corollary 2.3.2 For 0 ≤ r ≤ n, C(n, n - k) = C(n, k) -/ -lemma choose_sub_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k := - Nat.choose_symm hk +-- This theorem has already been formalized in Mathlib under the name Nat.choose_symm. /-- @@ -28,12 +31,11 @@ lemma choose_sub_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k -/ theorem Pascal_formula {n k : ℕ} (hk1 : 1 ≤ k)(hkn : k ≤ n - 1) : choose n k = choose (n - 1) (k - 1) + choose (n - 1) k := by - have hn : 0 < n := by omega - have hk : 0 < k := by omega - rw [Nat.choose_eq_choose_pred_add hn hk] + rw [Nat.choose_eq_choose_pred_add (show 0 < n by omega) (show 0 < k by omega)] -/-- + + +/- Theorem 2.3.4 For n ≥ 0, C(n, 0) + C(n, 1) + ... + C(n, n) = 2^n. -/ -theorem sum_range_choose_two {n : ℕ} : ∑ k ∈ range (n + 1), choose n k = 2 ^ n := - Nat.sum_range_choose n +-- This theorem has already been formalized in Mathlib under the name Nat.sum_range_choose. diff --git a/Combinatorics/PermutationsCombinations/permutation.lean b/Combinatorics/PermutationsCombinations/permutation.lean deleted file mode 100644 index 71b28ba..0000000 --- a/Combinatorics/PermutationsCombinations/permutation.lean +++ /dev/null @@ -1,55 +0,0 @@ -import Mathlib.Data.List.Perm.Basic -import Mathlib.Data.Nat.Factorial.Basic -import Mathlib.Data.Finset.Card - -namespace List - -/-- -For each element x of the list l returns it and the remaining part. --/ -def permutationsLengthAux : List α → List (α × List α) - | [] => [] - | x :: xs => (x, xs) :: (permutationsLengthAux xs).map (fun ⟨y, ys⟩ => ⟨y, x :: ys⟩) - -/-- -List of all r-permutations of the list l --/ -def permutationsLength : ℕ → List α → List (List α) - | 0, _ => [[]] - | r + 1, l => List.flatten ((permutationsLengthAux l).map (fun ⟨x, xs⟩ => (permutationsLength r xs).map (List.cons x))) - -end List - -#eval List.permutationsLength 2 [1, 2, 3] - -namespace Multiset - -open List - -theorem permutationsLength_perm {r : ℕ} {l₁ l₂ : List α} (h : l₁ ~ l₂) : - permutationsLength r l₁ ~ permutationsLength r l₂ := by sorry - -def permutationsLength (r : ℕ) (s : Multiset α) : Multiset (List α) := - Quot.liftOn s (fun l => List.permutationsLength r l) (fun _ _ h => Quot.sound (permutationsLength_perm h)) - -namespace Nodup - -def permutationsLength {r : ℕ} {s : Multiset α} (h : s.Nodup) : - (permutationsLength r s).Nodup := by sorry - -end Nodup - -end Multiset - -namespace Finset - -def permutationsLength (r : ℕ) (s : Finset α) : Finset (List α) := - ⟨s.1.permutationsLength r, s.2.permutationsLength⟩ - -/-- -Theorem 2.2.1 For n and r positive integers with r ≤ s, P(n, r) = n × (n - 1) × … × (n - r + 1) --/ -theorem permutationsLength_card (r : ℕ) (s : Finset α) (h : r ≤ s.card) : - (permutationsLength r s).card = s.card.factorial / (s.card - r).factorial := by sorry - -end Finset