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.
A power weight fails at both A_p endpoints
Statement refuted
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()).
Fix . The claims that the power weight is in also at the endpoints of its admissible interval are false:
- at the upper endpoint the function is a weight but not an weight;
- at the lower endpoint the function is not even locally integrable, so it is not a weight.
Hence the admissible interval is open at both ends and cannot be enlarged.
Facts & Assumptions
Given: Countable Choice; , , the power function and a radius .
For the function is a weight, and the characteristic is the supremum of over cubes (The A_p range of a power weight, Muckenhoupt A_p and A_1 weights, Weights, their associated measures, and the spaces L^p(w)).
Polar coordinates give for and for , and for every (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, Continuity and derivatives of positive-base real powers, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, Comparison tests for improper integrals).
Counterexample
At the upper endpoint: for one has , so polar coordinates give for every by the logarithmic divergence of . The second factor of the defining product is therefore on the cube containing , so the defining supremum is and is not in , while it is locally integrable and hence a weight.
At the lower endpoint: for polar coordinates give , so and no membership is defined; this is the same logarithmic divergence of the radial integral .
Steps 1.1 and 1.2 show the failure at both endpoints, so the range determined in The A_p range of a power weight is exactly the open admissible interval and cannot be enlarged.
Depends on
- The A_p range of a power weight
- Muckenhoupt A_p and A_1 weights
- Weights, their associated measures, and the spaces L^p(w)
- Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
- Comparison tests for improper integrals
- Continuity and derivatives of positive-base real powers
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
59 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)