theorem EQuasinorm.jNorm_zero.{u_1}EQuasinorm.jNorm_zero.{u_1} {α : Type u_1} [AddCommMonoid α] {A₀ A₁ : EQuasinorm α} (t : ℝ≥0∞) : A₀.jNorm A₁ t 0 = 0 {α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] {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{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}
  (tℝ≥0∞ : ℝ≥0∞ENNReal : Type) : A₀EQuasinorm α.jNormEQuasinorm.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$J(t,x)$ in Section 3.2. For $t = 1$ this is the norm of $A₀ ⊓ A₁$.  A₁EQuasinorm α tℝ≥0∞ 0 =Eq.{u_1} {α : Sort u_1} : α → α → Prop 0

theorem EQuasinorm.jNorm_add_le_mul.{u_1}EQuasinorm.jNorm_add_le_mul.{u_1} {α : Type u_1} [AddCommMonoid α] {A₀ A₁ : EQuasinorm α} (t : ℝ≥0∞) (x y : α) :
  A₀.jNorm A₁ t (x + y) ≤ max A₀.C A₁.C * (A₀.jNorm A₁ t x + A₀.jNorm A₁ t y)
  {α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]
  {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{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} (tℝ≥0∞ : ℝ≥0∞ENNReal : Type)
  (xα yα : αType u_1) :
  A₀EQuasinorm α.jNormEQuasinorm.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$J(t,x)$ in Section 3.2. For $t = 1$ this is the norm of $A₀ ⊓ A₁$.  A₁EQuasinorm α tℝ≥0∞ (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γxα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ yα)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop
    maxMax.max.{u} {α : Type u} [self : Max α] : α → α → α A₀EQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddCommMonoid α] (self : EQuasinorm α) : ℝ≥0∞The subadditivity constant.  A₁EQuasinorm α.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 α β γ] : α → β → γA₀EQuasinorm α.jNormEQuasinorm.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$J(t,x)$ in Section 3.2. For $t = 1$ this is the norm of $A₀ ⊓ A₁$.  A₁EQuasinorm α tℝ≥0∞ xα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ A₀EQuasinorm α.jNormEQuasinorm.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$J(t,x)$ in Section 3.2. For $t = 1$ this is the norm of $A₀ ⊓ A₁$.  A₁EQuasinorm α tℝ≥0∞ yα)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ

theorem EQuasinorm.enorm_rpow_mul_enorm_rpow_le_rpow_neg_mul_jNorm.{u_1}EQuasinorm.enorm_rpow_mul_enorm_rpow_le_rpow_neg_mul_jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] {A₀ A₁ : EQuasinorm α}
  {t : ℝ≥0∞} {x : α} {θ : ℝ} (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) (ht₀ : t ≠ 0) (ht : t ≠ ∞) :
  ‖x‖ₑ[A₀] ^ (1 - θ) * ‖x‖ₑ[A₁] ^ θ ≤ t ^ (-θ) * A₀.jNorm A₁ t x
  {α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]
  {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{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} {tℝ≥0∞ : ℝ≥0∞ENNReal : Type}
  {xα : αType u_1} {θℝ : ℝReal : Type} (hθ₀0 ≤ θ : 0 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop θℝ)
  (hθ₁θ ≤ 1 : θℝ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop 1) (ht₀t ≠ 0 : tℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop 0)
  (htt ≠ ∞ : tℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop ∞Top.top.{u_1} {α : Type u_1} [self : Top α] : α) :
  ‖xα‖ₑ[A₀EQuasinorm α] ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ1 -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ θℝ)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ ‖xα‖ₑ[A₁EQuasinorm α] ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ θℝ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop
    tℝ≥0∞ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ (Neg.neg.{u} {α : Type u} [self : Neg α] : α → α-Neg.neg.{u} {α : Type u} [self : Neg α] : α → αθℝ)Neg.neg.{u} {α : Type u} [self : Neg α] : α → α *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ A₀EQuasinorm α.jNormEQuasinorm.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$J(t,x)$ in Section 3.2. For $t = 1$ this is the norm of $A₀ ⊓ A₁$.  A₁EQuasinorm α tℝ≥0∞ xα

theorem EQuasinorm.jNorm_swap.{u_1}EQuasinorm.jNorm_swap.{u_1} {α : Type u_1} [AddCommMonoid α] {A₀ A₁ : EQuasinorm α} {t : ℝ≥0∞} (ht₀ : t ≠ 0)
  (ht : t ≠ ∞) (x : α) : A₁.jNorm A₀ t x = t * A₀.jNorm A₁ t⁻¹ xSwapping the two quasinorms: $J(t,x;A_1,A_0) = t\,J(t^{-1},x;A_0,A_1)$.  {α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] {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{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}
  {tℝ≥0∞ : ℝ≥0∞ENNReal : Type} (ht₀t ≠ 0 : tℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop 0) (htt ≠ ∞ : tℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop ∞Top.top.{u_1} {α : Type u_1} [self : Top α] : α)
  (xα : αType u_1) :
  A₁EQuasinorm α.jNormEQuasinorm.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$J(t,x)$ in Section 3.2. For $t = 1$ this is the norm of $A₀ ⊓ A₁$.  A₀EQuasinorm α tℝ≥0∞ xα =Eq.{u_1} {α : Sort u_1} : α → α → Prop tℝ≥0∞ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ A₀EQuasinorm α.jNormEQuasinorm.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$J(t,x)$ in Section 3.2. For $t = 1$ this is the norm of $A₀ ⊓ A₁$.  A₁EQuasinorm α tℝ≥0∞⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α xα

theorem EQuasinorm.jNorm_swap_zpow.{u_1}EQuasinorm.jNorm_swap_zpow.{u_1} {α : Type u_1} [AddCommMonoid α] {A₀ A₁ : EQuasinorm α} (ν : ℤ) (x : α) :
  A₁.jNorm A₀ (2 ^ ν) x = 2 ^ ν * A₀.jNorm A₁ (2 ^ (-ν)) xThe dyadic case of `jNorm_swap`: $J_\nu(x;A_1,A_0) = 2^\nu J_{-\nu}(x;A_0,A_1)$. 
  {α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]
  {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{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} (νℤ : ℤInt : Type) (xα : αType u_1) :
  A₁EQuasinorm α.jNormEQuasinorm.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$J(t,x)$ in Section 3.2. For $t = 1$ this is the norm of $A₀ ⊓ A₁$.  A₀EQuasinorm α (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ νℤ)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ xα =Eq.{u_1} {α : Sort u_1} : α → α → Prop
    2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ νℤ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ A₀EQuasinorm α.jNormEQuasinorm.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$J(t,x)$ in Section 3.2. For $t = 1$ this is the norm of $A₀ ⊓ A₁$.  A₁EQuasinorm α (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ (Neg.neg.{u} {α : Type u} [self : Neg α] : α → α-Neg.neg.{u} {α : Type u} [self : Neg α] : α → ανℤ)Neg.neg.{u} {α : Type u} [self : Neg α] : α → α)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ xα

theorem EQuasinorm.kNorm_zero.{u_1}EQuasinorm.kNorm_zero.{u_1} {α : Type u_1} [AddCommMonoid α] {A₀ A₁ : EQuasinorm α} (t : ℝ≥0∞) : A₀.kNorm A₁ t 0 = 0 {α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] {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{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}
  (tℝ≥0∞ : ℝ≥0∞ENNReal : Type) : A₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$K(t,x)$ in Section 3.1. For $t = 1$ this is the norm of $A₀ ⊔ A₁$.  A₁EQuasinorm α tℝ≥0∞ 0 =Eq.{u_1} {α : Sort u_1} : α → α → Prop 0

theorem EQuasinorm.kNorm_add_le_mul.{u_1}EQuasinorm.kNorm_add_le_mul.{u_1} {α : Type u_1} [AddCommMonoid α] {A₀ A₁ : EQuasinorm α} (t : ℝ≥0∞) (x y : α) :
  A₀.kNorm A₁ t (x + y) ≤ max A₀.C A₁.C * (A₀.kNorm A₁ t x + A₀.kNorm A₁ t y)
  {α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]
  {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{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} (tℝ≥0∞ : ℝ≥0∞ENNReal : Type)
  (xα yα : αType u_1) :
  A₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$K(t,x)$ in Section 3.1. For $t = 1$ this is the norm of $A₀ ⊔ A₁$.  A₁EQuasinorm α tℝ≥0∞ (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γxα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ yα)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop
    maxMax.max.{u} {α : Type u} [self : Max α] : α → α → α A₀EQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddCommMonoid α] (self : EQuasinorm α) : ℝ≥0∞The subadditivity constant.  A₁EQuasinorm α.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 α β γ] : α → β → γA₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$K(t,x)$ in Section 3.1. For $t = 1$ this is the norm of $A₀ ⊔ A₁$.  A₁EQuasinorm α tℝ≥0∞ xα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ A₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$K(t,x)$ in Section 3.1. For $t = 1$ this is the norm of $A₀ ⊔ A₁$.  A₁EQuasinorm α tℝ≥0∞ yα)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ

theorem EQuasinorm.kNorm_swap.{u_1}EQuasinorm.kNorm_swap.{u_1} {α : Type u_1} [AddCommMonoid α] {A₀ A₁ : EQuasinorm α} {t : ℝ≥0∞} (ht₀ : t ≠ 0)
  (ht : t ≠ ∞) (x : α) : A₁.kNorm A₀ t x = t * A₀.kNorm A₁ t⁻¹ xSwapping the two quasinorms: $K(t,x;A_1,A_0) = t\,K(t^{-1},x;A_0,A_1)$.  {α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] {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{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}
  {tℝ≥0∞ : ℝ≥0∞ENNReal : Type} (ht₀t ≠ 0 : tℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop 0) (htt ≠ ∞ : tℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop ∞Top.top.{u_1} {α : Type u_1} [self : Top α] : α)
  (xα : αType u_1) :
  A₁EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$K(t,x)$ in Section 3.1. For $t = 1$ this is the norm of $A₀ ⊔ A₁$.  A₀EQuasinorm α tℝ≥0∞ xα =Eq.{u_1} {α : Sort u_1} : α → α → Prop tℝ≥0∞ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ A₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$K(t,x)$ in Section 3.1. For $t = 1$ this is the norm of $A₀ ⊔ A₁$.  A₁EQuasinorm α tℝ≥0∞⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α xα

theorem EQuasinorm.kNorm_swap_zpow.{u_1}EQuasinorm.kNorm_swap_zpow.{u_1} {α : Type u_1} [AddCommMonoid α] {A₀ A₁ : EQuasinorm α} (ν : ℤ) (x : α) :
  A₁.kNorm A₀ (2 ^ ν) x = 2 ^ ν * A₀.kNorm A₁ (2 ^ (-ν)) xThe dyadic case of `kNorm_swap`: $K_\nu(x;A_1,A_0) = 2^\nu K_{-\nu}(x;A_0,A_1)$. 
  {α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]
  {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{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} (νℤ : ℤInt : Type) (xα : αType u_1) :
  A₁EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$K(t,x)$ in Section 3.1. For $t = 1$ this is the norm of $A₀ ⊔ A₁$.  A₀EQuasinorm α (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ νℤ)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ xα =Eq.{u_1} {α : Sort u_1} : α → α → Prop
    2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ νℤ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ A₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$K(t,x)$ in Section 3.1. For $t = 1$ this is the norm of $A₀ ⊔ A₁$.  A₁EQuasinorm α (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ (Neg.neg.{u} {α : Type u} [self : Neg α] : α → α-Neg.neg.{u} {α : Type u} [self : Neg α] : α → ανℤ)Neg.neg.{u} {α : Type u} [self : Neg α] : α → α)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ xα

theorem EQuasinorm.monotone_kNorm.{u_1}EQuasinorm.monotone_kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] {A₀ A₁ : EQuasinorm α} {x : α} :
  Monotone fun x_1 ↦ A₀.kNorm A₁ x_1 xPart of Lemma 3.1.1: $t ↦ K(t,x)$ is monotone, for every $x$. 
  {α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]
  {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{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} {xα : αType u_1} :
  MonotoneMonotone.{u, v} {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) : Prop fun x_1ℝ≥0∞ ↦ A₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞$K(t,x)$ in Section 3.1. For $t = 1$ this is the norm of $A₀ ⊔ A₁$.  A₁EQuasinorm α x_1ℝ≥0∞ xα

theorem EQuasinorm.IsSolid.enorm_le_mul_of_modulus_le.{u_1,
    u_2}EQuasinorm.IsSolid.enorm_le_mul_of_modulus_le.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β]
  [AddCommMonoid M] [Preorder M] [Modulus β M] {B : EQuasinorm β} {a b c : β} [Modulus.IsDecomposable β M] [B.IsSolid]
  (h : |a|ₑ ≤ |b|ₑ + |c|ₑ) : ‖a‖ₑ[B] ≤ B.C * (‖b‖ₑ[B] + ‖c‖ₑ[B])A modulus inequality $|a| ≤ |b| + |c|$ transfers to any solid quasinorm, up to its
subadditivity constant. 
  {βType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {MType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 βType u_1] [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 MType u_2]
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 MType u_2] [ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4)A modulus $β → M$, with values in a second type $M$.  βType u_1 MType u_2]
  {BEQuasinorm β : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_1} {aβ bβ cβ : βType u_1}
  [Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : PropA decomposable modulus, following the lattice-normed spaces of Kantorovich \(see Kusraev,
**Dominated Operators**, Ch. 2\), with decomposability weakened to bounds by values of $|\cdot|$.

todo: what about definition 3.5.1 in BL \("is of class"\)? a different possible approach would be to
quantify over all spaces that are of the class of the couple.
 βType u_1 MType u_2] [BEQuasinorm β.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : PropA quasinorm is solid if it is monotone along the modulus. ]
  (h|a|ₑ ≤ |b|ₑ + |c|ₑ : |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Maβ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mbβ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mcβ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M) :
  ‖aβ‖ₑ[BEQuasinorm β] ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop BEQuasinorm β.CEQuasinorm.C.{u_1} {α : Type u_1} [AddCommMonoid α] (self : EQuasinorm α) : ℝ≥0∞ *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 α β γ] : α → β → γ‖bβ‖ₑ[BEQuasinorm β] +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ ‖cβ‖ₑ[BEQuasinorm β])HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ

theorem EQuasinorm.kNorm_le_kNorm_of_modulus_le.{u_1,
    u_2}EQuasinorm.kNorm_le_kNorm_of_modulus_le.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [AddCommMonoid M]
  [Preorder M] [Modulus β M] {A₀ A₁ : EQuasinorm β} {x y : β} [Modulus.IsDecomposable β M] [A₀.IsSolid] [A₁.IsSolid]
  (h : |x|ₑ ≤ |y|ₑ) (t : ℝ≥0∞) : A₀.kNorm A₁ t x ≤ A₀.kNorm A₁ t yThe supremum of a couple of solid quasinorms, with the norm $J(K,-)$, is solid. 
  {βType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {MType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 βType u_1] [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 MType u_2]
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 MType u_2] [ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4)A modulus $β → M$, with values in a second type $M$.  βType u_1 MType u_2]
  {A₀EQuasinorm β A₁EQuasinorm β : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_1} {xβ yβ : βType u_1}
  [Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : PropA decomposable modulus, following the lattice-normed spaces of Kantorovich \(see Kusraev,
**Dominated Operators**, Ch. 2\), with decomposability weakened to bounds by values of $|\cdot|$.

todo: what about definition 3.5.1 in BL \("is of class"\)? a different possible approach would be to
quantify over all spaces that are of the class of the couple.
 βType u_1 MType u_2]
  [A₀EQuasinorm β.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : PropA quasinorm is solid if it is monotone along the modulus. ] [A₁EQuasinorm β.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : PropA quasinorm is solid if it is monotone along the modulus. ]
  (h|x|ₑ ≤ |y|ₑ : |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mxβ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Myβ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M) (tℝ≥0∞ : ℝ≥0∞ENNReal : Type) :
  A₀EQuasinorm β.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ A₁EQuasinorm β tℝ≥0∞ xβ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop A₀EQuasinorm β.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A₀ A₁ : EQuasinorm α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ A₁EQuasinorm β tℝ≥0∞ yβ

theorem EQuasinorm.IsSolid.ofModulus.{u_1, u_2}EQuasinorm.IsSolid.ofModulus.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [AddCommMonoid M] [Preorder M]
  [Modulus β M] [Modulus.IsDecomposable β M] (g : EQuasinorm M) (hg : Monotone fun m ↦ ‖m‖ₑ[g]) :
  (EQuasinorm.ofModulus β g hg).IsSolidA quasinorm induced by a modulus is solid. 
  {βType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {MType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 βType u_1] [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 MType u_2]
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 MType u_2] [ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4)A modulus $β → M$, with values in a second type $M$.  βType u_1 MType u_2]
  [Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : PropA decomposable modulus, following the lattice-normed spaces of Kantorovich \(see Kusraev,
**Dominated Operators**, Ch. 2\), with decomposability weakened to bounds by values of $|\cdot|$.

todo: what about definition 3.5.1 in BL \("is of class"\)? a different possible approach would be to
quantify over all spaces that are of the class of the couple.
 βType u_1 MType u_2]
  (gEQuasinorm M : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 MType u_2)
  (hgMonotone fun m ↦ ‖m‖ₑ[g] : MonotoneMonotone.{u, v} {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) : Prop fun mM ↦ ‖mM‖ₑ[gEQuasinorm M]) :
  (EQuasinorm.ofModulusEQuasinorm.ofModulus.{u_1, u_2} (β : Type u_1) {M : Type u_2} [AddCommMonoid β] [AddCommMonoid M] [Preorder M]
  [Modulus β M] [Modulus.IsDecomposable β M] (g : EQuasinorm M) (hg : Monotone fun m ↦ ‖m‖ₑ[g]) : EQuasinorm βThe quasinorm $x ↦ ‖|x|‖_g$ on $β$ induced by a monotone quasinorm $g$ on $M$, with the
same constant as $g$.  βType u_1 gEQuasinorm M hgMonotone fun m ↦ ‖m‖ₑ[g]).IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : PropA quasinorm is solid if it is monotone along the modulus.