Prove Lemma 5.2.1

[js2357]

Prove Lemma 5.2.1.

Notes:

• I changed the definition of highDensityTiles to use a strict inequality. I think this was a typo in the blueprint, since everything else seems consistent with a strict inequality. I also updated the definition in the blueprint.
• The proof in the blueprint had an extra factor of 2, so the Lemma 5.2.1 that I proved is stronger by a factor of 2. I also updated the statement and proof in the blueprint.
• I changed the statement of measure_biUnion_le_lintegral to use ℝ≥0∞ rather than ℝ≥0. This was only to avoid some annoying casting; none of the numbers involved in the proof are infinite, so the ℝ≥0 version should theoretically be adequate. If the ℝ≥0∞ version turns out to be substantially harder to prove, it should be possible to change back to the original version and deal with the casts in the proof of Lemma 5.2.1 instead. I added a comment to this effect before measure_biUnion_le_lintegral.

[fpvandoorn]

Thanks, this is great! The changes look good to me.