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.

Distribution decay from maximal cubes for A_p weights

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $1 \leq p < \infty$ , let $w \in A_{p}$ (Muckenhoupt A_p and A_1 weights), let $Q_{0}$ be an axis-parallel cube with $α_{0} : = ⟨ w ⟩_{Q_{0}} > 0$ , and fix $0 < α < 1$ . Put $α_{k} : = (2^{n} α^{- 1})^{k} α_{0}$ and let $U_{k}$ be the union of the maximal dyadic subcubes $R \subseteq Q_{0}$ (in the sense of Maximal dyadic subcubes of a cube at a height) with $⟨ w ⟩_{R} > α_{k}$ , with $U_{k} = \emptyset$ when there is none. Then $U_{k + 1} \subseteq U_{k}$ , $∣ U_{k + 1} ∣ \leq α ∣ U_{k} ∣$ and $∣ U_{k} ∣ \leq α^{k} ∣ Q_{0} ∣$ , and with $β : = 1 - \frac{(1 - α)^{p}}{K_{p}}$ one has $w (U_{k + 1}) \leq β w (U_{k})$ and $w (U_{k}) \leq β^{k} w (Q_{0})$ ; moreover $w \leq α_{k}$ almost everywhere on $Q_{0} ∖ U_{k}$ .

Here $K_{p} = [w]_{A_{p}}$ for $p > 1$ , and $K_{1} = \sup_{Q} ⟨ w ⟩_{Q} / ({ess inf}_{Q} w)$ ; by The two defining forms of A_1 agree, $1 \leq K_{1} \leq c_{n} [w]_{A_{1}}$ . Thus the constants remain controlled by the stated $A_{p}$ data, including the ball-normalized endpoint characteristic.

Facts & Assumptions

Given: Countable Choice, $1 \leq p < \infty$ , $w \in A_{p}$ , the cube $Q_{0}$ with $α_{0} = ⟨ w ⟩_{Q_{0}} > 0$ , $0 < α < 1$ , the levels $α_{k}$ and the sets $U_{k}$ .

[F1]

For every $k \geq 0$ one has $α_{k} \geq α_{0}$ because $2^{n} α^{- 1} > 1$ , so the subcube lemma applies at the height $α_{k}$ : the maximal dyadic subcubes $R \subseteq Q_{0}$ with $⟨ w ⟩_{R} > α_{k}$ are pairwise disjoint, at most countable, their union equals ${M_{d, Q_{0}} w > α_{k}}$ up to a null set, and each of them satisfies $⟨ w ⟩_{R} \leq 2^{n} α_{k}$ (Maximal dyadic subcubes of a cube at a height).

[F2]

Since $w > 0$ a.e. and $w (Q_{0}) > 0$ , all the sets $U_{k}$ and their intersections with the maximal cubes are measurable, and $w$ is finite on $Q_{0}$ (Muckenhoupt A_p and A_1 weights).

[F3]

Density-to-mass: for $1 \leq p < \infty$ , $w \in A_{p}$ , a cube $Q$ and a measurable $S \subseteq Q$ with $∣ S ∣ \leq α ∣ Q ∣$ one has $w (S) \leq β w (Q)$ with $β = 1 - (1 - α)^{p} / K_{p}$ for $p > 1$ ; for $p = 1$ use $w \geq ⟨ w ⟩_{Q} / K_{1}$ a.e. to get $w (Q ∖ S) \geq (1 - α) w (Q) / K_{1}$ . (Weighted average comparison and the density-to-mass estimate for A_p weights, The two defining forms of A_1 agree).

[F4]

For a locally integrable function and almost every point, the averages over a family of sets shrinking nicely to the point converge to the value of the function (Lebesgue differentiation theorem on $R^{n}$ , Differentiation holds along families shrinking nicely); the dyadic subcubes of $Q_{0}$ containing a point of $Q_{0}$ contain cubes of arbitrarily small side length, and such a cube $R$ satisfies $R \subseteq B (x, \sqrt{n} ℓ (R))$ , so the family shrinks nicely.

Proof

technique · direct

1.1F1F2givenalgebra

Since $α_{k + 1} > α_{k}$ , every dyadic subcube counted in step [F1] at level $α_{k + 1}$ has average exceeding $α_{k}$ as well, so it is contained in a maximal subcube at level $α_{k}$ ; hence $U_{k + 1} \subseteq U_{k}$ . For a maximal level- $α_{k}$ cube $R$ , the set $S : = R \cap U_{k + 1}$ is contained in $R$ and measurable, and $α_{k + 1} ∣ S ∣ \leq \int_{S} w d λ \leq \int_{R} w d λ \leq 2^{n} α_{k} ∣ R ∣$ by [F1]; since $α_{k + 1} = 2^{n} α^{- 1} α_{k}$ , this gives $∣ S ∣ \leq α ∣ R ∣$ . Summing over the pairwise disjoint maximal level- $α_{k}$ cubes gives $∣ U_{k + 1} ∣ \leq α ∣ U_{k} ∣$ , and iterating with $U_{0} \subseteq Q_{0}$ gives $∣ U_{k} ∣ \leq α^{k} ∣ Q_{0} ∣$ .

2.1F2F3step 1.1givenalgebra

With the same set $S = R \cap U_{k + 1}$ of step 1.1 we have $∣ S ∣ \leq α ∣ R ∣$ , so the density-to-mass estimate [F3] applies: $w (S) \leq β w (R)$ with $β = 1 - (1 - α)^{p} / K_{p}$ . Summing over the pairwise disjoint maximal level- $α_{k}$ cubes, whose union is $U_{k}$ , gives $w (U_{k + 1}) \leq β w (U_{k})$ ; iterating with $U_{0} \subseteq Q_{0}$ gives $w (U_{k}) \leq β^{k} w (Q_{0})$ .

2.2F1F4step 1.1givenalgebra

Almost everywhere bound. Fix $x \in Q_{0} ∖ U_{k}$ outside the null sets of [F4] and outside the null set on which the union of the maximal subcubes differs from ${M_{d, Q_{0}} w > α_{k}}$ . Then no dyadic subcube $R \subseteq Q_{0}$ containing $x$ has $⟨ w ⟩_{R} > α_{k}$ , for such an $R$ would lie in a maximal subcube counted at level $α_{k}$ and hence in $U_{k}$ . The dyadic subcubes of $Q_{0}$ containing $x$ shrink nicely to $x$ by [F4], so their averages of $w$ converge to $w (x)$ ; since every such average is at most $α_{k}$ , the limit satisfies $w (x) \leq α_{k}$ . Thus $w \leq α_{k}$ almost everywhere on $Q_{0} ∖ U_{k}$ .

3.1step 1.1step 2.1step 2.2∎

Steps 1.1, 2.1 and 2.2 are exactly the assertions of the Statement, namely nesting and the two chains of measure bounds together with the almost everywhere bound.

Depends on

Used by

Reverse Holder self-improvement for Aₚ weights Theorem

Dependency tree · two levels

40 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)