From a one-sided hole to two-sided avoidance

If g is L-Lipschitz on A, then near every level-n grid point A misses an interval of length margin L n on one of the two sides. A single such hole is a vanishing fraction of any ball, so it cannot by itself force A to be null. What it does force is that a density point of A cannot sit within margin L n of a level-n grid point for infinitely many n: such a point has a hole of relative size 1/4 in the ball of radius 2 * margin L n about it, so its density along that sequence of radii is at most 3/4.

Hence almost every point of A eventually avoids the grid on both sides, and the nested recursion of LeanPool.Besicovitch.Example.Zero applies to the resulting sets.

theorem LeanPool.Besicovitch.Example.measure_inter_closedBall_le {L : NNReal} {A : Set ℝ} (hg : LipschitzOnWith L besicovitchFun A) {n : ℕ} (hn : 1 ≤ n) {x : ℝ} {i : ℤ} (hx : |x - gridPoint n i| < margin (↑L) n) : MeasureTheory.volume (A ∩ Metric.closedBall x (2 * margin (↑L) n)) ≤ ENNReal.ofReal (3 * margin (↑L) n)

A point within margin of a grid point has a hole of relative size 1/4 about it.

theorem LeanPool.Besicovitch.Example.tendsto_margin (L : ℝ) (hL : 0 ≤ L) : Filter.Tendsto (margin L) Filter.atTop (nhds 0)

The margins tend to zero.

theorem LeanPool.Besicovitch.Example.ae_eventually_mem_avoid {L : NNReal} {A : Set ℝ} (hg : LipschitzOnWith L besicovitchFun A) : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict A, ∀ᶠ (n : ℕ) in Filter.atTop, x ∈ avoid (↑L) n

Almost every point of a set on which g is Lipschitz eventually avoids the grid.