English
For all n, n# ≤ 4^n.
Русский
Для всех n выполняется неравенство n# ≤ 4^n.
LaTeX
$$$n\# \le 4^n$$$
Lean4
theorem primorial_le_4_pow (n : ℕ) : n# ≤ 4 ^ n := by
induction n using Nat.strong_induction_on with
| h n ihn =>
rcases n with - | n; · rfl
rcases n.even_or_odd with (⟨m, rfl⟩ | ho)
· rcases m.eq_zero_or_pos with (rfl | hm)
· decide
calc
(m + m + 1)# = (m + 1 + m)# := by rw [add_right_comm]
_ ≤ (m + 1)# * choose (m + 1 + m) (m + 1) := (primorial_add_le m.le_succ)
_ = (m + 1)# * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
_ ≤ 4 ^ (m + 1) * 4 ^ m :=
(mul_le_mul' (ihn _ <| succ_lt_succ <| (lt_add_iff_pos_left _).2 hm) (choose_middle_le_pow _))
_ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]
· rcases Decidable.eq_or_ne n 1 with (rfl | hn)
· decide
·
calc
(n + 1)# = n# := primorial_succ hn ho
_ ≤ 4 ^ n := (ihn n n.lt_succ_self)
_ ≤ 4 ^ (n + 1) := Nat.pow_le_pow_right four_pos n.le_succ
