Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-23 (gpt-6-sol)
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.

Continuous compactly supported functions are translation-continuous in Lp

Statement

Assume the Axiom of Countable Choice.

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

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

Facts & Assumptions

Given: The Axiom of Countable Choice (The Axiom of Countable Choice (ACω)), 1≤p<∞, and f∈Cc(Rn).

[L1]

Continuous functions on compact metric spaces are uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L3]

Translation is the convention of Translation of a function on Rn, and Cc(Rn) is defined in The spaces Cc(Rn) and Cc∞(Rn).

Proof

technique · direct
1.1L1L3givenchoose

If n=0, the only translation vector is zero, so the difference is identically zero. Assume n≥1. Let K=supp⁡(f) and choose R>0 with K⊆B(0,R). For ∣h∣≤1, the support of τhf−f lies in B(0,R+1)‾. Apply [L1] to f on the larger compact ball B(0,R+2)‾; this includes both x and x−h whenever x∈B(0,R+1)‾ and ∣h∣≤1.

2.1L1L2step 1.1choosealgebra

Let ε>0. Uniform continuity in step 1.1 gives 0<δ≤1 such that ∣f(x−h)−f(x)∣<ε for ∣h∣<δ and every x∈B(0,R+1)‾. Outside that ball both terms vanish by the support bound. Translation invariance preserves measurability; the compact ball has finite measure V by [L2]. Thus ∥τhf−f∥pp≤εpV.

3.1step 2.1∎

Given any target η>0, choose ε>0 with εpV<ηp in step 2.1. Then ∣h∣<δ implies ∥τhf−f∥p<η. Hence ∥τhf−f∥p→0 as h→0.

Depends on

Used by

Dependency tree · two levels

49 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