The set (as a Finset
) of exceptions to the abc conjecture at ε
inside [1, X] ^ 3, in particular
the set of triples (a, b, c)
which are
- pairwise coprime,
- contained in
[1, X] ^ 3
, - satisfy
a + b = c
, - have
radical (a * b * c) < c ^ (1 - ε)
Note this has a slight difference from the usual formulation, which has
radical (a * b * c) ^ (1 + ε) < c
instead.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The number of exceptions to the abc conjecture for a given ε
which are bounded by X
.
Equations
- countTriples ε X = (Finset.abcExceptionsBelow ε X).card
Instances For
The set of exceptions to the abc conjecture for ε
, in particular
the set of triples (a, b, c)
which are
Equations
- One or more equations did not get rendered due to their size.
Instances For
The abc conjecture: the set of exceptional triples is finite.
Equations
- abcConjecture = ∀ ε > 0, (abcExceptions ε).Finite
Instances For
This is $$S^*_{α,β,γ}(X)$$ in the paper and blueprint.
Equations
- refinedCountTriplesStar α β γ X = (dyadicPoints α β γ X).card
Instances For
The supremum that appears in lemma 2.2, taken over a finite subset of α, β, γ > 0 such that α + β + γ ≤ 1 - ε
Equations
Instances For
The finite set of d
-tuples a i
such that a i ~ X i
for all i
.
Equations
- dyadicTuples X = Fintype.piFinset fun (i : Fin d) => Finset.Icc (X i) (2 * X i)
Instances For
The finite set counted by B_d(C, X, Y, X)
. We choose to add C
as an entry in these tuples,
as this allows us to write down a surjective map from a union of these sets back to triples
(a, b, c)
in dyadicTriples α β γ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
y j
is the product of primes dividing n
with multiplicity j
.
Equations
- NiceFactorization.y j = ∏ p ∈ NiceFactorization.ProofData.n.primeFactors with NiceFactorization.ProofData.n.factorization p = j, p
Instances For
K
in the proof of lemma 2.5
Instances For
x
in the proof of lemma 2.5
Equations
- One or more equations did not get rendered due to their size.
Instances For
Proposition 2.5. The bulk of the proof is in the section NiceFactorization
.
Some basic consequences of Proposition 2.5, phrased in a way that make them more useful in the proof of Proposition 2.6.
A surjective map ⋃_{c, X, Y ,Z} B (c, X, Y, Z) → S*_α β γ (X)