LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Finite atomic sums are dense in H1

Statement

Assume Countable Choice. The finite linear combinations of $H^{1}$ atoms are dense in $H^{1} (R^{n})$ : for every $f \in H^{1} (R^{n})$ and every $ε > 0$ there are finitely many atoms $a_{1}, \dots, a_{N}$ and coefficients $λ_{1}, \dots, λ_{N}$ with $∥ f - \sum_{1 \leq j \leq N} λ_{j} a_{j} ∥_{H^{1}} < ε$ .

Facts & Assumptions

Given: Countable Choice, $f \in H^{1} (R^{n})$ and $ε > 0$ , with the $(1, \infty, 0)$ -atoms of $H^{p}$ atoms with a prescribed moment order and the $H^{1}$ functional of The real Hardy space $H^{p}$ defined by a radial maximal function.

[F1]

The atomic characterisation of $H^{1}$ gives a sequence $(λ_{j}) \in ℓ^{1}$ and $(1, \infty, 0)$ -atoms $a_{j}$ , reindexed by $j \geq 1$ , with $f = \sum_{j} λ_{j} a_{j}$ converging in $S^{'}$ , with $\sum_{j} ∣ λ_{j} ∣ \leq C ∥ f ∥_{H^{1}}$ for a suitable constant; moreover every such series converges also in the $H^{1}$ quasi-norm, which for $p = 1$ is the norm $∥ \cdot ∥_{H^{1}}$ (Atomic characterisation of real $H^{p}$ for $0 < p \leq 1$ , The real Hardy space $H^{p}$ defined by a radial maximal function).

[F2]

For an $ℓ^{1}$ sum of atoms indexed by $j \geq 1$ , the partial sums converge to the sum in the $H^{1}$ quasi-norm and the tail bound $∥ g - \sum_{1 \leq j \leq N} λ_{j} a_{j} ∥_{H^{1}} \leq C (\sum_{j > N} ∣ λ_{j} ∣)$ holds ( $ℓ^{p}$ sums of atoms converge in $S^{'}$ and in $H^{p}$ with $p = 1$ ).

Proof

technique · direct

1.1F1

By [F1] fix $ℓ^{1}$ -coefficients $(λ_{j})$ and atoms $(a_{j})$ , indexing both sequences by $j \geq 1$ , with $f = \sum_{j} λ_{j} a_{j}$ converging in $S^{'}$ and with $\sum_{j} ∣ λ_{j} ∣ \leq C ∥ f ∥_{H^{1}}$ ; by the same item the partial sums $S_{N} : = \sum_{1 \leq j \leq N} λ_{j} a_{j}$ converge to $f$ in the $H^{1}$ norm.

2.1step 1.1F2

Since $∥ f - S_{N} ∥_{H^{1}} \to 0$ as $N \to \infty$ by step 1.1 and $ε > 0$ , there is $N \geq 1$ with $∥ f - S_{N} ∥_{H^{1}} < ε$ ; the sum $S_{N}$ is a finite linear combination of the atoms $a_{1}, \dots, a_{N}$ with coefficients $λ_{1}, \dots, λ_{N}$ , and [F2] gives the same conclusion with the explicit tail bound.

3.1step 2.1∎

Thus for every $f \in H^{1} (R^{n})$ and every $ε > 0$ there is a finite atomic sum within $ε$ in the $H^{1}$ norm, which is density. Countable Choice is inherited from the atomic characterisation.

Depends on

Used by

BMO classes define bounded functionals on H1 Theorem
Real H1-BMO duality Theorem

Dependency tree · two levels

29 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

Mark Williams, Notes on Harmonic Analysis (January 11, 2022) (standard reference, not scraped)