Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: Port Data.Nat.Choose.Central #2140

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat: Port Data.Nat.Choose.Central #2140

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
8fd7b86
feat: port Data.Nat.Choose.Central
casavaca Feb 7, 2023
c62aadf
Initial file copy from mathport
casavaca Feb 7, 2023
4bd95f1
automated fixes
casavaca Feb 7, 2023
66629e3
Mostly fixed, needs `decide!`
dupuisf Dec 18, 2022
92f2532
Make it build
casavaca Feb 7, 2023
4b80dd0
Supercedes #1091. Lint style and documentation.
casavaca Feb 7, 2023
2a9385b
Remove newly-added docstring.
casavaca Feb 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
3 changes: 3 additions & 0 deletions Mathlib/Data/Nat/Choose/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,9 @@ theorem choose_succ_succ (n k : ℕ) : choose (succ n) (succ k) = choose n k + c
rfl
#align nat.choose_succ_succ Nat.choose_succ_succ

theorem choose_succ_succ' (n k : ℕ) : choose (n + 1) (k + 1) = choose n k + choose n (k + 1) :=
rfl

theorem choose_eq_zero_of_lt : ∀ {n k}, n < k → choose n k = 0
| _, 0, hk => absurd hk (Nat.not_lt_zero _)
| 0, k + 1, _ => choose_zero_succ _
Expand Down
85 changes: 42 additions & 43 deletions Mathlib/Data/Nat/Choose/Central.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,15 @@
Copyright (c) 2021 Patrick Stevens. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Stevens, Thomas Browning
Ported by: Frédéric Dupuis

! This file was ported from Lean 3 source module data.nat.choose.central
! leanprover-community/mathlib commit 0a0ec35061ed9960bf0e7ffb0335f44447b58977
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Tactic.Linarith.Default
import Mathlib.Tactic.Linarith

/-!
# Central binomial coefficients
Expand All @@ -18,36 +19,40 @@ This file proves properties of the central binomial coefficients (that is, `nat.

## Main definition and results

* `nat.central_binom`: the central binomial coefficient, `(2 * n).choose n`.
* `nat.succ_mul_central_binom_succ`: the inductive relationship between successive central binomial
* `Nat.centralBinom`: the central binomial coefficient, `(2 * n).choose n`.
* `Nat.succ_mul_centralBinom_succ`: the inductive relationship between successive central binomial
coefficients.
* `nat.four_pow_lt_mul_central_binom`: an exponential lower bound on the central binomial
* `Nat.four_pow_lt_mul_centralBinom`: an exponential lower bound on the central binomial
coefficient.
* `succ_dvd_central_binom`: The result that `n+1 ∣ n.central_binom`, ensuring that the explicit
* `succ_dvd_centralBinom`: The result that `n+1 ∣ n.centralBinom`, ensuring that the explicit
definition of the Catalan numbers is integer-valued.
-/


namespace Nat

/-- The central binomial coefficient, `nat.choose (2 * n) n`.
/-- The central binomial coefficient, `Nat.choose (2 * n) n`.
-/
def centralBinom (n : ℕ) :=
(2 * n).choose n
#align nat.central_binom Nat.centralBinom

/-- expand centralBinom to its definition. -/
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
/-- expand centralBinom to its definition. -/
/-- expand `centralBinom` to its definition. -/

Also elsewhere. I applaud the fact that you want to improve documentation. But I would rather encourage you to not fix documentation while porting. Because it means an extra review duty while reviewing porting PRs. Let's stick to doing one thing at a time.

theorem centralBinom_eq_two_mul_choose (n : ℕ) : centralBinom n = (2 * n).choose n :=
rfl
#align nat.central_binom_eq_two_mul_choose Nat.centralBinom_eq_two_mul_choose

/-- centralBinom n > 0. -/
theorem centralBinom_pos (n : ℕ) : 0 < centralBinom n :=
choose_pos (Nat.le_mul_of_pos_left zero_lt_two)
#align nat.central_binom_pos Nat.centralBinom_pos

/-- centralBinom n ≠ 0. -/
theorem centralBinom_ne_zero (n : ℕ) : centralBinom n ≠ 0 :=
(centralBinom_pos n).ne'
#align nat.central_binom_ne_zero Nat.centralBinom_ne_zero

/-- The central binomial coefficient of 0 is 1. -/
@[simp]
theorem centralBinom_zero : centralBinom 0 = 1 :=
choose_zero_right _
Expand All @@ -59,15 +64,15 @@ theorem choose_le_centralBinom (r n : ℕ) : choose (2 * n) r ≤ centralBinom n
calc
(2 * n).choose r ≤ (2 * n).choose (2 * n / 2) := choose_le_middle r (2 * n)
_ = (2 * n).choose n := by rw [Nat.mul_div_cancel_left n zero_lt_two]

#align nat.choose_le_central_binom Nat.choose_le_centralBinom

theorem two_le_centralBinom (n : ℕ) (n_pos : 0 < n) : 2 ≤ centralBinom n :=
calc
2 ≤ 2 * n := le_mul_of_pos_right n_pos
_ = (2 * n).choose 1 := (choose_one_right (2 * n)).symm
_ ≤ centralBinom n := choose_le_centralBinom 1 n

#align nat.two_le_central_binom Nat.two_le_centralBinom

/-- An inductive property of the central binomial coefficient.
Expand All @@ -78,11 +83,11 @@ theorem succ_mul_centralBinom_succ (n : ℕ) :
(n + 1) * (2 * (n + 1)).choose (n + 1) = (2 * n + 2).choose (n + 1) * (n + 1) := mul_comm _ _
_ = (2 * n + 1).choose n * (2 * n + 2) := by rw [choose_succ_right_eq, choose_mul_succ_eq]
_ = 2 * ((2 * n + 1).choose n * (n + 1)) := by ring
_ = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) := by
rw [two_mul n, add_assoc, Nat.add_sub_cancel_left]
_ = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) := by rw [two_mul n, add_assoc,
Nat.add_sub_cancel_left]
_ = 2 * ((2 * n).choose n * (2 * n + 1)) := by rw [choose_mul_succ_eq]
_ = 2 * (2 * n + 1) * (2 * n).choose n := by rw [mul_assoc, mul_comm (2 * n + 1)]

#align nat.succ_mul_central_binom_succ Nat.succ_mul_centralBinom_succ

/-- An exponential lower bound on the central binomial coefficient.
Expand All @@ -92,63 +97,57 @@ This bound is of interest because it appears in
theorem four_pow_lt_mul_centralBinom (n : ℕ) (n_big : 4 ≤ n) : 4 ^ n < n * centralBinom n := by
induction' n using Nat.strong_induction_on with n IH
rcases lt_trichotomy n 4 with (hn | rfl | hn)
· clear IH
decide!
· norm_num [central_binom, choose]
obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (zero_lt_four.trans hn).ne'
· clear IH; exact False.elim ((not_lt.2 n_big) hn)
· norm_num [centralBinom, choose]
obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.not_eq_zero_of_lt hn)
calc
4 ^ (n + 1) < 4 * (n * central_binom n) :=
4 ^ (n + 1) < 4 * (n * centralBinom n) := lt_of_eq_of_lt (pow_succ'' n 4) $
(mul_lt_mul_left <| zero_lt_four' ℕ).mpr (IH n n.lt_succ_self (Nat.le_of_lt_succ hn))
_ ≤ 2 * (2 * n + 1) * central_binom n :=
by
rw [← mul_assoc]
linarith
_ = (n + 1) * central_binom (n + 1) := (succ_mul_central_binom_succ n).symm

_ ≤ 2 * (2 * n + 1) * centralBinom n := by rw [← mul_assoc]; linarith
_ = (n + 1) * centralBinom (n + 1) := (succ_mul_centralBinom_succ n).symm

#align nat.four_pow_lt_mul_central_binom Nat.four_pow_lt_mul_centralBinom

/-- An exponential lower bound on the central binomial coefficient.
This bound is weaker than `nat.four_pow_lt_mul_central_binom`, but it is of historical interest
This bound is weaker than `Nat.four_pow_lt_mul_centralBinom`, but it is of historical interest
because it appears in Erdős's proof of Bertrand's postulate.
-/
theorem four_pow_le_two_mul_self_mul_centralBinom :
∀ (n : ℕ) (n_pos : 0 < n), 4 ^ n ≤ 2 * n * centralBinom n
∀ (n : ℕ) (_ : 0 < n), 4 ^ n ≤ 2 * n * centralBinom n
| 0, pr => (Nat.not_lt_zero _ pr).elim
| 1, pr => by norm_num [central_binom, choose]
| 2, pr => by norm_num [central_binom, choose]
| 3, pr => by norm_num [central_binom, choose]
| n@(m + 4), _ =>
| 1, _ => by norm_num [centralBinom, choose]
| 2, _ => by norm_num [centralBinom, choose]
| 3, _ => by norm_num [centralBinom, choose]
| n + 4, _ =>
calc
4 ^ n ≤ n * centralBinom n := (four_pow_lt_mul_centralBinom _ le_add_self).le
_ ≤ 2 * n * centralBinom n := by
rw [mul_assoc]
refine' le_mul_of_pos_left zero_lt_two

4 ^ (n+4) ≤ (n+4) * centralBinom (n+4) := (four_pow_lt_mul_centralBinom _ le_add_self).le
_ ≤ 2 * (n+4) * centralBinom (n+4) := by rw [mul_assoc];
refine' le_mul_of_pos_left zero_lt_two
#align nat.four_pow_le_two_mul_self_mul_central_binom Nat.four_pow_le_two_mul_self_mul_centralBinom

/-- centralBinom (n+1) is dividable by two. -/
theorem two_dvd_centralBinom_succ (n : ℕ) : 2 ∣ centralBinom (n + 1) := by
use (n + 1 + n).choose n
rw [central_binom_eq_two_mul_choose, two_mul, ← add_assoc, choose_succ_succ, choose_symm_add, ←
two_mul]
rw [centralBinom_eq_two_mul_choose, two_mul, ← add_assoc,
choose_succ_succ' (n + 1 + n) n, choose_symm_add, ← two_mul]
#align nat.two_dvd_central_binom_succ Nat.two_dvd_centralBinom_succ

/-- centralBinom n, where 0 < n, is dividable by two. -/
theorem two_dvd_centralBinom_of_one_le {n : ℕ} (h : 0 < n) : 2 ∣ centralBinom n := by
rw [← Nat.succ_pred_eq_of_pos h]
exact two_dvd_central_binom_succ n.pred
exact two_dvd_centralBinom_succ n.pred
#align nat.two_dvd_central_binom_of_one_le Nat.two_dvd_centralBinom_of_one_le

/-- A crucial lemma to ensure that Catalan numbers can be defined via their explicit formula
`catalan n = n.central_binom / (n + 1)`. -/
`catalan n = n.centralBinom / (n + 1)`. -/
theorem succ_dvd_centralBinom (n : ℕ) : n + 1 ∣ n.centralBinom := by
have h_s : (n + 1).coprime (2 * n + 1) :=
by
have h_s : (n + 1).coprime (2 * n + 1) := by
rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
exact coprime_one_left n
apply h_s.dvd_of_dvd_mul_left
apply dvd_of_mul_dvd_mul_left zero_lt_two
rw [← mul_assoc, ← succ_mul_central_binom_succ, mul_comm]
exact mul_dvd_mul_left _ (two_dvd_central_binom_succ n)
apply Nat.dvd_of_mul_dvd_mul_left zero_lt_two
rw [← mul_assoc, ← succ_mul_centralBinom_succ, mul_comm]
exact mul_dvd_mul_left _ (two_dvd_centralBinom_succ n)
#align nat.succ_dvd_central_binom Nat.succ_dvd_centralBinom

end Nat