Skip to content

Erdős problem 1126

Start work

If f(x+y)=f(x)+f(y)f(x+y)=f(x)+f(y) for almost all x,y∈Rx,y\in \mathbb{R} then there exists a function gg such that g(x+y)=g(x)+g(y)g(x+y)=g(x)+g(y) for all x,y∈Rx,y\in\mathbb{R} such that f(x)=g(x)f(x)=g(x) for almost all xx.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1126.lean

Retained formal statement1 of 1

If f(x+y)=f(x)+f(y)f(x+y)=f(x)+f(y) for almost all x,y∈Rx,y\in \mathbb{R} then there exists a function gg such that g(x+y)=g(x)+g(y)g(x+y)=g(x)+g(y) for all x,y∈Rx,y\in\mathbb{R} such that f(x)=g(x)f(x)=g(x) for almost all xx.

Proved independently by de Bruijn [dB66] and Jurkat [Ju65].

FormalConjectures/ErdosProblems/1126.leanErdos1126.erdos_11264 linesExact file
True ↔  ∀ (f : ℝ → ℝ),    (∀ᵐ (p : ℝ × ℝ) ∂MeasureTheory.volume.prod MeasureTheory.volume, f (p.1 + p.2) = f p.1 + f p.2) →      ∃ h, (∀ (x y : ℝ), h (x + y) = h x + h y) ∧ ∀ᵐ (x : ℝ), f x = h x
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.