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.

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

[Merged by Bors] - feat: The double factorial is positive #9102

Closed
wants to merge 2 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
12 changes: 12 additions & 0 deletions Mathlib/Data/Nat/Factorial/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -456,4 +456,16 @@ theorem descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k

end DescFactorial

lemma factorial_two_mul_le (n : ℕ) : (2 * n)! ≤ (2 * n) ^ n * n ! := by
rw [two_mul, ← factorial_mul_ascFactorial, mul_comm]
exact mul_le_mul_right' (ascFactorial_le_pow_add _ _) _

lemma two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) : 2 ^ n * n ! ≤ (2 * n) ! := by
obtain _ | n := n
· simp
rw [mul_comm, two_mul]
calc
_ ≤ (n + 1)! * (n + 2) ^ (n + 1) := mul_le_mul_left' (pow_le_pow_of_le_left le_add_self _) _
_ ≤ _ := Nat.factorial_mul_pow_le_factorial

end Nat
11 changes: 4 additions & 7 deletions Mathlib/Data/Nat/Factorial/BigOperators.lean
Original file line number Diff line number Diff line change
Expand Up @@ -30,13 +30,10 @@ theorem prod_factorial_pos : 0 < ∏ i in s, (f i)! :=
#align nat.prod_factorial_pos Nat.prod_factorial_pos

theorem prod_factorial_dvd_factorial_sum : (∏ i in s, (f i)!) ∣ (∑ i in s, f i)! := by
classical
induction' s using Finset.induction with a' s' has ih
· simp only [prod_empty, factorial, dvd_refl]
· simp only [Finset.prod_insert has, Finset.sum_insert has]
refine' dvd_trans (mul_dvd_mul_left (f a')! ih) _
apply Nat.factorial_mul_factorial_dvd_factorial_add
#align nat.prod_factorial_dvd_factorial_sum Nat.prod_factorial_dvd_factorial_sum
induction' s using Finset.cons_induction_on with a s has ih
· simp
· rw [prod_cons, Finset.sum_cons]
exact (mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)

theorem descFactorial_eq_prod_range (n : ℕ) : ∀ k, n.descFactorial k = ∏ i in range k, (n - i)
| 0 => rfl
Expand Down
27 changes: 27 additions & 0 deletions Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,10 @@ def doubleFactorial : ℕ → ℕ
-- This notation is `\!!` not two !'s
scoped notation:10000 n "‼" => Nat.doubleFactorial n

lemma doubleFactorial_pos : ∀ n, 0 < n‼
| 0 | 1 => zero_lt_one
| _n + 2 => mul_pos (succ_pos _) (doubleFactorial_pos _)

theorem doubleFactorial_add_two (n : ℕ) : (n + 2)‼ = (n + 2) * n‼ :=
rfl
#align nat.double_factorial_add_two Nat.doubleFactorial_add_two
Expand All @@ -50,6 +54,11 @@ theorem factorial_eq_mul_doubleFactorial : ∀ n : ℕ, (n + 1)! = (n + 1)‼ *
mul_assoc]
#align nat.factorial_eq_mul_double_factorial Nat.factorial_eq_mul_doubleFactorial

lemma doubleFactorial_le_factorial : ∀ n, n‼ ≤ n !
| 0 => le_rfl
| n + 1 => by
rw [factorial_eq_mul_doubleFactorial]; exact le_mul_of_pos_right n.doubleFactorial_pos

theorem doubleFactorial_two_mul : ∀ n : ℕ, (2 * n)‼ = 2 ^ n * n !
| 0 => rfl
| n + 1 => by
Expand Down Expand Up @@ -78,3 +87,21 @@ theorem doubleFactorial_eq_prod_odd :
#align nat.double_factorial_eq_prod_odd Nat.doubleFactorial_eq_prod_odd

end Nat

namespace Mathlib.Meta.Positivity
open Lean Meta Qq

/-- Extension for `Nat.doubleFactorial`. -/
@[positivity Nat.doubleFactorial _]
def evalDoubleFactorial : PositivityExt where eval {u α} _ _ e := do
if let 0 := u then -- lean4#3060 means we can't combine this with the match below
match α, e with
| ~q(ℕ), ~q(Nat.doubleFactorial $n) =>
assumeInstancesCommute
return .positive q(Nat.doubleFactorial_pos $n)
| _, _ => throwError "not Nat.doubleFactorial"
else throwError "not Nat.doubleFactorial"

example (n : ℕ) : 0 < n‼ := by positivity

end Mathlib.Meta.Positivity