4. K-Method🔗

Definition2.1

uses 0

Used by 60

Reverse dependency previews

Preview

Definition 1.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

A quasinorm on a monoid α is a function α → [0,∞] and a finite constant C that sends 0 : α to zero and is C-subadditive.

Lean code for Definition2.1●1 definition

structure(6 fields)defined in MultilinearInterpolation/EQuasinorm/Basic.lean

complete

structure EQuasinorm.{u_1}EQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1A quasinorm on a monoid $α$ is a function $α → [0,∞]$ and a finite constant
$C$ that sends $0 : α$ to zero and is $C$-subadditive.  (αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1] : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.

structure EQuasinorm.{u_1}EQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1A quasinorm on a monoid $α$ is a function $α → [0,∞]$ and a finite constant
$C$ that sends $0 : α$ to zero and is $C$-subadditive.  (αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1] : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.

A quasinorm on a monoid α is a function α → [0,∞] and a finite constant C that sends 0 : α to zero and is C-subadditive.

Fields

enormENorm αThe raw `enorm` associated to the quasinorm.  : ENormENorm.{u_4} (E : Type u_4) : Type u_4 αType u_1

The raw enorm associated to the quasinorm.

Cℝ≥0∞The subadditivity constant.  : ℝ≥0∞ENNReal : Type

The subadditivity constant.

C_lt_topself.C < ∞The subadditivity constant is finite.  : selfEQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddCommMonoid α] (self : EQuasinorm α) : ℝ≥0∞The subadditivity constant.  <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop ∞Top.top.{u_1} {α : Type u_1} [self : Top α] : α

The subadditivity constant is finite.

C_ge_one1 ≤ self.CThe subadditivity constant is at least one.  : 1 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop selfEQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddCommMonoid α] (self : EQuasinorm α) : ℝ≥0∞The subadditivity constant.

The subadditivity constant is at least one.

enorm_zero‖0‖ₑ = 0The enorm of zero is zero.  : ‖ENorm.enorm.{u_4} {E : Type u_4} [self : ENorm E] : E → ℝ≥0∞0‖ₑENorm.enorm.{u_4} {E : Type u_4} [self : ENorm E] : E → ℝ≥0∞ =Eq.{u_1} {α : Sort u_1} : α → α → Prop 0

The enorm of zero is zero.

enorm_add_le_mul∀ (x y : α), ‖x + y‖ₑ ≤ self.C * (‖x‖ₑ + ‖y‖ₑ)The quasinorm is `C`-subadditive.  : ∀ (xα yα : αType u_1), ‖ENorm.enorm.{u_4} {E : Type u_4} [self : ENorm E] : E → ℝ≥0∞xα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ yα‖ₑENorm.enorm.{u_4} {E : Type u_4} [self : ENorm E] : E → ℝ≥0∞ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop selfEQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddCommMonoid α] (self : EQuasinorm α) : ℝ≥0∞The subadditivity constant.  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ‖ENorm.enorm.{u_4} {E : Type u_4} [self : ENorm E] : E → ℝ≥0∞xα‖ₑENorm.enorm.{u_4} {E : Type u_4} [self : ENorm E] : E → ℝ≥0∞ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ ‖ENorm.enorm.{u_4} {E : Type u_4} [self : ENorm E] : E → ℝ≥0∞yα‖ₑENorm.enorm.{u_4} {E : Type u_4} [self : ENorm E] : E → ℝ≥0∞)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ

The quasinorm is C-subadditive.

Empty.