The Lipschitz pieces of Besicovitch's graph are null

A point of [0, 1] that avoids every grid of level N, N + 1, … on both sides lies in a set of measure zero. Indeed, inside a level-M cell the survivors of the levels up to M form an interval, and the level-M + 1 grid punches holes of total relative size 1 / ((M+1) (L+1)) into every interval, up to an error of a few holes per cell. The errors are summable while ∑ 1 / ((M + 1) (L + 1)) diverges, so the recursion of LeanPool.Besicovitch.Example.Recursion forces the surviving measure to zero.

Combined with ae_eventually_mem_avoid, every subset of [0, 1] on which g is Lipschitz is Lebesgue-null.

theorem LeanPool.Besicovitch.Example.volume_ne_top_of_subset_Icc {S : Set ℝ} (hS : S ⊆ Set.Icc 0 1) : MeasureTheory.volume S ≠ ⊤

A subset of [0, 1] has finite Lebesgue measure.

Holes around grid points

theorem LeanPool.Besicovitch.Example.two_mul_margin_div_cellLength {L : ℝ} (hL : 0 ≤ L) {m : ℕ} (hm : 1 ≤ m) : 2 * margin L m / cellLength m = 1 / (↑m * (L + 1))

The relative width 2 * margin L m / cellLength m of a hole is 1 / (m (L + 1)).

def LeanPool.Besicovitch.Example.hole (L : ℝ) (m : ℕ) (k : ℤ) : Set ℝ

The open hole of radius margin L m around the level-m grid point with index k.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Besicovitch.Example.measurableSet_hole (L : ℝ) (m : ℕ) (k : ℤ) : MeasurableSet (hole L m k)

A hole is measurable.

theorem LeanPool.Besicovitch.Example.volume_hole (L : ℝ) (m : ℕ) (k : ℤ) : MeasureTheory.volume (hole L m k) = ENNReal.ofReal (2 * margin L m)

A hole has measure 2 * margin L m.

theorem LeanPool.Besicovitch.Example.disjoint_hole_avoid (L : ℝ) (m : ℕ) (k : ℤ) : Disjoint (hole L m k) (avoid L m)

A hole misses the avoided set.

theorem LeanPool.Besicovitch.Example.pairwiseDisjoint_hole {L : ℝ} (hL : 0 ≤ L) {m : ℕ} (hm : 1 ≤ m) (I : Finset ℤ) : (↑I).PairwiseDisjoint (hole L m)

Distinct holes of the same level are disjoint.

The estimate on one interval

theorem LeanPool.Besicovitch.Example.volume_inter_avoid_le {L : ℝ} (hL : 0 ≤ L) {m : ℕ} (hm : 1 ≤ m) {S : Set ℝ} (hS : S.OrdConnected) (hS1 : S ⊆ Set.Icc 0 1) : (MeasureTheory.volume (S ∩ avoid L m)).toReal ≤ (1 - 1 / (↑m * (L + 1))) * (MeasureTheory.volume S).toReal + 4 * margin L m

Per-interval estimate. An order-connected subset S of [0, 1] loses the fraction 1 / (m (L + 1)) of its measure, up to an error of 4 * margin L m, when the level-m grid is avoided: the holes around the level-m grid points inside S are disjoint, are removed, and number at least volume S / cellLength m - 2.

Summing over the cells of the previous level

theorem LeanPool.Besicovitch.Example.Icc_subset_biUnion_cell (M : ℕ) : Set.Icc 0 1 ⊆ ⋃ i ∈ Finset.Icc 0 (cellIndex M 1), cell M i

[0, 1] is covered by the level-M cells with indices 0, …, cellIndex M 1.

theorem LeanPool.Besicovitch.Example.card_Icc_cellIndex_le (M : ℕ) : ↑(Finset.Icc 0 (cellIndex M 1)).card ≤ 1 / cellLength M + 1

There are at most 1 / cellLength M + 1 level-M cells meeting [0, 1].

theorem LeanPool.Besicovitch.Example.cellLength_succ_eq (M : ℕ) : cellLength (M + 1) = cellLength M * (1 / 2) ^ (2 * M + 1)

Consecutive cell lengths: cellLength (M + 1) = cellLength M * (1/2) ^ (2 M + 1).

theorem LeanPool.Besicovitch.Example.error_le {L : ℝ} (hL : 0 ≤ L) (M : ℕ) : (1 / cellLength M + 1) * margin L (M + 1) ≤ (1 / 2) ^ (M + 1)

The total error from the 1 / cellLength M + 1 cells of level M is geometrically small.

theorem LeanPool.Besicovitch.Example.volume_inter_avoid_succ_le {L : ℝ} (hL : 0 ≤ L) (M : ℕ) {S : Set ℝ} (hS1 : S ⊆ Set.Icc 0 1) (hS : ∀ (i : ℤ), (S ∩ cell M i).OrdConnected) : (MeasureTheory.volume (S ∩ avoid L (M + 1))).toReal ≤ (1 - 1 / ((↑M + 1) * (L + 1))) * (MeasureTheory.volume S).toReal + 4 * (1 / 2) ^ (M + 1)

One level of the recursion. If S ⊆ [0, 1] meets every level-M cell in an order-connected set, then avoiding the level-M + 1 grid removes the fraction 1 / ((M + 1) (L + 1)) of its measure, up to an error 4 * (1/2) ^ (M + 1).

The survivors of the first n levels

def LeanPool.Besicovitch.Example.survivors (L : ℝ) (N : ℕ) : ℕ → Set ℝ

The points of [0, 1] avoiding the grids of levels N + 1, …, N + n.

Equations

• LeanPool.Besicovitch.Example.survivors L N 0 = Set.Icc 0 1
• LeanPool.Besicovitch.Example.survivors L N n.succ = LeanPool.Besicovitch.Example.survivors L N n ∩ LeanPool.Besicovitch.Example.avoid L (N + n + 1)

theorem LeanPool.Besicovitch.Example.survivors_subset_Icc (L : ℝ) (N n : ℕ) : survivors L N n ⊆ Set.Icc 0 1

The survivors lie in [0, 1].

theorem LeanPool.Besicovitch.Example.volume_survivors_ne_top (L : ℝ) (N n : ℕ) : MeasureTheory.volume (survivors L N n) ≠ ⊤

The survivors have finite measure.

theorem LeanPool.Besicovitch.Example.ordConnected_survivors_inter_cell (L : ℝ) (N n M : ℕ) : N + n ≤ M → ∀ (i : ℤ), (survivors L N n ∩ cell M i).OrdConnected

Inside a cell of level M ≥ N + n the survivors of n levels form an order-connected set.

theorem LeanPool.Besicovitch.Example.volume_survivors_succ_le {L : ℝ} (hL : 0 ≤ L) (N n : ℕ) : (MeasureTheory.volume (survivors L N (n + 1))).toReal ≤ (1 - 1 / ((↑N + ↑n + 1) * (L + 1))) * (MeasureTheory.volume (survivors L N n)).toReal + 4 * (1 / 2) ^ (n + 1)

The recursive estimate for the measure of the survivors.

theorem LeanPool.Besicovitch.Example.tendsto_sum_one_div_atTop {L : ℝ} (hL : 0 ≤ L) {N : ℕ} (hN : 1 ≤ N) : Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, 1 / ((↑N + ↑k) * (L + 1))) Filter.atTop Filter.atTop

The sums ∑_{k < n} 1 / ((N + k) (L + 1)) diverge, by comparison with the harmonic series.

theorem LeanPool.Besicovitch.Example.tendsto_volume_survivors {L : ℝ} (hL : 0 ≤ L) {N : ℕ} (hN : 1 ≤ N) : Filter.Tendsto (fun (n : ℕ) => (MeasureTheory.volume (survivors L N n)).toReal) Filter.atTop (nhds 0)

The measure of the survivors tends to zero.

The main theorems

theorem LeanPool.Besicovitch.Example.volume_Icc_inter_iInter_avoid_eq_zero (L : ℝ) (hL : 0 ≤ L) (N : ℕ) : MeasureTheory.volume (Set.Icc 0 1 ∩ ⋂ (n : ℕ), avoid L (N + n)) = 0

The two-sided avoiders are null. The points of [0, 1] at distance at least margin L n from every level-n grid point, for all n ≥ N, form a null set.

theorem LeanPool.Besicovitch.Example.volume_eq_zero_of_lipschitzOnWith {L : NNReal} {A : Set ℝ} (hA : A ⊆ Set.Icc 0 1) (hg : LipschitzOnWith L besicovitchFun A) : MeasureTheory.volume A = 0

Lipschitz pieces are null. A subset of [0, 1] on which Besicovitch's function is Lipschitz has Lebesgue measure zero.