Documentation

ABCExceptions.Section4

Section 4 #

In this file we formalise section 4 of the paper. Currently, we formalise section 4.3 onwards, taking as assumptions the bounds in the earlier parts of the paper.

structure baseAssumptions (d : ) (a : ) :

A structure containing the basic assumptions for each vector.

Instances For
    theorem baseAssumptions.sum_restrict_bound {d : } {a : } (ha : baseAssumptions d a) :
    iFinset.Icc 1 d, i * a i 1
    def Bound4Point3 (d : ) (ε : ) (a b : ) :

    A statement of equation 4.3 from the paper, formulated for a, b. We explicitly take a, b as inputs to simplify symmetry arguments in the conclusion.

    Equations
      Instances For
        theorem Bound4Point3.symm {d : } {ε : } {a b : } (h43ab : Bound4Point3 d ε a b) :
        Bound4Point3 d ε b a

        The bound 4.3 is symmetric in a, b

        def Bound4Point4 (d : ) (δ ε : ) (a b c : ) :

        A statement of equation 4.4 from the paper, formulated for a, b, c. We explicitly take a, b, c as inputs to simplify symmetry arguments in the conclusion.

        Equations
          Instances For
            theorem Bound4Point4.left_comm {d : } {δ ε : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) :
            Bound4Point4 d δ ε b a c
            theorem Bound4Point4.right_comm {d : } {δ ε : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) :
            Bound4Point4 d δ ε a c b
            theorem Bound4Point4.rotate {d : } {δ ε : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) :
            Bound4Point4 d δ ε b c a
            structure Bound4Point5 (d : ) (δ ε : ) (a : ) :

            A statement of equation 4.5 from the paper, formulated for a.

            We will at some point show that 4.5 can be safely assumed in context, after we've assumed 1.2 and 4.4

            Instances For
              def FourierBound (d : ) (δ ν : ) (a b : ) :

              A statement of the Fourier bound. Note that this is not saying the bound holds, but defining what it means for the bound to hold. In Section4.lean, we will take this as an assumption to many statements in order to deduce bounds on ν. Elsewhere we will show that the bound holds, and thus its proof can be fed in to those lemmas which have it as an assumption.

              Equations
                Instances For
                  theorem FourierBound.special {d : } {δ ν : } {a b : } (hfab : FourierBound d δ ν a b) (j : ) (hj : j Set.Ioc 1 d) :
                  ν < 1 / 2 * (1 + δ + iFinset.Iic d, max (a i) (b i) - max (a j) (b j))

                  From the Fourier bound, we can deduce bounds for each j ∈ (1, d].

                  theorem FourierBound.special' {d : } {δ ν : } {a b : } (hfab : FourierBound d δ ν a b) (j : ) (hj : j Set.Ioc 1 d) :
                  ν < 1 / 2 * (1 + δ + iFinset.Iic d with i j, max (a i) (b i))
                  theorem FourierBound.two {d : } {δ ν : } {a b : } (hfab : FourierBound d δ ν a b) (hd : 2 d) :
                  ν < 1 / 2 * (1 + δ + iFinset.Iic d, max (a i) (b i) - max (a 2) (b 2))
                  theorem FourierBound.three {d : } {δ ν : } {a b : } (hfab : FourierBound d δ ν a b) (hd : 3 d) :
                  ν < 1 / 2 * (1 + δ + iFinset.Iic d, max (a i) (b i) - max (a 3) (b 3))
                  theorem FourierBound.symm {d : } {δ ν : } {a b : } (hfab : FourierBound d δ ν a b) :
                  FourierBound d δ ν b a
                  def DeterminantBound (d : ) (δ ν : ) (a b : ) :

                  A statement of the Determinant bound. Note that this is not saying the bound holds, but defining what it means for the bound to hold. In Section4.lean, we will take this as an assumption to many statements in order to deduce bounds on ν. Elsewhere we will show that the bound holds, and thus its proof can be fed in to those lemmas which have it as an assumption.

                  Equations
                    Instances For
                      theorem determinantBound_set_finite {d : } {δ : } {a b : } :
                      {x : | ∃ (p : ) (q : ) (_ : p Set.Ioc 1 d) (_ : q Set.Ioc 1 d), 1 + δ - a p - b q + min (a p / q) (b q / p) = x}.Finite
                      theorem DeterminantBound.symm {d : } {δ ν : } {a b : } (hdab : DeterminantBound d δ ν a b) :
                      DeterminantBound d δ ν b a
                      theorem DeterminantBound.application {d : } {δ ν : } {a b c : } (ha : baseAssumptions d a) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (hd : 4 d) (M : ) (hM : M = sSup {x : | iSet.Icc 4 d, max (b i) (c i) = x}) :
                      ν < 1 + δ - a 3 - M + min (a 3 / 4) (M / 3)

                      A particular application of the determinant bound used in subcase 2.1

                      def ThueBound (d : ) (δ ν : ) (a b : ) :

                      A statement of the Thue bound. Note that this is not saying the bound holds, but defining what it means for the bound to hold. In Section4.lean, we will take this as an assumption to many statements in order to deduce bounds on ν. Elsewhere we will show that the bound holds, and thus its proof can be fed in to those lemmas which have it as an assumption.

                      Equations
                        Instances For
                          theorem ThueBound.symm {d : } {δ ν : } {a b : } (htab : ThueBound d δ ν a b) :
                          ThueBound d δ ν b a
                          theorem ThueBound.special {d : } {δ ν : } {a b : } (htab : ThueBound d δ ν a b) (p : ) (hp : p Set.Ioc 1 d) :
                          ν < 1 + δ - iFinset.Iic d with p i, (a i + b i)
                          theorem ThueBound.very_special {d : } {δ ν : } {a b : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (htab : ThueBound d δ ν a b) (p : ) (hp : p Set.Ioc 1 d) :
                          ν < 1 + δ - (a p + b p)
                          theorem ThueBound.special_two {d : } {δ ν : } {a b : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (htab : ThueBound d δ ν a b) (hd : 4 d) :
                          ν < 1 + δ - (a 2 + a 4 + (b 2 + b 4))
                          def S (a b c : ) (i : ) :

                          We define S i to be a i + b i + c i.

                          Equations
                            Instances For
                              theorem s_apply (a b c : ) (i : ) :
                              S a b c i = a i + b i + c i
                              theorem s_nonneg {d : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (i : ) :
                              0 S a b c i
                              theorem s_zero {d : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) :
                              S a b c 0 = 0
                              theorem s_rotate {a b c : } :
                              S b c a = S a b c
                              theorem s_left_comm {a b c : } :
                              S b a c = S a b c
                              theorem s_right_comm {a b c : } :
                              S a c b = S a b c
                              theorem Bound4Point4.s_version {d : } {δ ε : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) :
                              iFinset.Iic d, S a b c i 1 + δ - ε
                              def GeometryBound (d : ) (ε ν : ) (a b c : ) :

                              A statement of the Geometry bound. Note that this is not saying the bound holds, but defining what it means for the bound to hold. In Section4.lean, we will take this as an assumption to many statements in order to deduce bounds on ν. Elsewhere we will show that the bound holds, and thus its proof can be fed in to those lemmas which have it as an assumption.

                              Equations
                                Instances For
                                  theorem geometryBound_set_finite {d : } {a b c : } :
                                  {x : | IFinset.Icc 1 d, I'Finset.Icc 1 d, I''Finset.Icc 1 d, max 1 (iI, i * a i + iI', i * b i + iI'', i * c i) - (iI, a i + iI', b i + iI'', c i) = x}.Finite

                                  The set that we are taking the infimum over in the geometry bound is a finite set.

                                  theorem GeometryBound.special {d : } {δ ε ν : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (Ia Ib Ic : Finset ) (hIa : Ia Finset.Icc 1 d) (hIb : Ib Finset.Icc 1 d) (hIc : Ic Finset.Icc 1 d) :
                                  ν < δ + (max 1 (iIa, i * a i + iIb, i * b i + iIc, i * c i) - (iIa, a i + iIb, b i + iIc, c i))
                                  theorem GeometryBound.special_s {d : } {δ ε ν : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (I : Finset ) (hI : I Finset.Icc 1 d) :
                                  ν < δ + (max 1 (∑ iI, i * S a b c i) - iI, S a b c i)
                                  theorem GeometryBound.left_comm {d : } {ε ν : } {a b c : } (hg : GeometryBound d ε ν a b c) :
                                  GeometryBound d ε ν b a c
                                  theorem GeometryBound.right_comm {d : } {ε ν : } {a b c : } (hg : GeometryBound d ε ν a b c) :
                                  GeometryBound d ε ν a c b
                                  theorem GeometryBound.rotate {d : } {ε ν : } {a b c : } (hg : GeometryBound d ε ν a b c) :
                                  GeometryBound d ε ν b c a
                                  def δ_ (d : ) (f : ) :

                                  Define δ_ f to be 1 / 3 - ∑ i ≤ d, f i.

                                  Equations
                                    Instances For
                                      theorem sum_eq_δ_ (d : ) (f : ) :
                                      iFinset.Iic d, f i = 1 / 3 - δ_ d f

                                      4.7

                                      theorem bound_4_point_8 {d : } {ε : } {a b : } (h43 : Bound4Point3 d ε a b) :
                                      δ_ d a + δ_ d b 2 / 300 + ε ^ 2
                                      theorem bound_4_point_9_lower {d : } {δ ε : } ( : 0 < ε) (f : ) (h45 : Bound4Point5 d δ ε f) :
                                      -2 / 300 - δ δ_ d f
                                      theorem bound_4_point_9_upper {d : } {δ ε : } ( : 0 < ε) (f : ) (h45 : Bound4Point5 d δ ε f) :
                                      δ_ d f 1 / 75 + δ + ε
                                      def delta_s (d : ) (a b c : ) :

                                      Define δₛ to be the sum of the δ_ values for a, b, c.

                                      Equations
                                        Instances For
                                          theorem δₛ_eq {d : } {a b c : } :
                                          delta_s d a b c = δ_ d a + δ_ d b + δ_ d c
                                          theorem bound_4_point_10_lower {d : } {δ ε : } {a b c : } ( : 0 < ε) (h44 : Bound4Point4 d δ ε a b c) :
                                          -δ < delta_s d a b c
                                          theorem sum_s {d : } {a b c : } :
                                          iFinset.Iic d, S a b c i = 1 - delta_s d a b c
                                          theorem bound_4_point_10_upper {d : } {ε : } {a b c : } ( : 0 < ε) (hε₁ : ε 2 / 3) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) :
                                          delta_s d a b c 1e-2 + ε
                                          theorem bound_4_point_11_2 {d : } {a : } (h : baseAssumptions d a) (hd : 1 d) :
                                          iFinset.Icc 2 d, (i - 1) * a i 2 / 3 + δ_ d a
                                          theorem bound_4_point_11_3 {d : } {a : } (ha : baseAssumptions d a) (hd : 2 d) :
                                          iFinset.Icc 3 d, (i - 2) * a i 1 / 3 + a 1 + 2 * δ_ d a
                                          theorem bound_4_point_11_4 {d : } {a : } (ha : baseAssumptions d a) (hd : 3 d) :
                                          iFinset.Icc 4 d, (i - 3) * a i 2 * a 1 + a 2 + 3 * δ_ d a
                                          theorem bound_4_point_12 {d : } {δ ν : } {a b : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (htab : ThueBound d δ ν a b) (j : ) (hj : j Set.Ioc 1 d) ( : 0.66 < ν) :
                                          a j + b j < 0.34 + δ
                                          theorem bound_4_point_13 {d : } {δ ν : } {a b : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (htab : ThueBound d δ ν a b) (hd : 4 d) ( : 0.66 < ν) :
                                          a 2 + a 4 + (b 2 + b 4) < 0.34 + δ
                                          theorem bound_4_point_14_general {d : } {δ ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (j : ) (hj : j Set.Ioc 1 d) ( : 0.66 < ν) :
                                          S a b c j < 0.51 + 1.5 * δ
                                          theorem bound_4_point_14_two_four {d : } {δ ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hd : 4 d) ( : 0.66 < ν) :
                                          S a b c 2 + S a b c 4 < 0.51 + 1.5 * δ
                                          theorem sum_s_2 {d : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hd : 1 d) :
                                          iFinset.Icc 2 d, (i - 1) * S a b c i 2 + delta_s d a b c
                                          theorem sum_s_3 {d : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hd : 2 d) :
                                          iFinset.Icc 3 d, (i - 2) * S a b c i 1 + S a b c 1 + 2 * delta_s d a b c
                                          theorem sum_s_4 {d : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hd : 3 d) :
                                          iFinset.Icc 4 d, (i - 3) * S a b c i 2 * S a b c 1 + S a b c 2 + 3 * delta_s d a b c
                                          theorem bound_4_point_15 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) ( : δ 6e-2) ( : 0.66 < ν) (hd : 2 d) :
                                          S a b c 1 + S a b c 2 0.34 + δ
                                          def SubSums (j : ) (a b c : ) :

                                          4.16

                                          Equations
                                            Instances For
                                              theorem GeometryBound.subSums {d : } {δ ε ν : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) {τ : } (j : ) (hj : j Set.Icc 3 d) ( : τ SubSums j a b c) :
                                              ν < δ + (max 1 (S a b c 1 + 2 * S a b c 2 + j * τ) - (S a b c 1 + S a b c 2 + τ)) ν < δ + (max 1 (S a b c 1 + j * τ) - (S a b c 1 + τ))
                                              theorem bound_4_point_17 {d : } {δ ε ν : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (τ : ) {j : } ( : τ SubSums j a b c) ( : 0.66 < ν) (hj : j Set.Icc 3 d) :
                                              τSet.Icc (0.34 - S a b c 1 - S a b c 2 + δ) ((0.66 - S a b c 2 - δ) / (j - 1))
                                              theorem bound_4_point_17_3 {d : } {δ ε ν : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (τ : ) ( : τ SubSums 3 a b c) ( : 0.66 < ν) (hd : 3 d) :
                                              τSet.Icc (0.34 - S a b c 1 - S a b c 2 + δ) (0.33 - 1 / 2 * S a b c 2 - 1 / 2 * δ)
                                              theorem bound_4_point_18_aux {d : } {δ ε ν : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (τ : ) ( : τ SubSums 3 a b c) ( : 0.66 < ν) (hd : 3 d) :
                                              τSet.Icc (0.34 - S a b c 1 + δ) (0.33 - 1 / 2 * δ)
                                              theorem bound_4_point_18 {d : } {δ ε ν : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (τ : ) ( : τ SubSums 3 a b c) (hd : 3 d) ( : 0.66 < ν) :
                                              τSet.Icc (0.34 - S a b c 1 - S a b c 2 + δ) (0.33 - 1 / 2 * S a b c 2 - 1 / 2 * δ) Set.Icc (0.34 - S a b c 1 + δ) (0.33 - 1 / 2 * δ)
                                              theorem bound_4_point_19_first {d : } {a : } (ha : baseAssumptions d a) (hd : 3 d) :
                                              1 / 3 - 4 * δ_ d a - 3 * a 1 - 2 * a 2 a 3
                                              theorem bound_4_point_19_second {d : } {a : } (ha : baseAssumptions d a) (hd : 4 d) :
                                              1 / 3 - 5 / 2 * δ_ d a - 2 * a 1 - 3 / 2 * a 2 - 1 / 2 * a 4 a 3
                                              theorem bound_4_point_20 {d : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hd : 3 d) :
                                              1 - 4 * delta_s d a b c - 3 * S a b c 1 - 2 * S a b c 2 S a b c 3
                                              theorem bound_4_point_21 {d : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hd : 4 d) :
                                              1 - 5 / 2 * delta_s d a b c - 2 * S a b c 1 - 3 / 2 * S a b c 2 - 1 / 2 * S a b c 4 S a b c 3
                                              theorem bound_4_point_22 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) ( : 0.66 < ν) (hs₂ : 0.3 S a b c 2) ( : δ 6e-2) (hd : 2 d) :
                                              S a b c 1 4e-2 + δ
                                              theorem case_1_helper {d : } {δ ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) ( : 0.66 < ν) (hs₂ : 0.3 S a b c 2) (hd : 4 d) :
                                              S a b c 4 < 0.21 + 3 / 2 * δ
                                              theorem subcase_1_point_1 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 4 d) ( : 0.66 < ν) ( : δ 3e-3) (hcb : c 3 b 3) (hs₂ : 0.3 S a b c 2) ( : ε 1 / 10000) (hε₀ : 0 < ε) (hb₃ : b 3 0.34 - S a b c 1 - S a b c 2 + δ) :
                                              theorem bound_4_point_23 {d : } {δ ε ν : } {a b c : } (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (hd : 3 d) ( : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) :
                                              0.33 - 1 / 2 * S a b c 2 - 1 / 2 * δ < b 3
                                              theorem b4_bound {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 4 d) ( : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) ( : δ 3e-3) ( : ε 1 / 10000) :
                                              b 4 < (0.66 - S a b c 2 - δ) / 3
                                              theorem b5_bound {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 d) ( : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) ( : δ 3e-3) ( : ε 1 / 10000) :
                                              b 5 < (0.66 - S a b c 2 - δ) / 4
                                              theorem b6_bound {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 d) ( : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) ( : δ 3e-3) ( : ε 1 / 10000) :
                                              b 6 < (0.66 - S a b c 2 - δ) / 5
                                              theorem a4_bound {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 4 d) ( : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) ( : δ 3e-3) ( : ε 1 / 10000) (hba : b 3 a 3) :
                                              a 4 < (0.66 - S a b c 2 - δ) / 3
                                              theorem a5_bound {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 d) ( : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) ( : δ 3e-3) ( : ε 1 / 10000) (hba : b 3 a 3) :
                                              a 5 < (0.66 - S a b c 2 - δ) / 4
                                              theorem a6_bound {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 d) ( : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) ( : δ 3e-3) ( : ε 1 / 10000) (hba : b 3 a 3) :
                                              a 6 < (0.66 - S a b c 2 - δ) / 5
                                              theorem self_improve_bounds {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 d) ( : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) ( : δ 3e-3) ( : ε 1 / 10000) (hba : b 3 a 3) :
                                              max (a 4) (b 4) < 0.34 - S a b c 1 - S a b c 2 + δ max (a 5) (b 5) < 0.34 - S a b c 1 - S a b c 2 + δ max (a 6) (b 6) < 0.34 - S a b c 1 - S a b c 2 + δ
                                              theorem test {α : Type u_1} [AddCommMonoid α] {a b : } {f : α} (hab : a b) :
                                              iFinset.Iic a, f i + iFinset.Icc (a + 1) b, f i = iFinset.Iic b, f i
                                              theorem apply_fourier {d : } {δ ν : } {a b : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hfab : FourierBound d δ ν a b) (hd : 6 d) :
                                              2 * ν - 1 - δ < 2 / 3 - (δ_ d a + δ_ d b) - iFinset.Iic 6with i 2, min (a i) (b i) - (a 2 + b 2)
                                              theorem two_bound {d : } {a : } (ha : baseAssumptions d a) (hd : 6 d) :
                                              4 / 15 - 1 / 5 * iFinset.Iic 6with i 2, (7 - i) * a i - 7 / 5 * δ_ d a a 2
                                              theorem summation_range_eq :
                                              {xFinset.Iic 6 | x 2} = {0, 1, 3, 4, 5, 6}
                                              theorem bound_4_point_24 {d : } {δ ν : } {a b : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hfab : FourierBound d δ ν a b) (hd : 6 d) (hba : b 3 a 3) :
                                              2 * ν - 1 - δ < 2 / 15 + 2 / 5 * (δ_ d a + δ_ d b) + 1 / 5 * (6 * max (a 1) (b 1) + min (a 1) (b 1) + 4 * a 3 - b 3 + 3 * max (a 4) (b 4) + 2 * max (a 5) (b 5) + max (a 6) (b 6))
                                              theorem subcase_1_point_2_aux {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (hg : GeometryBound d ε ν a b c) (hd : 3 d) ( : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) :
                                              4 * a 3 - b 3 5 / 2 * S a b c 2 - 0.29 + 13 / 2 * δ
                                              theorem subcase_1_point_2 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (hfab : FourierBound d δ ν a b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 d) ( : 0.66 < ν) (hba : b 3 a 3) (hs₂ : 0.3 S a b c 2) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) ( : δ 3e-3) ( : ε 1 / 10000) :
                                              theorem case_1 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (hfab : FourierBound d δ ν a b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 d) ( : 0.66 < ν) (hs₂ : 0.3 S a b c 2) ( : δ 3e-3) (hε₀ : 0 < ε) ( : ε 1 / 10000) (hcb : c 3 b 3) (hba : b 3 a 3) :
                                              theorem bound_4_point_25 {d : } {δ ν : } {a b : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (htab : ThueBound d δ ν a b) (hd : 3 d) ( : 0.66 < ν) (h : b 3 a 3) :
                                              b 3 < 0.17 + 1 / 2 * δ
                                              theorem bound_4_point_26_aux {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (hg : GeometryBound d ε ν a b c) (hd : 3 d) ( : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) ( : δ 1e-2) (hba : b 3 a 3) (hcb : c 3 b 3) :
                                              b 3 < 0.34 - S a b c 1 - S a b c 2 + δ c 3 < 0.34 - S a b c 1 - S a b c 2 + δ
                                              theorem bound_4_point_26 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (hg : GeometryBound d ε ν a b c) (hd : 3 d) ( : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) ( : δ 1e-2) (hba : b 3 a 3) (hcb : c 3 b 3) :
                                              0.32 - 4 * delta_s d a b c - S a b c 1 - 2 * δ a 3
                                              theorem case_2_subcase_1_large_sum {d : } {δ ν : } {a b c : } (ha : baseAssumptions d a) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (hd : 4 d) ( : 0.66 < ν) ( : δ 15e-3) (h : 0.32 a 3) (hmax : iSet.Icc 4 d, 3 / 4 * 9e-2 < max (b i) (c i)) :
                                              theorem GeometryBound.s21_application_basic {d : } {ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hg : GeometryBound d ε ν a b c) (hd : 4 d) :
                                              ν < ε + a 3 + b 3 + min (b 4) (c 4) + iFinset.Icc 5 d, (b i + c i) + max 0 (iFinset.Icc 1 d, i * a i + (b 1 + c 1) + 2 * (b 2 + c 2) - 3 * (a 3 - c 3) + 4 * max (b 4) (c 4) - 1)
                                              theorem min_le_half_add {x y : } :
                                              min x y (x + y) / 2
                                              theorem case_2_subcase_1_subsubcase_1 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43bc : Bound4Point3 d ε b c) (htab : ThueBound d δ ν a b) (hd : 5 d) ( : 0.66 < ν) (h₅ : b 5 + c 5 0.135) (hε₀ : 0 ε) ( : ε 1 / 10000) ( : δ 5e-3) (h : iFinset.Iic d, (i - 1) * (b i + c i) 4 / 3 + (δ_ d b + δ_ d c)) :
                                              a 3 + b 3 + min (b 4) (c 4) + iFinset.Icc 5 d, (b i + c i) < 0.645
                                              theorem case_2_subcase_1_subsubcase_2 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (htac : ThueBound d δ ν a c) (hd : 4 d) ( : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (h₄ : max (b 4) (c 4) 3 / 4 * 9e-2) (hε₀ : 0 < ε) ( : δ 5e-3) (h : 0.32 a 3) :
                                              a 3 + b 3 + min (b 4) (c 4) + iFinset.Icc 5 d, (b i + c i) + (iFinset.Icc 1 d, i * a i + (b 1 + c 1) + 2 * (b 2 + c 2) - 3 * (a 3 - c 3) + 4 * max (b 4) (c 4) - 1) < 0.61
                                              theorem case_2_subcase_1 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43bc : Bound4Point3 d ε b c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (hg : GeometryBound d ε ν a b c) (hd : 5 d) ( : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) ( : δ 5e-3) (hε₀ : 0 < ε) ( : ε 1 / 10000) (h : 0.32 a 3) :
                                              theorem case_2_subcase_2 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 d) ( : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) ( : δ 5e-3) (hε₀ : 0 < ε) ( : ε 1 / 10000) (h : b 3 + c 3 < 0.33 - 1 / 2 * S a b c 2 - 1 / 2 * δ) :
                                              theorem case_2_subcase_3 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 d) ( : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) ( : δ 3e-3) (hε₀ : 0 < ε) ( : ε 1 / 10000) (hba : b 3 a 3) (hcb : c 3 b 3) (h : 0.73 < 4 * S a b c 1 + 3 * S a b c 2) :
                                              theorem case_2_subcase_4 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 d) ( : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) ( : δ 4e-3) (hε₀ : 0 < ε) ( : ε 1 / 100000) (hba : b 3 a 3) (hcb : c 3 b 3) (h : 4 * S a b c 1 + S a b c 2 < 0.35) :
                                              theorem case_2_subcase_5 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 d) ( : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) ( : δ 3e-3) (hε₀ : 0 < ε) ( : ε 1 / 100000) (hba : b 3 a 3) (hcb : c 3 b 3) (h : S a b c 2 Set.Icc 7e-2 0.199) :
                                              theorem case_2_subcase_6_end_ab {d : } {δ ε ν : } {a b : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (hfab : FourierBound d δ ν a b) (hd : 5 d) ( : δ 1e-3) (hε₀ : 0 < ε) ( : ε 1 / 100000) (hba : b 3 a 3) :
                                              ν 0.78451 + 1 / 3 * (max (a 2) (b 2) - a 3) - 1 / 2 * b 3
                                              theorem case_2_subcase_6_end_ec {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hfab : FourierBound d δ ν a b) (hfac : FourierBound d δ ν a c) (hfbc : FourierBound d δ ν b c) (hd : 5 d) ( : 0.66 < ν) ( : δ 1e-3) (hε₀ : 0 < ε) ( : ε 1 / 100000) (hba : b 3 a 3) (hcb : c 3 b 3) (hbc3' : 0.33 - 1 / 2 * δ b 3 + c 3) (hs2 : S a b c 2 7e-2) :
                                              theorem case_2_subcase_6 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hfab : FourierBound d δ ν a b) (hfac : FourierBound d δ ν a c) (hfbc : FourierBound d δ ν b c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 d) ( : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) ( : δ 1e-3) (hε₀ : 0 < ε) ( : ε 1 / 100000) (hba : b 3 a 3) (hcb : c 3 b 3) (h : 25e-3 < 2 * S a b c 1 - S a b c 2) :
                                              theorem case_2 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hfab : FourierBound d δ ν a b) (hfac : FourierBound d δ ν a c) (hfbc : FourierBound d δ ν b c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 d) ( : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) ( : δ 1e-3) (hε₀ : 0 < ε) ( : ε 1 / 100000) (hba : b 3 a 3) (hcb : c 3 b 3) :
                                              theorem thm_4_point_3_asymm {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hfab : FourierBound d δ ν a b) (hfac : FourierBound d δ ν a c) (hfbc : FourierBound d δ ν b c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 d) ( : δ 1e-3) (hε₀ : 0 < ε) ( : ε 1 / 100000) (hba : b 3 a 3) (hcb : c 3 b 3) :
                                              ν 0.66
                                              theorem thm_4_point_3 {d : } {δ ε ν : } {a b c : } (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hfab : FourierBound d δ ν a b) (hfac : FourierBound d δ ν a c) (hfbc : FourierBound d δ ν b c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (hdbc : DeterminantBound d δ ν b c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 d) ( : δ 1e-3) (hε₀ : 0 < ε) ( : ε 1 / 100000) :
                                              ν 0.66