LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Seminorm

`Seminorm.continuousAt_zero'` theorem Seminorm.continuousAt_zero' : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ}, p.closedBall 0 r ∈ nhds 0 → ContinuousAt (⇑p) 0 This theorem states that for a given nontrivial normed field `𝕜`, an additive commutative group `E` with a scalar multiplication operation by `𝕜` that forms a module, and a topological structure on `E` that allows for continuous scalar multiplication, if the closed ball of radius `r` at `0` with respect to a seminorm `p` is in the neighborhood of `0`, then the function given by the seminorm `p` is continuous at `0`. This essentially means that as we approach `0` from any direction within this closed ball, the value of the seminorm function approaches the value at `0` continuously, without any abrupt changes or discontinuity. More concisely: If a normed module `(𝕜, E, ∗)` over a nontrivial normed field `𝕜` with continuous scalar multiplication has a seminorm `p` such that the closed ball `B(0, r)` is in the neighborhood of `0`, then `p` is continuous at `0`.
`Seminorm.vadd_closedBall` theorem Seminorm.vadd_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {x y : E} {r : ℝ} (p : Seminorm 𝕜 E), x +ᵥ p.closedBall y r = p.closedBall (x +ᵥ y) r The theorem states that for any given seminormed ring `𝕜` and additive commutative group `E` with scalar multiplication, for any elements `x` and `y` of `E` and a real number `r`, when we add `x` to each element of the closed ball centered at `y` with radius `r` in the given seminorm, we get the closed ball centered at `x + y` with the same radius `r` in the seminorm. In mathematical terms, for a seminorm `p`, this means `x +ᵥ p.closedBall y r = p.closedBall (x + y) r`. More concisely: For any seminormed ring `𝕜`, additive commutative group `E` with scalar multiplication, seminorm `p`, elements `x, y` in `E`, and real number `r`, we have `p.closedBall x r + y = p.closedBall (x + y) r`.
`Mathlib.Analysis.Seminorm._auxLemma.6` theorem Mathlib.Analysis.Seminorm._auxLemma.6 : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {x y : E} {r : ℝ}, (y ∈ p.ball x r) = (p (y - x) < r) The theorem `Mathlib.Analysis.Seminorm._auxLemma.6` states that for any seminormed ring `𝕜`, additively commutative group `E`, and scalar multiplication `SMul 𝕜 E`, with a seminorm `p` on `E` and any elements `x` and `y` of `E` along with a real number `r`, the membership of `y` in the ball with radius `r` centered at `x` with respect to seminorm `p` is equivalent to the statement that the seminorm of the difference `(y - x)` is less than `r`. In simpler terms, `y` is in the ball of radius `r` around `x` if and only if the distance of `y` from `x`, measured by the seminorm `p`, is less than `r`. More concisely: For any seminormed ring 𝕜, additively commutative group E, and seminorm p on E, the element y belongs to the ball of radius r centered at x if and only if p(y - x) < r.
`Seminorm.balanced_closedBall_zero` theorem Seminorm.balanced_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) (r : ℝ), Balanced 𝕜 (p.closedBall 0 r) The theorem `Seminorm.balanced_closedBall_zero` states that for any seminormed ring `𝕜`, an additive commutative group `E`, and a `𝕜`-module structure on `E`, for any seminorm `p` on `𝕜` and `E`, and any real number `r`, the closed ball of radius `r` centered at the origin in the seminorm space is balanced. In other words, if we scale any element in the closed ball by a scalar whose norm is at most `1`, the result is still in the closed ball. More concisely: For any seminormed ring `𝕜`, additive commutative group `E` with a `𝕜`-module structure, seminorm `p` on `𝕜` and `E`, and real number `r`, the closed ball `{x ∈ E \| p(x) ≤ r}` in the seminorm space is balanced.
`Seminorm.convex_ball` theorem Seminorm.convex_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : NormedSpace ℝ 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : Module ℝ E] [inst_5 : IsScalarTower ℝ 𝕜 E] (p : Seminorm 𝕜 E) (x : E) (r : ℝ), Convex ℝ (p.ball x r) The theorem `Seminorm.convex_ball` asserts that for any normed field `𝕜`, additively commutative group `E`, and any real number `r`, the 'ball' in the seminorm `p` centered at a point `x` in `E` with radius `r` is a convex set. In particular, given the necessary structures of normed space, module, and scalar tower, this theorem generalizes the notion of convexity to seminorms, which can be seen as generalized norms in vector spaces. More concisely: For any normed field 𝕜, additively commutative group E, and real number r, the seminorm ball {x in E \| p(x - x0) ≤ r} in the seminorm p over E is a convex set.
`ball_normSeminorm` theorem ball_normSeminorm : ∀ (𝕜 : Type u_3) (E : Type u_7) [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E], (normSeminorm 𝕜 E).ball = Metric.ball The theorem `ball_normSeminorm` states that for any normed field `𝕜` and any seminormed additive commutative group `E` that is also a normed space over `𝕜`, the ball of a given radius at a specific point as defined by the norm seminorm of `E` is the same as the ball of the same radius at the same point as defined by the metric space structure of `E`. In other words, the sets of points within a certain distance from a given point, when measured using the seminorm or the metric, are the same. More concisely: For any normed field `𝕜` and seminormed additive commutative group `E` that is also a normed space over `𝕜`, the balls defined using the norm seminorm and the metric space structure of `E` are equal in radius and center.
`rescale_to_shell` theorem rescale_to_shell : ∀ {𝕜 : Type u_3} {F : Type u_10} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {c : 𝕜}, 1 < ‖c‖ → ∀ {ε : ℝ}, 0 < ε → ∀ {x : F}, x ≠ 0 → ∃ d, d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖ The theorem 'rescale_to_shell' states that in a normed space over a normed field, given a scalar `c` with its norm greater than 1, for any positive real number `ε` and any non-zero element `x`, there exists a scalar `d` such that `d` is not zero and the norm of the scaled vector `d•x` lies within the shell of width `ε` and also respects properties of the norm of the rescaling element `d` in relation to the scalar `c` and the norm of the vector `x`. This theorem is often used in applications where one needs to rescale elements to a certain range. More concisely: Given a normed space over a normed field, for any non-zero vector `x`, scalar `c` with norm greater than 1, and positive real number `ε`, there exists a non-zero scalar `d` such that the norm of `d•x` is within the shell of width `ε` around `c•x`.
`Seminorm.bound_of_shell` theorem Seminorm.bound_of_shell : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p q : Seminorm 𝕜 E) {ε C : ℝ}, 0 < ε → ∀ {c : 𝕜}, 1 < ‖c‖ → (∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x) → ∀ {x : E}, p x ≠ 0 → q x ≤ C * p x The theorem `Seminorm.bound_of_shell` states that given two seminorms `p` and `q` on a vector space over a nontrivially normed field, if we have the inequality `q x ≤ C * p x` holds on a shell defined by `{x \| ε/‖c‖ ≤ p x < ε}` where `ε` is positive and `‖c‖` is greater than 1, then this inequality also holds for all `x` such that `p x` is not zero. More concisely: If seminorms `p` and `q` satisfy `q x ≤ C p x` for all `x` in the shell `{x \| ε/��\|\|c��\|\| ≤ p x < ε}`, then `q x ≤ C * p x` for all non-zero `x`.*
`Seminorm.continuous_of_continuousAt_zero` theorem Seminorm.continuous_of_continuousAt_zero : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] {p : Seminorm 𝕝 E}, ContinuousAt (⇑p) 0 → Continuous ⇑p This theorem states that for any seminorm `p` on a semi-normed ring `𝕝` and an additive commutative group `E` that is also a `𝕝`-module with a topology compatible with the group structure, if the seminorm `p` is continuous at the zero element, then `p` is a continuous function. In other words, if for every sequence of elements in `E` that converges to zero, the corresponding sequence of their seminorms also converges to zero, then for every convergent sequence in `E`, the sequence of their seminorms is also convergent. More concisely: If a seminorm on a semi-normed ring is continuous at the zero element, then it is a continuous function on the associated topology of the compatible additive commutative group.
`Seminorm.uniformContinuous_of_forall` theorem Seminorm.uniformContinuous_of_forall : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : UniformSpace E] [inst_4 : UniformAddGroup E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.ball 0 r ∈ nhds 0) → UniformContinuous ⇑p This theorem states that, for a given seminorm `p` over a seminormed ring `𝕝` and an additive commutative group `E` that is also a module over `𝕝` (with `E` being a uniform space with a uniform additive group structure), if for every positive real number `r`, the ball of radius `r` centered at 0 under the seminorm `p` is a neighborhood of 0, then the function represented by the seminorm `p` is uniformly continuous. Uniform continuity, in this context, means that given any two points `x` and `y` in the space, if `x` and `y` are sufficiently close to each other, then the values `p(x)` and `p(y)` will also be close to each other, regardless of the actual locations of `x` and `y` in the space. It is worth noting that this condition is quite strong. In a nontrivially normed field, it is enough to check this condition for some positive `r`, not all, as stated in `Seminorm.uniformContinuous`. More concisely: If a seminorm over a seminormed ring on a uniform space with a uniform additive group structure satisfies the property that the ball of radius r around 0 is a neighborhood of 0 for every positive r, then the seminorm is uniformly continuous.
`Seminorm.continuousAt_zero_of_forall` theorem Seminorm.continuousAt_zero_of_forall : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.ball 0 r ∈ nhds 0) → ContinuousAt (⇑p) 0 The theorem `Seminorm.continuousAt_zero_of_forall` states that for any type 𝕝 and type E, where 𝕝 is a seminormed ring, E is an additive commutative group and also a 𝕝-module, and E has a topological space structure, if for a given seminorm p on 𝕝 and E, the ball with radius r around 0 under p is an element of the neighborhood filter of 0 for every positive r, then the seminorm p is continuous at 0. The context implies that the "ball" here refers to the set of all elements in E that have their p-norm less than r. This theorem also mentions that over a non-trivially normed field, it is enough to check this condition for just some positive r, which is the content of another theorem `Seminorm.continuousAt_zero'`. More concisely: If for a seminormed ring 𝕝 and its 𝕝-module E with topological space structure, the ball with radius r around 0 under the seminorm p is a neighborhood of 0 for every positive r, then p is continuous at 0. Over a non-trivially normed field, it's sufficient to check this condition for some positive r's.
`Seminorm.absorbent_ball` theorem Seminorm.absorbent_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} {x : E}, p x < r → Absorbent 𝕜 (p.ball x r) This theorem states that for any normed field '𝕜', additive commutative group 'E', and module '𝕜 E', and any seminorm 'p' on '𝕜 E', any 'r' in the real numbers, and any 'x' in 'E', if the seminorm of 'x' is less than 'r', then the seminorm-ball centered at 'x' with radius 'r' is absorbent. In simpler terms, it says that balls in the space, defined by the seminorm 'p' and containing the origin point, have the property of absorbing any single-point set, provided the seminorm of the point is less than the radius of the ball. More concisely: For any seminormed vector space (𝕜, E, p), any real number r, and any x in E with p(x) < r, the semiball B(x, r) = {y in E \| p(y - x) < r} absorbs the singleton {-x}.
`rescale_to_shell_semi_normed` theorem rescale_to_shell_semi_normed : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {c : 𝕜}, 1 < ‖c‖ → ∀ {ε : ℝ}, 0 < ε → ∀ {x : E}, ‖x‖ ≠ 0 → ∃ d, d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖ This theorem, `rescale_to_shell_semi_normed`, states that given a scalar `c` of a normed field `𝕜` with a norm greater than 1, and a non-zero element `x` from a semi-normed additive commutative group `E` over `𝕜`, for any real number `ε` greater than 0, there exists a non-zero scalar `d` such that the norm of `d` times `x` is less than `ε`, greater than or equal to `ε` divided by the norm of `c`, and the reciprocal of the norm of `d` is less than or equal to the reciprocal of `ε` times the norm of `c` times the norm of `x`. In simpler terms, this theorem states that any non-zero element can be rescaled to lie within any shell of width `‖c‖` where a shell in this context is a spherical layer between two concentric spheres. More concisely: Given a normed field `𝕜`, a non-zero element `x` from a semi-normed additive commutative group `E` over `𝕜`, a scalar `c` with norm greater than 1 in `𝕜`, and a real number `ε > 0`, there exists a non-zero scalar `d` such that `‖d * x‖ < ε` and `1 / (ε * ‖c‖ * ‖x‖) <= 1 / ‖d‖ <= 1 / (ε * ‖c‖)`.
`Seminorm.mem_closedBall_zero` theorem Seminorm.mem_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {y : E} {r : ℝ}, y ∈ p.closedBall 0 r ↔ p y ≤ r This theorem states that for any seminorm `p` on a seminormed ring `𝕜` acting on an additive commutative group `E`, any element `y` of `E` and any real number `r`, `y` belongs to the closed ball of radius `r` at `0` with respect to the seminorm `p` if and only if the seminorm of `y` is less than or equal to `r`. In more mathematical terms, `y` is in the closed ball centered at `0` with radius `r` under the seminorm `p` (denoted as `Seminorm.closedBall p 0 r`) if and only if `p(y) ≤ r`. More concisely: For any seminorm `p` on a seminormed ring `𝕜` and any additive commutative group `E`, an element `y` in `E` lies in the closed ball of radius `r` with respect to `p` if and only if `p(y) ≤ r`.
`Seminorm.absorbent_closedBall_zero` theorem Seminorm.absorbent_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ}, 0 < r → Absorbent 𝕜 (p.closedBall 0 r) This theorem states that for any normed field `𝕜`, any additive commutative group `E`, and any module `𝕜 E`, given a seminorm `p` on `𝕜 E` and a real number `r` greater than zero, the closed seminorm-ball centered at the origin with radius `r` is absorbent with respect to `𝕜`. In other words, every singleton set is absorbed by this closed seminorm-ball. More concisely: For any normed field `𝕜`, any additive commutative group `E` making `𝕜 E` a module, and any seminorm `p` on `𝕜 E` and real number `r > 0`, the closed semiball `{x ∈ 𝕜 E \| p(x) ≤ r}` centered at the origin is absorbent in `𝕜`, i.e., for all `x, y ∈ 𝕜 E`, there exists a real number `s > 0` such that `x + y` is in the closed semiball when `s * \|x\| ≤ r`.
`Seminorm.bound_of_shell_smul` theorem Seminorm.bound_of_shell_smul : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p q : Seminorm 𝕜 E) {ε : ℝ} {C : NNReal}, 0 < ε → ∀ {c : 𝕜}, 1 < ‖c‖ → (∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ (C • p) x) → ∀ {x : E}, p x ≠ 0 → q x ≤ (C • p) x This theorem, named `Seminorm.bound_of_shell_smul`, states that for any normed field `𝕜`, any additive commutative group `E`, and any module `𝕜 E`, given two seminorms `p` and `q` on `E`, a real number `ε` greater than 0, an element `c` of `𝕜` such that its norm is greater than 1, and a nonnegative real number `C`, if for every element `x` of `E`, whenever the seminorm `p` of `x` is between `ε / ‖c‖` and `ε`, the seminorm `q` of `x` is less than or equal to `C` times the seminorm `p` of `x`, then for every element `x` of `E` not annihilated by `p`, the seminorm `q` of `x` is less than or equal to `C` times the seminorm `p` of `x`. This is a version of the `Seminorm.bound_of_shell` theorem, expressed using pointwise scalar multiplication of seminorms. More concisely: If for all x in a normed vector space E and for all ε > 0, whenever the seminorm p of x satisfies ε / \|\|c\|\| < p(x) < ε, then q(cx) ≤ C * p(x) for all nonzero x in E, where q is another seminorm on E, c is a nonzero scalar in the field, and C is a nonnegative real number.
`absorbent_ball` theorem absorbent_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ} {x : E}, ‖x‖ < r → Absorbent 𝕜 (Metric.ball x r) This theorem states that for any normed field '𝕜' and any semi-normed add commutative group 'E' which is also a normed space over '𝕜', for any real number 'r' and any element 'x' of 'E', if the norm of 'x' is less than 'r', then the open ball with center 'x' and radius 'r' in the metric space is an absorbent set in '𝕜'. In other words, the open ball centered at 'x' and of radius 'r' absorbs every singleton in the normed field '𝕜'. This open ball is defined as the set of all points 'y' such that the distance between 'y' and 'x' is less than 'r'. More concisely: For any normed field '𝕜' and semi-normed add commutative group 'E' over '𝕜' that is also a normed space, the open ball with center 'x' in 'E' and radius 'r' in the metric space absorbs every singleton in '𝕜' when the norm of 'x' in 'E' is less than 'r'.
`Seminorm.mem_ball` theorem Seminorm.mem_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {x y : E} {r : ℝ}, y ∈ p.ball x r ↔ p (y - x) < r The theorem `Seminorm.mem_ball` states that for any seminormed ring `𝕜`, any additive commutative group `E` and any scalar multiplication of `𝕜` and `E`, with a given seminorm `p` on `E`, an element `y` of `E`, a center `x` in `E`, and a radius `r` in real numbers, `y` is in the ball of radius `r` at `x` with respect to seminorm `p` if and only if the seminorm of the difference between `y` and `x` is less than `r`. In other words, it characterizes the elements of a ball in a seminorm space. More concisely: For any seminormed ring 𝕜, additive commutative group E, and scalar multiplication, an element y of E belongs to the ball of radius r at x in the seminormed space (E, p) if and only if p(y - x) < r.
`Seminorm.ext` theorem Seminorm.ext : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E] {p q : Seminorm 𝕜 E}, (∀ (x : E), p x = q x) → p = q This theorem states that given any two seminorms `p` and `q` on a vector space `E` over a seminormed ring `𝕜`, if for every `x` in `E`, `p(x)` equals `q(x)`, then `p` and `q` are the same seminorm. The essential idea is that two seminorms are identical if they assign the same seminorm value to every vector in the space. More concisely: If two seminorms on a vector space over a seminormed ring assign the same value to every vector, then they are equal.
`Seminorm.smul'` theorem Seminorm.smul' : ∀ {𝕜 : Type u_13} {E : Type u_14} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E] (self : Seminorm 𝕜 E) (a : 𝕜) (x : E), self.toFun (a • x) = ‖a‖ * self.toFun x This theorem states that for any scalar `a` of type `𝕜` from a seminormed ring and any element `x` of an additive group `E` that is also a scalar multiple, the seminorm of the scalar multiplication `a` times `x` is equal to the product of the absolute value (or norm) of `a` and the seminorm of `x`. In mathematical terms, this can be written as ‖a•x‖ = \|a\| * ‖x‖, where ‖•‖ represents the seminorm. More concisely: For any scalar `a` in a seminormed ring and any element `x` in an additive group, the seminorm of the scalar multiplication `a` times `x` equals the product of the absolute value of `a` and the seminorm of `x`. In Lean notation, `‖a • x‖ = \|a\| * ‖x‖`.
`Seminorm.continuousAt_zero_of_forall'` theorem Seminorm.continuousAt_zero_of_forall' : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.closedBall 0 r ∈ nhds 0) → ContinuousAt (⇑p) 0 The theorem `Seminorm.continuousAt_zero_of_forall'` states that a seminorm, denoted as `p`, is continuous at `0` if the closed ball of any radius `r` greater than `0` centered at `0` with respect to seminorm `p` is a neighborhood of `0`. This is applicable in the context of a seminormed ring `𝕝` and a topological space `E` that is also an additive commutative group and an `𝕝`-module. More precisely, a seminorm `p` is continuous at `0` if for every real number `r` greater than `0`, the set of elements `y` in `E` such that the seminorm of `y - 0` is less than or equal to `r` belongs to the neighborhood filter at `0`. Over a `NontriviallyNormedField`, it is sufficient to check this condition for some `r` greater than `0`, as stated in `Seminorm.continuousAt_zero'`. More concisely: A seminorm `p` on an additive commutative group and `𝕝`-module `E` is continuous at `0` if for every `r` > 0, the closed ball `B(0, r)` with respect to `p` is a neighborhood of `0`.
`Seminorm.mem_ball_zero` theorem Seminorm.mem_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {y : E} {r : ℝ}, y ∈ p.ball 0 r ↔ p y < r The theorem `Seminorm.mem_ball_zero` states that for any seminorm `p` over a seminormed ring `𝕜` and an additive commutative group `E` that forms a scalar multiplication system with `𝕜`, an element `y` from `E` belongs to the ball of radius `r` at `0` (with respect to seminorm `p`) if and only if the seminorm of `y` is less than `r`. In simpler terms, `y` lies within the `r`-radius ball centered at zero under seminorm `p` if the `p`-seminorm of `y` is less than `r`. More concisely: For any seminorm `p` over a seminormed ring `𝕜` and an additive commutative group `E`, an element `y` from `E` lies within the `r`-radius ball centered at zero under `p` if and only if `p(y) < r`.
`Mathlib.Analysis.Seminorm._auxLemma.22` theorem Mathlib.Analysis.Seminorm._auxLemma.22 : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t u : Set β}, (s • t ⊆ u) = ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u The theorem `Mathlib.Analysis.Seminorm._auxLemma.22` states that for any types `α` and `β`, given a scalar multiplication operation on `β` by elements of `α` and three sets, `s` of type `α` and `t` and `u` of type `β`, the condition that the scalar multiplication of every element of `s` with every element of `t` falls within the set `u` (represented as `s • t ⊆ u`) is equivalent to the statement that for every element `a` in `s` and every element `b` in `t`, the result of `a` scaling `b` is an element of `u`. In other words, the set of all scalar multiples `a • b` where `a` is from `s` and `b` is from `t` is a subset of `u` if and only if every such scalar multiple `a • b` is an element of `u`. More concisely: For sets $s \subseteq \alpha, t \subseteq \beta$, the condition that $a \cdot b \in u$ for all $a \in s$ and $b \in t$ is equivalent to $s \cdot t \subseteq u$, where $s \cdot t = \{ a \cdot b \mid a \in s, b \in t \}$.
`Seminorm.continuous_of_forall'` theorem Seminorm.continuous_of_forall' : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.closedBall 0 r ∈ nhds 0) → Continuous ⇑p This theorem states that a seminorm is continuous if the closed ball around 0 of radius `r` is in the neighborhood of 0 for all `r` greater than 0. It implies that, over a NontriviallyNormedField, it is sufficient to check this condition for some `r` rather than for all `r`. The theorem is defined for any type `𝕝` that is a seminormed ring, any type `E` that is an additive commutative group and a module over `𝕝`, and where `E` has a topological structure and is a topological additive group. The seminorm `p` over `𝕝` and `E` is continuous if for every `r` greater than 0, the closed ball of `p` with center 0 and radius `r` is in the neighborhood of 0. More concisely: A seminorm on a seminormed ring is continuous if and only if the closed ball around the origin with radius greater than 0 is a neighborhood of the origin.
`Mathlib.Analysis.Seminorm._auxLemma.16` theorem Mathlib.Analysis.Seminorm._auxLemma.16 : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] {a : E} {r : ℝ}, (a ∈ Metric.closedBall 0 r) = (‖a‖ ≤ r) This theorem states that for any type `E` that forms a semi-normed add group, and any element `a` of this type and real number `r`, the element `a` belongs to the closed ball centered at 0 with radius `r` in the pseudo metric space defined by the distance function if and only if the semi-norm of `a` is less than or equal to `r`. In mathematical notation, this could be expressed as $a \in B[0,r] \iff \\|a\\| \leq r$. More concisely: For any semi-normed add group `E` and real number `r`, an element `a` in `E` belongs to the closed ball `B[0,r]` if and only if the semi-norm of `a` is less than or equal to `r`. In symbols: $a \in B[0,r] \iff \\|a\\| \leq r$.
`Seminorm.convex_closedBall` theorem Seminorm.convex_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : NormedSpace ℝ 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : Module ℝ E] [inst_5 : IsScalarTower ℝ 𝕜 E] (p : Seminorm 𝕜 E) (x : E) (r : ℝ), Convex ℝ (p.closedBall x r) The theorem `Seminorm.convex_closedBall` states that for any normed field `𝕜`, add commutative group `E`, where `𝕜` and `E` are also equipped with a normed space structure over the real numbers, ℝ, and `E` is a module over both `𝕜` and `ℝ` (with `ℝ` acting on `𝕜` and the action of `𝕜` on `E` extending the action of `ℝ`), for any seminorm `p` on `E` over the field `𝕜`, any element `x` of `E`, and any real number `r`, the closed ball in `E` centered at `x` with radius `r` under the seminorm `p` is a convex set. In simpler terms, for any point and radius, the set of all points whose distance under the seminorm to the fixed point is no more than the given radius, is a convex set. More concisely: For any normed field `𝕜`, add commutative group `E` with a normed space structure over the real numbers, and any seminorm `p` on `E` over `𝕜`, the closed ball in `E` under `p` is a convex set.
`Seminorm.convexOn` theorem Seminorm.convexOn : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : NormedSpace ℝ 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : SMul ℝ E] [inst_5 : IsScalarTower ℝ 𝕜 E] (p : Seminorm 𝕜 E), ConvexOn ℝ Set.univ ⇑p This theorem states that for any given seminorm `p` on a normed space over a normed field `𝕜` with additive commutative group structure `E` (where `𝕜` has a real normed space structure, `E` has a `𝕜`-module structure, ℝ acts on `E` by scalar multiplication, and ℝ is a subfield of `𝕜`), the seminorm `p` is convex on the entire space. In other words, for any two elements `x` and `y` in the universal set (which contains all elements of `E`), any weighted average of `p(x)` and `p(y)` is greater than or equal to `p` applied to the corresponding weighted average of `x` and `y`, where the weights are nonnegative real numbers summing to one. This is a property associated with the convexity of functions. More concisely: Given a seminorm `p` on a real normed vector space `E` over a normed field `𝕜`, `p` is convex, i.e., for all `x, y ∈ E` and nonnegative real numbers `α, β` with `α + β = 1`, `p(αx + βy) ≤ αp(x) + βp(y)`.
`Mathlib.Analysis.Seminorm._auxLemma.23` theorem Mathlib.Analysis.Seminorm._auxLemma.23 : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {y : E} {r : ℝ}, (y ∈ p.ball 0 r) = (p y < r) The theorem `Mathlib.Analysis.Seminorm._auxLemma.23` states that for any seminorm `p` on a seminormed ring `𝕜` acting on an additive commutative group `E` and for any element `y` from `E` and any real number `r`, `y` is in the seminorm ball centered at the origin with radius `r` if and only if the seminorm of `y` is less than `r`. In other words, it's a characterization of the seminorm ball in terms of the seminorm of elements. More concisely: For any seminorm `p` on a seminormed ring `𝕜` over an additive commutative group `E`, an element `y` in `E` lies in the seminorm ball centered at the origin with radius `r` if and only if `p(y) < r`.
`Seminorm.ball_zero_eq` theorem Seminorm.ball_zero_eq : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ}, p.ball 0 r = {y \| p y < r} The theorem `Seminorm.ball_zero_eq` states that for any seminorm `p` on a scalar multiplication structure `SMul` over an additive commutative group `E` and a seminormed ring `𝕜`, and for any real number `r`, the ball of radius `r` at `0` with respect to seminorm `p` is equal to the set of all elements `y` in `E` such that `p y < r`. In geometrical terms, this describes the set of all points in the space `E` that are less than a given distance `r` from the origin, according to the particular measure of distance given by the seminorm `p`. More concisely: For any seminorm `p` on a scalar multiplication structure `SMul` over an additive commutative group `E` and a seminormed ring `𝕜`, the ball of radius `r` centered at `0` with respect to `p` equals the set of elements `y` in `E` satisfying `p(y) < r`.
`Seminorm.rescale_to_shell_zpow` theorem Seminorm.rescale_to_shell_zpow : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) {c : 𝕜}, 1 < ‖c‖ → ∀ {ε : ℝ}, 0 < ε → ∀ {x : E}, p x ≠ 0 → ∃ n, c ^ n ≠ 0 ∧ p (c ^ n • x) < ε ∧ ε / ‖c‖ ≤ p (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x This theorem states that given a seminorm `p` on a vector space over a `NormedField`, if there exists a scalar 'c' such that the norm of 'c' is greater than 1, then for any non-zero vector 'x', it is possible to scale 'x' by 'c' raised to some power 'n' to land it within any desired 'p'-shell of width equal to the norm of 'c'. More specifically, for any given positive real number 'ε', there exists an integer 'n' such that 'c' to the power 'n' is non-zero and the seminorm of the scaled vector is less than 'ε', greater than or equal to 'ε' divided by the norm of 'c', and the reciprocal of the norm of 'c' to the power 'n' is less than or equal to the reciprocal of 'ε' times the norm of 'c' times the seminorm of 'x'. This theorem also contains useful information about the value of the seminorm on the rescaled vector, which is often useful in applications. More concisely: Given a seminorm `p` on a vector space over a NormedField and a scalar `c` with norm greater than 1, for any non-zero vector `x` and positive real `ε`, there exists an integer `n` such that `c^n * x` lies in the `p`-shell of width `ε` around the origin and satisfies `\|c\|^n * \|p(x)\| <= ε * \|p(c^n * x)\|`.
`balanced_ball_zero` theorem balanced_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ}, Balanced 𝕜 (Metric.ball 0 r) This theorem states that for any normed field `𝕜` and for any seminormed additive commutative group `E` with a normed space structure over `𝕜`, and for any real number `r`, the metric ball centered at the origin with radius `r` is a balanced set. In other words, any scalar multiple `a` of the ball, where `a` is a member of `𝕜` with a norm less than or equal to `1`, is a subset of the ball itself. More concisely: For any normed field `𝕜` and seminormed additive commutative group `E` with a normed space structure over `𝕜`, the open metric ball with radius `r` and center at the origin is a balanced set.
`Seminorm.mem_closedBall` theorem Seminorm.mem_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {x y : E} {r : ℝ}, y ∈ p.closedBall x r ↔ p (y - x) ≤ r The theorem `Seminorm.mem_closedBall` states that for all seminormed rings `𝕜`, and for all additive commutative groups `E` with scalar multiplication by `𝕜`, for any seminorm `p` on `E`, for all elements `x`, `y` of `E` and for all real numbers `r`, the element `y` belongs to the closed ball of radius `r` at `x` with respect to the seminorm `p` if and only if the seminorm of the difference between `y` and `x` is less than or equal to `r`. It's essentially a restatement of the definition of a closed ball in a seminormed vector space, specifying the condition that must hold for an element to be included in a closed ball. More concisely: For any seminormed ring `𝕜` and additive commutative group `E` with scalar multiplication by `𝕜`, and for any seminorm `p` on `E`, an element `y` belongs to the closed ball of radius `r` around `x` in `E` with respect to `p` if and only if `p(x - y) ≤ r`.
`Seminorm.absorbent_closedBall` theorem Seminorm.absorbent_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} {x : E}, p x < r → Absorbent 𝕜 (p.closedBall x r) This theorem states that for any normed field `𝕜`, additive commutative group `E`, and module over `𝕜` and `E`, given a seminorm `p` on `E` and a real number `r`, any element `x` in `E` whose seminorm is less than `r` is absorbed by the closed ball centred at `x` with radius `r` under the seminorm `p`. In other words, seminorm-closed balls that contain the origin are absorbent. More concisely: For any seminorm `p` on a normed vector space `(𝕜, E)`, and real number `r`, every element `x` in `E` with `p(x) < r` is absorbed by the closed ball `B(x, r)` under `p`.
`Seminorm.uniformContinuous_of_continuousAt_zero` theorem Seminorm.uniformContinuous_of_continuousAt_zero : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : UniformSpace E] [inst_4 : UniformAddGroup E] {p : Seminorm 𝕝 E}, ContinuousAt (⇑p) 0 → UniformContinuous ⇑p The theorem `Seminorm.uniformContinuous_of_continuousAt_zero` states that for any type `𝕝` that forms a seminormed ring, and any type `E` that forms an additive commutative group, a module over `𝕝`, a uniform space, and a uniform additive group, given a seminorm `p` on `E` over `𝕝`, if the seminorm `p` is continuous at zero, then `p` is uniformly continuous. In other words, if the value of `p` tends to `p(0)` when its input tends to `0`, then for any two points in `E` that are sufficiently close to each other, the values of `p` at these two points are also close, regardless of their location in `E`. More concisely: If a seminorm on a module over a seminormed ring is continuous at zero, then it is uniformly continuous.
`Seminorm.absorbent_ball_zero` theorem Seminorm.absorbent_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ}, 0 < r → Absorbent 𝕜 (p.ball 0 r) The theorem `Seminorm.absorbent_ball_zero` states that for any seminorm `p` and any positive real number `r`, the seminorm ball of radius `r` centered at the origin is an absorbent set. Here, a set is said to be absorbent if it "absorbs" every singleton, i.e., for every element `x`, there is a scalar `m` such that `m * x` is in the set. The seminorm ball of radius `r` at the origin is the set of all elements `y` such that the seminorm of `y - 0` (i.e., `y` itself) is less than `r`. More concisely: For any seminorm `p` and positive real number `r`, the seminorm ball of radius `r` centered at the origin is an absorbent set. In other words, for all `x`, there exists a scalar `m` such that `m * x` belongs to the seminorm ball of `x` with radius `r`.
`rescale_to_shell_semi_normed_zpow` theorem rescale_to_shell_semi_normed_zpow : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {c : 𝕜}, 1 < ‖c‖ → ∀ {ε : ℝ}, 0 < ε → ∀ {x : E}, ‖x‖ ≠ 0 → ∃ n, c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖ This theorem states that for any scalar `c` with a norm greater than 1 (`‖c‖>1`), there is a way to rescale any non-zero element in a seminormed addition commutative group `E` (over a normed field `𝕜`) to fit into any given "shell" of width `ε` (where `ε` is a positive real number). More specifically, it asserts that there exists an integer `n` such that, when the scalar `c` is raised to the power `n` and this value is used to scale the vector `x`, the norm of the rescaled vector lies within the shell and satisfies certain inequalities involving the norm of the rescaling factor and the original vector. The theorem also emphasizes that the rescaling factor `c ^ n` is non-zero, which is important in applications where the scaling factor must be invertible. More concisely: For any non-zero element `x` in a seminormed addition commutative group `E` over a normed field `𝕜`, and any positive real number `ε` and scalar `c` with `‖c‖ > 1`, there exists an integer `n` such that `‖c ^ n * x‖ ≤ ε * ‖x‖` and `‖c ^ n‖ > 1`.
`SeminormClass.map_smul_eq_mul` theorem SeminormClass.map_smul_eq_mul : ∀ {F : Type u_13} {𝕜 : outParam (Type u_14)} {E : outParam (Type u_15)} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E] [inst_3 : FunLike F E ℝ] [self : SeminormClass F 𝕜 E] (f : F) (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x This theorem states that for any seminorm `f`, scalar `a`, and vector `x`, the seminorm of the scalar multiplication of `a` and `x` is equal to the product of the absolute value of `a` and the seminorm of `x`. It applies in the context where `𝕜` is a seminormed ring, `E` is an additive group which also supports scalar multiplication by `𝕜`, and `F` is a type that behaves like a function from `E` to the reals (`ℝ`). The theorem is a property of `SeminormClass`, which represents a seminorm on a space `E` over a normed field `𝕜` with codomain type `F`. More concisely: For any seminorm `f` on a seminormed ring `𝕜`, vector `x`, and scalar `a`, the seminorm of the scalar multiplication `a x` equals the product of the absolute value of `a` and the seminorm of `x`.*
`Seminorm.vadd_ball` theorem Seminorm.vadd_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {x y : E} {r : ℝ} (p : Seminorm 𝕜 E), x +ᵥ p.ball y r = p.ball (x +ᵥ y) r This theorem states that for any given seminormed ring 𝕜, additive commutative group E, and scalar multiplication operation over 𝕜 and E, if you take a ball in the seminormed space centered at some point 'y' with radius 'r', and translate every point in the ball by adding a fixed point 'x', the resulting set is the same as the ball centered at 'x + y' with radius 'r'. In other words, translating a ball in a seminormed space is equivalent to moving the center of the ball by the same vector. More concisely: For any seminormed space (𝕜, E, ⋅), given a point 'x' in E and a ball B(y, r) in E centered at 'y' with radius 'r', translated ball x + B(y, r) = B(x + y, r).
`Seminorm.ball_subset_closedBall` theorem Seminorm.ball_subset_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) (x : E) (r : ℝ), p.ball x r ⊆ p.closedBall x r The theorem `Seminorm.ball_subset_closedBall` states that for any seminorm `p` on a type `E` over a seminormed ring `𝕜`, any point `x` in `E`, and any real number `r`, the ball of radius `r` centered at `x` with respect to `p` is a subset of the closed ball of the same radius and center. In other words, all the points `y` that satisfy `p (y - x) < r` also satisfy `p (y - x) ≤ r`. More concisely: For every seminorm `p` on a type `E` over a seminormed ring `𝕜`, every point `x` in `E`, and every real number `r`, the open ball `{y : E \| p(y - x) < r}` is contained in the closed ball `{y : E \| p(y - x) ≤ r}`.
`Seminorm.smul_apply` theorem Seminorm.smul_apply : ∀ {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E] [inst_3 : SMul R ℝ] [inst_4 : SMul R NNReal] [inst_5 : IsScalarTower R NNReal ℝ] (r : R) (p : Seminorm 𝕜 E) (x : E), (r • p) x = r • p x This theorem, `Seminorm.smul_apply`, states that for any seminormed ring `𝕜`, add group `E`, and types `R`, `𝕜` and `E` with scalar multiplication (`SMul`) defined between them, the application of a scalar `r` from `R` to the seminorm `p` of the element `x` from `E` is equal to the scalar multiplication of `r` and the seminorm `p` of `x`. In other words, it asserts that scalar multiplication commutes with the seminorm operation. The `IsScalarTower R NNReal ℝ` instance indicates that scalar multiplication is associative between `R`, nonnegative real numbers (`NNReal`), and real numbers (`ℝ`). More concisely: For any seminormed ring `𝕜`, add group `E`, and types `R`, `𝕜`, and `E` with scalar multiplication, the scalar multiplication of `r` in `R` by the seminorm `p` of `x` in `E` is equal to the seminorm of the scalar multiplication of `r` and `x` in `E`.
`Seminorm.continuous_of_forall` theorem Seminorm.continuous_of_forall : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.ball 0 r ∈ nhds 0) → Continuous ⇑p This theorem states that for a given seminorm `p` on a seminormed ring `𝕝` and a module `E` with associated topological space and topological add group structures, if for every positive `r`, the open ball centered at `0` with radius `r` in the seminorm is a neighborhood of `0`, then the function defined by the seminorm is continuous. Over a `NontriviallyNormedField`, it is sufficient to verify this condition for some positive `r` as claimed by `Seminorm.continuous`. More concisely: If for every positive radius `r` in a seminormed ring `𝕝` and its associated topological space, the open ball of radius `r` centered at `0` is a neighborhood of `0`, then the seminorm function is continuous.
`Seminorm.balanced_ball_zero` theorem Seminorm.balanced_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) (r : ℝ), Balanced 𝕜 (p.ball 0 r) The theorem `Seminorm.balanced_ball_zero` states that for any seminormed ring `𝕜`, an additive commutative group `E`, a module structure over `E` with `𝕜` as the scalar, a seminorm `p` on `E` over `𝕜`, and a real number `r`, the seminorm ball with radius `r` centered at the origin is a balanced set. In other words, if any scalar `a` from `𝕜` has a norm less than or equal to 1, then scaling the seminorm ball by `a` remains within the original seminorm ball. More concisely: For any seminormed ring `𝕜`, group `E` with a module structure over `𝕜`, seminorm `p` on `E` over `𝕜`, and real number `r`, the seminorm ball `{x : E \| p x ≤ r}` centered at the origin is a balanced set, i.e., for all scalars `a` in `𝕜` with `\|a\| ≤ 1`, the scaled set `{x : E \| p(ax) ≤ r}` is contained in the original seminorm ball.
`Seminorm.uniformContinuous_of_forall'` theorem Seminorm.uniformContinuous_of_forall' : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : UniformSpace E] [inst_4 : UniformAddGroup E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.closedBall 0 r ∈ nhds 0) → UniformContinuous ⇑p The theorem `Seminorm.uniformContinuous_of_forall'` states that for any seminorm `p` on an additive commutative group `E` that is a module over a seminormed ring `𝕝`, if for all `r > 0`, the closed ball centered at `0` with radius `r` under the seminorm `p` is a neighborhood of `0` (i.e., contains an open set around `0`), then the function that applies `p` is uniformly continuous. In other words, given any two points `x` and `y` in `E` that are sufficiently close, the seminorm values `p(x)` and `p(y)` are also close, regardless of the actual location of `x` and `y` in `E`. This theorem is true in the context of a uniform space `E` that also forms a uniform additive group. Note that this theorem provides a necessary condition for the uniform continuity of a seminorm. It's also stated that for a non-trivially normed field, it is sufficient to check this condition for some `r > 0`, not necessarily for all `r > 0`, as detailed in `Seminorm.uniformContinuous'`. More concisely: If a seminorm on an additive commutative group that is a module over a seminormed ring satisfies the property that for some positive radius, the closed ball centered at zero under the seminorm is a neighborhood of zero, then the seminorm function is uniformly continuous.
`Seminorm.rescale_to_shell` theorem Seminorm.rescale_to_shell : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) {c : 𝕜}, 1 < ‖c‖ → ∀ {ε : ℝ}, 0 < ε → ∀ {x : E}, p x ≠ 0 → ∃ d, d ≠ 0 ∧ p (d • x) < ε ∧ ε / ‖c‖ ≤ p (d • x) ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x The theorem `Seminorm.rescale_to_shell` states that for a given seminorm `p` on a vector space over a NormedField, if there exist a scalar `c` where the norm of `c` is greater than 1, then any vector `x` in the vector space that does not belong to the null space of the seminorm, can be rescaled to any `p`-shell of width `‖c‖`. This rescaling element and its properties are important in applications. Specifically, for any positive real number `ε`, there exists a scalar `d` that is not zero, and it rescales the vector `x` in such a way that the seminorm `p` of the rescaled vector is less than `ε` and at least `ε` divided by the norm of `c`, and the reciprocal of the norm of `d` is less than or equal to the reciprocal of `ε` times the norm of `c` times the seminorm `p` of `x`. More concisely: Given a seminorm `p` on a vector space over a NormedField and a scalar `c` with norm greater than 1, there exists a scalar `d` and a vector `y = dx` such that `p(y) < ε` and `p(y) > ε/‖c‖,` and the reciprocal of `d` is bounded by `ε/‖c‖ * p(x)`.
`absorbent_ball_zero` theorem absorbent_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ}, 0 < r → Absorbent 𝕜 (Metric.ball 0 r) This theorem states that for any normed field `𝕜`, seminormed additive commutative group `E`, and normed space over `𝕜` and `E`, any ball centered at the origin with a positive radius `r` is an absorbent set. In other words, for every point `x` in the normed space, there exists a scalar in `𝕜` such that multiplying `x` by this scalar will result in a point inside the specified ball. This is a fundamental property in analysis and is often used in proofs related to boundedness and compactness. More concisely: For any normed field `𝕜`, seminormed additive commutative group `E`, and normed space `X` over `𝕜` and `E`, the open ball of radius `r` around the origin in `X` is absorbent.
`Seminorm.bddBelow_range_add` theorem Seminorm.bddBelow_range_add : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p q : Seminorm 𝕜 E} {x : E}, BddBelow (Set.range fun u => p u + q (x - u)) The theorem `Seminorm.bddBelow_range_add` states that for any types 𝕜 and E, where 𝕜 is a normed field and E is an additive commutative group which is also a 𝕜-module, and for any seminorms p and q on E, and any element x of E, the range of the function that maps any u to the sum of the application of p on u and q on the difference of x and u, is bounded below. In simpler terms, it asserts that there is a lower bound for the set of values obtained by applying the function `u => p u + q (x - u)` for all u. More concisely: For any normed field 𝕜, additive commutative group and 𝕜-module E, seminorms p and q on E, and element x in E, the function that maps u to p(u) + q(x - u) is bounded below on E.

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Seminorm

Seminorm.continuousAt_zero'

Seminorm.vadd_closedBall

theorem Seminorm.vadd_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {x y : E} {r : ℝ} (p : Seminorm 𝕜 E), x +ᵥ p.closedBall y r = p.closedBall (x +ᵥ y) r

Mathlib.Analysis.Seminorm._auxLemma.6

theorem Mathlib.Analysis.Seminorm._auxLemma.6 : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {x y : E} {r : ℝ}, (y ∈ p.ball x r) = (p (y - x) < r)

Seminorm.balanced_closedBall_zero

theorem Seminorm.balanced_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) (r : ℝ), Balanced 𝕜 (p.closedBall 0 r)

Seminorm.convex_ball

ball_normSeminorm

theorem ball_normSeminorm : ∀ (𝕜 : Type u_3) (E : Type u_7) [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E], (normSeminorm 𝕜 E).ball = Metric.ball

rescale_to_shell

Seminorm.bound_of_shell

Seminorm.continuous_of_continuousAt_zero

theorem Seminorm.continuous_of_continuousAt_zero : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] {p : Seminorm 𝕝 E}, ContinuousAt (⇑p) 0 → Continuous ⇑p

Seminorm.uniformContinuous_of_forall

Seminorm.continuousAt_zero_of_forall

theorem Seminorm.continuousAt_zero_of_forall : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.ball 0 r ∈ nhds 0) → ContinuousAt (⇑p) 0

Seminorm.absorbent_ball

theorem Seminorm.absorbent_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} {x : E}, p x < r → Absorbent 𝕜 (p.ball x r)

rescale_to_shell_semi_normed

Seminorm.mem_closedBall_zero

theorem Seminorm.mem_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {y : E} {r : ℝ}, y ∈ p.closedBall 0 r ↔ p y ≤ r

Seminorm.absorbent_closedBall_zero

theorem Seminorm.absorbent_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ}, 0 < r → Absorbent 𝕜 (p.closedBall 0 r)

Seminorm.bound_of_shell_smul

absorbent_ball

theorem absorbent_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ} {x : E}, ‖x‖ < r → Absorbent 𝕜 (Metric.ball x r)

Seminorm.mem_ball

theorem Seminorm.mem_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {x y : E} {r : ℝ}, y ∈ p.ball x r ↔ p (y - x) < r

Seminorm.ext

theorem Seminorm.ext : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E] {p q : Seminorm 𝕜 E}, (∀ (x : E), p x = q x) → p = q

Seminorm.smul'

theorem Seminorm.smul' : ∀ {𝕜 : Type u_13} {E : Type u_14} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E] (self : Seminorm 𝕜 E) (a : 𝕜) (x : E), self.toFun (a • x) = ‖a‖ * self.toFun x

Seminorm.continuousAt_zero_of_forall'

theorem Seminorm.continuousAt_zero_of_forall' : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.closedBall 0 r ∈ nhds 0) → ContinuousAt (⇑p) 0

Seminorm.mem_ball_zero

theorem Seminorm.mem_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {y : E} {r : ℝ}, y ∈ p.ball 0 r ↔ p y < r

Mathlib.Analysis.Seminorm._auxLemma.22

theorem Mathlib.Analysis.Seminorm._auxLemma.22 : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t u : Set β}, (s • t ⊆ u) = ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u

Seminorm.continuous_of_forall'

Mathlib.Analysis.Seminorm._auxLemma.16

theorem Mathlib.Analysis.Seminorm._auxLemma.16 : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] {a : E} {r : ℝ}, (a ∈ Metric.closedBall 0 r) = (‖a‖ ≤ r)

Seminorm.convex_closedBall

Seminorm.convexOn

theorem Seminorm.convexOn : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : NormedSpace ℝ 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : SMul ℝ E] [inst_5 : IsScalarTower ℝ 𝕜 E] (p : Seminorm 𝕜 E), ConvexOn ℝ Set.univ ⇑p

Mathlib.Analysis.Seminorm._auxLemma.23

theorem Mathlib.Analysis.Seminorm._auxLemma.23 : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {y : E} {r : ℝ}, (y ∈ p.ball 0 r) = (p y < r)

Seminorm.ball_zero_eq

theorem Seminorm.ball_zero_eq : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ}, p.ball 0 r = {y | p y < r}

Seminorm.rescale_to_shell_zpow

balanced_ball_zero

theorem balanced_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ}, Balanced 𝕜 (Metric.ball 0 r)

Seminorm.mem_closedBall

theorem Seminorm.mem_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) {x y : E} {r : ℝ}, y ∈ p.closedBall x r ↔ p (y - x) ≤ r

Seminorm.absorbent_closedBall

theorem Seminorm.absorbent_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} {x : E}, p x < r → Absorbent 𝕜 (p.closedBall x r)

Seminorm.uniformContinuous_of_continuousAt_zero

Seminorm.absorbent_ball_zero

theorem Seminorm.absorbent_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ}, 0 < r → Absorbent 𝕜 (p.ball 0 r)

rescale_to_shell_semi_normed_zpow

SeminormClass.map_smul_eq_mul

Seminorm.vadd_ball

theorem Seminorm.vadd_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {x y : E} {r : ℝ} (p : Seminorm 𝕜 E), x +ᵥ p.ball y r = p.ball (x +ᵥ y) r

Seminorm.ball_subset_closedBall

theorem Seminorm.ball_subset_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] (p : Seminorm 𝕜 E) (x : E) (r : ℝ), p.ball x r ⊆ p.closedBall x r

Seminorm.smul_apply

Seminorm.continuous_of_forall

theorem Seminorm.continuous_of_forall : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.ball 0 r ∈ nhds 0) → Continuous ⇑p

Seminorm.balanced_ball_zero

theorem Seminorm.balanced_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (p : Seminorm 𝕜 E) (r : ℝ), Balanced 𝕜 (p.ball 0 r)

Seminorm.uniformContinuous_of_forall'

Seminorm.rescale_to_shell

absorbent_ball_zero

theorem absorbent_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ}, 0 < r → Absorbent 𝕜 (Metric.ball 0 r)

Seminorm.bddBelow_range_add

theorem Seminorm.bddBelow_range_add : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p q : Seminorm 𝕜 E} {x : E}, BddBelow (Set.range fun u => p u + q (x - u))

`Seminorm.continuousAt_zero'`

`Seminorm.vadd_closedBall`

`Mathlib.Analysis.Seminorm._auxLemma.6`

`Seminorm.balanced_closedBall_zero`

`Seminorm.convex_ball`

`ball_normSeminorm`

`rescale_to_shell`

`Seminorm.bound_of_shell`

`Seminorm.continuous_of_continuousAt_zero`

`Seminorm.uniformContinuous_of_forall`

`Seminorm.continuousAt_zero_of_forall`

`Seminorm.absorbent_ball`

`rescale_to_shell_semi_normed`

`Seminorm.mem_closedBall_zero`

`Seminorm.absorbent_closedBall_zero`

`Seminorm.bound_of_shell_smul`

`absorbent_ball`

`Seminorm.mem_ball`

`Seminorm.ext`

`Seminorm.smul'`

`Seminorm.continuousAt_zero_of_forall'`

`Seminorm.mem_ball_zero`

`Mathlib.Analysis.Seminorm._auxLemma.22`

`Seminorm.continuous_of_forall'`

`Mathlib.Analysis.Seminorm._auxLemma.16`

`Seminorm.convex_closedBall`

`Seminorm.convexOn`

`Mathlib.Analysis.Seminorm._auxLemma.23`

`Seminorm.ball_zero_eq`

`Seminorm.rescale_to_shell_zpow`

`balanced_ball_zero`

`Seminorm.mem_closedBall`

`Seminorm.absorbent_closedBall`

`Seminorm.uniformContinuous_of_continuousAt_zero`

`Seminorm.absorbent_ball_zero`

`rescale_to_shell_semi_normed_zpow`

`SeminormClass.map_smul_eq_mul`

`Seminorm.vadd_ball`

`Seminorm.ball_subset_closedBall`

`Seminorm.smul_apply`

`Seminorm.continuous_of_forall`

`Seminorm.balanced_ball_zero`

`Seminorm.uniformContinuous_of_forall'`

`Seminorm.rescale_to_shell`

`absorbent_ball_zero`

`Seminorm.bddBelow_range_add`