Erdős Problem 226

References:

• erdosproblems.com/226
• [BaSc70] Barth, K. F. and Schneider, W. J., Entire functions mapping countable dense subsets of the reals onto each other monotonically. J. London Math. Soc. (2) (1970), 620--626.
• [BaSc71] Barth, K. F. and Schneider, W. J., Entire functions mapping arbitrary countable dense sets and their complements onto each other. J. London Math. Soc. (2) (1971/72), 482--488.
• [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180.

def Erdos226.PreservesRationality (f : ℝ → ℝ) : Prop

A real function preserves rationality.

Equations

• Erdos226.PreservesRationality f = ∀ (x : ℝ), x ∈ Set.range Rat.cast ↔ f x ∈ Set.range Rat.cast

theorem Erdos226.erdos_226 : True ↔ ∃ (F : ℂ → ℂ), Differentiable ℂ F ∧ (∀ (x : ℝ), (F ↑x).im = 0) ∧ (∀ (g : ℝ →ᵃ[ℝ] ℝ), (fun (x : ℝ) => (F ↑x).re) ≠ ⇑g) ∧ PreservesRationality fun (x : ℝ) => (F ↑x).re

Is there an entire non-linear function $f$ such that, for all $x\in\mathbb{R}$, $x$ is rational if and only if $f(x)$ is?

Barth and Schneider [BaSc70] proved the stronger result for countable dense subsets of $\mathbb{R}$.