Exponential functional equation

TheoremContinuous solutions of the exponential functional equation#✓fully proved

If a continuous function \(f : \mathbb{R} \to \mathbb{C}\) satisfies \(f(0) = 1\) and \(f(r + s) = f(r) f(s)\) for all real \(r\) and \(s\), then there is a complex number \(L\) such that \(f(r) = e^{rL}\) for every real \(r\).

theorem exists_eq_exp_mul_of_continuous_add_mul (f : ℝ → ℂ) (hf : Continuous f)
    (hzero : f 0 = 1) (hadd : ∀ r s : ℝ, f (r + s) = f r * f s) :
    ∃ L : ℂ, ∀ r : ℝ, f r = Complex.exp ((r : ℂ) * L)

Used by 1

Used byRamanujan's Lagrange series

TheoremContinuous nonzero solutions of \(f(x)f(y) = f(x+y)\) are exponentials#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be a continuous function that is not identically zero and satisfies \(f(x)f(y) = f(x+y)\) for all real \(x\) and \(y\). Then there is a real constant \(c\) such that \(f(x) = e^{cx}\) for every real \(x\).

public theorem_wanted exists_eq_exp_mul_of_map_add_eq_mul
    {f : ℝ → ℝ}
    (hadd : ∀ x y : ℝ, f x * f y = f (x + y))
    (hcont : Continuous f)
    (hnz : f ≠ 0) :
    ∃ c : ℝ, ∀ x : ℝ, f x = Real.exp (c * x)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_32.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.