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} [AddMonoid α] {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)`. } [AddMonoidAddMonoid.{u} (M : Type u) : Type uAn `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`.  αType u_1]
  {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddMonoid α] : 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 : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. }
  {xα : αType u_1} {θℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } (hθ₀0 ≤ θ : 0 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. θℝ)
  (hθ₁θ ≤ 1 : θℝ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. 1) (ht₀t ≠ 0 : tℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0)
  (htt ≠ ∞ : tℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. ∞Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`.) :
  ‖xα‖ₑ[A₀EQuasinorm α] ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).1 -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). θℝ)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. ‖xα‖ₑ[A₁EQuasinorm α] ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. θℝ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    tℝ≥0∞ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. (Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).θℝ)Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator). *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. A₀EQuasinorm α.jNormEQuasinorm.jNorm.{u_1} {α : Type u_1} [AddMonoid α] (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.kNorm_zero.{u_1}EQuasinorm.kNorm_zero.{u_1} {α : Type u_1} [AddMonoid α] {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)`. }
  [AddMonoidAddMonoid.{u} (M : Type u) : Type uAn `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`.  αType u_1] {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddMonoid α] : 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 : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ) : A₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddMonoid α] (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} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 0

theorem EQuasinorm.kNorm_add_le_mul.{u_1}EQuasinorm.kNorm_add_le_mul.{u_1} {α : Type u_1} [AddMonoid α] {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)`. } [AddMonoidAddMonoid.{u} (M : Type u) : Type uAn `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`.  αType u_1]
  {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddMonoid α] : 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 : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. )
  (xα yα : αType u_1) :
  A₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddMonoid α] (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 α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.xα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. yα)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.
    maxMax.max.{u} {α : Type u} [self : Max α] : α → α → αReturns the greater of its two arguments. 

Conventions for notations in identifiers:

 * The recommended spelling of `max` in identifiers is `max`.

 * The recommended spelling of `⊔` in identifiers is `sup` (`⊔` is the preferred notation for `max` when the type is not linearly ordered.). A₀EQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddMonoid α] (self : EQuasinorm α) : ℝ≥0∞The subadditivity constant.  A₁EQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddMonoid α] (self : EQuasinorm α) : ℝ≥0∞The subadditivity constant.  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.A₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddMonoid α] (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 + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. A₀EQuasinorm α.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddMonoid α] (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 α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.

theorem EQuasinorm.IsSolid.enorm_le_mul_of_abs_le.{u_1}EQuasinorm.IsSolid.enorm_le_mul_of_abs_le.{u_1} {β : Type u_1} [AddMonoid β] [Abs β] [Preorder β] {B : EQuasinorm β}
  {a b c : β} [Abs.IsModulus β] [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)`. } [AddMonoidAddMonoid.{u} (M : Type u) : Type uAn `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`.  βType u_1] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) βType u_1]
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2A preorder is a reflexive, transitive relation `≤`.
In a preorder, `a < b` means `a ≤ b ∧ ¬b ≤ a`, and `<` is defined this way by default.
You can override this definition to set a better def-eq.
 βType u_1] {BEQuasinorm β : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddMonoid α] : 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}
  {aβ bβ cβ : βType u_1} [Abs.IsModulusAbs.IsModulus.{u_1} (β : Type u_1) [AddMonoid β] [Preorder β] [Abs β] : Prop βType u_1]
  [BEQuasinorm β.IsSolidEQuasinorm.IsSolid.{u_1} {β : Type u_1} [AddMonoid β] [Abs β] [Preorder β] (B : EQuasinorm β) : Prop] (h|a|ₑ ≤ |b|ₑ + |c|ₑ : |Abs.toFun.{u_2} {β : Sort u_2} [self : Abs β] : β → βaβ|ₑAbs.toFun.{u_2} {β : Sort u_2} [self : Abs β] : β → β ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. |Abs.toFun.{u_2} {β : Sort u_2} [self : Abs β] : β → βbβ|ₑAbs.toFun.{u_2} {β : Sort u_2} [self : Abs β] : β → β +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. |Abs.toFun.{u_2} {β : Sort u_2} [self : Abs β] : β → βcβ|ₑAbs.toFun.{u_2} {β : Sort u_2} [self : Abs β] : β → β) :
  ‖aβ‖ₑ[BEQuasinorm β] ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. BEQuasinorm β.CEQuasinorm.C.{u_1} {α : Type u_1} [AddMonoid α] (self : EQuasinorm α) : ℝ≥0∞The subadditivity constant.  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.‖bβ‖ₑ[BEQuasinorm β] +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. ‖cβ‖ₑ[BEQuasinorm β])HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.

theorem EQuasinorm.kNorm_le_kNorm_of_abs_le.{u_1}EQuasinorm.kNorm_le_kNorm_of_abs_le.{u_1} {β : Type u_1} [AddMonoid β] [Abs β] [Preorder β] {A₀ A₁ : EQuasinorm β}
  {x y : β} [Abs.IsModulus β] [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)`. } [AddMonoidAddMonoid.{u} (M : Type u) : Type uAn `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`.  βType u_1] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) βType u_1]
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2A preorder is a reflexive, transitive relation `≤`.
In a preorder, `a < b` means `a ≤ b ∧ ¬b ≤ a`, and `<` is defined this way by default.
You can override this definition to set a better def-eq.
 βType u_1] {A₀EQuasinorm β A₁EQuasinorm β : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddMonoid α] : 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β yβ : βType u_1} [Abs.IsModulusAbs.IsModulus.{u_1} (β : Type u_1) [AddMonoid β] [Preorder β] [Abs β] : Prop βType u_1] [A₀EQuasinorm β.IsSolidEQuasinorm.IsSolid.{u_1} {β : Type u_1} [AddMonoid β] [Abs β] [Preorder β] (B : EQuasinorm β) : Prop]
  [A₁EQuasinorm β.IsSolidEQuasinorm.IsSolid.{u_1} {β : Type u_1} [AddMonoid β] [Abs β] [Preorder β] (B : EQuasinorm β) : Prop] (h|x|ₑ ≤ |y|ₑ : |Abs.toFun.{u_2} {β : Sort u_2} [self : Abs β] : β → βxβ|ₑAbs.toFun.{u_2} {β : Sort u_2} [self : Abs β] : β → β ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. |Abs.toFun.{u_2} {β : Sort u_2} [self : Abs β] : β → βyβ|ₑAbs.toFun.{u_2} {β : Sort u_2} [self : Abs β] : β → β)
  (tℝ≥0∞ : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ) :
  A₀EQuasinorm β.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddMonoid α] (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β ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. A₀EQuasinorm β.kNormEQuasinorm.kNorm.{u_1} {α : Type u_1} [AddMonoid α] (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β

theorem EQuasinorm.discreteKMethod_equiv_kmethod.{u_1}EQuasinorm.discreteKMethod_equiv_kmethod.{u_1} {α : Type u_1} [AddMonoid α] {A₀ A₁ : EQuasinorm α} {θ : ℝ} {q : ℝ≥0∞} :
  A₀.discreteKMethod A₁ θ q ≈ A₀.kMethod A₁ θ qLemma 3.1.3. 
  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddMonoidAddMonoid.{u} (M : Type u) : Type uAn `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`.  αType u_1]
  {A₀EQuasinorm α A₁EQuasinorm α : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddMonoid α] : 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} {θℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. }
  {qℝ≥0∞ : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. } :
  A₀EQuasinorm α.discreteKMethodEQuasinorm.discreteKMethod.{u_1} {α : Type u_1} [AddMonoid α] (A₀ A₁ : EQuasinorm α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm αThe discrete version of $K_{θ,q}(\bar{A})$.  A₁EQuasinorm α θℝ qℝ≥0∞ ≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v`x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass,
the notion of equivalence is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `≈` in identifiers is `equiv`.
    A₀EQuasinorm α.kMethodEQuasinorm.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A₀ A₁ : EQuasinorm α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm αThe space $K_{θ,q}(\bar{A})$ in Section 3.1.  A₁EQuasinorm α θℝ qℝ≥0∞

theorem EQuasinorm.eLorentz_equiv_kMethod_of_neq.{u_1,
    u_2}EQuasinorm.eLorentz_equiv_kMethod_of_neq.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α)
  {β : Type u_2} [TopologicalSpace β] [ESeminormedAddMonoid β] [ContinuousAdd β] (p₀ q₀ p₁ q₁ q p : ℝ≥0∞)
  (hp₀₁ : p₀ ≠ p₁) (t : ℝ≥0) (hpos : 0 < p₀ ∧ 0 < p₁ ∧ 0 < q₀ ∧ 0 < q₁ ∧ 0 < q) (hp : p⁻¹ = (1 - ↑t) / p₀ + ↑t / p₁) :
  eLorentz μ β p q ≈ (eLorentzCouple μ β p₀ q₀ p₁ q₁).kMethod (↑t) qFor a Banach couple $A = (A_0,A_1)$ given by two Lorentz spaces
$A_0 = L_{p_0,q_0}$ and $A_1 = L_{p_1,q_1}$ where $p_0,p_1,q_0,q_1 \in (0,\infty]$ with
$p_0 \neq p_1$, for all $0 < \theta < 1$ and $q \in (0,\infty]$, the real interpolation space
$(A)_{\theta,q}$ is the Lorentz space $L_{p,q}$ where
$p^{-1} = (1 - \theta) p_0^{-1} + \theta p_1^{-1}$.

  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [mαMeasurableSpace α : MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.  αType u_1]
  (μMeasure α : MeasureMeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] : Type u_6A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.
 αType u_1) {βType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  βType u_2]
  [ESeminormedAddMonoidESeminormedAddMonoid.{u_8} (E : Type u_8) [TopologicalSpace E] : Type u_8An e-seminormed monoid is an additive monoid endowed with a continuous enorm.
Note that we do not ask for the enorm to be positive definite:
non-trivial elements may have enorm zero.  βType u_2]
  [ContinuousAddContinuousAdd.{u_1} (M : Type u_1) [TopologicalSpace M] [Add M] : PropBasic hypothesis to talk about a topological additive monoid or a topological additive
semigroup. A topological additive monoid over `M`, for example, is obtained by requiring both the
instances `AddMonoid M` and `ContinuousAdd M`.

Continuity in each argument separately can be stated using `SeparatelyContinuousAdd α`. If one wants
only continuity in either the left or right argument, but not both one can use
`ContinuousConstVAdd α α`/`ContinuousConstVAdd αᵐᵒᵖ α`.  βType u_2]
  (p₀ℝ≥0∞ q₀ℝ≥0∞ p₁ℝ≥0∞ q₁ℝ≥0∞ qℝ≥0∞ pℝ≥0∞ : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. )
  (hp₀₁p₀ ≠ p₁ : p₀ℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. p₁ℝ≥0∞) (tℝ≥0 : ℝ≥0NNReal : TypeNonnegative real numbers, denoted as `ℝ≥0` within the NNReal namespace )
  (hpos0 < p₀ ∧ 0 < p₁ ∧ 0 < q₀ ∧ 0 < q₁ ∧ 0 < q :
    0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. p₀ℝ≥0∞ ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.
      0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. p₁ℝ≥0∞ ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`. 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. q₀ℝ≥0∞ ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`. 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. q₁ℝ≥0∞ ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`. 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. qℝ≥0∞)
  (hpp⁻¹ = (1 - ↑t) / p₀ + ↑t / p₁ : pℝ≥0∞⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).1 -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). ↑tℝ≥0)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. p₀ℝ≥0∞ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. ↑tℝ≥0 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. p₁ℝ≥0∞) :
  eLorentzEQuasinorm.eLorentz.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) (β : Type u_2)
  [TopologicalSpace β] [ESeminormedAddMonoid β] [ContinuousAdd β] (p q : ℝ≥0∞) : EQuasinorm (α → β) μMeasure α βType u_2 pℝ≥0∞ qℝ≥0∞ ≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v`x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass,
the notion of equivalence is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `≈` in identifiers is `equiv`.
    (eLorentzCoupleEQuasinorm.eLorentzCouple.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) (β : Type u_2)
  [TopologicalSpace β] [ESeminormedAddMonoid β] [ContinuousAdd β] (p₀ p₁ q₀ q₁ : ℝ≥0∞) : Couple (α → β) μMeasure α βType u_2 p₀ℝ≥0∞ q₀ℝ≥0∞ p₁ℝ≥0∞
          q₁ℝ≥0∞).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α
      (↑tℝ≥0) qℝ≥0∞