We prove a weighted version of the Szemerédi regularity lemma, which is sufficient for the grid application. For disjoint nonempty vertex sets in a graph, write for their edge density of a bipartite graph. Call the pair -regular if every , with and satisfies .
The weighted Szemerédi regularity lemma states that, for every , there are integers such that every graph on vertices has a set partition into at most nonempty cells , each of size at most , for which
The sum is ordered. The cells need not have equal sizes; their weights replace the usual unweighted count of bad pairs.
To prove it, start with nearly equal cells, taking . Each has size at most . Define the regularity energy
Here even diagonal rectangles use the mean adjacency indicator, counting ordered pairs of vertices. Thus . Under a refinement, the old rectangle density is the weighted mean of the new ones, and the refinement variance identity for regularity energy gives
In particular refinement cannot decrease energy.
If the irregular-pair weight exceeds , choose witness subsets , for every irregular unordered pair, and split each cell simultaneously by all its witnesses. There are at most such subsets in any one cell, so the new number of cells is at most . In an irregular rectangle, its witness has relative area at least and density discrepancy greater than . Since the witness rectangle is now a union of refined rectangles, the Cauchy-Schwarz inequality applied to their weighted density discrepancies bounds the variance contribution from below by
Summing over both orientations of all irregular pairs raises by more than . Since , after at most rounds the required weight bound must hold. The finite recurrence , starting at , supplies ; all cells remain small because we only refine. This proves the stated weighted Szemerédi regularity lemma.
We next derive the triangle removal lemma from this version. First, three disjoint classes whose pairs are -regular pairs of density at least have many triangles if and . Fewer than vertices of have fewer than neighbours in : otherwise that set of vertices, paired with all of , would violate regularity. The same holds for . For each of the at least remaining vertices, both neighbour sets have relative size at least . Regularity of then supplies at least times the product of those two neighbour-set sizes edges. Thus the regular triangle counting lemma, also for unequal class sizes, gives
For a desired deletion tolerance , take , , and a weighted regularity partition with at most cells. Put . Delete edges inside cells, between irregular pairs, between regular pairs of density less than , and incident to cells smaller than . The first two deletions each cost at most . The sparse-pair deletion costs at most . For the last deletion, small-cell deletion in weighted regularity removes at most vertices and at most incident edges. The total is bounded by
A triangle surviving these deletions would lie in three distinct cells, all of size at least , with all their pairs regular and of density at least . The original graph would then have at least triangles. Therefore, with
a graph on sufficiently many vertices with at most triangles can be made triangle-free by deleting fewer than edges. This establishes the triangle removal lemma with every parameter depending only on .
Now apply a tripartite graph encoding of a grid. Take separate vertex classes , , . For each grid point in the given set, put in the three edges
where their endpoints belong respectively to , , and . Each point supplies a triangle. These triangles are edge-disjoint triangles, since any one of the three edge types uniquely determines the point that supplied it.
Conversely, any triangle with vertices , , forces the three points
to belong to . Put . For these form a corner in an integer grid; for they all arise from the same grid point. Thus if there is no corner, the graph has exactly triangles, yet destroying all triangles requires at least edge deletions.
We may suppose , since larger densities make the request vacuous. Use the triangle removal lemma with . Our graph has vertices, so, for sufficiently large , its bound on the number of triangles is at most . The lemma would delete fewer than
edges to destroy all triangles. This contradicts the lower bound from the edge-disjoint family. Hence every sufficiently large positive-density square grid contains a nondegenerate corner, proving the requested corners theorem and in particular the existence of a suitable .