nat.factorial lemmas

Stream: Is there code for X?

[Yaël Dillies]

I have a goal of the form

import data.real.basic
import nat.choose.basic

example (n : ℕ) : (n.choose 2 : ℝ) ≤ n ^ 2 / 2 :=
begin
  sorry
end

Is there anything close to what I want, and if not what's the biggest generality I can prove stuff in? I can probably prove

lemma nat.choose_le_pow(n k : ℕ) : (n.choose k : ℝ) ≤ n^k / k.factorial :=
begin
  sorry
end

but I assume ℝ is not general enough?

[Yaël Dillies]

I already know this by the way: https://leanprover-community.github.io/mathlib_docs/data/nat/choose/dvd.html#nat.choose_eq_factorial_div_factorial

[Eric Rodriguez]

I'd probably prove it for docs#nat.desc_fac? With something like docs#nat.desc_fac_eq_factorial_mul_choose, I think that's essentially what you're doing, and then you can use a couple of the lemmas below there to transfer it to nCk. Also, desc_fac is well-linked to docs#pochhammer, which is a sweeping generalization, and all results transfer almost automatically

[Kevin Buzzard]

You asked a slightly different question on the Discord and here's my answer to that one:

import data.real.basic
import tactic

-- should be in mathlib?
theorem nat.cast_div {D : Type*} [division_ring D] (a b : ℕ) (hba : b ∣ a) (hb : (b : D) ≠ 0) :
  ((a / b : ℕ) : D) = a / b :=
by rw [← (mul_left_inj' hb), div_mul_cancel _ hb, ← nat.cast_mul, nat.div_mul_cancel hba]

-- might already be in mathlib?
@[elab_as_eliminator]
def nat.parity.cases_on (n : ℕ) {P : ℕ → Prop}
  (h_even : ∀ k, P (2 * k)) (h_odd : ∀ k, P (2 * k + 1)) :
  P n :=
begin
  rw ← nat.div_add_mod n 2,
  have hn : n % 2 < 2 := nat.mod_lt _ zero_lt_two,
  interval_cases (n%2); rw h,
  { exact h_even (n/2) },
  { exact h_odd (n/2) }
end

example (n : ℕ) : ((n * (n - 1)/2 : ℕ) : ℝ) = (n * (n - 1) : ℕ)/2 :=
begin
  rw nat.cast_div,
  { norm_cast },
  { apply nat.parity.cases_on n,
    { intro k, use k * (2 * k - 1), ring },
    { intro k, use k * (2 * k + 1), rw nat.add_sub_cancel, ring } },
  { norm_num }
end

Probably people can build on this.

[Ruben Van de Velde]

Simpler proofs (though why use nat subtraction?):

@[elab_as_eliminator]
def nat.parity.cases_on (n : ℕ) {P : ℕ → Prop}
  (h_even : ∀ k, P (2 * k)) (h_odd : ∀ k, P (2 * k + 1)) :
  P n :=
begin
  obtain ⟨k, (rfl|rfl)⟩ := nat.even_or_odd' n,
  exacts [h_even k, h_odd k],
end

example (n : ℕ) : ((n * (n - 1)/2 : ℕ) : ℝ) = (n * (n - 1) : ℕ)/2 :=
begin
  rw nat.cast_div,
  { norm_cast },
  { cases n,
    { simp },
    simp only [nat.succ_sub_succ_eq_sub, nat.sub_zero, mul_comm],
    exact nat.even_mul_succ_self n },
  { norm_num }
end

[Bhavik Mehta]

Ultimately the original question doesn't use nat subtraction anyway, so it would be nice to get solutions which don't introduce nat subtraction - Eric's approach seems promising

[Eric Rodriguez]

import data.nat.factorial

open nat

lemma asda {n} : ∀ {k}, desc_fac n k ≤ (n + k)^k
| 0 := by simp
| (k + 1) := by { rw [desc_fac_succ, pow_succ],
  exact nat.mul_le_mul (le_refl _) (by simp [asda.trans, pow_le_pow_of_le_left]) }

this will get you very close to the original lemma, and the desc_fac api will extend that to pochhammer, choose very easily

[Yaël Dillies]

Great! Thanks!

[Yaël Dillies]

Sorry, but why is desc_fac the ascending factorial?

[Eric Rodriguez]

yikes, I just googled and found out there's actually a convention

[Eric Rodriguez]

that's just how I named it at the time, that's pretty bad and probably deserves a rename

[Yaël Dillies]

I'm making a PR now :)

[Yaël Dillies]

I'm also taking the opportunity to define the actual descending factorial, as it seems more relevant in my use case.Real mathmos do not deal with nat substraction!

[Eric Rodriguez]

is this why I'm in Durham instead of Oxford/Cam? ;b

[Yaël Dillies]

If I remember correctly, the point of defining desc_fac (soon-to-be-called asc_fac!) was to allow for quick computation using norm_num for the birthday problem. Did you investigate whether it was preferable to multiply from the left vs from the right time-wise?

[Eric Rodriguez]

I didn't, I'm afraid - sorry! left mul made a lot more sense to me while writing lemmata, though

[Mario Carneiro]

Actually, neither order is optimal. Factorials can be calculated in O(n log n)

[Eric Rodriguez]

What algorithm calculates factorials that fast?

[Mario Carneiro]

Here's a simple recursive algorithm, called "Product Recursive" from http://www.luschny.de/math/factorial/index.html:

import data.nat.factorial

def factorial'_aux : ℕ → ℕ → ℕ
| n k := if k ≤ 1 then n else let l := k / 2 in
  factorial'_aux n l * factorial'_aux (n + l) (k - l)
using_well_founded {dec_tac := `[sorry]}

def factorial' (n : ℕ) := factorial'_aux 1 n

theorem factorial'_aux_eq (n k : ℕ) : factorial'_aux (n+1) k = nat.desc_fac n k := sorry

theorem factorial'_eq (n k : ℕ) : factorial' n = nat.factorial n := sorry

[Mario Carneiro]

The reason this is faster is that by binary splitting the factors we ensure that all multiplications are well balanced. The cost of a (naive) multiplication is the product of the number of digits of the factors, so it is a good idea to minimize the number of multiplications with a size close to the actual target value

[Mario Carneiro]

This is not the fastest algorithm (that luschny page describes 21(!) algorithms for calculating factorials); the fastest ones do some kind of prime factorization

[Yaël Dillies]

Nice! Will look that up.

[Yaël Dillies]

Where should I put lemmas about inequalities not using natural division? And how should I state them? Should I coerce to ℝ? to ℚ? to something more general?

[Kevin Buzzard]

a division ring if you don't need commutativity of multiplcation, and a field if you do, or maybe a semifield if such a thing exists (maybe the nonnegative reals are one??)

[Kevin Buzzard]

oh you need an order too -- @Damiano Testa what should Yael do here? What axioms do you use in your proofs Yael?

[Damiano Testa]

I would have to take a look, but if the proof mixes add and mul, then the ordered refactor has not reached it yet! I do not have time to look at this now, though. Also, since the lemmas that use the new typeclasses are still in PR, there is not much for you to try either...

[Mario Carneiro]

There are files ordered_group, ordered_ring, ordered_field in algebra roughly corresponding to whether you need addition, multiplication, or division

[Mario Carneiro]

so if you have a general theorem about le and div it would go in ordered_field

[Mario Carneiro]

like docs#le_div_iff

[Yaël Dillies]

My proof uses the def of nat.choose and monotonicity of division by a natural. That's it I think.

lemma choose_le_pow (r n : ℕ) : (n.choose r : ℚ) ≤ n^r / r.factorial :=
begin
  rw le_div_iff',
  { norm_cast,
    rw [←desc_fact_eq_factorial_mul_choose],
    exact desc_fact_le_pow n r },
  exact_mod_cast r.factorial_pos,
end

So I think ordered_field sounds right.

[Yaël Dillies]

Actually I'm probably missing something. How should I coerce naturals to α where [linear_ordered_field α]? Surely there's a "canonical" way to do that, given that we have a 1 and addition.

[Scott Morrison]

Can't you just write (n : α)? Or just pass the natural number where Lean is expecting an α?

[Yaël Dillies]

Not in the file algebra/ordered_field. Maybe the coercion is set up in a later file?

[Johan Commelin]

In that case the lemma you are proving probably belongs in a later file.

[Johan Commelin]

But I guess the coercion is set up in algebra/group.* which is probably imported by algebra/ordered_field

[Yaël Dillies]

Ahah! I think the cast is in data.nat.cast.

[Yaël Dillies]

But that doesn't sound like a great place to put my inequality. What do you think of me creating a new file for those two lemmas?

[Yaël Dillies]

It looks like there's an instance linear_ordered_field α to ordered_semiring α missing.

import data.nat.choose.basic
import data.nat.cast

variables {α : Type*} [linear_ordered_field α] [nontrivial α]

lemma choose_le_pow (r n : ℕ) : (n.choose r : α) ≤ n^r / r.factorial :=
begin
  rw le_div_iff',
  { norm_cast,
    rw ←nat.desc_fact_eq_factorial_mul_choose,
    rw nat.cast_le, --fails
    exact n.desc_fact_le_pow r },
  exact_mod_cast r.factorial_pos,
end

[Yaël Dillies]

#7759

[Yaël Dillies]

Could anyone review the PR one last time? :grinning_face_with_smiling_eyes: