NormedRing.inverse_add_norm_diff_nth_order
theorem NormedRing.inverse_add_norm_diff_nth_order :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : Rˣ) (n : ℕ),
(fun t => Ring.inverse (↑x + t) - ((Finset.range n).sum fun i => (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[nhds 0] fun t =>
‖t‖ ^ n
This theorem states that for any normed ring `R` that is also a complete space, given a non-zero element `x` of `R` and a natural number `n`, the function `t ↦ Ring.inverse (x + t) - (∑ i in Finset.range n, (- x⁻¹ * t) ^ i) * x⁻¹` is `O(t ^ n)` as `t` tends to `0`. In other words, the difference between the inverse of `x + t` and the sum (up to `n` terms) of `(-x⁻¹ * t)` raised to the power of `i` times `x⁻¹`, behaves asymptotically as `t` raised to the power of `n` when `t` approaches `0`. Here, `-x⁻¹` represents the negative multiplicative inverse of `x`, `t` is a variable, `^` denotes exponentiation, and `O(t ^ n)` represents Big O notation, which is a way to express the upper bound of a function's growth rate.
The term `nhds 0` refers to a neighborhood filter at `0` in the topological space, which in this context describes the limit process of `t` tending to `0`.
More concisely: For any complete normed ring `R` and non-zero element `x` in `R`, the function `t �mapsto x⁻¹ - ∑ₙ₀ⁱ (x⁻¹ * t)ⁱ` is `O(t ^ n)` as `t` approaches `0`.
|
NormedRing.inverse_add
theorem NormedRing.inverse_add :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : Rˣ),
∀ᶠ (t : R) in nhds 0, Ring.inverse (↑x + t) = Ring.inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
This theorem states that for a given non-zero element `x` in a Complete Normed Ring `R`, there exists a neighborhood of `0` (i.e., a set containing numbers sufficiently close to `0`) such that for all `t` in this neighborhood, the inverse function of `(x + t)` equals the product of the inverse function of `(1 + x⁻¹ * t)` and `x⁻¹`. This inverse function is defined in the context of a monoid with zero, and returns the multiplicative inverse of the input if it exists, or `0` otherwise.
More concisely: For every non-zero element `x` in a Complete Normed Ring `R`, there exists a neighborhood of `0` such that for all `t` in this neighborhood, `(x + t)⁻¹ = x⁻¹ * (1 + x⁻¹ * t)⁻¹`.
|
Ideal.eq_top_of_norm_lt_one
theorem Ideal.eq_top_of_norm_lt_one :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] (I : Ideal R) {x : R},
x ∈ I → ‖1 - x‖ < 1 → I = ⊤
The theorem `Ideal.eq_top_of_norm_lt_one` states that for any type `R` which is a normed ring and a complete space, if an ideal `I` of `R` contains an element `x` such that the norm of `1 - x` is less than 1, then `I` is the unit ideal. In other words, if an ideal includes an element which is within 1 unit of unity in the normed ring, it must be the unit ideal and therefore contain all elements of the ring.
More concisely: If `I` is an ideal in the complete, normed ring `R` and there exists an element `x` in `I` with norm `||1 - x||<1`, then `I` is the unit ideal.
|
Ideal.IsMaximal.closure_eq
theorem Ideal.IsMaximal.closure_eq :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] {I : Ideal R}, I.IsMaximal → I.closure = I := by
sorry
This theorem states that for any type `R` that is a normed ring and a complete space, and for any ideal `I` in `R`, if `I` is maximal, then the closure of `I` is equal to `I` itself. In other words, in the context of complete normed rings, the closure of a maximal ideal does not extend beyond the ideal itself.
More concisely: In a complete normed ring, the closure of a maximal ideal is equal to the ideal itself.
|
Units.openEmbedding_val
theorem Units.openEmbedding_val :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R], OpenEmbedding Units.val
This theorem states that in a normed ring `R` which is also a complete space, the coercion from the non-zero elements of `R` (denoted as `Rˣ`, and equipped with the topology induced from the embedding in `R × R`) to `R` is an open embedding. Here, an open embedding means that the image of an open set under the function is open and the function is injective and continuous. The function in consideration is `Units.val`, which essentially takes a non-zero element of the ring and returns its underlying value in the base `Monoid`.
More concisely: In a complete and normed ring `R`, the coercion map from its non-zero elements `Rˣ` to `R` is an open, injective, and continuous function. (Or equivalently, the `Units.val` function is an open embedding from `Rˣ` to `R`.)
|
NormedRing.inverse_add_norm_diff_first_order
theorem NormedRing.inverse_add_norm_diff_first_order :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : Rˣ),
(fun t => Ring.inverse (↑x + t) - ↑x⁻¹) =O[nhds 0] fun t => ‖t‖
The theorem `NormedRing.inverse_add_norm_diff_first_order` states that for any non-zero element `x` of a complete normed ring `R`, the function that maps `t` to the difference between the inverse of `(x + t)` and the inverse of `x`, is big O of the norm of `t` as `t` converges to `0` in the topology of `R`. In other words, as `t` approaches `0`, the growth rate of the difference between the inverses is at most proportional to the absolute value of `t`.
More concisely: For any complete normed ring R and non-zero element x in R, the function that maps t to |(x^(-1) - (x + t)^(-1)| is big O of the norm of t as t approaches 0.
|
nonunits.subset_compl_ball
theorem nonunits.subset_compl_ball :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R], nonunits R ⊆ (Metric.ball 1 1)ᶜ
The theorem `nonunits.subset_compl_ball` states that for any complete normed ring `R`, the set of non-invertible elements (also known as `nonunits`) is a subset of the complement of the ball of radius `1` centered at `1` in `R`. In other words, all non-invertible elements of `R` have a norm (or distance) that is greater than or equal to `1` from the element `1` in the ring.
More concisely: For any complete normed ring R, the set of non-invertible elements is contained in the complement of the closed ball of radius 1 around 1.
|
Ideal.closure_ne_top
theorem Ideal.closure_ne_top :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] (I : Ideal R), I ≠ ⊤ → I.closure ≠ ⊤
The theorem `Ideal.closure_ne_top` states that for any type `R` that has the structure of a `NormedRing` and a `CompleteSpace`, if `I` is a proper ideal in this ring `R` (i.e., `I` is not equal to the whole ring `R` indicated by `I ≠ ⊤`), then the closure of `I` (which is the smallest closed set containing `I`) is also a proper subset of the ring `R` (i.e., `I.closure ≠ ⊤`). In other words, the closure of a proper ideal in a complete normed ring remains proper.
More concisely: In a complete normed ring, the closure of a proper ideal is a proper subset of the ring.
|
NormedRing.inverse_continuousAt
theorem NormedRing.inverse_continuousAt :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : Rˣ), ContinuousAt Ring.inverse ↑x
This theorem states that for every unit `x` in a normed ring `R` that is also a complete space, the function `Ring.inverse`, which computes the multiplicative inverse of elements in `R` (or yields zero for non-invertible elements), is continuous at `x`. In other words, as elements of the ring approach `x`, their inverses approach the inverse of `x`.
More concisely: The multiplicative inverse function in a complete, normed ring is continuous at every invertible element.
|
NormedRing.inverse_add_nth_order
theorem NormedRing.inverse_add_nth_order :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : Rˣ) (n : ℕ),
∀ᶠ (t : R) in nhds 0,
Ring.inverse (↑x + t) =
((Finset.range n).sum fun i => (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * Ring.inverse (↑x + t)
This theorem states that for any normed ring `R`, which is also a complete space, and for any nonzero element `x` of `R` and natural number `n`, there exists a neighborhood of zero such that for all `t` in this neighborhood, the inverse of `x + t` is equal to the sum of `(- inverse of x * t) ^ i` for all `i` in the set of natural numbers less than `n`, all multiplied by the inverse of `x`, plus `(- inverse of x * t) ^ n` multiplied by the inverse of `x + t`. This holds when `t` is sufficiently close to zero.
More concisely: For any normed ring `R` that is complete, and any nonzero `x` in `R` and natural number `n`, there exists a neighborhood of zero such that for all `t` in this neighborhood, the inverse of `x + t` is equal to the sum of the geometric series `(-x^(-1) * t)^i * x^(-1)` for `i` in `[0, n)`, plus `(-x^(-1) * t)^n * (x^(-1) + t)^(-1)`.
|
Units.isOpenMap_val
theorem Units.isOpenMap_val : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R], IsOpenMap Units.val
This theorem states that in a normed ring `R` which is also a complete space, the function `Units.val` is an open map. The function `Units.val` takes a unit (an element with a multiplicative inverse) in the ring and returns the underlying value in the base ring. Here, the units are equipped with the topology induced from the embedding in `R × R`. An open map is a function such that the image of any open set in the domain is also an open set in the codomain. Hence, for any open set of units, the set of their underlying values in the ring is also open.
More concisely: In a complete, normed ring equipped with the topology of its embedding in the ring's Cartesian square, the function mapping units to their underlying values is an open map.
|
Units.isOpen
theorem Units.isOpen : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R], IsOpen {x | IsUnit x} := by
sorry
This theorem states that for any complete normed ring `R`, the set of units in `R` forms an open subset of the ring. Here, a unit is defined as an element in the ring that has a two-sided inverse. An open set, in the context of the topological space associated with the ring, is a set where each point is an interior point. A complete space is a space in which every Cauchy sequence converges to a point in the same space.
More concisely: The set of units in a complete normed ring forms an open subset of the ring.
|
NormedRing.inverse_add_norm_diff_second_order
theorem NormedRing.inverse_add_norm_diff_second_order :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : Rˣ),
(fun t => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[nhds 0] fun t => ‖t‖ ^ 2
The theorem `NormedRing.inverse_add_norm_diff_second_order` states that for any normed ring `R` that is also a complete space, and for any nonzero element `x` of `R`, the function `f(t) = Ring.inverse(x + t) - x⁻¹ + x⁻¹ * t * x⁻¹` is of order `O(t ^ 2)` as `t` approaches 0, with respect to the neighborhood filter of 0. In other words, the difference between the function `f(t)` and the function `g(t) = ‖t‖ ^ 2` is negligible as `t` gets arbitrarily close to 0. This means that `f(t)` behaves like `g(t)` near 0, up to a constant factor and lower order terms.
More concisely: For any complete normed ring `R` and nonzero element `x` in `R`, the function `f(t) = Ring.inverse(x + t) - x⁻¹ + x⁻¹ * t * x⁻¹` is approximated by the quadratic function `g(t) = ‖t‖ ^ 2` as `t` approaches 0.
|
NormedRing.inverse_add_norm
theorem NormedRing.inverse_add_norm :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : Rˣ),
(fun t => Ring.inverse (↑x + t)) =O[nhds 0] fun _t => 1
The theorem `NormedRing.inverse_add_norm` asserts that for any type `R` that is a normed ring and a complete space, and for any nonzero element `x` of `R`, the function `fun t ↦ inverse (x + t)` is big O of 1 as `t` approaches 0. In other words, the change in the function's value remains bounded as `t` becomes close to 0. Here, the function `inverse` is defined on a monoid with zero and the neighborhood filter at `x` is defined as the infimum over the principal filters of all open sets containing `x`. This theorem is particularly important in ring theory and analyses the behavior of inverse functions in normed rings in the neighborhood of 0.
More concisely: For any complete normed ring `R` and nonzero element `x` in `R`, the function `t mapsto inverse(x + t)` is a bounded function near `0`.
|