LeanPool.ABCExceptions.Section2

noncomputable def Finset.abcExceptionsBelow (ε : ℝ) (X : ℕ) : Finset (ℕ × ℕ × ℕ)

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.

@[simp]

theorem Finset.mem_abcExceptionsBelow (ε : ℝ) (X a b c : ℕ) : (a, b, c) ∈ abcExceptionsBelow ε X ↔ a.Coprime b ∧ a.Coprime c ∧ b.Coprime c ∧ a + b = c ∧ ↑(UniqueFactorizationMonoid.radical (a * b * c)) < ↑c ^ (1 - ε) ∧ (a, b, c) ∈ Set.Icc (1, 1, 1) (X, X, X)

theorem Finset.abcExceptionsBelow_mono_right {ε : ℝ} {X Y : ℕ} (hXY : X ≤ Y) : abcExceptionsBelow ε X ⊆ abcExceptionsBelow ε Y

theorem Finset.abcExceptionsBelow_mono_left {ε₁ ε₂ : ℝ} {X : ℕ} (hε : ε₁ ≤ ε₂) : abcExceptionsBelow ε₂ X ⊆ abcExceptionsBelow ε₁ X

theorem Finset.abcExceptionsBelow_mono {ε₁ ε₂ : ℝ} {X Y : ℕ} (hε : ε₁ ≤ ε₂) (hXY : X ≤ Y) : abcExceptionsBelow ε₂ X ⊆ abcExceptionsBelow ε₁ Y

noncomputable def countTriples (ε : ℝ) (X : ℕ) : ℕ

The number of exceptions to the abc conjecture for a given ε which are bounded by X.

Equations

• countTriples ε X = (Finset.abcExceptionsBelow ε X).card

theorem countTriples_mono {ε₁ ε₂ : ℝ} {X Y : ℕ} (hε : ε₁ ≤ ε₂) (hXY : X ≤ Y) : countTriples ε₂ X ≤ countTriples ε₁ Y

theorem countTriples_mono_left {ε : ℝ} {X Y : ℕ} (hXY : X ≤ Y) : countTriples ε X ≤ countTriples ε Y

theorem countTriples_mono_right {ε₁ ε₂ : ℝ} {X : ℕ} (hε : ε₁ ≤ ε₂) : countTriples ε₂ X ≤ countTriples ε₁ X

def abcExceptions (ε : ℝ) : Set (ℕ × ℕ × ℕ)

The set of exceptions to the abc conjecture for ε, in particular the set of triples (a, b, c) which are

• pairwise coprime,
• positive,
• satisfy a + b = c,
• have radical (a * b * c) ^ (1 + ε) < c

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem mem_abcExceptions (ε : ℝ) (a b c : ℕ) : (a, b, c) ∈ abcExceptions ε ↔ 0 < a ∧ 0 < b ∧ 0 < c ∧ a.Coprime b ∧ a.Coprime c ∧ b.Coprime c ∧ a + b = c ∧ ↑(UniqueFactorizationMonoid.radical (a * b * c)) ^ (1 + ε) < ↑c

theorem abcExceptions_mono {ε₁ ε₂ : ℝ} (hε : ε₂ ≤ ε₁) : abcExceptions ε₁ ⊆ abcExceptions ε₂

theorem abcExceptions_subset_Ici_one (ε : ℝ) : abcExceptions ε ⊆ Set.Ici 1

def abcConjecture : Prop

The abc conjecture: the set of exceptional triples is finite.

Equations

• abcConjecture = ∀ ε > 0, (abcExceptions ε).Finite

theorem abcConjecture_iff_eventually : abcConjecture ↔ ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), (abcExceptions ε).Finite

theorem abcExceptionsBelow_eq_abcExceptions_inter (ε : ℝ) (X : ℕ) (hε : ε < 1) : ↑(Finset.abcExceptionsBelow ε X) = abcExceptions ((1 - ε)⁻¹ - 1) ∩ Set.Icc (1, 1, 1) (X, X, X)

theorem abcExceptionsBelow_eq_abcExceptions_inter' (ε : ℝ) (X : ℕ) (hε : 0 < ε) : ↑(Finset.abcExceptionsBelow (1 - (1 + ε)⁻¹) X) = abcExceptions ε ∩ Set.Icc (1, 1, 1) (X, X, X)

theorem forall_increasing' {α : Type u_1} (f : ℕ → Set α) (hf : Monotone f) (hf' : ∀ (n : ℕ), (f n).Finite) {C : ℕ} (hC : ∀ (n : ℕ), (f n).ncard ≤ C) : (⋃ (n : ℕ), f n).Finite

theorem forall_increasing {α : Type u_1} (f : ℕ → Set α) (hf : Monotone f) {s : Set α} (hf' : ∀ (n : ℕ), (s ∩ f n).Finite) {C : ℕ} (hC : ∀ (n : ℕ), (s ∩ f n).ncard ≤ C) : (s ∩ ⋃ (n : ℕ), f n).Finite

theorem abcConjecture_iff_countTriples : abcConjecture ↔ ∀ ε > 0, ε < 1 → (fun (x : ℕ) => ↑(countTriples ε x)) =O[Filter.atTop] fun (x : ℕ) => 1

theorem abcConjecture_iff_eventually_countTriples : abcConjecture ↔ ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), (fun (x : ℕ) => ↑(countTriples ε x)) =O[Filter.atTop] fun (x : ℕ) => 1

theorem radical_dvd_div_mul_radical_of_dvd (a b : ℕ) (h : a ∣ b) : UniqueFactorizationMonoid.radical b ∣ b / a * UniqueFactorizationMonoid.radical a

def tripleAt (n : ℕ) : ℕ × ℕ × ℕ

A concrete construction of a triple which has rad(abc) < c.

Equations

• tripleAt n = (1, 2 ^ (6 * n) - 1, 2 ^ (6 * n))

theorem tripleAt_mem_abcExceptions (n : ℕ) (hn : 0 < n) : tripleAt n ∈ abcExceptions 0

theorem tripleAt_strictMono : StrictMono tripleAt

theorem abcExceptions_zero_infinite : (abcExceptions 0).Infinite

def similar (x X : ℝ) : Prop

We define reals x and X to be similar if x ∈ [X, 2X].

Equations

• similar x X = (x ∈ Set.Icc X (2 * X))

theorem similar_pow_natLog (x : ℕ) (hx : x ≠ 0) : similar (↑x) (2 ^ Nat.log 2 x)

noncomputable def dyadicPoints (α β γ : ℝ) (X : ℕ) : Finset (ℕ × ℕ × ℕ)

The finite set of exceptions (a, b, c) to the abc conjecture for which X/2 ≤ c ≤ X and rad a ~ X^α, rad b ~ X^β, rad c ~ X^γ. S* counts the size of this set.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem mem_dyadicPoints (α β γ : ℝ) (X a b c : ℕ) : (a, b, c) ∈ dyadicPoints α β γ X ↔ 0 < a ∧ 0 < b ∧ 0 < c ∧ a.Coprime b ∧ a.Coprime c ∧ b.Coprime c ∧ a + b = c ∧ similar (↑(UniqueFactorizationMonoid.radical a)) (↑X ^ α) ∧ similar (↑(UniqueFactorizationMonoid.radical b)) (↑X ^ β) ∧ similar (↑(UniqueFactorizationMonoid.radical c)) (↑X ^ γ) ∧ X ≤ 2 * c ∧ c ≤ X

noncomputable def refinedCountTriplesStar (α β γ : ℝ) (X : ℕ) : ℕ

This is $$S^*_{α,β,γ}(X)$$ in the paper and blueprint.

Equations

• refinedCountTriplesStar α β γ X = (dyadicPoints α β γ X).card

noncomputable def indexSet (ε : ℝ) (X : ℕ) : Finset (ℕ × ℕ × ℕ × ℕ)

The set over which we take the supremum in lemma 2.2.

Equations

• One or more equations did not get rendered due to their size.

theorem Nat.Coprime.isRelPrime (a b : ℕ) (h : a.Coprime b) : IsRelPrime a b

theorem Finset.abcExceptionsBelow_subset_union_dyadicPoints (ε : ℝ) (X : ℕ) : abcExceptionsBelow ε X ⊆ (indexSet ε X).biUnion fun (x : ℕ × ℕ × ℕ × ℕ) => match x with | (i, j, k, n) => dyadicPoints (↑i / ↑n) (↑j / ↑n) (↑k / ↑n) (2 ^ n)

theorem sum_le_card_mul_sup {ι : Type u_1} (f : ι → ℕ) (s : Finset ι) : ∑ i ∈ s, f i ≤ s.card * s.sup f

theorem card_union_dyadicPoints_le_log_pow_mul_sup (ε : ℝ) (X : ℕ) : ((indexSet ε X).biUnion fun (x : ℕ × ℕ × ℕ × ℕ) => match x with | (i, j, k, n) => dyadicPoints (↑i / ↑n) (↑j / ↑n) (↑k / ↑n) (2 ^ n)).card ≤ (Nat.log 2 X + 1) ^ 4 * (indexSet ε X).sup fun (x : ℕ × ℕ × ℕ × ℕ) => match x with | (i, j, k, n) => refinedCountTriplesStar (↑i / ↑n) (↑j / ↑n) (↑k / ↑n) (2 ^ n)

noncomputable def dyadicSupBound (ε : ℝ) (X : ℕ) : ℕ

The supremum that appears in lemma 2.2, taken over a finite subset of α, β, γ > 0 such that α + β + γ ≤ 1 - ε

Equations

• dyadicSupBound ε X = (indexSet ε X).sup fun (x : ℕ × ℕ × ℕ × ℕ) => match x with | (i, j, k, n) => refinedCountTriplesStar (↑i / ↑n) (↑j / ↑n) (↑k / ↑n) (2 ^ n)

theorem countTriples_le_log_pow_mul_sup (ε : ℝ) (X : ℕ) : countTriples ε X ≤ (Nat.log 2 X + 1) ^ 4 * dyadicSupBound ε X

theorem Real.natLog_isBigO_logb (b : ℕ) : (fun (x : ℕ) => ↑(Nat.log b x)) =O[Filter.atTop] fun (x : ℕ) => logb ↑b ↑x

theorem Real.logb_isBigO_log (b : ℝ) : logb b =O[Filter.atTop] log

theorem Real.log_isBigO_logb (b : ℝ) (hb : 1 < b) : log =O[Filter.atTop] logb b

theorem Nat.log_isBigO_log (b : ℕ) : (fun (x : ℕ) => ↑(log b x)) =O[Filter.atTop] fun (x : ℕ) => Real.log ↑x

theorem countTriples_isBigO_dyadicSup (ε : ℝ) : (fun (X : ℕ) => ↑(countTriples ε X)) =O[Filter.atTop] fun (X : ℕ) => Real.log ↑X ^ 4 * ↑(dyadicSupBound ε X)

def dyadicTuples {d : ℕ} (X : Fin d → ℕ) : Finset (Fin d → ℕ)

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)

@[simp]

theorem mem_dyadicTuples {d : ℕ} (X x : Fin d → ℕ) : x ∈ dyadicTuples X ↔ ∀ (i : Fin d), similar ↑(x i) ↑(X i)

noncomputable def BFinset (d : ℕ) (C : Fin 3 → ℕ) (X Y Z : Fin d → ℕ) : Finset ((Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ))

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.

theorem mem_B_finset (d : ℕ) (C : Fin 3 → ℕ) (X Y Z x y z : Fin d → ℕ) (c : Fin 3 → ℕ) : (x, y, z, c) ∈ BFinset d C X Y Z ↔ C = c ∧ (∀ (i : Fin d), similar ↑(x i) ↑(X i)) ∧ (∀ (i : Fin d), similar ↑(y i) ↑(Y i)) ∧ (∀ (i : Fin d), similar ↑(z i) ↑(Z i)) ∧ c 0 * ∏ i : Fin d, x i ^ (↑i + 1) + c 1 * ∏ i : Fin d, y i ^ (↑i + 1) = c 2 * ∏ i : Fin d, z i ^ (↑i + 1) ∧ (c 0 * ∏ i : Fin d, x i).gcd (c 1 * ∏ i : Fin d, y i) = 1 ∧ (c 0 * ∏ i : Fin d, x i).gcd (c 2 * ∏ i : Fin d, z i) = 1 ∧ (c 1 * ∏ i : Fin d, y i).gcd (c 2 * ∏ i : Fin d, z i) = 1

noncomputable def B (d : ℕ) (c : Fin 3 → ℕ) (X Y Z : Fin d → ℕ) : ℕ

Definition 2.4

Equations

• B d c X Y Z = (BFinset d c X Y Z).card

theorem Nat.factorization_le_right (p n : ℕ) (hp : Prime p) : n.factorization p ≤ n

theorem Nat.ceil_lt_floor (a b : ℝ) (ha : 0 ≤ a) (hab : a + 2 ≤ b) : ⌈a⌉₊ < ⌊b⌋₊

class NiceFactorization.ProofData : Type

The data and assumptions of lemma 2.5. We treat d as a free variable constrained by hd here because d appears in a type and this gives the user some leeway to rewrite the value of d.

• ε : ℝ

  The value of epsilon in Lemma 2.5

• hε_pos : 0 < ε
• hε : ε < 1 / 2
• d : ℕ

  d in Lemma 2.5

• hd : d = ⌊5 / 2 * ε⁻¹ ^ 2⌋₊
• n : ℕ

  n in Lemma 2.5

• X : ℕ

  X in Lemma 2.5

• h1n : 1 ≤ n
• hnX : n ≤ X

def NiceFactorization.y [data : ProofData] (j : ℕ) : ℕ

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

theorem Nat.prod_squarefree {ι : Type u_1} (f : ι → ℕ) {s : Finset ι} (hf : ∀ i ∈ s, Squarefree (f i)) (h : (↑s).Pairwise (Function.onFun Coprime f)) : Squarefree (∏ i ∈ s, f i)

theorem Associated.nat_eq {a b : ℕ} (h : Associated a b) : a = b

theorem NiceFactorization.y_squarefree [data : ProofData] {i : ℕ} : Squarefree (y i)

noncomputable def NiceFactorization.K [data : ProofData] : ℕ

K in the proof of lemma 2.5

Equations

• NiceFactorization.K = ⌈NiceFactorization.ProofData.ε⁻¹⌉₊

instance NiceFactorization.hd_ne_zero [data : ProofData] : NeZero ProofData.d

noncomputable def NiceFactorization.x [data : ProofData] (j : Fin ProofData.d) : ℕ

x in the proof of lemma 2.5

Equations

• One or more equations did not get rendered due to their size.

theorem NiceFactorization.x_pos [data : ProofData] (j : Fin ProofData.d) : 0 < x j

noncomputable def NiceFactorization.c [data : ProofData] : ℕ

c in the proof of lemma 2.5

Equations

• NiceFactorization.c = ∏ m ∈ Finset.Ioc NiceFactorization.ProofData.d NiceFactorization.ProofData.n, NiceFactorization.y m ^ (m % NiceFactorization.K)

theorem NiceFactorization.nat_eq_fin_iff {n a : ℕ} {b : Fin n} [NeZero n] (ha : a < n) : Fin.ofNat n a = b ↔ a = ↑b

theorem NiceFactorization.fin_eq_nat_iff {n a : ℕ} {b : Fin n} [NeZero n] (ha : a < n) : b = Fin.ofNat n a ↔ ↑b = a

noncomputable def NiceFactorization.KIndex [data : ProofData] : Fin ProofData.d

The distinguished index K - 1, viewed in Fin d.

Equations

• NiceFactorization.KIndex = Fin.ofNat NiceFactorization.ProofData.d (NiceFactorization.K - 1)

theorem NiceFactorization.x_K_le_X_pow [data : ProofData] : ↑(x KIndex) ≤ ↑ProofData.X ^ ProofData.ε

theorem NiceFactorization.exists_nice_factorization [data : ProofData] : ∃ (x : Fin ProofData.d → ℕ) (c : ℕ), ProofData.n = c * ∏ j : Fin ProofData.d, x j ^ (↑j + 1) ∧ ↑c ≤ ↑ProofData.X ^ ProofData.ε ∧ (∀ (i j : Fin ProofData.d), i ≠ j → (x i).gcd (x j) = 1) ∧ ↑ProofData.X ^ (-ProofData.ε) * ↑(∏ j : Fin ProofData.d, x j) ≤ ↑(UniqueFactorizationMonoid.radical ProofData.n) ∧ ↑(UniqueFactorizationMonoid.radical ProofData.n) ≤ ↑ProofData.X ^ ProofData.ε * ↑(∏ j : Fin ProofData.d, x j)

theorem exists_nice_factorization {ε : ℝ} (hε_pos : 0 < ε) (hε : ε < 1 / 2) {d : ℕ} (hd : d = ⌊5 / 2 * ε⁻¹ ^ 2⌋₊) {n X : ℕ} (h1n : 1 ≤ n) (hnX : n ≤ X) : ∃ (x : Fin d → ℕ) (c : ℕ), n = c * ∏ j : Fin d, x j ^ (↑j + 1) ∧ ↑c ≤ ↑X ^ ε ∧ (∀ (i j : Fin d), i ≠ j → (x i).gcd (x j) = 1) ∧ ↑X ^ (-ε) * ↑(∏ j : Fin d, x j) ≤ ↑(UniqueFactorizationMonoid.radical n) ∧ ↑(UniqueFactorizationMonoid.radical n) ≤ ↑X ^ ε * ↑(∏ j : Fin d, x j) ∧ 0 < c ∧ (∀ (i : Fin d), 0 < x i) ∧ ∀ (i : Fin d), x i ≤ X

Proposition 2.5. The bulk of the proof is in the section NiceFactorization.

theorem exists_nice_factorization' {ε : ℝ} (hε_pos : 0 < ε) (hε : ε < 1 / 2) {d : ℕ} (hd : d = ⌊10 * ε⁻¹ ^ 4⌋₊) {n X : ℕ} (h1n : 1 ≤ n) (hnX : n ≤ X) (α : ℝ) (hsim : similar (↑(UniqueFactorizationMonoid.radical n)) (↑X ^ α)) : ∃ (x : Fin d → ℕ) (c : ℕ), n = c * ∏ j : Fin d, x j ^ (↑j + 1) ∧ ↑c ≤ ↑X ^ ε ^ 2 ∧ c ≤ ⌊↑X ^ (ε / 4)⌋₊ ∧ (∀ (i j : Fin d), i ≠ j → (x i).gcd (x j) = 1) ∧ ↑X ^ (α - ε) ≤ ↑(∏ j : Fin d, x j) ∧ ↑(∏ j : Fin d, x j) ≤ 2 * ↑X ^ (α + ε) ∧ 0 < c ∧ (∀ (i : Fin d), 0 < x i) ∧ ∀ (i : Fin d), x i ≤ X

Some basic consequences of Proposition 2.5, phrased in a way that make them more useful in the proof of Proposition 2.6.

def BToTriple {d : ℕ} : (Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ) → ℕ × ℕ × ℕ

A surjective map ⋃_{c, X, Y ,Z} B (c, X, Y, Z) → S*_α β γ (X)

Equations

• BToTriple (x_1, y, z, c) = (c 0 * ∏ i : Fin d, x_1 i ^ (↑i + 1), c 1 * ∏ i : Fin d, y i ^ (↑i + 1), c 2 * ∏ i : Fin d, z i ^ (↑i + 1))

noncomputable def indexSet' (α β γ : ℝ) (d x : ℕ) (ε : ℝ) : Finset ((Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ))

The finite set over which we will take a supremum in proposition 2.6

Equations

• One or more equations did not get rendered due to their size.

theorem card_indexSet'_le (α β γ : ℝ) (d x : ℕ) (ε : ℝ) : (indexSet' α β γ d x ε).card ≤ (Nat.log 2 x + 1) ^ (3 * d) * ⌊↑x ^ (ε / 4)⌋₊ ^ 3

noncomputable def BUnion (α β γ : ℝ) {d : ℕ} (x : ℕ) (ε : ℝ) : Finset ((Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ))

The union of B-sets used in the proof of proposition 2.6.

Equations

• One or more equations did not get rendered due to their size.

theorem similar_pow_log {x : ℕ} (hx : 0 < x) : similar (↑x) (2 ^ Nat.log 2 x)

theorem coprime_mul_prod_aux {ι : Type u_1} {s : Finset ι} {f g u v : ι → ℕ} {a b : ℕ} (hu : ∀ (i : ι), 0 < u i) (hv : ∀ (i : ι), 0 < v i) (hcop : (a * ∏ i ∈ s, f i ^ u i).Coprime (b * ∏ i ∈ s, g i ^ v i)) : (a * ∏ i ∈ s, f i).Coprime (b * ∏ i ∈ s, g i)

theorem Nat.sum_Ico_choose (n k : ℕ) : ∑ m ∈ Finset.Ico k n, m.choose k = n.choose (k + 1)

theorem Nat.sum_range_add_choose' (n k : ℕ) : ∑ i ∈ Finset.range n, (i + k).choose k = (n + k).choose (k + 1)

theorem sum_range_id_add_one {d : ℕ} : ∑ i ∈ Finset.range d, (i + 1) = (d + 1).choose 2

theorem B_to_triple_surjOn {α β γ : ℝ} (x : ℕ) (ε : ℝ) (hε_pos : 0 < ε) (hε : ε < 1 / 2) {d : ℕ} (hd : d = ⌊10 * ε⁻¹ ^ 4⌋₊) : Set.SurjOn BToTriple ↑(BUnion α β γ x ε) ↑(dyadicPoints α β γ x)

theorem refinedCountTriplesStar_le_card_BUnion (α β γ : ℝ) {d : ℕ} (x : ℕ) (ε : ℝ) (hε_pos : 0 < ε) (hε : ε < 1 / 2) (hd : d = ⌊10 * ε⁻¹ ^ 4⌋₊) : refinedCountTriplesStar α β γ x ≤ (BUnion α β γ x ε).card

theorem log_le_const_mul_pow {ε : ℝ} (hε : 0 < ε) (d : ℕ) (hd : 0 < d) : ∃ c ≥ 0, ∀ (x : ℕ), Real.log ↑x ^ d ≤ c * ↑x ^ ε

theorem tmp {ε : ℝ} (hε : 0 < ε) (d : ℕ) (hd : 0 < d) : ∃ (c : ℝ), ∀ (x : ℕ), 2 ≤ x → (↑(Nat.log 2 x) + 1) ^ (3 * d) ≤ c * ↑x ^ (ε / 4)

noncomputable def const (ε : ℝ) : ℝ

The implicit coefficient in the conclusion of proposition 2.6

Equations

• const ε = if h : 0 < ε then if h' : ε < 1 / 2 then let d := ⌊10 * ε⁻¹ ^ 4⌋₊; have this := ⋯; have this := ⋯; have hd := ⋯; Classical.choose ⋯ else 0 else 0

theorem const_spec {ε : ℝ} (hε_pos : 0 < ε) (hε : ε < 1 / 2) : have d := ⌊10 * ε⁻¹ ^ 4⌋₊; ∀ (x : ℕ), 2 ≤ x → (↑(Nat.log 2 x) + 1) ^ (3 * d) ≤ const ε * ↑x ^ (ε / 4)

theorem const_nonneg {ε : ℝ} : 0 ≤ const ε

theorem card_indexSet'_le_pow (ε α β γ : ℝ) (d x : ℕ) (hd : d = ⌊10 * ε⁻¹ ^ 4⌋₊) (hx : 2 ≤ x) (hε_pos : 0 < ε) (hε : ε < 1 / 2) : ↑(indexSet' α β γ d x ε).card ≤ const ε * ↑x ^ ε

noncomputable def d (ε : ℝ) : ℕ

The value of d chosen in proposition 2.6

Equations

• d ε = ⌊10 * ε⁻¹ ^ 4⌋₊

theorem refinedCountTriplesStar_isBigO_B {α β γ : ℝ} {x : ℕ} (h2X : 2 ≤ x) {ε : ℝ} (hε_pos : 0 < ε) (hε : ε < 1 / 2) : ∃ (s : Finset ((Fin (d ε) → ℕ) × (Fin (d ε) → ℕ) × (Fin (d ε) → ℕ) × (Fin 3 → ℕ))), ↑(refinedCountTriplesStar α β γ x) ≤ const ε * ↑x ^ ε * ↑(s.sup fun (x : (Fin (d ε) → ℕ) × (Fin (d ε) → ℕ) × (Fin (d ε) → ℕ) × (Fin 3 → ℕ)) => match x with | (X, Y, Z, c) => B (d ε) c X Y Z) ∧ ∀ (X Y Z : Fin (d ε) → ℕ) (c : Fin 3 → ℕ), (X, Y, Z, c) ∈ s → ↑x ^ (α - ε) ≤ 2 ^ d ε * ↑(∏ j : Fin (d ε), X j) ∧ ↑(∏ j : Fin (d ε), X j) ≤ 2 * ↑x ^ (α + ε) ∧ ↑x ^ (β - ε) ≤ 2 ^ d ε * ↑(∏ j : Fin (d ε), Y j) ∧ ↑(∏ j : Fin (d ε), Y j) ≤ 2 * ↑x ^ (β + ε) ∧ ↑x ^ (γ - ε) ≤ 2 ^ d ε * ↑(∏ j : Fin (d ε), Z j) ∧ ↑(∏ j : Fin (d ε), Z j) ≤ 2 * ↑x ^ (γ + ε) ∧ ∏ i : Fin (d ε), X i ^ (↑i + 1) ≤ x ∧ ∏ i : Fin (d ε), Y i ^ (↑i + 1) ≤ x ∧ ∏ i : Fin (d ε), Z i ^ (↑i + 1) ≤ x ∧ ↑x ^ (1 - ε ^ 2) ≤ 2 ^ ((d ε + 1).choose 2 + 1) * ↑(∏ i : Fin (d ε), Z i ^ (↑i + 1)) ∧ (c 0).Coprime (c 1) ∧ (c 1).Coprime (c 2) ∧ (c 0).Coprime (c 2) ∧ (∀ (i : Fin 3), 1 ≤ c i) ∧ ∀ (i : Fin 3), ↑(c i) ≤ ↑x ^ ε