The Hausdorff measure of the graph over an arbitrary set

An open set is the increasing union of the cells it contains; the graph over such a union of level-n cells has Hausdorff measure at most twice its Lebesgue measure by the cell bound, and the monotone-union limit carries this to the open set. Outer regularity of Lebesgue measure then gives μH[1] (graphMap '' A) ≤ 2 * volume A for every A ⊆ ℝ; in particular the graph over a Lebesgue-null set is μH[1]-null.

def LeanPool.Besicovitch.Example.cellHull (n : ℕ) (U : Set ℝ) : Set ℝ

The union of the level-n cells contained in U.

Equations

• LeanPool.Besicovitch.Example.cellHull n U = ⋃ i ∈ {i : ℤ | LeanPool.Besicovitch.Example.cell n i ⊆ U}, LeanPool.Besicovitch.Example.cell n i

theorem LeanPool.Besicovitch.Example.cellHull_subset (n : ℕ) (U : Set ℝ) : cellHull n U ⊆ U

theorem LeanPool.Besicovitch.Example.cell_subset_of_mem {m n : ℕ} (hmn : m ≤ n) {i j : ℤ} {x : ℝ} (hx : x ∈ cell n j) (hx' : x ∈ cell m i) : cell n j ⊆ cell m i

A finer cell meeting a coarser one is contained in it.

theorem LeanPool.Besicovitch.Example.cellHull_subset_succ (n : ℕ) (U : Set ℝ) : cellHull n U ⊆ cellHull (n + 1) U

theorem LeanPool.Besicovitch.Example.monotone_cellHull (U : Set ℝ) : Monotone fun (n : ℕ) => cellHull n U

theorem LeanPool.Besicovitch.Example.cell_subset_ball (n : ℕ) (x : ℝ) : cell n (cellIndex n x) ⊆ Metric.ball x (cellLength n)

The cell of x lies within cellLength n of x.

theorem LeanPool.Besicovitch.Example.iUnion_cellHull_of_isOpen {U : Set ℝ} (hU : IsOpen U) : ⋃ (n : ℕ), cellHull n U = U

theorem LeanPool.Besicovitch.Example.volume_cellHull (n : ℕ) (U : Set ℝ) : MeasureTheory.volume (cellHull n U) = ∑' (i : { i : ℤ // cell n i ⊆ U }), MeasureTheory.volume (cell n ↑i)

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_graphMap_image_cell_le {n : ℕ} (i : ℤ) : (MeasureTheory.Measure.hausdorffMeasure 1) (graphMap '' cell n i) ≤ 2 * MeasureTheory.volume (cell n i)

The graph over a level-n ≥ 1 cell has Hausdorff measure at most twice the cell's length.

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_graphMap_image_cellHull_le (n : ℕ) (U : Set ℝ) : (MeasureTheory.Measure.hausdorffMeasure 1) (graphMap '' cellHull n U) ≤ 2 * MeasureTheory.volume (cellHull n U)

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_graphMap_image_le_of_isOpen {U : Set ℝ} (hU : IsOpen U) : (MeasureTheory.Measure.hausdorffMeasure 1) (graphMap '' U) ≤ 2 * MeasureTheory.volume U

(B≤ on open sets)

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_graphMap_image_le (A : Set ℝ) : (MeasureTheory.Measure.hausdorffMeasure 1) (graphMap '' A) ≤ 2 * MeasureTheory.volume A

(B≤) The graph over any set has Hausdorff measure at most twice its Lebesgue measure.

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_graphMap_image_eq_zero {A : Set ℝ} (hA : MeasureTheory.volume A = 0) : (MeasureTheory.Measure.hausdorffMeasure 1) (graphMap '' A) = 0

The graph over a Lebesgue-null set is μH[1]-null.