Compfiles/CIIM2022P6.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

5 declarations, 0 contain sorry, 0 declared as axioms

Iberoamerican Interuniversity Mathematics Competition 2022, Problem 6

Given a positive integer m, let d(m) be the number of postive divisors of m. Show that for every positive integer n, one has d((n + 1)!) ≤ 2d(n!).

Imports (2)
Imported by 1 file
  1. def CIIM2022P6.d line 27 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: Finset.card, Nat.divisors

  2. lemma CIIM2022P6.mul_le_self_pow If p ≥ 2 and 1 ≤ v then v * p ≤ p ^ v line 33 source

    Source documentation

    If p ≥ 2 and 1 ≤ v then v * p ≤ p ^ v.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow

    Proof uses: HSub.hSub, LT.lt, Nat.lt_two_pow_self, Nat.pow_le_pow_left, LE.le.trans, Trans.trans, Eq, Nat.mul_le_mul, le_rfl, Eq.mpr, HAdd.hAdd, id, congrArg, Eq.symm, pow_succ, HPow, Eq.rec, Eq.refl

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

    lemma mul_le_self_pow {p v : ℕ} (hp : 2 ≤ p) (hv : 1 ≤ v) : v * p ≤ p ^ v := by
…
  3. lemma CIIM2022P6.sum_div_pow_le_one Key combinatorial estimate line 46 source

    Source documentation

    Key combinatorial estimate. Let P be a finset of primes with multiplicities v p ≥ 1, and set N = ∏ p ∈ P, p ^ v p. Then the sum of (∏ p ∈ S, p ^ v p) / N ^ |S| over nonempty S ⊆ P is at most 1. (Proof: induction on P, peeling off one prime.) This is the exact estimate behind d((n+1)!) ≤ 2 d(n!).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Finset, Nat, Membership.mem, Nat.Prime, LE.le, OfNat.ofNat, Rat, Finset.sum, Finset.erase, Finset.powerset, EmptyCollection.emptyCollection, HDiv.hDiv, Finset.prod, HPow.hPow, Finset.card

    Proof uses: Finset.strongInductionOn, LT.lt, Eq, Finset.Nonempty, Or, Finset.eq_empty_or_nonempty, of_eq_true, Eq.trans, True, congrFun', congrArg, congr, Finset.erase_singleton, funext, Nat.cast_prod, Finset.prod_congr, Eq.refl, Nat.cast_pow, Nat.cast_one, one_pow and 212 more

    209 instances, coercions and auxiliary constants left out.

    Tactic trace: 179 steps

    Open to load the checked before-and-after goal states.

    lemma sum_div_pow_le_one (P : Finset ℕ) (v : ℕ → ℕ) :
    (∀ p ∈ P, p.Prime) → (∀ p ∈ P, 1 ≤ v p) →
    ∑ S ∈ P.powerset.erase ∅, ((∏ p ∈ S, p ^ v p : ℕ) : ℚ) / (∏ p ∈ P, p ^ v p : ℕ) ^ S.card ≤ 1 := by
…

    Mentions: P, S

  4. lemma CIIM2022P6.prod_factorization_le The multiplicative bound ∏_{p | n+1} (v_p(n!) + v_p(n+1) + 1) ≤ 2 ∏_{p | n+1} (v_p(n!) + 1) line 223 source

    Source documentation

    The multiplicative bound ∏_{p | n+1} (v_p(n!) + v_p(n+1) + 1) ≤ 2 ∏_{p | n+1} (v_p(n!) + 1). Together with the factorization of (n+1)! this is the heart of the problem.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Finset.prod, Nat.primeFactors, HAdd.hAdd, Finsupp, Nat.factorization, Nat.factorial, HMul.hMul

    Proof uses: Finset, Eq.mpr, id, Eq, congrArg, rfl, Ne, Membership.mem, Nat.Prime, And.left, And, Dvd.dvd, Iff.mp, Nat.mem_primeFactors, Nat.Prime.factorization_pos_of_dvd, And.right, HPow.hPow, Eq.symm, Nat.prod_primeFactors_pow_factorization, Or and 147 more

    203 instances, coercions and auxiliary constants left out.

    Tactic trace: 91 steps

    Open to load the checked before-and-after goal states.

    lemma prod_factorization_le (n : ℕ) (hn : 0 < n) :
    ∏ p ∈ (n + 1).primeFactors, ((Nat.factorial n).factorization p + (n + 1).factorization p + 1)
      ≤ 2 * ∏ p ∈ (n + 1).primeFactors, ((Nat.factorial n).factorization p + 1) := by
…
  5. problem CIIM2022P6.ciim2022_p6 line 347 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, CIIM2022P6.d, Nat.factorial, HAdd.hAdd, HMul.hMul

    Proof uses: Ne, Nat.factorial_ne_zero, Eq, Finsupp, Nat.factorization, Eq.mpr, id, congrArg, Nat.factorial_succ, Nat.factorization_mul, Finsupp.add_apply, Nat.add_comm, Eq.refl, Finset, Nat.primeFactors, Union.union, Finset.ext, Iff, Membership.mem, And and 74 more

    67 instances, coercions and auxiliary constants left out.

    Tactic trace: 73 steps

    Open to load the checked before-and-after goal states.