Besicovitch's set in the plane

The graph Π = {(x, g x) : x ∈ [0, 1]} of Besicovitch's function, as a subset of EuclideanSpace ℝ (Fin 2), together with the elementary metric facts used later: the distance formula on the graph, the first-coordinate projection is 1-Lipschitz (so the Hausdorff measure of a piece of the graph is at least the Lebesgue measure of its base), and the graph over a level-n cell has diameter at most twice the cell length.

@[reducible, inline]

abbrev LeanPool.Besicovitch.Example.Plane : Type

The plane.

Equations

• LeanPool.Besicovitch.Example.Plane = EuclideanSpace ℝ (Fin 2)

noncomputable def LeanPool.Besicovitch.Example.graphMap (x : ℝ) : Plane

The graph map x ↦ (x, g x).

Equations

• LeanPool.Besicovitch.Example.graphMap x = !₂[x, LeanPool.Besicovitch.Example.besicovitchFun x]

def LeanPool.Besicovitch.Example.besicovitchSet : Set Plane

Besicovitch's set: the graph of g over [0, 1].

Equations

• LeanPool.Besicovitch.Example.besicovitchSet = LeanPool.Besicovitch.Example.graphMap '' Set.Icc 0 1

@[simp]

theorem LeanPool.Besicovitch.Example.graphMap_apply_zero (x : ℝ) : (graphMap x).ofLp 0 = x

@[simp]

theorem LeanPool.Besicovitch.Example.graphMap_apply_one (x : ℝ) : (graphMap x).ofLp 1 = besicovitchFun x

theorem LeanPool.Besicovitch.Example.graphMap_injective : Function.Injective graphMap

theorem LeanPool.Besicovitch.Example.dist_graphMap (x y : ℝ) : dist (graphMap x) (graphMap y) = √((x - y) ^ 2 + (besicovitchFun x - besicovitchFun y) ^ 2)

The distance between two points of the graph.

theorem LeanPool.Besicovitch.Example.lipschitzWith_proj : LipschitzWith 1 fun (p : Plane) => p.ofLp 0

The first coordinate is 1-Lipschitz.

theorem LeanPool.Besicovitch.Example.proj_image_graphMap_image (A : Set ℝ) : (fun (p : Plane) => p.ofLp 0) '' graphMap '' A = A

The first coordinate recovers the base of a piece of the graph.

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

(B≥) The Hausdorff measure of a piece of the graph is at least the measure of its base.

Cells

def LeanPool.Besicovitch.Example.cell (n : ℕ) (i : ℤ) : Set ℝ

The level-n cell with index i.

Equations

• LeanPool.Besicovitch.Example.cell n i = Set.Ico (↑i * LeanPool.Besicovitch.Example.cellLength n) ((↑i + 1) * LeanPool.Besicovitch.Example.cellLength n)

theorem LeanPool.Besicovitch.Example.mem_cell_iff {n : ℕ} {i : ℤ} {x : ℝ} : x ∈ cell n i ↔ cellIndex n x = i

theorem LeanPool.Besicovitch.Example.mem_cell_cellIndex (n : ℕ) (x : ℝ) : x ∈ cell n (cellIndex n x)

theorem LeanPool.Besicovitch.Example.volume_cell (n : ℕ) (i : ℤ) : MeasureTheory.volume (cell n i) = ENNReal.ofReal (cellLength n)

theorem LeanPool.Besicovitch.Example.cell_disjoint {n : ℕ} {i j : ℤ} (h : i ≠ j) : Disjoint (cell n i) (cell n j)

theorem LeanPool.Besicovitch.Example.diam_graphMap_image_cell_le {n : ℕ} (hn : 1 ≤ n) (i : ℤ) : Metric.ediam (graphMap '' cell n i) ≤ ENNReal.ofReal (2 * cellLength n)

The graph over a level-n ≥ 1 cell has diameter at most twice the cell length.