Besicovitch's function

Besicovitch's purely unrectifiable set with lower density 1/2 is the graph of the function g = ∑ₙ fₙ, where fₙ is a square wave of period 2 * 2^(-n²) and amplitude 2^(-n²) / n. This file defines the function and proves the two estimates that everything else rests on: inside a level-n cell g varies by at most 4 * 2^(-(n+1)²) / (n+1), and across a level-n cell boundary it jumps by at least 2^(-n²) / n.

The construction follows Capdevila, Besicovitch's example in higher dimensions, arXiv:2607.05206, §2, which in turn follows Besicovitch (1938) and Dickinson (1939).

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

The length 2^(-n²) of a level-n cell.

Equations

• LeanPool.Besicovitch.Example.cellLength n = (1 / 2) ^ n ^ 2

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

The amplitude 2^(-n²) / n of the level-n square wave.

Equations

• LeanPool.Besicovitch.Example.jumpHeight n = LeanPool.Besicovitch.Example.cellLength n / ↑n

noncomputable def LeanPool.Besicovitch.Example.cellIndex (n : ℕ) (x : ℝ) : ℤ

The index of the level-n cell [i * cellLength n, (i + 1) * cellLength n) containing x.

Equations

• LeanPool.Besicovitch.Example.cellIndex n x = ⌊x / LeanPool.Besicovitch.Example.cellLength n⌋

noncomputable def LeanPool.Besicovitch.Example.squareWave (n : ℕ) (x : ℝ) : ℝ

The level-n square wave: -jumpHeight n on even cells, +jumpHeight n on odd cells.

Equations

• LeanPool.Besicovitch.Example.squareWave n x = if Even (LeanPool.Besicovitch.Example.cellIndex n x) then -LeanPool.Besicovitch.Example.jumpHeight n else LeanPool.Besicovitch.Example.jumpHeight n

noncomputable def LeanPool.Besicovitch.Example.besicovitchFun (x : ℝ) : ℝ

Besicovitch's function, the sum of the square waves of every level n ≥ 1.

Equations

• LeanPool.Besicovitch.Example.besicovitchFun x = ∑' (n : ℕ), LeanPool.Besicovitch.Example.squareWave (n + 1) x

The cell lengths

theorem LeanPool.Besicovitch.Example.cellLength_pos (n : ℕ) : 0 < cellLength n

theorem LeanPool.Besicovitch.Example.cellLength_le_one (n : ℕ) : cellLength n ≤ 1

theorem LeanPool.Besicovitch.Example.cellLength_succ_le (n : ℕ) : cellLength (n + 1) ≤ cellLength n / 2

Consecutive cell lengths shrink by a factor of at least two.

theorem LeanPool.Besicovitch.Example.cellLength_succ_le_of_pos {n : ℕ} (hn : 1 ≤ n) : cellLength (n + 1) ≤ cellLength n / 8

At level n ≥ 1 consecutive cell lengths shrink by a factor of at least eight.

theorem LeanPool.Besicovitch.Example.cellLength_add_le (n m : ℕ) : cellLength (n + m) ≤ cellLength n * (1 / 2) ^ m

theorem LeanPool.Besicovitch.Example.cellLength_antitone : Antitone cellLength

theorem LeanPool.Besicovitch.Example.cellLength_eq_mul {j n : ℕ} (h : j ≤ n) : cellLength j = cellLength n * ↑(2 ^ (n ^ 2 - j ^ 2))

A coarser cell length is a natural multiple of a finer one.

theorem LeanPool.Besicovitch.Example.jumpHeight_nonneg (n : ℕ) : 0 ≤ jumpHeight n

theorem LeanPool.Besicovitch.Example.jumpHeight_le_cellLength (n : ℕ) : jumpHeight n ≤ cellLength n

The square waves

theorem LeanPool.Besicovitch.Example.abs_squareWave (n : ℕ) (x : ℝ) : |squareWave n x| = jumpHeight n

theorem LeanPool.Besicovitch.Example.squareWave_eq_of_cellIndex_eq {n : ℕ} {x y : ℝ} (h : cellIndex n x = cellIndex n y) : squareWave n x = squareWave n y

theorem LeanPool.Besicovitch.Example.squareWave_add_squareWave_of_adjacent {n : ℕ} {x y : ℝ} (h : cellIndex n y = cellIndex n x + 1 ∨ cellIndex n x = cellIndex n y + 1) : squareWave n x + squareWave n y = 0

On adjacent cells the square waves have opposite signs.

theorem LeanPool.Besicovitch.Example.cellIndex_sub_le {n : ℕ} {x y : ℝ} (h : |x - y| < cellLength n) : |cellIndex n x - cellIndex n y| ≤ 1

Points less than a cell length apart lie in the same or in adjacent cells.

theorem LeanPool.Besicovitch.Example.cellIndex_eq_of_le {j n : ℕ} (hjn : j ≤ n) {x y : ℝ} (h : cellIndex n x = cellIndex n y) : cellIndex j x = cellIndex j y

Cells of a coarser level are unions of cells of a finer level.

Summability and the tail bound

theorem LeanPool.Besicovitch.Example.cellLength_le_geom (n : ℕ) : cellLength n ≤ (1 / 2) ^ n

theorem LeanPool.Besicovitch.Example.tendsto_cellLength : Filter.Tendsto cellLength Filter.atTop (nhds 0)

theorem LeanPool.Besicovitch.Example.cellLength_succ_le_geom (n : ℕ) : cellLength (n + 1) ≤ (1 / 2) ^ n

theorem LeanPool.Besicovitch.Example.summable_squareWave (x : ℝ) : Summable fun (n : ℕ) => squareWave (n + 1) x

theorem LeanPool.Besicovitch.Example.summable_jumpHeight (n : ℕ) : Summable fun (m : ℕ) => jumpHeight (n + 1 + m)

theorem LeanPool.Besicovitch.Example.tsum_jumpHeight_tail_le (n : ℕ) : ∑' (m : ℕ), jumpHeight (n + 1 + m) ≤ 2 * cellLength (n + 1) / (↑n + 1)

The amplitudes beyond level n sum to at most 2 * cellLength (n+1) / (n+1).

The two estimates

theorem LeanPool.Besicovitch.Example.besicovitchFun_sub_eq (n : ℕ) (x y : ℝ) : besicovitchFun x - besicovitchFun y = ∑ m ∈ Finset.range n, (squareWave (m + 1) x - squareWave (m + 1) y) + ∑' (m : ℕ), (squareWave (n + 1 + m) x - squareWave (n + 1 + m) y)

The difference of g at two points, with the first n levels separated off.

theorem LeanPool.Besicovitch.Example.abs_squareWave_sub_le (n : ℕ) (x y : ℝ) : |squareWave n x - squareWave n y| ≤ 2 * jumpHeight n

theorem LeanPool.Besicovitch.Example.abs_tail_le (n : ℕ) (x y : ℝ) : |∑' (m : ℕ), (squareWave (n + 1 + m) x - squareWave (n + 1 + m) y)| ≤ 4 * cellLength (n + 1) / (↑n + 1)

The tail beyond level n contributes at most 4 * cellLength (n+1) / (n+1).

theorem LeanPool.Besicovitch.Example.abs_besicovitchFun_sub_le {n : ℕ} {x y : ℝ} (h : cellIndex n x = cellIndex n y) : |besicovitchFun x - besicovitchFun y| ≤ 4 * cellLength (n + 1) / (↑n + 1)

(E1) Inside a level-n cell, g varies by at most 4 * cellLength (n+1) / (n+1).

theorem LeanPool.Besicovitch.Example.abs_sub_lt_of_adjacent {n : ℕ} {x y : ℝ} (h : cellIndex n y = cellIndex n x + 1 ∨ cellIndex n x = cellIndex n y + 1) : |x - y| < 2 * cellLength n

Adjacent cells at level n are less than two cell lengths apart.

theorem LeanPool.Besicovitch.Example.le_abs_besicovitchFun_sub {n : ℕ} (hn : 1 ≤ n) {x y : ℝ} (h : cellIndex n y = cellIndex n x + 1 ∨ cellIndex n x = cellIndex n y + 1) : cellLength n / ↑n ≤ |besicovitchFun x - besicovitchFun y|

(E2) Across a level-n cell boundary, g jumps by at least cellLength n / n.