Documentation

LeanPool.Redhill.General.Defs

Definitions for the general case #

In this section h is the variable such that tup n F h ∈ factorFreeTuples F (n + 6) for sufficiently large h.

The lower bound s for primeChain in U was originally 200 * Y F ^ 6.

source
def GeneralCase.Y (F : Finset ℕ) :
ℕ

An optimised version of the paper's y.

Equations
Instances For
    source
    def GeneralCase.X (F : Finset ℕ) (h : ℕ) :
    ℕ

    x in the paper, but using the optimised y.

    Equations
    Instances For
      source
      theorem GeneralCase.Y_lower_bound {F : Finset ℕ} :
      33330 ≤ Y F
      source
      theorem GeneralCase.Y_pos {F : Finset ℕ} :
      0 < Y F
      source
      theorem GeneralCase.Y_lt_X {F : Finset ℕ} {h : ℕ} :
      Y F < X F h
      source
      def GeneralCase.U (n : ℕ) (F : Finset ℕ) :
      ℕ

      The sum of tup over all indices save n and n + 1, i.e. the input u to VWPair.

      Equations
      Instances For
        source
        theorem GeneralCase.U_lower_bound {n : ℕ} {F : Finset ℕ} :
        (100 * 33330 - 2) * 33330 ^ 5 ≤ U n F
        source
        theorem GeneralCase.U_pos {n : ℕ} {F : Finset ℕ} :
        0 < U n F
        source
        def GeneralCase.VW (n : ℕ) (F : Finset ℕ) :
        VWPair (U n F) (U n F)

        The VWPair generated from the inputs u = m = U n F.

        Equations
        Instances For
          source
          def GeneralCase.tup (n : ℕ) (F : Finset ℕ) (h : ℕ) (i : Fin (n + 6)) :
          ℤ

          The sequence of (n + 6)-tuples whose tail is in factorFreeTuples and has quality tending to 5 / 4.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem GeneralCase.tup_castAdd {n : ℕ} {F : Finset ℕ} {h : ℕ} {i : Fin n} :
            tup n F h (Fin.castAdd 6 i) = ↑(primeChain (100 * Y F ^ 6) ↑i)
            source
            @[simp]
            theorem GeneralCase.tup_natAdd_zero {n : ℕ} {F : Finset ℕ} {h : ℕ} :
            tup n F h (Fin.natAdd n 0) = ↑(VW n F).v
            source
            @[simp]
            theorem GeneralCase.tup_natAdd_one {n : ℕ} {F : Finset ℕ} {h : ℕ} :
            tup n F h (Fin.natAdd n 1) = -↑(VW n F).w
            source
            @[simp]
            theorem GeneralCase.tup_natAdd_two {n : ℕ} {F : Finset ℕ} {h : ℕ} :
            tup n F h (Fin.natAdd n 2) = (↑(X F h) ^ 2 + 10 * ↑(Y F) ^ 3) ^ 2
            source
            @[simp]
            theorem GeneralCase.tup_natAdd_three {n : ℕ} {F : Finset ℕ} {h : ℕ} :
            tup n F h (Fin.natAdd n 3) = (10 * ↑(Y F) - 1) * ↑(X F h) ^ 4
            source
            @[simp]
            theorem GeneralCase.tup_natAdd_four {n : ℕ} {F : Finset ℕ} {h : ℕ} :
            tup n F h (Fin.natAdd n 4) = (↑(X F h) - ↑(Y F)) ^ 5
            source
            @[simp]
            theorem GeneralCase.tup_natAdd_five {n : ℕ} {F : Finset ℕ} {h : ℕ} :
            tup n F h (Fin.natAdd n 5) = -(↑(X F h) + ↑(Y F)) ^ 5
            source
            theorem GeneralCase.sum_tup {n : ℕ} {F : Finset ℕ} {h : ℕ} :
            ∑ i : Fin (n + 6), tup n F h i = 0
            source
            theorem GeneralCase.dvd_Y_of_mem_F {F : Finset ℕ} {f : ℕ} (mf : f ∈ F.erase 0) :
            f ∣ Y F
            source
            theorem GeneralCase.X_modEq_one_of_mem_F {F : Finset ℕ} {h f : ℕ} (mf : f ∈ F) (lf : 3 ≤ f) :
            X F h ≡ 1 [MOD f]
            source
            theorem GeneralCase.le_Y_of_mem_F {F : Finset ℕ} {f : ℕ} (mf : f ∈ F) :
            f ≤ Y F
            source
            theorem GeneralCase.lt_primeChain_of_mem_F {n : ℕ} {F : Finset ℕ} {f : ℕ} (mf : f ∈ F) :
            f < primeChain (100 * Y F ^ 6) n
            source
            theorem GeneralCase.le_U_of_mem_F {n : ℕ} {F : Finset ℕ} {f : ℕ} (mf : f ∈ F) :
            f ≤ U n F
            source
            theorem GeneralCase.not_dvd_tup {n : ℕ} {F : Finset ℕ} {h f : ℕ} (mf : f ∈ F) (lf : 3 ≤ f) (i : Fin (n + 6)) :
            ¬↑f ∣ tup n F h i