Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01
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.

∥τhf−f∥p→0 in Lp(Rn) as h→0, for 1≤p<∞

Statement

Assume the Axiom of Countable Choice.

Let 1≤p<∞ and f∈Lp(Rn). Then

∥τhf−f∥p⟶0(h→0).

Facts & Assumptions

Given: The Axiom of Countable Choice, 1≤p<∞, f∈Lp(Rn), and ε>0.

[L1]

Cc(Rn) is dense in Lp(Rn) (Cc(Rn) is dense in Lp(Rn) for 1≤p<∞).

[L2]

Compactly supported continuous functions are translation-continuous in Lp (Continuous compactly supported functions are translation-continuous in Lp).

[L3]

Lebesgue measure is translation invariant, so ∥τhu∥p=∥u∥p (Translation of a function on Rn, Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).

[L4]

Minkowski's inequality is available (Minkowski's inequality for integrals, including p=∞).

Proof

technique · direct
1.1L1L2givenchoose

By [L1], choose g∈Cc(Rn) with [L1, L2, given, choose] ∥f−g∥p<ε/3. By [L2], choose δ>0 such that ∣h∣<δ implies ∥τhg−g∥p<ε/3.

2.1L3L4step 1.1algebra

For ∣h∣<δ, [L3] and [L4] give [L3, L4, step 1.1, algebra] ∥τhf−f∥p≤∥τh(f−g)∥p+∥τhg−g∥p+∥g−f∥p=2∥f−g∥p+∥τhg−g∥p<ε.

3.1step 2.1∎

Since ε>0 was arbitrary, ∥τhf−f∥p→0 as [step 2.1] h→0.

Depends on

Used by

Dependency tree · two levels

31 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