Classification of a twisted exponential functional equation

Proved

WorkbookRestored.plus_13164

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

Fix $a>0$ , $a\ne1$ . A function $f:\mathbb R\to\mathbb R$ satisfies $f(x+y)=f(y)a^x$ for every $x,y$ if and only if $f(x)=ka^x$ for a real constant $k$ .

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_13164 (Apache-2.0).

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real

Formal statement

theorem WorkbookRestored.plus_13164 (a : ℝ) (ha : a ≠ 1) (ha' : a > 0) : ∀ f : ℝ → ℝ, (∀ x y : ℝ, f (x + y) = f y * a ^ x) ↔ ∃ k :ℝ, ∀ x : ℝ, f x = k * a ^ x   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_13164; original Prove2Me node c6195dac-9c78-4073-ae3a-4937919f5f93; Apache-2.0

View graph