initial-factorization-small-prim… to erdos-sol-2
Lemmainitial-factorization-small-prime-le#
A small prime \(p \leq \sqrt{n}\) can be in surplus by at most \(M\log n\).
Proof
Routine computation using Legendre's formula, noting that at most \(\log n / \log 2\) powers of \(p\) divide any given number up to \(n\).
Lean
Formalized as Erdos392.Params.initial.balance_small_prime_le.
Sources
Uses 4 · Used by 1
Lemmainitial-factorization-small-prime-ge#
A small prime \(L < p \leq \sqrt{n}\) can be in deficit by at most \(M\log n\).
Proof
Routine computation using Legendre's formula, noting that at most \(\log n / \log 2\) powers of \(p\) divide any given number up to \(n\).
Lean
Formalized as Erdos392.Params.initial.balance_small_prime_ge.
Sources
Uses 4 · Used by 1
Lemmainitial-factorization-tiny-prime-ge#
A tiny prime \(p \leq L\) can be in deficit by at most \(M\log n + ML\pi(n)\).
Proof
In addition to the Legendre calculations, one potentially removes factors of the form \(plq\) with \(l \leq L\) and \(q \leq n\) a prime up to \(M\) times each, with at most \(L\) copies of \(p\) removed at each factor.
Lean
Formalized as Erdos392.Params.initial.balance_tiny_prime_ge.
Sources
Uses 4 · Used by 1
Propositioninitial-score-bound#
The initial score is bounded by
Proof
Combine Lemma initial-factorization-waste, Sublemma initial-factorization-large-prime-le, Sublemma initial-factorization-large-prime-ge, Sublemma initial-factorization-medium-prime-le, Sublemma initial-factorization-medium-prime-ge, Sublemma initial-factorization-small-prime-le, Sublemma initial-factorization-small-prime-ge, and Sublemma initial-factorization-tiny-prime-ge, and combine \(\log p\) and \(\log (n/p)\) to \(\log n\).
Lean
Formalized as Erdos392.Params.initial.score_bound.
Sources
Uses 13 · Used by 1
Lemmabound-score-1#
If \(M\) is sufficiently large depending on \(\varepsilon\), then \(n \log(1-1/M)^{-1} \leq \varepsilon n\).
Proof
Use the fact that \(\log(1-1/M)^{-1}\) goes to zero as \(M \to \infty\).
Lean
Formalized as Erdos392.Params.initial.bound_score_1.
Sources
Uses 1 · Used by 1
Lemmabound-score-2#
If \(L\) is sufficiently large depending on \(M, \varepsilon\), and \(n\) sufficiently large depending on \(L\), then \(\sum_{p \leq n/L} M \log n \leq \varepsilon n\).
Proof
Use the prime number theorem (or the Chebyshev bound).
Lean
Formalized as Erdos392.Params.initial.bound_score_2.
Sources
Uses 2 · Used by 1
Lemmabound-score-3#
If \(n\) sufficiently large depending on \(M, \varepsilon\), then \(\sum_{p \leq \sqrt{n}} M \log^2 n / \log 2 \leq \varepsilon n\).
Proof
Crude estimation.
Lean
Formalized as Erdos392.Params.initial.bound_score_3.
Sources
Uses 2 · Used by 1
LemmaprimeCounting-is-o-id#
Proof
Given \(\varepsilon > 0\), choose \(a \neq 0\) with \(\varphi(a)/a < \varepsilon/2\) (using \(\prod_{p \leq n}(1 - 1/p) \to 0\)). For \(n \geq a + 2\),
Since \(\varphi(a)/a < \varepsilon/2\), for \(n\) large enough the constant terms are absorbed, giving \(\pi(n) < \varepsilon n\).
Lean
Formalized as Erdos392.primeCounting_is_o_id.
Sources
Used by 1
Lemmabound-score-4#
If \(n\) sufficiently large depending on \(L, \varepsilon\), then \(\sum_{n/L < p \leq n} \frac{n}{p} \log \frac{n}{p} \leq \varepsilon n\).
Proof
Bound \(\frac{n}{p}\) by \(L\) and use the prime number theorem (or the Chebyshev bound).
Lean
Formalized as Erdos392.Params.initial.bound_score_4.
Sources
Uses 2 · Used by 1
LemmaprimeCounting-le-bound#
For all \(n \geq 2\), one has
Proof
By Chebyshev's bound, \(\prod_{p \leq n} p \leq 4^n\), so \(\sum_{p \leq n} \log p \leq n \log 4\). The number of primes \(p \leq \sqrt{n}\) is trivially at most \(\sqrt{n}\). For primes \(p > \sqrt{n}\), we have \(\log p > \frac{1}{2} \log n\), hence
giving \(\pi(n) - \pi(\sqrt{n}) < \frac{2n \log 4}{\log n}\). Adding \(\pi(\sqrt{n}) \leq \sqrt{n}\) yields the result.
Lean
Formalized as Erdos392.primeCounting_le_bound.
Sources
Used by 1
Lemmabound-score-5#
If \(n\) sufficiently large depending on \(M, L, \varepsilon\), then \(\sum_{p \leq L} (M \log n + M L \pi(n)) \log L \leq \varepsilon n\).
Proof
Use the prime number theorem (or the Chebyshev bound).
Lean
Formalized as Erdos392.Params.initial.bound_score_5.
Sources
Uses 2 · Used by 1
Propositioninitial-score#
The score of the initial factorization can be taken to be \(o(n)\).
Proof
Pick \(M\) large depending on \(\varepsilon\), then \(L\) sufficiently large depending on \(M, \varepsilon\), then \(n\) sufficiently large depending on \(M,L,\varepsilon\), so that the bounds in Sublemma bound-score-1, Sublemma bound-score-2, Sublemma bound-score-3, Sublemma bound-score-4, and Sublemma bound-score-5 each contribute at most \((\varepsilon/5) n\). Then use Proposition initial-score-bound.
Lean
Formalized as Erdos392.Params.initial.score.
Sources
Uses 9 · Used by 1
Theoremerdos-sol-1#
One can find a balanced factorization of \(n!\) with cardinality at most \(n - n / \log n + o(n / \log n)\).-
Proof
Combine Proposition initial-score with Proposition card-bound and the Stirling approximation.
Lean
Formalized as Erdos392.Solution_1.
Sources
Uses 7 · Used by 1
Theoremerdos-sol-2#
One can factorize \(n!\) into at most \(n/2 - n / 2\log n + o(n / \log n)\) numbers of size at most \(n^2\).-
Proof
Group the factorization arising in Theorem erdos-sol-1 into pairs, using Lemma balance-zero.
Lean
Formalized as Erdos392.Solution_2.
Sources
Uses 4
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.