/
DoubleFactorial.lean
106 lines (82 loc) · 3.33 KB
/
DoubleFactorial.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
/-
Copyright (c) 2023 Jake Levinson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jake Levinson
-/
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Positivity.Core
#align_import data.nat.factorial.double_factorial from "leanprover-community/mathlib"@"7daeaf3072304c498b653628add84a88d0e78767"
/-!
# Double factorials
This file defines the double factorial,
`n‼ := n * (n - 2) * (n - 4) * ...`.
## Main declarations
* `Nat.doubleFactorial`: The double factorial.
-/
open Nat
namespace Nat
/-- `Nat.doubleFactorial n` is the double factorial of `n`. -/
@[simp]
def doubleFactorial : ℕ → ℕ
| 0 => 1
| 1 => 1
| k + 2 => (k + 2) * doubleFactorial k
#align nat.double_factorial Nat.doubleFactorial
-- This notation is `\!!` not two !'s
@[inherit_doc] 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
theorem doubleFactorial_add_one (n : ℕ) : (n + 1)‼ = (n + 1) * (n - 1)‼ := by cases n <;> rfl
#align nat.double_factorial_add_one Nat.doubleFactorial_add_one
theorem factorial_eq_mul_doubleFactorial : ∀ n : ℕ, (n + 1)! = (n + 1)‼ * n‼
| 0 => rfl
| k + 1 => by
rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼,
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 Nat.le_mul_of_pos_right _ n.doubleFactorial_pos
theorem doubleFactorial_two_mul : ∀ n : ℕ, (2 * n)‼ = 2 ^ n * n !
| 0 => rfl
| n + 1 => by
rw [mul_add, mul_one, doubleFactorial_add_two, factorial, pow_succ, doubleFactorial_two_mul _,
succ_eq_add_one]
ring
#align nat.double_factorial_two_mul Nat.doubleFactorial_two_mul
open BigOperators
theorem doubleFactorial_eq_prod_even : ∀ n : ℕ, (2 * n)‼ = ∏ i in Finset.range n, 2 * (i + 1)
| 0 => rfl
| n + 1 => by
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_even _, mul_comm (2 * n)‼,
(by ring : 2 * (n + 1) = 2 * n + 2)]
rfl
#align nat.double_factorial_eq_prod_even Nat.doubleFactorial_eq_prod_even
theorem doubleFactorial_eq_prod_odd :
∀ n : ℕ, (2 * n + 1)‼ = ∏ i in Finset.range n, (2 * (i + 1) + 1)
| 0 => rfl
| n + 1 => by
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_odd _, mul_comm (2 * n + 1)‼,
(by ring : 2 * (n + 1) + 1 = 2 * n + 1 + 2)]
rfl
#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
match u, α, e with
| 0, ~q(ℕ), ~q(Nat.doubleFactorial $n) =>
assumeInstancesCommute
return .positive q(Nat.doubleFactorial_pos $n)
| _, _ => throwError "not Nat.doubleFactorial"
example (n : ℕ) : 0 < n‼ := by positivity
end Mathlib.Meta.Positivity