Skip to content

Erdős problem 1126

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.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1126.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1126
  • PLBY Lean proofsErdosProblems.Erdos1126

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page