The partition π(G, k)
of Grid X
by volume, given in (5.1.1) and (5.1.2).
Note: the G
is fixed with properties in ProofData
.
The definition dens'_k(π')
given in (5.1.6).
Equations
- One or more equations did not get rendered due to their size.
The partition β(k, n)
of π(k)
by density, given in (5.1.7).
Lemma 5.3.11
Lemma 5.3.12
The subset π
(p)
of π(k, n)
, given in (5.1.8).
The subset ββ(k, n, j)
of β(k, n)
, given in (5.1.9).
Together with πβ(k, n)
this forms a partition.
The subset πβ(k, n)
of β(k, n)
, given in (5.1.10).
Not to be confused with πβ(k, n, j)
which is called πβ'
in Lean.
πβ(k, n, j, l)
consists of the minimal elements in ββ(k, n, j)
not in
πβ(k, n, j, l')
for some l' < l
. Defined near (5.1.11).
The subset ββ(k, n, j)
of ββ(k, n, j)
, given in (5.1.13).
The subset πβ(k, n, j)
of ββ(k, n, j)
, given in (5.1.14).
Equations
- One or more equations did not get rendered due to their size.
The subset πβ(k, n, j)
of ββ(k, n, j)
, given in (5.1.15).
The subset ββ(k, n, j)
of ββ(k, n, j)
, given in (5.1.16).
πβ(k, n, j, l)
consists of the maximal elements in ββ(k, n, j)
not in
πβ(k, n, j, l')
for some l' < l
. Defined near (5.1.17).
The subset ββ(k, n, j)
of ββ(k, n, j)
, given in (5.1.19).
The subset π(u)
of Grid X
, given near (5.1.20).
Note: It seems to also depend on n
.
The subset πβ(k, n, j)
of ββ(k, n, j)
, given near (5.1.22).
Todo: we may need to change the definition to say that p
is at most the least upper bound of π n u
in Grid X
.
The subset ββ
(k, n, j)
of ββ(k, n, j)
, given in (5.1.23).
The set
The exceptional set Gβ
, defined in (5.1.25).
Equations
- Gβ = β p β highDensityTiles, β(π p)
Finset of cubes in setA
. Appears in the proof of Lemma 5.2.5.