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.
The bound 4.3 is symmetric in a, b
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
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
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
A particular application of the determinant bound used in subcase 2.1
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
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
The set that we are taking the infimum over in the geometry bound is a finite set.