Documentation

ABCExceptions.Section2

noncomputable def Finset.abcExceptionsBelow (ε : ) (X : ) :

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
    @[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_left {ε₁ ε₂ : } {X : } ( : ε₁ ε₂) :
    theorem Finset.abcExceptionsBelow_mono {ε₁ ε₂ : } {X Y : } ( : ε₁ ε₂) (hXY : X Y) :
    noncomputable def countTriples (ε : ) (X : ) :

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

    Equations
    Instances For
      theorem countTriples_mono {ε₁ ε₂ : } {X Y : } ( : ε₁ ε₂) (hXY : X Y) :
      countTriples ε₂ X countTriples ε₁ Y
      theorem countTriples_mono_left {ε : } {X Y : } (hXY : X Y) :
      theorem countTriples_mono_right {ε₁ ε₂ : } {X : } ( : ε₁ ε₂) :
      countTriples ε₂ X countTriples ε₁ X

      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.
      Instances For
        @[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 {ε₁ ε₂ : } ( : ε₂ ε₁) :

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

        Equations
        Instances For
          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
          def tripleAt (n : ) :

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

          Equations
          Instances For
            def similar (x X : ) :

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

            Equations
            Instances For
              theorem similar_pow_natLog (x : ) (hx : x 0) :
              similar (↑x) (2 ^ Nat.log 2 x)
              noncomputable def dyadicPoints (α β γ : ) (X : ) :

              The finite set of exceptions (a, b, c) to the abc conjecture for which X/2 ≤ cX 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.
              Instances For
                @[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
                Instances For
                  theorem Nat.Coprime.isRelPrime (a b : ) (h : a.Coprime 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 ι) :
                  is, 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
                  Instances For
                    theorem Real.natLog_isBigO_logb (b : ) :
                    (fun (x : ) => (Nat.log b x)) =O[Filter.atTop] fun (x : ) => logb b x
                    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
                    Instances For
                      @[simp]
                      theorem mem_dyadicTuples {d : } (X x : Fin d) :
                      x dyadicTuples X ∀ (i : Fin d), similar (x i) (X i)
                      noncomputable def B_finset (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.
                      Instances For
                        theorem mem_B_finset (d : ) (C : Fin 3) (X Y Z x y z : Fin d) (c : Fin 3) :
                        (x, y, z, c) B_finset 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
                        Instances For
                          theorem Nat.ceil_lt_floor (a b : ) (ha : 0 a) (hab : a + 2 b) :

                          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.

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

                            y j is the product of primes dividing n with multiplicity j.

                            Equations
                            Instances For
                              theorem Nat.prod_squarefree {ι : Type u_1} (f : ι) {s : Finset ι} (hf : is, Squarefree (f i)) (h : (↑s).Pairwise (Function.onFun Coprime f)) :
                              Squarefree (∏ is, f i)
                              theorem Associated.nat_eq {a b : } (h : Associated a b) :
                              a = b
                              noncomputable def NiceFactorization.K [data : ProofData] :

                              K in the proof of lemma 2.5

                              Equations
                              Instances For
                                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.
                                Instances For
                                  theorem NiceFactorization.nat_eq_fin_iff {n a : } {b : Fin n} [NeZero n] (ha : a < n) :
                                  a = b a = b
                                  theorem NiceFactorization.fin_eq_nat_iff {n a : } {b : Fin n} [NeZero n] (ha : a < n) :
                                  b = a b = a
                                  theorem exists_nice_factorization {ε : } (hε_pos : 0 < ε) ( : ε < 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 < ε) ( : ε < 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 B_to_triple {d : } :
                                  (Fin d) × (Fin d) × (Fin d) × (Fin 3) × ×

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

                                  Equations
                                  Instances For
                                    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.
                                    Instances For
                                      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.
                                      Instances For
                                        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 * is, f i ^ u i).Coprime (b * is, g i ^ v i)) :
                                        (a * is, f i).Coprime (b * is, g i)
                                        theorem Nat.sum_Ico_choose (n k : ) :
                                        mFinset.Ico k n, m.choose k = n.choose (k + 1)
                                        theorem Nat.sum_range_add_choose' (n k : ) :
                                        iFinset.range n, (i + k).choose k = (n + k).choose (k + 1)
                                        theorem sum_range_id_add_one {d : } :
                                        iFinset.range d, (i + 1) = (d + 1).choose 2
                                        theorem B_to_triple_surjOn {α β γ : } (x : ) (ε : ) (hε_pos : 0 < ε) ( : ε < 1 / 2) {d : } (hd : d = 10 * ε⁻¹ ^ 4⌋₊) :
                                        Set.SurjOn B_to_triple (BUnion α β γ x ε) (dyadicPoints α β γ x)
                                        theorem refinedCountTriplesStar_le_card_BUnion (α β γ : ) {d : } (x : ) (ε : ) (hε_pos : 0 < ε) ( : ε < 1 / 2) (hd : d = 10 * ε⁻¹ ^ 4⌋₊) :
                                        refinedCountTriplesStar α β γ x (BUnion α β γ x ε).card
                                        theorem log_le_const_mul_pow {ε : } ( : 0 < ε) (d : ) (hd : 0 < d) :
                                        c0, ∀ (x : ), Real.log x ^ d c * x ^ ε
                                        theorem tmp {ε : } ( : 0 < ε) (d : ) (hd : 0 < d) :
                                        ∃ (c : ), ∀ (x : ), 2 x → ((Nat.log 2 x) + 1) ^ (3 * d) c * x ^ (ε / 4)
                                        noncomputable def const (ε : ) :

                                        The implicit constant in the conclusion of proposition 2.6

                                        Equations
                                        Instances For
                                          theorem const_spec {ε : } (hε_pos : 0 < ε) ( : ε < 1 / 2) :
                                          let 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 < ε) ( : ε < 1 / 2) :
                                          (indexSet' α β γ d x ε).card const ε * x ^ ε
                                          noncomputable def d (ε : ) :

                                          The value of d chosen in proposition 2.6

                                          Equations
                                          Instances For
                                            theorem refinedCountTriplesStar_isBigO_B {α β γ : } {x : } (h2X : 2 x) {ε : } (hε_pos : 0 < ε) ( : ε < 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) sx ^ (α - ε) 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 ^ ε