LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.NormedSpace.Basic

`NormedSpace.exists_lt_norm` theorem NormedSpace.exists_lt_norm : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst : NormedSpace 𝕜 E] [inst : Nontrivial E] (c : ℝ), ∃ x, c < ‖x‖ The theorem `NormedSpace.exists_lt_norm` asserts that if `E` is a nontrivial normed space over a nontrivially normed field `𝕜`, then `E` is unbounded. Specifically, for any real number `c`, there exists a vector `x` in `E` such that the norm of `x` is strictly greater than `c`. More concisely: In a nontrivial normed space over a nontrivially normed field, there exists a vector with strictly larger norm than any given real number.
`NormedSpace.norm_smul_le` theorem NormedSpace.norm_smul_le : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [self : NormedSpace 𝕜 E] (a : 𝕜) (b : E), ‖a • b‖ ≤ ‖a‖ * ‖b‖ This theorem states that for any normed field `𝕜` and a semi-normed additive commutative group `E` (which together form a normed space), the norm of the scaled vector `a • b` is less than or equal to the product of the norm of the scalar `a` and the norm of the vector `b`. Here, the symbol `•` represents the scalar multiplication operation, and `‖x‖` denotes the norm of `x`. This theorem forms part of the definition of a normed space, and is used to prove the equality `‖a • b‖ = ‖a‖ * ‖b‖` in the `norm_smul` theorem. More concisely: For any normed field `𝕜` and semi-normed additive commutative group `E` (forming a normed space), the norm of the product of a scalar `a` and vector `b` (denoted `a • b`) is less than or equal to the product of the scalar's norm (`‖a‖`) and the vector's norm (`‖b‖`). In other words, `‖a • b‖ ≤ ‖a‖ * ‖b‖`.
`NormedAlgebra.norm_smul_le` theorem NormedAlgebra.norm_smul_le : ∀ {𝕜 : Type u_6} {𝕜' : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [self : NormedAlgebra 𝕜 𝕜'] (r : 𝕜) (x : 𝕜'), ‖r • x‖ ≤ ‖r‖ * ‖x‖ This theorem states that in a normed algebra `𝕜'` over `𝕜`, which is a normed module and an algebra, the norm of a scalar multiple `r • x` is less than or equal to the product of the norms of `r` and `x`. In other words, for any scalar `r` from `𝕜` and any element `x` from `𝕜'`, the inequality ‖r • x‖ ≤ ‖r‖ * ‖x‖ holds. This is a property of normed spaces and it is part of the definition of a norm in a normed algebra. It is particularly useful when dealing with inequalities involving norms in mathematical analysis. More concisely: In a normed algebra over a normed field, the norm of a scalar multiple is less than or equal to the product of the scalar's and the element's norms.
`algebraMap_isometry` theorem algebraMap_isometry : ∀ (𝕜 : Type u_1) (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] [inst_3 : NormOneClass 𝕜'], Isometry ⇑(algebraMap 𝕜 𝕜') This theorem states that in a normed algebra, the function that embeds the base field into the extended field, known as the algebra map, is an isometry. This means that for any two elements in the base field, their distance remains the same even after being embedded into the extended field. The theorem applies to any base field (`𝕜`) that is a Normed Field and any extended field (`𝕜'`) that is a Seminormed Ring, Normed Algebra over `𝕜`, and has a Norm One Class structure. More concisely: In a Normed Field `𝕜` and a Normed Algebra `𝕜'` over `𝕜` with a Norm One Class structure, the algebra map embedding `𝕜` into `𝕜'` is an isometry, i.e., for all `x, y ∈ 𝕜`, `\|\|x - y\|\| = \|\|x' - y'\|\|`, where `x'` and `y'` denote the images of `x` and `y` under the algebra map.
`NormedSpace.unbounded_univ` theorem NormedSpace.unbounded_univ : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst : NormedSpace 𝕜 E] [inst : Nontrivial E], ¬Bornology.IsBounded Set.univ This theorem, `NormedSpace.unbounded_univ`, states that for any nontrivially normed field `𝕜` and any normed additive commutative group `E` that forms a normed space over `𝕜` and is nontrivial itself, the universal set (or the set containing all elements) in this context is not bounded with respect to the ambient bornology on `E`. In other words, in such a normed space, there doesn't exist a finite set of balls of finite radius that can cover the entire space. More concisely: In any nontrivially normed field with a corresponding nontrivial normed additive commutative group, the universal set is unbounded in the bornology of the normed space.
`NormedSpace.noncompactSpace` theorem NormedSpace.noncompactSpace : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NormedField 𝕜] [inst_1 : Infinite 𝕜] [inst_2 : NormedAddCommGroup E] [inst_3 : Nontrivial E] [inst : NormedSpace 𝕜 E], NoncompactSpace E This theorem establishes that a normed vector space over an infinite normed field is a noncompact space. Specifically, given any type `𝕜` and `E`, if `𝕜` is a normed field and infinite, and `E` is a normed add commutative group which is nontrivial and a normed space over `𝕜`, then `E` is a noncompact space. This theorem can't be generally applied as an instance because Lean would need to search for `NormedSpace 𝕜 E` with an unknown `𝕜`. This theorem is instead registered as an instance in two specific cases: when `𝕜 = E` and when `𝕜 = ℝ`. More concisely: A normed vector space over an infinite normed field is a noncompact space.
`norm_algebraMap'` theorem norm_algebraMap' : ∀ {𝕜 : Type u_1} (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] [inst_3 : NormOneClass 𝕜'] (x : 𝕜), ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖ The theorem `norm_algebraMap'` states that for any types `𝕜` and `𝕜'`, where `𝕜` is a normed field, `𝕜'` is a seminormed ring, and `𝕜'` is a normed algebra over `𝕜` that also has a norm of one, the norm of any element `x` of type `𝕜` when mapped into `𝕜'` using the algebra map is equal to the norm of `x` in `𝕜`. This essentially says that the algebra map preserves the norm from `𝕜` to `𝕜'`. More concisely: For any normed field 𝕜, seminormed ring 𝕜' making it a normed algebra over 𝕜 with norm one, the norm map of the algebra homomorphism from 𝕜 to 𝕜' is the identity function.