Alphabeta Math
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.

BMO classes are determined by their pairings with H1 atoms

Statement

Let b∈BMO(Rn) and suppose ∫ab=0 for every H1 atom a. Then b is constant almost everywhere. Equivalently, the evaluation map on atoms is injective on BMO/C.

Facts & Assumptions

Given: b∈BMO(Rn) with ∫ab=0 for every (1,∞,0)-atom a, and a cube Q.

[F1]

A bounded mean-zero function g vanishing off Q is a scalar multiple of an atom: for ∥g∥∞>0, divide by ∣Q∣∥g∥∞ and choose the representative vanishing off the closed cube Q; a zero L∞ class has zero pairing (Hp atoms with a prescribed moment order).

[F2]

b is locally integrable, bQ=∣Q∣−1∫Qb, and the BMO seminorm vanishes exactly on the almost-everywhere constants (BMO seminorm and the quotient by constants).

Proof

technique · direct
1.1F1F2givenconstruct

Define h(x)=b(x)−bQ‾/∣b(x)−bQ∣ on Q where b(x)≠bQ, and h(x)=0 elsewhere. Then ∣h∣≤1, and g:=(h−hQ)1Q is bounded, supported in Q and mean zero. By [F1] and the hypothesis, ∫gb=0, including the zero-class case. All products are integrable because b∈L1(Q) and g is bounded.

2.1step 1.1F1F2algebra∎

Using ∫Q(b−bQ)=0 and the definition of h, we obtain 0=∫Qgb=∫Qg(b−bQ)=∫Qh(b−bQ)=∫Q∣b−bQ∣. Since Q was arbitrary, the BMO seminorm is zero, so b is constant almost everywhere by [F2]. Applying this to b−b′ proves injectivity on classes with equal atom pairings; conversely constants pair to zero by atom cancellation. No choice principle or local L2 estimate is used.

Depends on

Used by

Dependency tree · two levels

14 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