LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Maximal dyadic subcubes of a cube at a height

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $n \geq 1$ , let $Q_{0}$ be an axis-parallel cube with side length $ℓ > 0$ and centre $x_{0}$ , and let $Φ (y) : = x_{0} + ℓ (y - \frac{1}{2} (1, \dots, 1))$ be the unique translation-dilation carrying $(0, 1]^{n}$ onto the half-open box $R_{0}$ with the same centre and side length as $Q_{0}$ ; $R_{0}$ and $Q_{0}$ differ by a Lebesgue-null set. The dyadic subcubes of $Q_{0}$ are the images $Φ (D)$ of the dyadic cubes $D \subseteq (0, 1]^{n}$ of the all-generations grid (Dyadic cubes of all generations in R^n).

When forming averages over half-open descendants, extend functions on $Q_{0}$ by zero on $R_{0} ∖ Q_{0}$ ; all such boundary changes are null. Here a dyadic subcube of $Q_{0}$ means a descendant of $R_{0}$ , rather than literal inclusion in the open cube.

Let $f \geq 0$ satisfy $f \in L^{1} (Q_{0})$ , and let $α \geq ⟨ f ⟩_{Q_{0}}$ with $α > 0$ . Then the dyadic subcubes $R \subseteq Q_{0}$ with $⟨ f ⟩_{R} > α$ that are maximal under inclusion are pairwise disjoint and at most countable, their union equals ${M_{d, Q_{0}} f > α} = {x \in R_{0} : \sup_{R ∋ x} ⟨ f ⟩_{R} > α}$ up to a Lebesgue-null set, where the supremum is over the dyadic subcubes of $Q_{0}$ containing $x$ and $R_{0}$ is the half-open box above; since $Q_{0} ∖ R_{0}$ is Lebesgue null, this is the same as the corresponding set with $Q_{0}$ in place of $R_{0}$ , up to a null set. Each such maximal $R$ satisfies $⟨ f ⟩_{R} \leq 2^{n} α$ ; and $\sum_{R} ∣ R ∣ \leq α^{- 1} \int_{Q_{0}} f d λ$ .

Facts & Assumptions

Given: Countable Choice, $n \geq 1$ , the cube $Q_{0}$ and its dyadic subcubes via $Φ$ , a nonnegative $f \in L^{1} (Q_{0})$ , and $α \geq ⟨ f ⟩_{Q_{0}}$ and $α > 0$ .

[F1]

For dyadic cubes $D, D^{'}$ of generations $k \leq k^{'}$ with $D \cap D^{'} \neq \emptyset$ one has $D^{'} \subseteq D$ ; every dyadic cube of generation $k$ has a unique parent of generation $k - 1$ containing it, of volume $2^{n}$ times its own; and two dyadic cubes are disjoint or one contains the other (All-generation dyadic cubes: partition, volume and nesting, Dyadic cubes of all generations in R^n).

[F2]

A generation- $k$ dyadic cube $D \subseteq (0, 1]^{n}$ has centre $c_{D}$ and side $2^{- k}$ . Its image $Φ (D)$ is the half-open box with centre $Φ (c_{D})$ and side $2^{- k} ℓ$ , hence $∣ Φ (D) ∣ = ℓ^{n} ∣ D ∣$ by A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included. The map $Φ$ is bijective, so it preserves inclusion and disjointness; the images of the generation- $k$ descendants partition $R_{0}$ for each $k \geq 0$ .

[F3]

The set of all dyadic cubes is at most countable: the parameters $(k, m)$ inject into $Q^{n + 1}$ , which is at most countable ( $Q^{n}$ is a countable dense subset of $R^{n}$ , and rational open boxes form a countable basis, Every subset of an at most countable set is at most countable).

[F4]

For nonnegative measurable functions and measurable sets, integrals are monotone in the set (The indefinite integral of a nonnegative measurable function is a measure, Measures are monotone) and finite on $Q_{0}$ by the hypothesis $f \in L^{1} (Q_{0})$ .

Proof

technique · direct

1.1F1F2F4givenalgebra

Call a dyadic subcube $R$ of $Q_{0}$ bad when $⟨ f ⟩_{R} > α$ . Every bad $R$ satisfies $α ∣ R ∣ < \int_{R} f d λ \leq \int_{Q_{0}} f d λ < \infty$ by [F4], so $∣ R ∣ < α^{- 1} \int_{Q_{0}} f$ ; since the ancestors of a subcube have volumes $ℓ^{n} 2^{- k n}$ growing by the factor $2^{n}$ from generation to generation, only finitely many ancestors of a given bad cube can be bad. The top cube $Q_{0}$ is not bad because $α \geq ⟨ f ⟩_{Q_{0}}$ , and its subcube family is identified with the all-generations dyadic cubes inside $(0, 1]^{n}$ , so the ancestors of any bad subcube that lie inside $(0, 1]^{n}$ form a finite chain starting at the bad cube; a maximal bad subcube containing it is therefore obtained by taking the last bad member of that chain.

2.1F1F2F3step 1.1

The maximal bad subcubes are pairwise disjoint: if two of them meet, [F1] and injectivity of $Φ$ make one contain the other, and maximality forces equality. They are at most countable because they are images under the fixed map $Φ$ of a subfamily of the at most countable dyadic grid [F3].

3.1F1step 1.1step 2.1

The union of the maximal bad subcubes is exactly ${M_{d, Q_{0}} f > α}$ : if $x$ lies in a maximal bad $R$ , then $M_{d, Q_{0}} f (x) \geq ⟨ f ⟩_{R} > α$ ; conversely, if $M_{d, Q_{0}} f (x) > α$ then some dyadic subcube $R ∋ x$ is bad, and step 1.1 contains it in a maximal bad subcube $R^{'}$ , which also contains $x$ since $R \cap R^{'} \neq \emptyset$ and dyadic subcubes are nested [F1]. This is an equality of sets, hence a fortiori equality up to a null set.

4.1F1F2F4step 3.1algebra∎

For a maximal bad subcube $R$ : if $R \neq Q_{0}$ its parent $P = Φ (D^{'})$ exists with $Φ^{- 1} (R) ⊊ D^{'} \subseteq (0, 1]^{n}$ and $∣ P ∣ = 2^{n} ∣ R ∣$ by [F1] and [F2]; maximality makes $P$ good, so $\int_{R} f \leq \int_{P} f \leq α ∣ P ∣ = 2^{n} α ∣ R ∣$ by [F4], and hence $⟨ f ⟩_{R} \leq 2^{n} α$ . If $R = Q_{0}$ then $⟨ f ⟩_{Q_{0}} \leq α \leq 2^{n} α$ as well. Finally, pairwise disjointness gives $\sum_{R} ∣ R ∣ = ∣ ⋃_{R} R ∣ \leq ∣ {M_{d, Q_{0}} f > α} ∣$ , and on each bad $R$ one has $α ∣ R ∣ < \int_{R} f$ , so summing over the at most countable disjoint family and using $f \geq 0$ yields $\sum_{R} ∣ R ∣ \leq α^{- 1} \sum_{R} \int_{R} f \leq α^{- 1} \int_{Q_{0}} f$ .

Depends on

Used by

Dependency tree · two levels

94 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Loukas Grafakos, Classical Fourier Analysis, 3rd ed. (Springer GTM 249, 2014) (standard reference, not scraped)
Juha Kinnunen, Harmonic Analysis (Aalto University lecture notes) (standard reference, not scraped)