Cauchy's Functional Equation

This file contains the classical results about the Cauchy's functional equation f (x + y) = f x + f y for functions f : ℝ → ℝ. In this file, we prove that the solutions to this equation are linear up to the case when f is a Lebesgue measurable functions, while also deducing intermediate well-known variants.

theorem isLinearMap_iff_apply_eq_apply_one_mul {M : Type} [CommSemiring M] (f : M →+ M) : IsLinearMap M ⇑f ↔ ∀ (x : M), f x = f 1 * x

theorem is_linear_rat (f : ℝ →+ ℝ) (q : ℚ) : f ↑q = f 1 * ↑q

theorem additive_isBounded_of_isBounded_on_interval {s : Set ℝ} {a : ℝ} (f : ℝ →+ ℝ) (hs : s ∈ nhds a) (h : Bornology.IsBounded (⇑f '' s)) : ∃ V ∈ nhds 0, Bornology.IsBounded (⇑f '' V)

theorem AddMonoidHom.continuousAt_iff_continuousAt_zero {a : ℝ} (f : ℝ →+ ℝ) : ContinuousAt (⇑f) a ↔ ContinuousAt (⇑f) 0

theorem Continuous.isLinearMap_real (f : ℝ →+ ℝ) (h : Continuous ⇑f) : IsLinearMap ℝ ⇑f

theorem isLinearMap_real_of_isBounded_nhds {s : Set ℝ} {a : ℝ} (f : ℝ →+ ℝ) (hs : s ∈ nhds a) (hf : Bornology.IsBounded (⇑f '' s)) : IsLinearMap ℝ ⇑f

theorem MonotoneOn.isLinearMap_real {s : Set ℝ} {a : ℝ} (f : ℝ →+ ℝ) (hs : s ∈ nhds a) (hf : MonotoneOn (⇑f) s) : IsLinearMap ℝ ⇑f