Hyers–Ulam stability

DefinitionDyadic approximants in Hyers' proof#✓fully proved

The dyadic approximants 2 ^ (-n) • f (2 ^ n • x) used in Hyers' proof.

noncomputable def approx (f : E → F) (x : E) (n : ℕ) : F :=
  ((2 : ℝ) ^ n)⁻¹ • f ((2 : ℝ) ^ n • x)

Used by 1

Used byHyers' theorem (Hyers–Ulam stability of the Cauchy equation)

TheoremNorm of a natural-number multiple#✓fully proved

Norm of a natural-number multiple in a real normed space.

theorem norm_nsmul_eq {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
    (n : ℕ) (x : G) : ‖n • x‖ = (n : ℝ) * ‖x‖

Used by 2

Used byUniqueness in Hyers' theorem · Continuous Hyers–Ulam stability

TheoremHyers' theorem (Hyers–Ulam stability of the Cauchy equation)#✓fully proved

If f : E → F between real normed spaces, with F complete, satisfies ‖f (x + y) - f x - f y‖ ≤ δ for all x, y, then there is an additive map A : E →+ F with ‖f x - A x‖ ≤ δ for all x. The bound δ is sharp: for f x = x + c on ℝ the defect is ‖c‖ and the best additive approximant is the identity, at distance exactly ‖c‖.

theorem exists_addMonoidHom_of_additive_defect {f : E → F} {δ : ℝ}
    (hf : ∀ x y, ‖f (x + y) - f x - f y‖ ≤ δ) :
    ∃ A : E →+ F, ∀ x, ‖f x - A x‖ ≤ δ

Uses 1 · Used by 2

Proof usesDyadic approximants in Hyers' proof

Used byHyers–Ulam stability of Jensen's functional equation · Continuous Hyers–Ulam stability

TheoremUniqueness in Hyers' theorem#✓fully proved

Two additive maps both within δ of the same f are equal: their difference is additive, hence n-homogeneous, while staying bounded by 2 * δ.

theorem eq_of_forall_norm_sub_le {f : E → F} {δ : ℝ}
    {A₁ A₂ : E →+ F} (h₁ : ∀ x, ‖f x - A₁ x‖ ≤ δ)
    (h₂ : ∀ x, ‖f x - A₂ x‖ ≤ δ) : A₁ = A₂

Uses 1

Proof usesNorm of a natural-number multiple

TheoremHyers–Ulam stability of Jensen's functional equation#✓fully proved

If the midpoint (Jensen) defect ‖f ((1/2) • (x + y)) - (1/2) • (f x + f y)‖ is ≤ δ for all x, y, then f is within 4 * δ of an additive map plus the constant f 0. The factor 4 comes from doubling the two Jensen estimates at (x + y, 0) and (x, y).

theorem exists_addMonoidHom_of_jensen_defect {f : E → F} {δ : ℝ}
    (hf : ∀ x y, ‖f ((1 / 2 : ℝ) • (x + y)) - (1 / 2 : ℝ) • (f x + f y)‖ ≤ δ) :
    ∃ A : E →+ F, ∀ x, ‖f x - A x - f 0‖ ≤ 4 * δ

Uses 1

Proof usesHyers' theorem (Hyers–Ulam stability of the Cauchy equation)

TheoremContinuous Hyers–Ulam stability#✓fully proved

If f is continuous at 0 (in particular if f itself is continuous), the additive approximant from Hyers' theorem is continuous, hence a continuous real-linear map. The proof: continuity of f at 0 bounds f on a small ball, so the approximant is bounded on that ball, and an additive map bounded on a ball is continuous at 0 by the dyadic scaling argument.

theorem exists_continuousLinearMap_of_additive_defect_of_continuousAt
    {f : E → F} {δ : ℝ} (hδ : 0 ≤ δ) (hf : ∀ x y, ‖f (x + y) - f x - f y‖ ≤ δ)
    (hcont : ContinuousAt f 0) :
    ∃ A : E →L[ℝ] F, ∀ x, ‖f x - A x‖ ≤ δ

Uses 2

Proof usesHyers' theorem (Hyers–Ulam stability of the Cauchy equation) · Norm of a natural-number multiple

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.