Functions with continuous differences

DefinitionErdős Problem 907#✓fully proved

The statement that every function \(f : \mathbb{R} \to \mathbb{R}\) such that \(x \mapsto f(x + h) - f(x)\) is continuous for every \(h > 0\) can be written as \(f = g + a\) with \(g : \mathbb{R} \to \mathbb{R}\) continuous and \(a : \mathbb{R} \to \mathbb{R}\) additive, that is, \(a(x + y) = a(x) + a(y)\) for all real \(x\) and \(y\).

def conjecture : Prop :=
  ∀ f : ℝ → ℝ, (∀ h : ℝ, 0 < h → Continuous fun x => f (x + h) - f x) →
    ∃ g a : ℝ → ℝ, Continuous g ∧ (∀ x y, a (x + y) = a x + a y) ∧ f = g + a

Used by 1

Used byDe Bruijn's theorem on continuous differences (Erdős Problem 907)

TheoremDe Bruijn's theorem on continuous differences (Erdős Problem 907)#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be a function such that for every \(h > 0\) the function \(x \mapsto f(x + h) - f(x)\) is continuous. Then there are functions \(g, a : \mathbb{R} \to \mathbb{R}\) with \(g\) continuous and \(a\) additive, that is, \(a(x + y) = a(x) + a(y)\) for all real \(x\) and \(y\), such that \(f = g + a\).

public theorem_wanted conjecture_holds : conjecture

Sources

• N. G. de Bruijn, Functions whose differences belong to a given class, Nieuw Archief voor Wiskunde (2) (1951), 194–218, https://mathscinet.ams.org/mathscinet-getitem?mr=43870; External Lean proof of Erdős Problem 907, plby/lean-proofs, https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/v4.29.1/ErdosProblems/Erdos907.lean.

Uses 1

Statement usesErdős Problem 907

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.