LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.NormedSpace.ENorm

`ENorm.map_zero` theorem ENorm.map_zero : ∀ {𝕜 : Type u_1} {V : Type u_2} [inst : NormedField 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V] (e : ENorm 𝕜 V), ↑e 0 = 0 This theorem states that for any field 𝕜 with a norm (a NormedField), for any additive commutative group V, and for any module V over 𝕜, if e is an extended norm (ENorm) on V over 𝕜, then the value of e at the zero element of V is zero. In other words, the extended norm of zero is always zero, regardless of the particular field, additive group, or module in question. More concisely: For any NormedField 𝕜, any additive commutative group V as a 𝕜-module, and any extended norm e on V, we have e(0) = 0.
`ENorm.map_add_le` theorem ENorm.map_add_le : ∀ {𝕜 : Type u_1} {V : Type u_2} [inst : NormedField 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V] (e : ENorm 𝕜 V) (x y : V), ↑e (x + y) ≤ ↑e x + ↑e y This theorem states that for any normed field `𝕜`, an additive commutative group `V`, and a module over `𝕜` and `V`, the extended norm `e` of the sum of two elements `x` and `y` from `V` is less than or equal to the sum of the extended norms of `x` and `y` individually. In other words, the extended norm has the property of subadditivity: `e(x + y) ≤ e(x) + e(y)`. More concisely: For any normed field `𝕜` and normed additive commutative group `V` with module `M`, the extended norm `e` on `V` is subadditive, that is, `e(x + y) ≤ e(x) + e(y)` for all `x, y ∈ V`.
`ENorm.map_smul` theorem ENorm.map_smul : ∀ {𝕜 : Type u_1} {V : Type u_2} [inst : NormedField 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V] (e : ENorm 𝕜 V) (c : 𝕜) (x : V), ↑e (c • x) = ↑‖c‖₊ * ↑e x This theorem states that for any normed field `𝕜`, additively commutative group `V`, and `𝕜`-module `V`, given an extended norm `e` on `V`, a scalar `c` from `𝕜`, and a vector `x` from `V`, the extended norm of the scalar multiplication of `c` and `x` (`c • x`) is equal to the product of the nonnegative norm (or absolute value) of `c` (`‖c‖₊`) and the extended norm of `x`. In essence, it captures the principle that scaling a vector by a factor changes its norm by the absolute value of that factor. More concisely: For any normed field `𝕜`, additively commutative group `V`, and `𝕜`-module `V` with extended norm `e`, the extended norm of scalar multiplication `e(c • x) = ‖c‖₊ * e(x)` for all `c` from `𝕜` and `x` from `V`.