feat: The double factorial is positive (#9102)

and other basic results. Also include a positivity extension to encode that new result.

From LeanAPAP

Mathlib/Data/Nat/Factorial/Basic.lean

@@ -449,4 +449,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

Mathlib/Data/Nat/Factorial/BigOperators.lean

@@ -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

Mathlib/Data/Nat/Factorial/DoubleFactorial.lean

@@ -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
@@ -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
@@ -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