Where a Lipschitz piece of the graph can live

If g is L-Lipschitz on a set A, then A cannot meet both sides of a level-n grid point within margin L n = cellLength n / (2 n (L + 1)): two such points sit in adjacent cells, so g jumps by at least cellLength n / n between them by (E2), while the Lipschitz bound allows less.

avoid L n is the set of points at distance at least margin L n from every level-n grid point. Its intersection with any cell of level m ≥ n is order-connected, because every level-n grid point is a level-m grid point and hence lies outside the interior of that cell.

noncomputable def LeanPool.Besicovitch.Example.margin (L : ℝ) (n : ℕ) : ℝ

Half the width of the strip around a level-n grid point that A cannot straddle.

Equations

• LeanPool.Besicovitch.Example.margin L n = LeanPool.Besicovitch.Example.cellLength n / (2 * ↑n * (L + 1))

noncomputable def LeanPool.Besicovitch.Example.gridPoint (n : ℕ) (i : ℤ) : ℝ

The level-n grid point with index i.

Equations

• LeanPool.Besicovitch.Example.gridPoint n i = ↑i * LeanPool.Besicovitch.Example.cellLength n

def LeanPool.Besicovitch.Example.avoid (L : ℝ) (n : ℕ) : Set ℝ

Points at distance at least margin L n from every level-n grid point.

Equations

• LeanPool.Besicovitch.Example.avoid L n = {x : ℝ | ∀ (i : ℤ), LeanPool.Besicovitch.Example.margin L n ≤ |x - LeanPool.Besicovitch.Example.gridPoint n i|}

theorem LeanPool.Besicovitch.Example.margin_pos {L : ℝ} (hL : 0 ≤ L) {n : ℕ} (hn : 1 ≤ n) : 0 < margin L n

theorem LeanPool.Besicovitch.Example.margin_le_half {L : ℝ} (hL : 0 ≤ L) {n : ℕ} (hn : 1 ≤ n) : margin L n ≤ cellLength n / 2

theorem LeanPool.Besicovitch.Example.lipschitz_strip_lt {L : ℝ} (hL : 0 ≤ L) {n : ℕ} (hn : 1 ≤ n) : L * (2 * margin L n) < cellLength n / ↑n

The Lipschitz bound across a strip of width 2 * margin is below the jump cellLength n / n.

theorem LeanPool.Besicovitch.Example.not_both_sides {L : NNReal} {A : Set ℝ} (hg : LipschitzOnWith L besicovitchFun A) {n : ℕ} (hn : 1 ≤ n) (i : ℤ) {x y : ℝ} (hx : x ∈ A) (hy : y ∈ A) (hx' : x ∈ Set.Ioo (gridPoint n i - margin (↑L) n) (gridPoint n i)) (hy' : y ∈ Set.Ico (gridPoint n i) (gridPoint n i + margin (↑L) n)) : False

Key lemma. A set on which g is L-Lipschitz meets at most one side of a grid point.

Order-connectedness inside coarser cells

theorem LeanPool.Besicovitch.Example.gridPoint_eq_gridPoint {n m : ℕ} (hnm : n ≤ m) (i : ℤ) : ∃ (k : ℤ), gridPoint n i = gridPoint m k

A level-n grid point is a level-m grid point for every m ≥ n.

theorem LeanPool.Besicovitch.Example.gridPoint_le_or_ge (m : ℕ) (k j : ℤ) : gridPoint m k ≤ ↑j * cellLength m ∨ (↑j + 1) * cellLength m ≤ gridPoint m k

A level-m grid point is not strictly inside a level-m cell.

theorem LeanPool.Besicovitch.Example.ordConnected_avoid_inter_cell (L : ℝ) {n m : ℕ} (hnm : n ≤ m) (j : ℤ) : (avoid L n ∩ cell m j).OrdConnected

The avoided set meets every coarser cell in an order-connected set.

theorem LeanPool.Besicovitch.Example.isClosed_avoid (L : ℝ) (n : ℕ) : IsClosed (avoid L n)

theorem LeanPool.Besicovitch.Example.measurableSet_avoid (L : ℝ) (n : ℕ) : MeasurableSet (avoid L n)