<commit_before>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import analysis.specific_limits
import analysis.asymptotics.asymptotics

/-!
# 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`.

-/

noncomputable theory
open_locale topological_space
variables {R : Type*} [normed_ring R] [complete_space R]

namespace units

/-- 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.  -/
def one_sub (t : R) (h : ∥t∥ < 1) : units R :=
{ val := 1 - t,
  inv := ∑' n : ℕ, t ^ n,
  val_inv := mul_neg_geom_series t h,
  inv_val := geom_series_mul_neg t h }

@[simp] lemma one_sub_coe (t : R) (h : ∥t∥ < 1) : ↑(one_sub t h) = 1 - t := rfl

/-- 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. -/
def add (x : units R) (t : R) (h : ∥t∥ < ∥(↑x⁻¹ : R)∥⁻¹) : units R :=
x * (units.one_sub (-(↑x⁻¹ * t))
begin
  nontriviality R using [zero_lt_one],
  have hpos : 0 < ∥(↑x⁻¹ : R)∥ := units.norm_pos x⁻¹,
  calc ∥-(↑x⁻¹ * t)∥
      = ∥↑x⁻¹ * t∥                   : by { rw norm_neg }
  ... ≤ ∥(↑x⁻¹ : R)∥ * ∥t∥            : norm_mul_le x.inv _
  ... < ∥(↑x⁻¹ : R)∥ * ∥(↑x⁻¹ : R)∥⁻¹ : by nlinarith only [h, hpos]
  ... = 1                           : mul_inv_cancel (ne_of_gt hpos)
end)

@[simp] lemma add_coe (x : units R) (t : R) (h : ∥t∥ < ∥(↑x⁻¹ : R)∥⁻¹) :
  ((x.add t h) : R) = x + t := by { unfold units.add, simp [mul_add] }

/-- In a complete normed ring, an element `y` of distance less than `∥x⁻¹∥⁻¹` from `x` is a unit.
Here we construct its `units` structure. -/
def unit_of_nearby (x : units R) (y : R) (h : ∥y - x∥ < ∥(↑x⁻¹ : R)∥⁻¹) : units R :=
x.add ((y : R) - x) h

@[simp] lemma unit_of_nearby_coe (x : units R) (y : R) (h : ∥y - x∥ < ∥(↑x⁻¹ : R)∥⁻¹) :
  ↑(x.unit_of_nearby y h) = y := by { unfold units.unit_of_nearby, simp }

/-- The group of units of a complete normed ring is an open subset of the ring. -/
lemma is_open : is_open {x : R | is_unit x} :=
begin
  nontriviality R,
  apply metric.is_open_iff.mpr,
  rintros x' ⟨x, h⟩,
  refine ⟨∥(↑x⁻¹ : R)∥⁻¹, inv_pos.mpr (units.norm_pos x⁻¹), _⟩,
  intros y hy,
  rw [metric.mem_ball, dist_eq_norm, ←h] at hy,
  use x.unit_of_nearby y hy,
  simp
end

lemma nhds (x : units R) : {x : R | is_unit x} ∈ 𝓝 (x : R) :=
mem_nhds_sets is_open (by { rw [set.mem_set_of_eq], exact is_unit_unit x })

end units

namespace normed_ring
open_locale classical big_operators
open asymptotics filter metric finset ring

lemma inverse_one_sub (t : R) (h : ∥t∥ < 1) : inverse (1 - t) = ↑(units.one_sub t h)⁻¹ :=
begin
  rw ← inverse_unit (units.one_sub t h),
  refl,
end

/-- The formula `inverse (x + t) = inverse (1 + x⁻¹ * t) * x⁻¹` holds for `t` sufficiently small. -/
lemma inverse_add (x : units R) :
  ∀ᶠ t in (𝓝 0), inverse ((x : R) + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹ :=
begin
  nontriviality R,
  rw [eventually_iff, mem_nhds_iff],
  have hinv : 0 < ∥(↑x⁻¹ : R)∥⁻¹, by cancel_denoms,
  use [∥(↑x⁻¹ : R)∥⁻¹, hinv],
  intros t ht,
  simp only [mem_ball, dist_zero_right] at ht,
  have ht' : ∥-↑x⁻¹ * t∥ < 1,
  { refine lt_of_le_of_lt (norm_mul_le _ _) _,
    rw norm_neg,
    refine lt_of_lt_of_le (mul_lt_mul_of_pos_left ht x⁻¹.norm_pos) _,
    cancel_denoms },
  have hright := inverse_one_sub (-↑x⁻¹ * t) ht',<commit_msg>chore(analysis/normed_space/units): add `protected`, minor review (#6544)<commit_after>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import analysis.specific_limits
import analysis.asymptotics.asymptotics

/-!
# 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`.

-/

noncomputable theory
open_locale topological_space
variables {R : Type*} [normed_ring R] [complete_space R]

namespace units

/-- 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.  -/
def one_sub (t : R) (h : ∥t∥ < 1) : units R :=
{ val := 1 - t,
  inv := ∑' n : ℕ, t ^ n,
  val_inv := mul_neg_geom_series t h,
  inv_val := geom_series_mul_neg t h }

@[simp] lemma one_sub_coe (t : R) (h : ∥t∥ < 1) : ↑(one_sub t h) = 1 - t := rfl

/-- 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. -/
def add (x : units R) (t : R) (h : ∥t∥ < ∥(↑x⁻¹ : R)∥⁻¹) : units R :=
x * (units.one_sub (-(↑x⁻¹ * t))
begin
  nontriviality R using [zero_lt_one],
  have hpos : 0 < ∥(↑x⁻¹ : R)∥ := units.norm_pos x⁻¹,
  calc ∥-(↑x⁻¹ * t)∥
      = ∥↑x⁻¹ * t∥                    : by { rw norm_neg }
  ... ≤ ∥(↑x⁻¹ : R)∥ * ∥t∥            : norm_mul_le ↑x⁻¹ _
  ... < ∥(↑x⁻¹ : R)∥ * ∥(↑x⁻¹ : R)∥⁻¹ : by nlinarith only [h, hpos]
  ... = 1                             : mul_inv_cancel (ne_of_gt hpos)
end)

@[simp] lemma add_coe (x : units R) (t : R) (h : ∥t∥ < ∥(↑x⁻¹ : R)∥⁻¹) :
  ((x.add t h) : R) = x + t := by { unfold units.add, simp [mul_add] }

/-- In a complete normed ring, an element `y` of distance less than `∥x⁻¹∥⁻¹` from `x` is a unit.
Here we construct its `units` structure. -/
def unit_of_nearby (x : units R) (y : R) (h : ∥y - x∥ < ∥(↑x⁻¹ : R)∥⁻¹) : units R :=
x.add ((y : R) - x) h

@[simp] lemma unit_of_nearby_coe (x : units R) (y : R) (h : ∥y - x∥ < ∥(↑x⁻¹ : R)∥⁻¹) :
  ↑(x.unit_of_nearby y h) = y := by { unfold units.unit_of_nearby, simp }

/-- The group of units of a complete normed ring is an open subset of the ring. -/
protected lemma is_open : is_open {x : R | is_unit x} :=
begin
  nontriviality R,
  apply metric.is_open_iff.mpr,
  rintros x' ⟨x, rfl⟩,
  refine ⟨∥(↑x⁻¹ : R)∥⁻¹, inv_pos.mpr (units.norm_pos x⁻¹), _⟩,
  intros y hy,
  rw [metric.mem_ball, dist_eq_norm] at hy,
  exact ⟨x.unit_of_nearby y hy, unit_of_nearby_coe _ _ _⟩
end

protected lemma nhds (x : units R) : {x : R | is_unit x} ∈ 𝓝 (x : R) :=
mem_nhds_sets units.is_open (is_unit_unit x)

end units

namespace normed_ring
open_locale classical big_operators
open asymptotics filter metric finset ring

lemma inverse_one_sub (t : R) (h : ∥t∥ < 1) : inverse (1 - t) = ↑(units.one_sub t h)⁻¹ :=
by rw [← inverse_unit (units.one_sub t h), units.one_sub_coe]

/-- The formula `inverse (x + t) = inverse (1 + x⁻¹ * t) * x⁻¹` holds for `t` sufficiently small. -/
lemma inverse_add (x : units R) :
  ∀ᶠ t in (𝓝 0), inverse ((x : R) + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹ :=
begin
  nontriviality R,
  rw [eventually_iff, mem_nhds_iff],
  have hinv : 0 < ∥(↑x⁻¹ : R)∥⁻¹, by cancel_denoms,
  use [∥(↑x⁻¹ : R)∥⁻¹, hinv],
  intros t ht,
  simp only [mem_ball, dist_zero_right] at ht,
  have ht' : ∥-↑x⁻¹ * t∥ < 1,
  { refine lt_of_le_of_lt (norm_mul_le _ _) _,
    rw norm_neg,
    refine lt_of_lt_of_le (mul_lt_mul_of_pos_left ht x⁻¹.norm_pos) _,
    cancel_denoms },
  have hright := inverse_one_sub (-↑x⁻¹ * t) ht',
{'fraction_non_alphanumeric': 0.14910055350553506, 'fraction_numerical': 0.005996309963099631, 'mean_word_length': 3.2390029325513194, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3936103', 'n_tokens_mistral': 4020, 'n_tokens_neox': 3705, 'n_words': 1231}