Erdős problem 1126 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1126.lean

Retained formal statement1 of 1

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

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

FormalConjectures/ErdosProblems/1126.leanErdos1126.erdos_11264 linesExact file

1True ↔2  ∀ (f : ℝ → ℝ),3    (∀ᵐ (p : ℝ × ℝ) ∂MeasureTheory.volume.prod MeasureTheory.volume, f (p.1 + p.2) = f p.1 + f p.2) →4      ∃ 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.

Sources

Search problems.science