factorization-def to initial-factorization-medium-pri…

Definitionfactorization-def#

We work with (approximate) factorizations \(a_1 \dots a_t\) of a factorial \(n!\).

Lean

Formalized as Erdos392.Factorization.

Sources
LeanErdos392.Factorization
Used by 22
Used bybalance-def · balance-zero · card-bound · initial-factorization-card · initial-factorization-def · initial-factorization-large-prime-ge · initial-factorization-medium-prime-ge · initial-factorization-medium-prime-le · initial-factorization-waste · score-def · score-eq · score-lower-1 · score-lower-2 · score-lower-3 · score-lowest · waste-def · waste-eq · erdos-sol-1 · erdos-sol-2 · initial-factorization-small-prime-ge · initial-factorization-small-prime-le · initial-factorization-tiny-prime-ge

Definitionwaste-def#

The waste of a factorizations \(a_1 \dots a_t\) is defined as \(\sum_i \log (n / a_i)\).

Lean

Formalized as Erdos392.Factorization.waste.

Sources
LeanErdos392.Factorization.waste
Uses 1 · Used by 9
Statement usesfactorization-def
Used bycard-bound · initial-factorization-waste · score-def · score-eq · score-lower-1 · score-lower-2 · score-lower-3 · waste-eq · initial-score-bound

Definitionbalance-def#

The balance of a factorization \(a_1 \dots a_t\) at a prime \(p\) is defined as the number of times \(p\) divides \(a_1 \dots a_t\), minus the number of times \(p\) divides \(n!\).

Lean

Formalized as Erdos392.Factorization.balance, Erdos392.Factorization.total_imbalance.

Sources
LeanErdos392.Factorization.balance · Erdos392.Factorization.total_imbalance
Uses 1 · Used by 19
Statement usesfactorization-def
Used bybalance-zero · card-bound · initial-factorization-large-prime-ge · initial-factorization-large-prime-le · initial-factorization-medium-prime-ge · initial-factorization-medium-prime-le · score-def · score-eq · score-lower-1 · score-lower-2 · score-lower-3 · score-lowest · waste-eq · erdos-sol-1 · erdos-sol-2 · initial-factorization-small-prime-ge · initial-factorization-small-prime-le · initial-factorization-tiny-prime-ge · initial-score-bound

Lemmabalance-zero#

If a factorization has zero total imbalance, then it exactly factors \(n!\).

Lean

Formalized as Erdos392.Factorization.zero_total_imbalance.

Sources
LeanErdos392.Factorization.zero_total_imbalance
Uses 2 · Used by 2
Statement usesfactorization-def · balance-def
Used bywaste-eq · erdos-sol-2

Lemmawaste-eq#

The waste of a factorization is equal to \(t \log n - \log n!\), where \(t\) is the number of elements.

Lean

Formalized as Erdos392.Factorization.waste_eq.

Sources
LeanErdos392.Factorization.waste_eq
Uses 4 · Used by 1
Statement useswaste-def · factorization-def · balance-def
Proof usesbalance-zero
Used bycard-bound

Definitionscore-def#

The score of a factorization (relative to a cutoff parameter \(L\)) is equal to its waste, plus \(\log p\) for every surplus prime \(p\), \(\log (n/p)\) for every deficit prime above \(L\), \(\log L\) for every deficit prime below \(L\) and an additional \(\log n\) if one is not in total balance.

Lean

Formalized as Erdos392.Factorization.score.

Sources
LeanErdos392.Factorization.score
Uses 3 · Used by 9
Statement useswaste-def · factorization-def · balance-def
Used bycard-bound · score-eq · score-lower-1 · score-lower-2 · score-lower-3 · score-lowest · erdos-sol-1 · initial-score · initial-score-bound

Lemmascore-eq#

If one is in total balance, then the score is equal to the waste.

Lean

Formalized as Erdos392.Factorization.score_eq.

Sources
LeanErdos392.Factorization.score_eq
Uses 4 · Used by 2
Statement useswaste-def · score-def · factorization-def · balance-def
Used bycard-bound · score-lower-3

Lemmascore-lower-1#

If there is a prime \(p\) in surplus, one can remove it without increasing the score.

Proof

Locate a factor \(a_i\) that contains the surplus prime \(p\), then replace \(a_i\) with \(a_i/p\).

Lean

Formalized as Erdos392.Factorization.lower_score_1.

Sources
LeanErdos392.Factorization.lower_score_1
Uses 4 · Used by 2
Statement usesscore-def · factorization-def · balance-def
Proof useswaste-def
Used byscore-lower-3 · score-lowest

Lemmascore-lower-2#

If there is a prime \(p\) in deficit larger than \(L\), one can remove it without increasing the score.

Proof

Add an additional factor of \(p\) to the factorization.

Lean

Formalized as Erdos392.Factorization.lower_score_2.

Sources
LeanErdos392.Factorization.lower_score_2
Uses 4 · Used by 2
Statement usesscore-def · factorization-def · balance-def
Proof useswaste-def
Used byscore-lower-3 · score-lowest

Lemmascore-lower-3#

If there is a prime \(p\) in deficit less than \(L\), one can remove it without increasing the score.

Proof

Without loss of generality we may assume that one is not in the previous two situations, i.e., wlog there are no surplus primes and all primes in deficit are at most \(L\). If all deficit primes multiply to \(n\) or less, add that product to the factorization (this increases the waste by at most \(\log n\), but we save a \(\log n\) from now being in balance). Otherwise, greedily multiply all primes together while staying below \(n\) until one cannot do so any further; add this product to the factorization, increasing the waste by at most \(\log L\).

Lean

Formalized as Erdos392.Factorization.lower_score_3.

Sources
LeanErdos392.Factorization.lower_score_3
Uses 7 · Used by 1
Statement usesscore-def · factorization-def · balance-def
Proof useswaste-def · score-eq · score-lower-2 · score-lower-1
Used byscore-lowest

Lemmascore-lowest#

One can bring any factorization into balance without increasing the score.

Proof

Apply strong induction on the total imbalance of the factorization and use the previous three sublemmas.

Lean

Formalized as Erdos392.Factorization.lowest_score.

Sources
LeanErdos392.Factorization.lowest_score
Uses 6 · Used by 1
Statement usesscore-def · factorization-def · balance-def
Proof usesscore-lower-2 · score-lower-3 · score-lower-1
Used bycard-bound

Propositioncard-bound#

Starting from any factorization \(f\), one can find a factorization \(f'\) in balance whose cardinality is at most \(\log n!\) plus the score of \(f\), divided by \(\log n\).

Proof

Combine Lemma score-lowest, Lemma score-eq, and Lemma waste-eq.

Lean

Formalized as Erdos392.Factorization.card_bound.

Sources
LeanErdos392.Factorization.card_bound
Uses 7 · Used by 1
Statement usesscore-def · factorization-def · balance-def
Proof useswaste-eq · waste-def · score-eq · score-lowest
Used byerdos-sol-1

Definitionparams-set#

Now let \(M,L\) be additional parameters with \(n > L^2\); we also need the minor variant \(\lfloor n/L \rfloor > \sqrt{n}\).

Lean

Formalized as Erdos392.Params.

Sources
LeanErdos392.Params
Used by 18
Used byinitial-factorization-card · initial-factorization-def · initial-factorization-large-prime-ge · initial-factorization-large-prime-le · initial-factorization-medium-prime-ge · initial-factorization-medium-prime-le · initial-factorization-waste · bound-score-1 · bound-score-2 · bound-score-3 · bound-score-4 · bound-score-5 · erdos-sol-1 · initial-factorization-small-prime-ge · initial-factorization-small-prime-le · initial-factorization-tiny-prime-ge · initial-score · initial-score-bound

Definitioninitial-factorization-def#

We perform an initial factorization by taking the natural numbers between \(n-n/M\) (inclusive) and \(n\) (exclusive) repeated \(M\) times, deleting those elements that are not \(n/L\)-smooth (i.e., have a prime factor greater than or equal to \(n/L\)).

Lean

Formalized as Erdos392.Params.initial.

Sources
LeanErdos392.Params.initial
Uses 2 · Used by 12
Statement usesparams-set · factorization-def
Used byinitial-factorization-card · initial-factorization-large-prime-ge · initial-factorization-large-prime-le · initial-factorization-medium-prime-ge · initial-factorization-medium-prime-le · initial-factorization-waste · erdos-sol-1 · initial-factorization-small-prime-ge · initial-factorization-small-prime-le · initial-factorization-tiny-prime-ge · initial-score · initial-score-bound

Lemmainitial-factorization-card#

The number of elements in this initial factorization is at most \(n\).

Lean

Formalized as Erdos392.Params.initial.card.

Sources
LeanErdos392.Params.initial.card
Uses 3 · Used by 1
Statement usesparams-set · initial-factorization-def · factorization-def
Used byinitial-factorization-waste

Lemmainitial-factorization-waste#

The total waste in this initial factorization is at most \(n \log \frac{1}{1-1/M}\).

Lean

Formalized as Erdos392.Params.initial.waste.

Sources
LeanErdos392.Params.initial.waste
Uses 5 · Used by 1
Statement useswaste-def · params-set · initial-factorization-def
Proof usesinitial-factorization-card · factorization-def
Used byinitial-score-bound

Lemmainitial-factorization-large-prime-le#

A large prime \(p \geq n/L\) cannot be in surplus.

Proof

No such prime can be present in the factorization.

Lean

Formalized as Erdos392.Params.initial.balance_large_prime_le.

Sources
LeanErdos392.Params.initial.balance_large_prime_le
Uses 3 · Used by 1
Statement usesparams-set · initial-factorization-def · balance-def
Used byinitial-score-bound

Lemmainitial-factorization-large-prime-ge#

A large prime \(p \geq n/L\) can be in deficit by at most \(n/p\).

Proof

This is the number of times \(p\) can divide \(n!\).

Lean

Formalized as Erdos392.Params.initial.balance_large_prime_ge.

Sources
LeanErdos392.Params.initial.balance_large_prime_ge
Uses 4 · Used by 1
Statement usesparams-set · initial-factorization-def · balance-def
Proof usesfactorization-def
Used byinitial-score-bound

Lemmainitial-factorization-medium-prime-le#

A medium prime \(\sqrt{n} < p ≤ n/L\) can be in surplus by at most \(M\).

Proof

Routine computation using Legendre's formula.

Lean

Formalized as Erdos392.Params.initial.balance_medium_prime_le.

Sources
LeanErdos392.Params.initial.balance_medium_prime_le
Uses 4 · Used by 1
Statement usesparams-set · initial-factorization-def · balance-def
Proof usesfactorization-def
Used byinitial-score-bound

Lemmainitial-factorization-medium-prime-ge#

A medium prime \(\sqrt{n} < p ≤ n/L\) can be in deficit by at most \(M\).

Proof

The number of times \(p\) divides \(a_1 \dots a_t\) is at least \(M \lfloor n/Mp \rfloor ≥ n/p - M\) (note that the removal of the non-smooth numbers does not remove any multiples of \(p\)). Meanwhile, the number of times \(p\) divides \(n!\) is at most \(n/p\).

Lean

Formalized as Erdos392.Params.initial.balance_medium_prime_ge.

Sources
LeanErdos392.Params.initial.balance_medium_prime_ge
Uses 4 · Used by 1
Statement usesparams-set · initial-factorization-def · balance-def
Proof usesfactorization-def
Used byinitial-score-bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.