Covering the graph over an interval

The graph over [a, b) is covered, at level n, by the graphs over the level-n cells meeting [a, b). There are at most (b - a) / cellLength n + 2 of them, each of diameter at most 2 * cellLength n, so the Hausdorff measure of the graph over [a, b) is at most 2 (b - a). The constant 2 is crude but is all that is needed: the sharp value 1 is never used.

noncomputable def LeanPool.Besicovitch.Example.cellCount (n : ℕ) (a b : ℝ) : ℕ

The number of level-n cells meeting [a, b): from the cell of a to the cell of b.

Equations

• LeanPool.Besicovitch.Example.cellCount n a b = (LeanPool.Besicovitch.Example.cellIndex n b - LeanPool.Besicovitch.Example.cellIndex n a + 1).toNat

theorem LeanPool.Besicovitch.Example.cellCount_le (n : ℕ) {a b : ℝ} (hab : a ≤ b) : ↑(cellCount n a b) ≤ (b - a) / cellLength n + 2

theorem LeanPool.Besicovitch.Example.exists_cell_of_mem {n : ℕ} {a b x : ℝ} (hx : x ∈ Set.Ico a b) : ∃ (k : Fin (cellCount n a b)), x ∈ cell n (cellIndex n a + ↑↑k)

Every point of [a, b) lies in one of the counted cells.

theorem LeanPool.Besicovitch.Example.graphMap_image_Ico_subset {n : ℕ} (a b : ℝ) : graphMap '' Set.Ico a b ⊆ ⋃ (k : Fin (cellCount n a b)), graphMap '' cell n (cellIndex n a + ↑↑k)

The graph over [a, b) at level n ≥ 1 is covered by cellCount cylinders.

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_graphMap_image_Ico_le {a b : ℝ} (hab : a ≤ b) : (MeasureTheory.Measure.hausdorffMeasure 1) (graphMap '' Set.Ico a b) ≤ ENNReal.ofReal (2 * (b - a))

(B≤ on intervals) The graph over [a, b) has Hausdorff measure at most 2 (b - a).