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.

Weighted weak (1,1) bound for the maximal function under A_1

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $w \in A_{1}$ (Muckenhoupt A_p and A_1 weights) and $f \in L^{1} (w)$ (so $f \in L_{l o c}^{1} (λ)$ and the maximal functions of The centered and uncentered Hardy-Littlewood maximal functions are defined). Then for every $λ > 0$ , $w ({M f > λ}) \leq 5^{n} [w]_{A_{1}} λ^{- 1} \int_{R^{n}} ∣ f ∣ w d λ,$ and the uncentred maximal function satisfies the same estimate with constant $2^{n} 5^{n} [w]_{A_{1}}$ .

Facts & Assumptions

Given: Countable Choice, $w \in A_{1}$ , $f \in L^{1} (w)$ and $λ > 0$ .

[F1]

$M^{*} w \leq [w]_{A_{1}} w$ almost everywhere, and $w d λ$ is a locally finite regular Borel (Radon) measure; the cube-average/essential-infimum form of the $A_{1}$ condition is equivalent to this pointwise form (Muckenhoupt A_p and A_1 weights, The two defining forms of A_1 agree, Sigma-compact open sets make locally finite Borel measures regular, Radon measure on an LCH space).

[F2]

$f \in L^{1} (w)$ implies $f \in L_{l o c}^{1} (λ)$ by the weighted average comparison at $p = 1$ , so every ball average of $∣ f ∣$ is finite (Weighted average comparison and the density-to-mass estimate for A_p weights), and for every $r > 0$ the function $x \mapsto A_{r} ∣ f ∣ (x)$ is continuous in the centre and radius (Ball averages vary continuously with the centre and radius).

[F3]

Fivefold Vitali covering: for a finite family of balls $B_{1}, \dots, B_{m}$ there is a pairwise disjoint subfamily $B_{i_{1}}, \dots, B_{i_{ℓ}}$ with $⋃_{j} B_{j} \subseteq ⋃_{k} 5 B_{i_{k}}$ (Vitali covering lemma for Euclidean balls with fivefold dilates).

[F4]

Inner regularity: for the Radon measure $w d λ$ and a Borel set $E$ , $w (E) = \sup {w (K) : K \subseteq E compact}$ (Radon measure on an LCH space, Sigma-compact open sets make locally finite Borel measures regular).

Proof

technique · direct

1.1F2F4given

The level set $E_{λ} : = {M f > λ}$ is open: $M f$ is the supremum of the functions $x \mapsto A_{r} ∣ f ∣ (x)$ , $r > 0$ , each continuous by [F2], so $M f$ is lower semicontinuous. By [F4] its $w$ -measure is the supremum of $w (K)$ over compact $K \subseteq E_{λ}$ .

1.2F2F3givenchoose

Let $K \subseteq E_{λ}$ be compact. Each $x \in K$ has a ball $B_{x} ∋ x$ with $A_{r_{x}} ∣ f ∣ (x) > λ$ , i.e. $\int_{B_{x}} ∣ f ∣ d λ > λ ∣ B_{x} ∣$ ; finitely many of the open balls $B_{x}$ cover $K$ , and [F3] supplies pairwise disjoint balls $B_{x_{1}}, \dots, B_{x_{ℓ}}$ from that finite cover with $K \subseteq ⋃_{j} 5 B_{x_{j}}$ and $\int_{B_{x_{j}}} ∣ f ∣ > λ ∣ B_{x_{j}} ∣$ for every $j$ .

2.1F1step 1.2givenalgebra

For each ball $B_{j}$ of step 1.2 and each $y \in B_{j}$ one has $M^{*} w (y) \geq ∣ 5 B_{j} ∣^{- 1} \int_{5 B_{j}} w = w (5 B_{j}) / (5^{n} ∣ B_{j} ∣)$ because $B_{j} \subseteq 5 B_{j}$ ; integrating over $y \in B_{j}$ against $∣ f ∣$ gives $\int_{B_{j}} ∣ f (y) ∣ M^{*} w (y) d y \geq (w (5 B_{j}) / (5^{n} ∣ B_{j} ∣)) \int_{B_{j}} ∣ f ∣$ , and since $\int_{B_{j}} ∣ f ∣ > λ ∣ B_{j} ∣$ we get $w (5 B_{j}) \leq 5^{n} λ^{- 1} \int_{B_{j}} ∣ f (y) ∣ M^{*} w (y) d y$ .

3.1F1step 2.1givenalgebra

Summing over the pairwise disjoint $B_{j}$ and using $M^{*} w \leq [w]_{A_{1}} w$ almost everywhere from [F1], $w (K) \leq \sum_{j} w (5 B_{j}) \leq 5^{n} λ^{- 1} \sum_{j} \int_{B_{j}} ∣ f ∣ M^{*} w d λ \leq 5^{n} λ^{- 1} \int_{R^{n}} ∣ f ∣ M^{*} w d λ \leq 5^{n} [w]_{A_{1}} λ^{- 1} \int_{R^{n}} ∣ f ∣ w d λ$ .

4.1step 1.1step 3.1givenalgebra∎

Taking the supremum over compact $K \subseteq E_{λ}$ in step 3.1 and using the inner regularity of step 1.1 gives $w ({M f > λ}) \leq 5^{n} [w]_{A_{1}} λ^{- 1} \int ∣ f ∣ w d λ$ . For the uncentred maximal function, every ball $B = B (y, r) ∋ x$ satisfies $B \subseteq B (x, 2 r)$ and $∣ B (x, 2 r) ∣ = 2^{n} ∣ B ∣$ , so $⟨ ∣ f ∣ ⟩_{B} \leq 2^{n} ⟨ ∣ f ∣ ⟩_{B (x, 2 r)} \leq 2^{n} M f (x)$ and hence $M^{*} f \leq 2^{n} M f$ pointwise; consequently ${M^{*} f > λ} \subseteq {M f > λ / 2^{n}}$ and the centred estimate gives $w ({M^{*} f > λ}) \leq 2^{n} 5^{n} [w]_{A_{1}} λ^{- 1} \int ∣ f ∣ w d λ$ .

Depends on

Used by

Dependency tree · two levels

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