The Gelfand radius in a normed ring

This file defines the Gelfand radius in a normed ring as the limit of lim ‖a ^ k‖ ^ (1 / k) and proves basic properties.

Main definitions

• gelfandRadius a: the limit of the sequence ‖a ^ k‖ ^ (1 / k).

Main statements

• tendsto_gelfandRadius: the sequence ‖a ^ k‖ ^ (1 / k) converges to gelfandRadius.
• gelfandRadius_add_le: gelfandRadius is subadditive.
• gelfandRadius_mul_le: gelfandRadius is submultiplicative.

noncomputable def gelfandRadius {A : Type u_2} [SeminormedRing A] (a : A) : ℝ

The limit ‖a ^ k‖ ^ (1 / k) of an element a in a normed ring. We use k : ℕ+ to ease the eventual generalization to NonUnitalSeminormedRing.

Equations

• gelfandRadius a = Filter.atTop.limUnder fun (k : ℕ+) => ‖a ^ ↑k‖ ^ (↑↑k)⁻¹

theorem tendsto_gelfandRadius' {A : Type u_2} [SeminormedRing A] (a : A) : Filter.Tendsto (fun (k : ℕ+) => ‖a ^ ↑k‖ ^ (↑↑k)⁻¹) Filter.atTop (nhds (gelfandRadius a))

gelfandRadius a is the limit of ‖a ^ k‖ ^ (1 / k) over k : ℕ+. See tendsto_gelfandRadius for the limit over k : ℕ.

theorem tendsto_gelfandRadius {A : Type u_2} [SeminormedRing A] (a : A) : Filter.Tendsto (fun (k : ℕ) => ‖a ^ k‖ ^ (↑k)⁻¹) Filter.atTop (nhds (gelfandRadius a))

gelfandRadius a is the limit of ‖a ^ k‖ ^ (1 / k) over k : ℕ. See tendsto_gelfandRadius' for the limit over k : ℕ+.

theorem gelfandRadius_nonneg {A : Type u_2} [SeminormedRing A] (a : A) : 0 ≤ gelfandRadius a

def Mathlib.Meta.Positivity.evalGelfandRadius : PositivityExt

The positivity extension which identifies expressions of the form gelfandRadius a.

Equations

• One or more equations did not get rendered due to their size.

theorem gelfandRadius_le_norm {A : Type u_2} [SeminormedRing A] (a : A) : gelfandRadius a ≤ ‖a‖

theorem gelfandRadius_of_norm_nonpos {A : Type u_2} [SeminormedRing A] {a : A} (ha : ‖a‖ ≤ 0) : gelfandRadius a = 0

@[simp]

theorem gelfandRadius_zero {A : Type u_2} [SeminormedRing A] : gelfandRadius 0 = 0

@[simp]

theorem gelfandRadius_neg {A : Type u_2} [SeminormedRing A] (a : A) : gelfandRadius (-a) = gelfandRadius a

theorem gelfandRadius_smul {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [SeminormedRing A] [NormedAlgebra 𝕜 A] (c : 𝕜) (a : A) : gelfandRadius (c • a) = ‖c‖ * gelfandRadius a

theorem gelfandRadius_pow_of_ne_zero {A : Type u_2} [SeminormedRing A] (a : A) {n : ℕ} (hn : n ≠ 0) : gelfandRadius (a ^ n) = gelfandRadius a ^ n

@[simp]

theorem gelfandRadius_one {A : Type u_2} [SeminormedRing A] [NormOneClass A] : gelfandRadius 1 = 1

theorem gelfandRadius_pow {A : Type u_2} [SeminormedRing A] [NormOneClass A] (a : A) (n : ℕ) : gelfandRadius (a ^ n) = gelfandRadius a ^ n

theorem gelfandRadius_le_norm_pow {A : Type u_2} [SeminormedRing A] (a : A) {n : ℕ} (hn : n ≠ 0) : gelfandRadius a ≤ ‖a ^ n‖ ^ (↑n)⁻¹

theorem gelfandRadius_pow_le_norm_pow {A : Type u_2} [SeminormedRing A] (a : A) {n : ℕ} (hn : n ≠ 0) : gelfandRadius a ^ n ≤ ‖a ^ n‖

theorem norm_pow_le_mul_pow_of_gelfandRadius_lt {A : Type u_2} [SeminormedRing A] (a : A) {r : ℝ} (hr : gelfandRadius a < r) : ∃ C > 0, ∀ (n : ℕ), ‖a ^ n‖ ≤ C * r ^ n

If gelfandRadius a < r, then there is some C for which ‖a ^ n‖ ≤ C * r ^ n for all n. See gelfandRadius_le_of_bound for the converse.

theorem gelfandRadius_le_of_bound {A : Type u_2} [SeminormedRing A] {a : A} {C r : ℝ} (hr : 0 ≤ r) (h : ∀ (n : ℕ), ‖a ^ n‖ ≤ C * r ^ n) : gelfandRadius a ≤ r

If ‖a ^ n‖ ≤ C * r ^ n for all n, then gelfandRadius a ≤ r. See exists_le_gelfandRadius for the converse.

theorem Commute.gelfandRadius_add_le {A : Type u_2} [SeminormedRing A] {a b : A} (h : Commute a b) : gelfandRadius (a + b) ≤ gelfandRadius a + gelfandRadius b

theorem Commute.gelfandRadius_mul_le {A : Type u_2} [SeminormedRing A] {a b : A} (h : Commute a b) : gelfandRadius (a * b) ≤ gelfandRadius a * gelfandRadius b

theorem gelfandRadius_add_le {A : Type u_2} [SeminormedCommRing A] (a b : A) : gelfandRadius (a + b) ≤ gelfandRadius a + gelfandRadius b

gelfandRadius is subadditive.

theorem gelfandRadius_mul_le {A : Type u_2} [SeminormedCommRing A] (a b : A) : gelfandRadius (a * b) ≤ gelfandRadius a * gelfandRadius b

gelfandRadius is submultiplicative.