# mathlibdocumentation

analysis.normed_space.units

# The group of units of a complete normed ring

This file contains the basic theory for the group of units (invertible elements) of a complete normed ring (Banach algebras being a notable special case).

## Main results

The constructions one_sub, add and unit_of_nearby state, in varying forms, that perturbations of a unit are units. The latter two are not stated in their optimal form; more precise versions would use the spectral radius.

The first main result is is_open: the group of units of a complete normed ring is an open subset of the ring.

The function inverse (defined in algebra.ring), for a ring R, sends a : R to a⁻¹ if a is a unit and 0 if not. The other major results of this file (notably inverse_add, inverse_add_norm and inverse_add_norm_diff_nth_order) cover the asymptotic properties of inverse (x + t) as t → 0.

def units.one_sub {R : Type u_1} [normed_ring R] (t : R) :
t < 1

In a complete normed ring, a perturbation of 1 by an element t of distance less than 1 from 1 is a unit. Here we construct its units structure.

Equations
@[simp]
theorem units.one_sub_coe {R : Type u_1} [normed_ring R] (t : R) (h : t < 1) :
h) = 1 - t

def units.add {R : Type u_1} [normed_ring R] (x : units R) (t : R) :

In a complete normed ring, a perturbation of a unit x by an element t of distance less than ∥x⁻¹∥⁻¹ from x is a unit. Here we construct its units structure.

Equations
@[simp]
theorem units.add_coe {R : Type u_1} [normed_ring R] (x : units R) (t : R) (h : t < x⁻¹⁻¹) :
(x.add t h) = x + t

def units.unit_of_nearby {R : Type u_1} [normed_ring R] (x : units R) (y : R) :

In a complete normed ring, an element y of distance less than ∥x⁻¹∥⁻¹ from x is a unit. Here we construct its units structure.

Equations
@[simp]
theorem units.unit_of_nearby_coe {R : Type u_1} [normed_ring R] (x : units R) (y : R) (h : y - x < x⁻¹⁻¹) :

theorem units.is_open {R : Type u_1} [normed_ring R]  :
is_open {x : R | is_unit x}

The group of units of a complete normed ring is an open subset of the ring.

theorem units.nhds {R : Type u_1} [normed_ring R] (x : units R) :
{x : R | is_unit x} 𝓝 x

theorem normed_ring.inverse_one_sub {R : Type u_1} [normed_ring R] (t : R) (h : t < 1) :

theorem normed_ring.inverse_add {R : Type u_1} [normed_ring R] (x : units R) :
∀ᶠ (t : R) in 𝓝 0, ring.inverse (x + t) = (ring.inverse (1 + (x⁻¹) * t)) * x⁻¹

The formula inverse (x + t) = inverse (1 + x⁻¹ * t) * x⁻¹ holds for t sufficiently small.

theorem normed_ring.inverse_one_sub_nth_order {R : Type u_1} [normed_ring R] (n : ) :
∀ᶠ (t : R) in 𝓝 0, ring.inverse (1 - t) = ∑ (i : ) in , t ^ i + (t ^ n) * ring.inverse (1 - t)

theorem normed_ring.inverse_add_nth_order {R : Type u_1} [normed_ring R] (x : units R) (n : ) :
∀ᶠ (t : R) in 𝓝 0, ring.inverse (x + t) = (∑ (i : ) in , ((-x⁻¹) * t) ^ i) * x⁻¹ + (((-x⁻¹) * t) ^ n) * ring.inverse (x + t)

The formula inverse (x + t) = (∑ i in range n, (- x⁻¹ * t) ^ i) * x⁻¹ + (- x⁻¹ * t) ^ n * inverse (x + t) holds for t sufficiently small.

theorem normed_ring.inverse_one_sub_norm {R : Type u_1} [normed_ring R]  :
asymptotics.is_O (λ (t : R), ring.inverse (1 - t)) (λ (t : R), 1) (𝓝 0)

theorem normed_ring.inverse_add_norm {R : Type u_1} [normed_ring R] (x : units R) :
asymptotics.is_O (λ (t : R), ring.inverse (x + t)) (λ (t : R), 1) (𝓝 0)

The function λ t, inverse (x + t) is O(1) as t → 0.

theorem normed_ring.inverse_add_norm_diff_nth_order {R : Type u_1} [normed_ring R] (x : units R) (n : ) :
asymptotics.is_O (λ (t : R), ring.inverse (x + t) - (∑ (i : ) in , ((-x⁻¹) * t) ^ i) * x⁻¹) (λ (t : R), t ^ n) (𝓝 0)

The function λ t, inverse (x + t) - (∑ i in range n, (- x⁻¹ * t) ^ i) * x⁻¹ is O(t ^ n) as t → 0.

theorem normed_ring.inverse_add_norm_diff_first_order {R : Type u_1} [normed_ring R] (x : units R) :
asymptotics.is_O (λ (t : R), ring.inverse (x + t) - x⁻¹) (λ (t : R), t) (𝓝 0)

The function λ t, inverse (x + t) - x⁻¹ is O(t) as t → 0.

theorem normed_ring.inverse_add_norm_diff_second_order {R : Type u_1} [normed_ring R] (x : units R) :
asymptotics.is_O (λ (t : R), ring.inverse (x + t) - x⁻¹ + ((x⁻¹) * t) * x⁻¹) (λ (t : R), t ^ 2) (𝓝 0)

The function λ t, inverse (x + t) - x⁻¹ + x⁻¹ * t * x⁻¹ is O(t ^ 2) as t → 0.

theorem normed_ring.inverse_continuous_at {R : Type u_1} [normed_ring R] (x : units R) :

The function inverse is continuous at each unit of R.