The lower density of Besicovitch's set is at least 1/2

At an interior point graphMap x of the graph, the ball of radius r contains the graph over an interval of length at least θ * r, for every θ < 1 and every small r: let n be the last level with r ≤ cellLength n; inside the level-n cell of x the function g varies by at most 4 * cellLength (n+1) / (n+1) < 4 * r / (n+1), which is below (1 - θ) * r once n is large. Since the first-coordinate projection is 1-Lipschitz, the Hausdorff measure of the graph over that interval is at least θ * r, so the lower density (normalised by the diameter 2 * r of the ball) is at least θ / 2. Letting θ → 1 gives 1/2.

theorem LeanPool.Besicovitch.Example.exists_cellLength_lt_le {r : ℝ} (hr : 0 < r) {n₀ : ℕ} (hr₀ : r ≤ cellLength n₀) : ∃ (n : ℕ), n₀ ≤ n ∧ cellLength (n + 1) < r ∧ r ≤ cellLength n

Below any positive radius r ≤ cellLength n₀ there is a level n ≥ n₀ with cellLength (n + 1) < r ≤ cellLength n.

theorem LeanPool.Besicovitch.Example.dist_graphMap_lt {θ r : ℝ} (hθ : θ ∈ Set.Ioo 0 1) (hr : 0 < r) {n : ℕ} (hn : 4 / (↑n + 1) ≤ 1 - θ) (hrn : cellLength (n + 1) < r) {x y : ℝ} (hxy : cellIndex n x = cellIndex n y) (hd : |x - y| < θ * r) : dist (graphMap x) (graphMap y) < r

A point of the level-n cell of x at horizontal distance < θ * r from x lies within distance r of graphMap x on the graph, once 4 / (n + 1) ≤ 1 - θ and cellLength (n + 1) < r.

theorem LeanPool.Besicovitch.Example.eventually_ofReal_le_hausdorffMeasure_inter_ball {x : ℝ} (hx : x ∈ Set.Ioo 0 1) {θ : ℝ} (hθ : θ ∈ Set.Ioo 0 1) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ENNReal.ofReal (θ * r) ≤ (MeasureTheory.Measure.hausdorffMeasure 1) (besicovitchSet ∩ Metric.ball (graphMap x) r)

The key estimate. For every θ < 1 and every sufficiently small r, the ball of radius r about the interior graph point graphMap x meets the graph in a set of Hausdorff measure at least θ * r.

theorem LeanPool.Besicovitch.Example.ofReal_half_le_lowerOneDensity_graphMap {x : ℝ} (hx : x ∈ Set.Ioo 0 1) {θ : ℝ} (hθ : θ ∈ Set.Ioo 0 1) : ENNReal.ofReal (θ / 2) ≤ lowerOneDensity besicovitchSet (graphMap x)

For every θ < 1, the lower density of the graph at an interior graph point is at least θ / 2.

theorem LeanPool.Besicovitch.Example.one_half_le_lowerOneDensity_graphMap {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : ENNReal.ofReal (1 / 2) ≤ lowerOneDensity besicovitchSet (graphMap x)

The lower density of Besicovitch's set is at least 1/2 at every interior point of the graph.