FormalConjectures/ErdosProblems/392.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 project documentation, Formal Conjectures paper, arXiv v1

3 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 392

Reference: erdosproblems.com/392

Imports (1)
Imported by 1 file
  1. theorem Erdos392.erdos_392 Let $A(n)$ denote the least value of $t$ such that $$ n! = a_1 \cdots a_t $$ with $a_1 \leq \cdots \leq a_t\leq n^2$ sorry line 45 source

    Source documentation

    Let $A(n)$ denote the least value of $t$ such that $$ n! = a_1 \cdots a_t $$ with $a_1 \leq \cdots \leq a_t\leq n^2$. Then $$ A(n) = \frac{n}{2} - \frac{n}{2\log n} + o\left(\frac{n}{\log n}\right). $$

    depends on sorry what this means

    Statement uses: Nat, GT.gt, OfNat.ofNat, IsLeast, Set.ofPred, Exists, Fin, HAdd.hAdd, And, Eq, Nat.factorial, Finset.prod, Finset.univ, Monotone, LE.le, Fin.last, HPow.hPow, Asymptotics.IsLittleO, Real, Filter.atTop and 4 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_392 (A : ℕ → ℕ) (h : ∀ n > 0,
    IsLeast { t + 1 | (t) (_ : ∃ a : Fin (t + 1) → ℕ, (n)! = ∏ i, a i ∧
      Monotone a ∧ a (Fin.last t) ≤ n ^ 2) } (A n)) :
    ((fun (n : ℕ) => (A n - n / 2 + n / (2 * Real.log n) : ℝ)) =o[atTop] fun n => n / Real.log n)
  := by
…
  2. theorem Erdos392.erdos_392.variants.lower If we change the condition to $a_t \leq n$ it can be shown that $$ A(n) = n - \frac{n}{\log n} + o\left(\frac{n}{\log n}\right) $$ sorry line 59 source

    Source documentation

    If we change the condition to $a_t \leq n$ it can be shown that $$ A(n) = n - \frac{n}{\log n} + o\left(\frac{n}{\log n}\right) $$

    depends on sorry what this means

    Statement uses: Nat, GT.gt, OfNat.ofNat, IsLeast, Set.ofPred, Exists, Fin, HAdd.hAdd, And, Eq, Nat.factorial, Finset.prod, Finset.univ, Monotone, LE.le, Fin.last, Asymptotics.IsLittleO, Real, Filter.atTop, HSub.hSub and 2 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_392.variants.lower (A : ℕ → ℕ)
    (hA : ∀ n > 0, IsLeast
      { t + 1 | (t) (_ : ∃ a : Fin (t + 1) → ℕ, (n)! = ∏ i, a i ∧
        Monotone a ∧ a (Fin.last t) ≤ n) } (A n)) :
    (fun (n : ℕ) => (A n - n + n / Real.log n : ℝ)) =o[atTop] fun n => n / Real.log n := by
…
  3. theorem Erdos392.erdos_392.variants.implication Documented declaration: implication sorry line 72 source

    Source documentation

    Cambie has observed that a positive answer follows from the result above with $a_t \leq n$, simply by pairing variables together, e.g. taking $a'_i = a_{2i-1}a_{2i}$ (and the lower bound follows from Stirling's approximation).

    depends on sorry what this means

    Statement uses: Nat, GT.gt, OfNat.ofNat, IsLeast, Set.ofPred, Exists, Fin, HAdd.hAdd, And, Eq, Nat.factorial, Finset.prod, Finset.univ, Monotone, LE.le, Fin.last, Asymptotics.IsLittleO, Real, Filter.atTop, HSub.hSub and 4 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_392.variants.implication (h : type_of% erdos_392.variants.lower) :
    type_of% erdos_392 := by
…

    Mentions: Erdos392.erdos_392.variants.lower, Erdos392.erdos_392