Dyadic cubes in ι → ℝ

For k : ℤ and m : ι → ℤ, the dyadic cube of level k at position m is the half-open box

Q(k, m) = ∏ᵢ [mᵢ 2ᵏ, (mᵢ + 1) 2ᵏ)

(TauCeti.dyadicCube). The cubes of a fixed level partition ι → ℝ, the cube of level k containing x being Q(k, ⌊x / 2ᵏ⌋) (TauCeti.dyadicIndex), and the levels are nested: two dyadic cubes are either disjoint or one contains the other. Together with the Lebesgue differentiation theorem along dyadic cubes, which says that the averages of an integrable function over the dyadic cubes containing x converge to its value at x as the level tends to -∞, this is what the stopping-time arguments of harmonic analysis need, starting with the Calderón–Zygmund decomposition.

The ambient space carries the sup norm, for which closed balls are closed boxes. A dyadic cube is therefore a closed ball up to a null set of its boundary (TauCeti.dyadicCube_ae_eq_closedBall), and the differentiation theorem along dyadic cubes is Mathlib's differentiation theorem along closed balls with moving centres.

Main declarations

• TauCeti.dyadicIndex, TauCeti.dyadicCube, TauCeti.dyadicCube_eq_pi: dyadic cubes and the position of the cube of a given level containing a point.
• TauCeti.dyadicCube_nonempty, TauCeti.centre_mem_dyadicCube: dyadic cubes are nonempty, and contain their centres.
• TauCeti.dyadicIndex_add_one, TauCeti.dyadicCube_subset_dyadicCube, TauCeti.dyadicCube_subset_or_disjoint, TauCeti.disjoint_dyadicCube: the nesting of the dyadic levels.
• TauCeti.closure_dyadicCube: the closure of a dyadic cube is a closed sup-norm ball.
• TauCeti.ball_subset_dyadicCube: a dyadic cube contains the open sup-norm ball of half its side length around its centre.
• TauCeti.dist_lt_of_mem_dyadicCube: two points of a cube of level k are at sup distance less than 2ᵏ.
• TauCeti.volume_dyadicCube, TauCeti.volume_dyadicCube_add_one: a cube of level k has volume (2ᵏ)ⁿ, so its parent is 2ⁿ times larger.
• TauCeti.exists_forall_lt_of_mul_volume_dyadicCube_lt: in positive dimension, the dyadic cubes Q with δ |Q| < a, for δ ≠ 0 and a finite, have bounded level.
• TauCeti.exists_subset_pairwiseDisjoint_forall_dyadicCube_subset: in a family of dyadic cubes of bounded level, the maximal cubes are pairwise disjoint and contain every cube of the family.
• TauCeti.ae_tendsto_setLAverage_dyadicCube: the Lebesgue differentiation theorem along dyadic cubes.

References

• E. Stein, Harmonic Analysis, Chapter I, §3.
• L. Grafakos, Classical Fourier Analysis, Section 2.1.

noncomputable def TauCeti.dyadicIndex {ι : Type u_1} (k : ℤ) (x : ι → ℝ) : ι → ℤ

The position of the dyadic cube of level k containing x: its i-th coordinate is ⌊xᵢ / 2ᵏ⌋.

@[simp]

theorem TauCeti.dyadicIndex_apply {ι : Type u_1} (k : ℤ) (x : ι → ℝ) (i : ι) : dyadicIndex k x i = ⌊x i / 2 ^ k⌋

def TauCeti.dyadicCube {ι : Type u_1} (k : ℤ) (m : ι → ℤ) : Set (ι → ℝ)

The dyadic cube of level k at position m: the points whose dyadic index of level k is m, that is, the half-open box ∏ᵢ [mᵢ 2ᵏ, (mᵢ + 1) 2ᵏ) (TauCeti.dyadicCube_eq_pi).

@[simp]

theorem TauCeti.mem_dyadicCube {ι : Type u_1} {k : ℤ} {m : ι → ℤ} {x : ι → ℝ} : x ∈ dyadicCube k m ↔ dyadicIndex k x = m

theorem TauCeti.mem_dyadicCube_dyadicIndex {ι : Type u_1} (k : ℤ) (x : ι → ℝ) : x ∈ dyadicCube k (dyadicIndex k x)

Every point lies in the dyadic cube of each level indexed by its own dyadic index.

theorem TauCeti.dyadicCube_eq_pi {ι : Type u_1} (k : ℤ) (m : ι → ℤ) : dyadicCube k m = Set.univ.pi fun (i : ι) => Set.Ico (↑(m i) * 2 ^ k) ((↑(m i) + 1) * 2 ^ k)

A dyadic cube is the half-open box ∏ᵢ [mᵢ 2ᵏ, (mᵢ + 1) 2ᵏ).

theorem TauCeti.measurableSet_dyadicCube {ι : Type u_1} [Countable ι] (k : ℤ) (m : ι → ℤ) : MeasurableSet (dyadicCube k m)

Dyadic cubes are measurable.

theorem TauCeti.dyadicIndex_add_one {ι : Type u_1} (k : ℤ) (x : ι → ℝ) : dyadicIndex (k + 1) x = fun (i : ι) => dyadicIndex k x i / 2

The dyadic index of level k + 1 is obtained from the one of level k by halving and rounding down: the parent of a dyadic cube.

theorem TauCeti.dyadicIndex_eq_of_le {ι : Type u_1} {j k : ℤ} {x y : ι → ℝ} (hjk : j ≤ k) (h : dyadicIndex j x = dyadicIndex j y) : dyadicIndex k x = dyadicIndex k y

Points in the same dyadic cube of level j are in the same dyadic cube of every level k ≥ j.

theorem TauCeti.dyadicCube_subset_dyadicCube {ι : Type u_1} {j k : ℤ} {m : ι → ℤ} {x : ι → ℝ} (hjk : j ≤ k) (hx : x ∈ dyadicCube j m) : dyadicCube j m ⊆ dyadicCube k (dyadicIndex k x)

A dyadic cube of level j is contained in the dyadic cube of each level k ≥ j that meets it.

theorem TauCeti.dyadicCube_nonempty {ι : Type u_1} (k : ℤ) (m : ι → ℤ) : (dyadicCube k m).Nonempty

Dyadic cubes are nonempty: the cube Q(k, m) contains its corner m 2ᵏ.

theorem TauCeti.centre_mem_dyadicCube {ι : Type u_1} (k : ℤ) (m : ι → ℤ) : (fun (i : ι) => (↑(m i) + 2⁻¹) * 2 ^ k) ∈ dyadicCube k m

The centre (m + 1/2) 2ᵏ of a dyadic cube lies in it.

@[simp]

theorem TauCeti.disjoint_dyadicCube {ι : Type u_1} {k : ℤ} {m m' : ι → ℤ} : Disjoint (dyadicCube k m) (dyadicCube k m') ↔ m ≠ m'

Two dyadic cubes of the same level are disjoint if and only if they are distinct.

theorem TauCeti.dyadicCube_subset_or_disjoint {ι : Type u_1} {j k : ℤ} (hjk : j ≤ k) (m m' : ι → ℤ) : dyadicCube j m ⊆ dyadicCube k m' ∨ Disjoint (dyadicCube j m) (dyadicCube k m')

Of two dyadic cubes, either the one of lower level is contained in the other or they are disjoint.

theorem TauCeti.exists_subset_pairwiseDisjoint_forall_dyadicCube_subset {ι : Type u_1} {T : Set (ℤ × (ι → ℤ))} {N : ℤ} (hT : ∀ p ∈ T, p.1 ≤ N) : ∃ T' ⊆ T, (T'.PairwiseDisjoint fun (p : ℤ × (ι → ℤ)) => dyadicCube p.1 p.2) ∧ ∀ p ∈ T, ∃ p' ∈ T', dyadicCube p.1 p.2 ⊆ dyadicCube p'.1 p'.2

Maximal dyadic cubes. In a family T of dyadic cubes, recorded by level and position, whose levels are bounded above, the cubes maximal for inclusion form a pairwise disjoint subfamily T', and every cube of T lies in a cube of T'.

theorem TauCeti.dyadicCube_subset_closedBall {ι : Type u_1} [Fintype ι] (k : ℤ) (m : ι → ℤ) : dyadicCube k m ⊆ Metric.closedBall (fun (i : ι) => (↑(m i) + 2⁻¹) * 2 ^ k) (2 ^ k / 2)

A dyadic cube is contained in the closed sup-norm ball around its centre whose radius is half its side length.

theorem TauCeti.ball_subset_dyadicCube {ι : Type u_1} [Fintype ι] (k : ℤ) (m : ι → ℤ) : Metric.ball (fun (i : ι) => (↑(m i) + 2⁻¹) * 2 ^ k) (2 ^ k / 2) ⊆ dyadicCube k m

A dyadic cube contains the open sup-norm ball around its centre whose radius is half its side length.

theorem TauCeti.dyadicCube_ae_eq_closedBall {ι : Type u_1} [Fintype ι] (k : ℤ) (m : ι → ℤ) : dyadicCube k m =ᵐ[MeasureTheory.volume] Metric.closedBall (fun (i : ι) => (↑(m i) + 2⁻¹) * 2 ^ k) (2 ^ k / 2)

Up to a null set, a dyadic cube is the closed sup-norm ball around its centre whose radius is half its side length.

theorem TauCeti.closure_dyadicCube {ι : Type u_1} [Fintype ι] (k : ℤ) (m : ι → ℤ) : closure (dyadicCube k m) = Metric.closedBall (fun (i : ι) => (↑(m i) + 2⁻¹) * 2 ^ k) (2 ^ k / 2)

The closure of a dyadic cube is the closed sup-norm ball around its centre whose radius is half its side length.

theorem TauCeti.dist_lt_of_mem_dyadicCube {ι : Type u_1} {k : ℤ} {m : ι → ℤ} {x y : ι → ℝ} [Fintype ι] (hx : x ∈ dyadicCube k m) (hy : y ∈ dyadicCube k m) : dist x y < 2 ^ k

Two points of a dyadic cube of level k are at sup distance less than its side length 2ᵏ.

theorem TauCeti.volume_dyadicCube {ι : Type u_1} [Fintype ι] (k : ℤ) (m : ι → ℤ) : MeasureTheory.volume (dyadicCube k m) = ENNReal.ofReal ((2 ^ k) ^ Fintype.card ι)

A dyadic cube of level k has volume (2ᵏ)ⁿ.

theorem TauCeti.volume_dyadicCube_pos {ι : Type u_1} [Fintype ι] (k : ℤ) (m : ι → ℤ) : 0 < MeasureTheory.volume (dyadicCube k m)

Dyadic cubes have positive volume.

theorem TauCeti.volume_dyadicCube_ne_top {ι : Type u_1} [Fintype ι] (k : ℤ) (m : ι → ℤ) : MeasureTheory.volume (dyadicCube k m) ≠ ⊤

Dyadic cubes have finite volume.

theorem TauCeti.volume_dyadicCube_add_one {ι : Type u_1} [Fintype ι] (k : ℤ) (m m' : ι → ℤ) : MeasureTheory.volume (dyadicCube (k + 1) m') = 2 ^ Fintype.card ι * MeasureTheory.volume (dyadicCube k m)

Passing to the next dyadic level multiplies the volume of a cube by 2ⁿ.

theorem TauCeti.tendsto_volume_dyadicCube_atTop {ι : Type u_1} [Fintype ι] [Nonempty ι] (m : ℤ → ι → ℤ) : Filter.Tendsto (fun (k : ℤ) => MeasureTheory.volume (dyadicCube k (m k))) Filter.atTop (nhds ⊤)

In positive dimension, dyadic cubes become arbitrarily large as the level tends to +∞.

theorem TauCeti.exists_forall_lt_of_mul_volume_dyadicCube_lt {ι : Type u_1} [Fintype ι] [Nonempty ι] {a δ : ENNReal} (hδ : δ ≠ 0) (ha : a ≠ ⊤) : ∃ (N : ℤ), ∀ (k : ℤ) (m : ι → ℤ), δ * MeasureTheory.volume (dyadicCube k m) < a → k < N

In positive dimension, the dyadic cubes Q with δ |Q| < a, for δ ≠ 0 and a finite, have bounded level.

theorem TauCeti.ae_tendsto_setLAverage_dyadicCube {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} (hg : AEMeasurable g MeasureTheory.volume) (hg' : ∫⁻ (x : ι → ℝ), g x ≠ ⊤) : ∀ᵐ (x : ι → ℝ), Filter.Tendsto (fun (k : ℤ) => ⨍⁻ (y : ι → ℝ) in dyadicCube k (dyadicIndex k x), g y) Filter.atBot (nhds (g x))

Lebesgue's differentiation theorem along dyadic cubes: for an integrable g, at almost every x the averages of g over the dyadic cubes containing x converge to g x as the level tends to -∞.