Mathlib.Analysis.Normed.Ring.Units

Units.add definition

(x : Rˣ) (t : R) (h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹) : Rˣ

Full source

/-- In a normed ring with summable geometric series, 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. -/
@[simps! val]
def add (x : Rˣ) (t : R) (h : ‖t‖ < ‖(↑x⁻¹ : R)‖‖(↑x⁻¹ : R)‖⁻¹) : Rˣ :=
  Units.copy -- to make `add_val` true definitionally, for convenience
    (x * Units.oneSub (-((x⁻¹).1 * t)) (by
      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⁻¹).1 _
        _ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖‖(↑x⁻¹ : R)‖⁻¹ := by nlinarith only [h, hpos]
        _ = 1 := mul_inv_cancel₀ (ne_of_gt hpos)))
    (x + t) (by simp [mul_add]) _ rfl

Unit perturbation by addition in a normed ring

Informal description

Given a unit $ x $ in a normed ring $ R $ with summable geometric series and an element $ t \in R $ such that the norm of $ t $ is less than the reciprocal of the norm of $ x^{-1} $, the element $ x + t $ is also a unit. The unit structure of $ x + t $ is constructed using the geometric series expansion of $ 1 - (x^{-1} t) $.

Units.ofNearby definition

(x : Rˣ) (y : R) (h : ‖y - x‖ < ‖(↑x⁻¹ : R)‖⁻¹) : Rˣ

Full source

/-- In a normed ring with summable geometric series, an element `y` of distance less
than `‖x⁻¹‖⁻¹` from `x` is a unit. Here we construct its `Units` structure. -/
@[simps! val]
def ofNearby (x : Rˣ) (y : R) (h : ‖y - x‖ < ‖(↑x⁻¹ : R)‖‖(↑x⁻¹ : R)‖⁻¹) : Rˣ :=
  (x.add (y - x : R) h).copy y (by simp) _ rfl

Unit perturbation by nearby element in a normed ring

Informal description

Given a unit $ x $ in a normed ring $ R $ with summable geometric series and an element $ y \in R $ such that the distance between $ y $ and $ x $ is less than the reciprocal of the norm of $ x^{-1} $, the element $ y $ is also a unit. The unit structure of $ y $ is constructed by perturbing $ x $ with $ y - x $.

Units.isOpen theorem

: IsOpen {x : R | IsUnit x}

Full source

/-- The group of units of a normed ring with summable geometric series is an open subset
of the ring. -/
protected theorem isOpen : IsOpen { x : R | IsUnit x } := by
  nontriviality R
  rw [Metric.isOpen_iff]
  rintro _ ⟨x, rfl⟩
  refine ⟨‖(↑x⁻¹ : R)‖⁻¹, _root_.inv_pos.mpr (Units.norm_pos x⁻¹), fun y hy ↦ ?_⟩
  rw [mem_ball_iff_norm] at hy
  exact (x.ofNearby y hy).isUnit

Openness of the Group of Units in a Normed Ring with Summable Geometric Series

Informal description

The set of units (invertible elements) in a normed ring with summable geometric series is an open subset of the ring.

Units.nhds theorem

(x : Rˣ) : {x : R | IsUnit x} ∈ 𝓝 (x : R)

Full source

protected theorem nhds (x : Rˣ) : { x : R | IsUnit x }{ x : R | IsUnit x } ∈ 𝓝 (x : R) :=
  IsOpen.mem_nhds Units.isOpen x.isUnit

Units form a neighborhood of any unit in a normed ring with summable geometric series

Informal description

For any unit $x$ in a normed ring $R$ with summable geometric series, the set of units $\{y \in R \mid \text{$y$ is a unit}\}$ is a neighborhood of $x$ in the norm topology on $R$.

nonunits.subset_compl_ball theorem

: nonunits R ⊆ (Metric.ball (1 : R) 1)ᶜ

Full source

/-- The `nonunits` in a normed ring with summable geometric series are contained in the
complement of the ball of radius `1` centered at `1 : R`. -/
theorem subset_compl_ball : nonunitsnonunits R ⊆ (Metric.ball (1 : R) 1)ᶜ := fun x hx h₁ ↦ hx <|
  sub_sub_self 1 x ▸ (Units.oneSub (1 - x) (by rwa [mem_ball_iff_norm'] at h₁)).isUnit

Nonunits lie outside unit ball centered at identity

Informal description

In a normed ring $R$ with summable geometric series, the set of nonunits is contained in the complement of the open ball of radius 1 centered at the multiplicative identity $1 \in R$. In other words, if $x \in R$ is a nonunit, then $\|x - 1\| \geq 1$.

nonunits.isClosed theorem

: IsClosed (nonunits R)

Full source

protected theorem isClosed : IsClosed (nonunits R) :=
  Units.isOpen.isClosed_compl

Closedness of Nonunits in Normed Ring with Summable Geometric Series

Informal description

The set of nonunits in a normed ring with summable geometric series is a closed subset of the ring.

NormedRing.inverse_one_sub theorem

(t : R) (h : ‖t‖ < 1) : inverse (1 - t) = ↑(Units.oneSub t h)⁻¹

Full source

theorem inverse_one_sub (t : R) (h : ‖t‖ < 1) : inverse (1 - t) = ↑(Units.oneSub t h)⁻¹ := by
  rw [← inverse_unit (Units.oneSub t h), Units.val_oneSub]

Inverse of $1 - t$ via Geometric Series in Normed Ring

Informal description

Let $R$ be a normed ring with summable geometric series. For any element $t \in R$ with $\|t\| < 1$, the ring inverse of $1 - t$ is equal to the inverse of the unit element $(1 - t)^{-1}$ constructed via the geometric series sum, i.e., \[ \text{inverse}(1 - t) = (1 - t)^{-1}. \]

NormedRing.inverse_add theorem

(x : Rˣ) : ∀ᶠ t in 𝓝 0, inverse ((x : R) + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

Full source

/-- The formula `Ring.inverse (x + t) = Ring.inverse (1 + x⁻¹ * t) * x⁻¹` holds for `t` sufficiently
small. -/
theorem inverse_add (x : Rˣ) :
    ∀ᶠ t in 𝓝 0, inverse ((x : R) + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹ := by
  nontriviality R
  rw [Metric.eventually_nhds_iff]
  refine ⟨‖(↑x⁻¹ : R)‖⁻¹, by cancel_denoms, fun t ht ↦ ?_⟩
  rw [dist_zero_right] at ht
  rw [← x.val_add t ht, inverse_unit, Units.add, Units.copy_eq, mul_inv_rev, Units.val_mul,
    ← inverse_unit, Units.val_oneSub, sub_neg_eq_add]

Asymptotic Expansion of Ring Inverse for Perturbed Units: $\text{inverse}(x + t) = \text{inverse}(1 + x^{-1} t) \cdot x^{-1}$ as $t \to 0$

Informal description

Let $R$ be a normed ring with summable geometric series and let $x$ be a unit in $R$. Then, for all sufficiently small $t$ (i.e., in a neighborhood of $0$), the ring inverse of $x + t$ satisfies the identity: \[ \text{inverse}(x + t) = \text{inverse}(1 + x^{-1} t) \cdot x^{-1}. \]

NormedRing.inverse_one_sub_nth_order' theorem

(n : ℕ) {t : R} (ht : ‖t‖ < 1) : inverse ((1 : R) - t) = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t)

Full source

theorem inverse_one_sub_nth_order' (n : ℕ) {t : R} (ht : ‖t‖ < 1) :
    inverse ((1 : R) - t) = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t) :=
  have := _root_.summable_geometric_of_norm_lt_one ht
  calc inverse (1 - t) = ∑' i : ℕ, t ^ i := inverse_one_sub t ht
    _ = ∑ i ∈ range n, t ^ i + ∑' i : ℕ, t ^ (i + n) := (this.sum_add_tsum_nat_add _).symm
    _ = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t) := by
      simp only [inverse_one_sub t ht, add_comm _ n, pow_add, this.tsum_mul_left]; rfl

Partial Sum Expansion of Inverse of $1 - t$ in Normed Ring

Informal description

Let $R$ be a normed ring with summable geometric series. For any natural number $n$ and any element $t \in R$ with $\|t\| < 1$, the ring inverse of $1 - t$ can be expressed as: \[ \text{inverse}(1 - t) = \left( \sum_{i=0}^{n-1} t^i \right) + t^n \cdot \text{inverse}(1 - t). \]

NormedRing.inverse_one_sub_nth_order theorem

(n : ℕ) : ∀ᶠ t in 𝓝 0, inverse ((1 : R) - t) = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t)

Full source

theorem inverse_one_sub_nth_order (n : ℕ) :
    ∀ᶠ t in 𝓝 0, inverse ((1 : R) - t) = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t) :=
  Metric.eventually_nhds_iff.2 ⟨1, one_pos, fun t ht ↦ inverse_one_sub_nth_order' n <| by
    rwa [← dist_zero_right]⟩

Partial Sum Expansion of $\text{inverse}(1 - t)$ Near Zero

Informal description

Let $R$ be a normed ring with summable geometric series. For any natural number $n$, there exists a neighborhood of $0$ such that for all $t$ in this neighborhood, the ring inverse of $1 - t$ satisfies: \[ \text{inverse}(1 - t) = \left( \sum_{i=0}^{n-1} t^i \right) + t^n \cdot \text{inverse}(1 - t). \]

NormedRing.inverse_add_nth_order theorem

 (x : Rˣ) (n : ℕ) :
  ∀ᶠ t in 𝓝 0, inverse ((x : R) + t) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (x + t)

Full source

/-- The formula
`Ring.inverse (x + t) =
  (∑ i ∈ Finset.range n, (- x⁻¹ * t) ^ i) * x⁻¹ + (- x⁻¹ * t) ^ n * Ring.inverse (x + t)`
holds for `t` sufficiently small. -/
theorem inverse_add_nth_order (x : Rˣ) (n : ℕ) :
    ∀ᶠ t in 𝓝 0, inverse ((x : R) + t) =
      (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (x + t) := by
  have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) :=
    (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
  filter_upwards [inverse_add x, hzero.eventually (inverse_one_sub_nth_order n)] with t ht ht'
  rw [neg_mul, sub_neg_eq_add] at ht'
  conv_lhs => rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
  rw [ht]

Partial Sum Expansion of $\text{inverse}(x + t)$ Near Zero: $\text{inverse}(x + t) = \left(\sum_{i=0}^{n-1} (-x^{-1}t)^i\right) x^{-1} + (-x^{-1}t)^n \text{inverse}(x + t)$ for $t \to 0$

Informal description

Let $R$ be a normed ring with summable geometric series and let $x$ be a unit in $R$. For any natural number $n$, there exists a neighborhood of $0$ such that for all sufficiently small $t$ in this neighborhood, the ring inverse of $x + t$ satisfies: \[ \text{inverse}(x + t) = \left( \sum_{i=0}^{n-1} (-x^{-1}t)^i \right) x^{-1} + (-x^{-1}t)^n \cdot \text{inverse}(x + t). \]

NormedRing.inverse_one_sub_norm theorem

: (fun t : R => inverse (1 - t)) =O[𝓝 0] (fun _t => 1 : R → ℝ)

Full source

theorem inverse_one_sub_norm : (fun t : R => inverse (1 - t)) =O[𝓝 0] (fun _t => 1 : R → ℝ) := by
  simp only [IsBigO, IsBigOWith, Metric.eventually_nhds_iff]
  refine ⟨‖(1 : R)‖ + 1, (2 : ℝ)⁻¹, by norm_num, fun t ht ↦ ?_⟩
  rw [dist_zero_right] at ht
  have ht' : ‖t‖ < 1 := by linarith
  simp only [inverse_one_sub t ht', norm_one, mul_one, Set.mem_setOf_eq]
  change ‖∑' n : ℕ, t ^ n‖ ≤ _
  have := tsum_geometric_le_of_norm_lt_one t ht'
  have : (1 - ‖t‖)⁻¹ ≤ 2 := by
    rw [← inv_inv (2 : ℝ)]
    refine inv_anti₀ (by norm_num) ?_
    linarith
  linarith

Asymptotic Bound for Inverse of $1 - t$ Near Zero

Informal description

The function $t \mapsto \text{inverse}(1 - t)$ is asymptotically bounded by a constant function as $t$ approaches $0$ in a normed ring $R$ with summable geometric series.

NormedRing.inverse_add_norm theorem

(x : Rˣ) : (fun t : R => inverse (↑x + t)) =O[𝓝 0] fun _t => (1 : ℝ)

Full source

/-- The function `fun t ↦ inverse (x + t)` is O(1) as `t → 0`. -/
theorem inverse_add_norm (x : Rˣ) : (fun t : R => inverse (↑x + t)) =O[𝓝 0] fun _t => (1 : ℝ) := by
  refine EventuallyEq.trans_isBigO (inverse_add x) (one_mul (1 : ℝ) ▸ ?_)
  simp only [← sub_neg_eq_add, ← neg_mul]
  have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) :=
    (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
  exact (inverse_one_sub_norm.comp_tendsto hzero).mul (isBigO_const_const _ one_ne_zero _)

Asymptotic Bound for Inverse of Perturbed Unit Near Zero: $\text{inverse}(x + t) = O(1)$ as $t \to 0$

Informal description

Let $R$ be a normed ring with summable geometric series and let $x$ be a unit in $R$. Then the function $t \mapsto \text{inverse}(x + t)$ is asymptotically bounded by a constant function as $t$ approaches $0$.

NormedRing.inverse_add_norm_diff_nth_order theorem

 (x : Rˣ) (n : ℕ) :
  (fun t : R => inverse (↑x + t) - (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[𝓝 (0 : R)] fun t => ‖t‖ ^ n

Full source

/-- The function
`fun t ↦ Ring.inverse (x + t) - (∑ i ∈ Finset.range n, (- x⁻¹ * t) ^ i) * x⁻¹`
is `O(t ^ n)` as `t → 0`. -/
theorem inverse_add_norm_diff_nth_order (x : Rˣ) (n : ℕ) :
    (fun t : R => inverse (↑x + t) - (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[𝓝 (0 : R)]
      fun t => ‖t‖ ^ n := by
  refine EventuallyEq.trans_isBigO (.sub (inverse_add_nth_order x n) (.refl _ _)) ?_
  simp only [add_sub_cancel_left]
  refine ((isBigO_refl _ _).norm_right.mul (inverse_add_norm x)).trans ?_
  simp only [mul_one, isBigO_norm_left]
  exact ((isBigO_refl _ _).norm_right.const_mul_left _).pow _

$n$-th Order Asymptotic Expansion of $\text{inverse}(x + t)$ Near Zero

Informal description

Let $R$ be a normed ring with summable geometric series and let $x$ be a unit in $R$. For any natural number $n$, the function \[ t \mapsto \text{inverse}(x + t) - \left(\sum_{i=0}^{n-1} (-x^{-1}t)^i\right) x^{-1} \] is $O(\|t\|^n)$ as $t \to 0$.

NormedRing.inverse_add_norm_diff_first_order theorem

(x : Rˣ) : (fun t : R => inverse (↑x + t) - ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖

Full source

/-- The function `fun t ↦ Ring.inverse (x + t) - x⁻¹` is `O(t)` as `t → 0`. -/
theorem inverse_add_norm_diff_first_order (x : Rˣ) :
    (fun t : R => inverse (↑x + t) - ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ := by
  simpa using inverse_add_norm_diff_nth_order x 1

First-order asymptotic expansion of $\text{Ring.inverse}(x + t)$ near zero: $\text{Ring.inverse}(x + t) - x^{-1} = O(\|t\|)$

Informal description

Let $R$ be a normed ring with summable geometric series and let $x$ be a unit in $R$. The function $t \mapsto \text{Ring.inverse}(x + t) - x^{-1}$ is $O(\|t\|)$ as $t \to 0$.

NormedRing.inverse_add_norm_diff_second_order theorem

(x : Rˣ) : (fun t : R => inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ 2

Full source

/-- The function `fun t ↦ Ring.inverse (x + t) - x⁻¹ + x⁻¹ * t * x⁻¹` is `O(t ^ 2)` as `t → 0`. -/
theorem inverse_add_norm_diff_second_order (x : Rˣ) :
    (fun t : R => inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ 2 := by
  convert inverse_add_norm_diff_nth_order x 2 using 2
  simp only [sum_range_succ, sum_range_zero, zero_add, pow_zero, pow_one, add_mul, one_mul,
    ← sub_sub, neg_mul, sub_neg_eq_add]

Second-order asymptotic expansion of $\text{Ring.inverse}(x + t)$ near zero

Informal description

Let $R$ be a normed ring with summable geometric series and let $x$ be a unit in $R$. The function \[ t \mapsto \text{Ring.inverse}(x + t) - x^{-1} + x^{-1} t x^{-1} \] is $O(\|t\|^2)$ as $t \to 0$.

NormedRing.inverse_continuousAt theorem

(x : Rˣ) : ContinuousAt inverse (x : R)

Full source

/-- The function `Ring.inverse` is continuous at each unit of `R`. -/
theorem inverse_continuousAt (x : Rˣ) : ContinuousAt inverse (x : R) := by
  have h_is_o : (fun t : R => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] (fun _ => 1 : R → ℝ) :=
    (inverse_add_norm_diff_first_order x).trans_isLittleO (isLittleO_id_const one_ne_zero).norm_left
  have h_lim : Tendsto (fun y : R => y - x) (𝓝 x) (𝓝 0) := by
    refine tendsto_zero_iff_norm_tendsto_zero.mpr ?_
    exact tendsto_iff_norm_sub_tendsto_zero.mp tendsto_id
  rw [ContinuousAt, tendsto_iff_norm_sub_tendsto_zero, inverse_unit]
  simpa [Function.comp_def] using h_is_o.norm_left.tendsto_div_nhds_zero.comp h_lim

Continuity of Ring Inverse at Units in Normed Rings

Informal description

For any unit $x$ in a normed ring $R$ with summable geometric series, the function $\text{Ring.inverse}$ is continuous at $x$.

Units.isOpenEmbedding_val theorem

: IsOpenEmbedding (val : Rˣ → R)

Full source

/-- In a normed ring with summable geometric series, the coercion from `Rˣ` (equipped with the
induced topology from the embedding in `R × R`) to `R` is an open embedding. -/
theorem isOpenEmbedding_val : IsOpenEmbedding (val : Rˣ → R) where
  toIsEmbedding := isEmbedding_val_mk'
    (fun _ ⟨u, hu⟩ ↦ hu ▸ (inverse_continuousAt u).continuousWithinAt) Ring.inverse_unit
  isOpen_range := Units.isOpen

Open Embedding Property of Units Inclusion in Normed Rings

Informal description

In a normed ring $R$ with summable geometric series, the inclusion map from the group of units $R^\times$ to $R$ is an open embedding, where $R^\times$ is equipped with the topology induced by the embedding $R^\times \to R \times R$ that sends each unit to itself and its inverse.

Units.isOpenMap_val theorem

: IsOpenMap (val : Rˣ → R)

Full source

/-- In a normed ring with summable geometric series, the coercion from `Rˣ` (equipped with the
induced topology from the embedding in `R × R`) to `R` is an open map. -/
theorem isOpenMap_val : IsOpenMap (val : Rˣ → R) :=
  isOpenEmbedding_val.isOpenMap

Open Mapping Property of Units Inclusion in Normed Rings with Summable Geometric Series

Informal description

In a normed ring $R$ with summable geometric series, the canonical inclusion map from the group of units $R^\times$ to $R$ is an open map. Here, $R^\times$ is equipped with the topology induced by the embedding $R^\times \to R \times R$ that sends each unit to itself and its inverse.

Ideal.closure_ne_top theorem

(I : Ideal R) (hI : I ≠ ⊤) : I.closure ≠ ⊤

Full source

/-- The `Ideal.closure` of a proper ideal in a normed ring with summable
geometric series is proper. -/
theorem closure_ne_top (I : Ideal R) (hI : I ≠ ⊤) : I.closure ≠ ⊤ := by
  have h := closure_minimal (coe_subset_nonunits hI) nonunits.isClosed
  simpa only [I.closure.eq_top_iff_one, Ne] using mt (@h 1) one_not_mem_nonunits

Closure of Proper Ideal Remains Proper in Normed Ring with Summable Geometric Series

Informal description

Let $R$ be a normed ring with summable geometric series. For any proper ideal $I \subset R$ (i.e., $I \neq R$), the topological closure $\overline{I}$ is also a proper ideal (i.e., $\overline{I} \neq R$).

Ideal.IsMaximal.closure_eq theorem

{I : Ideal R} (hI : I.IsMaximal) : I.closure = I

Full source

/-- The `Ideal.closure` of a maximal ideal in a normed ring with summable
geometric series is the ideal itself. -/
theorem IsMaximal.closure_eq {I : Ideal R} (hI : I.IsMaximal) : I.closure = I :=
  (hI.eq_of_le (I.closure_ne_top hI.ne_top) subset_closure).symm

Closure of Maximal Ideal in Normed Ring with Summable Geometric Series Equals Itself

Informal description

For any maximal ideal $I$ in a normed ring $R$ with summable geometric series, the topological closure of $I$ is equal to $I$ itself, i.e., $\overline{I} = I$.

Ideal.IsMaximal.isClosed instance

{I : Ideal R} [hI : I.IsMaximal] : IsClosed (I : Set R)

Full source

/-- Maximal ideals in normed rings with summable geometric series are closed. -/
instance IsMaximal.isClosed {I : Ideal R} [hI : I.IsMaximal] : IsClosed (I : Set R) :=
  isClosed_of_closure_subset <| Eq.subset <| congr_arg ((↑) : Ideal R → Set R) hI.closure_eq

Maximal ideals are closed in normed rings with summable geometric series

Informal description

Every maximal ideal in a normed ring with summable geometric series is closed.

Main results