theorem MultisubadditiveMap.enorm_update_add_le_mul.{u_1,
    u_2, u_3}MultisubadditiveMap.enorm_update_add_le_mul.{u_1, u_2, u_3} {ι : Type u_1} {α : ι → Type u_2}
  [(i : ι) → AddMonoid (α i)] {β : Type u_3} [AddMonoid β] [Abs β] [Preorder β] (T : MultisubadditiveMap α β)
  (B : EQuasinorm β) [Abs.IsModulus β] [DecidableEq ι] [B.IsSolid] (f : (i : ι) → α i) (i : ι) (x y : α i) :
  ‖T (update f i (x + y))‖ₑ[B] ≤ B.C * (‖T (update f i x)‖ₑ[B] + ‖T (update f i y)‖ₑ[B])`EQuasinorm.IsSolid.enorm_le_mul_of_abs_le` applied to `subadditive`. 
  {ιType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {αι → Type u_2 : ιType u_1 → Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [(iι : ιType 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_2 iι)]
  {βType u_3 : Type u_3A 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_3] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) βType u_3]
  [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_3]
  (TMultisubadditiveMap α β : MultisubadditiveMapMultisubadditiveMap.{u_1, u_2, u_3} {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddMonoid (α i)] (β : Type u_3)
  [AddMonoid β] [Abs β] [Preorder β] : Type (max (max u_1 u_2) u_3)A map $f \colon ∏_i  α_i → β$ that is subadditive in the sense that forall $i \in ι$,
$$|f(a_1, \dots, a_i + b_i, \dots, a_k)| ≤
|f(a_1, \dots, a_i, \dots, a_k)| + |f(a_1, \dots, b_i, \dots, a_k)|.$$

For a function-valued $f$, this should be the pointwise absolute value, not
the norm of the function, and the inequality above lives in $β$.  αι → Type u_2 βType u_3)
  (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_3) [Abs.IsModulusAbs.IsModulus.{u_1} (β : Type u_1) [AddMonoid β] [Preorder β] [Abs β] : Prop βType u_3]
  [DecidableEqDecidableEq.{u} (α : Sort u) : Sort (max 1 u)Propositional equality is `Decidable` for all elements of a type.

In other words, an instance of `DecidableEq α` is a means of deciding the proposition `a = b` is
for all `a b : α`.
 ιType u_1] [BEQuasinorm β.IsSolidEQuasinorm.IsSolid.{u_1} {β : Type u_1} [AddMonoid β] [Abs β] [Preorder β] (B : EQuasinorm β) : Prop]
  (f(i : ι) → α i : (iι : ιType u_1) → αι → Type u_2 iι) (iι : ιType u_1)
  (xα i yα i : αι → Type u_2 iι) :
  ‖TMultisubadditiveMap α β (updateFunction.update.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
  β aReplacing the value of a function at a given point by a given value.  f(i : ι) → α i iι (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α i +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α i)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`.)‖ₑ[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`.‖TMultisubadditiveMap α β (updateFunction.update.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
  β aReplacing the value of a function at a given point by a given value.  f(i : ι) → α i iι xα i)‖ₑ[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`.
        ‖TMultisubadditiveMap α β (updateFunction.update.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
  β aReplacing the value of a function at a given point by a given value.  f(i : ι) → α i iι yα i)‖ₑ[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 MultisubadditiveMap.enorm_update_add_le.{u_1,
    u_2, u_3}MultisubadditiveMap.enorm_update_add_le.{u_1, u_2, u_3} {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddMonoid (α i)]
  {β : Type u_3} [AddMonoid β] [Abs β] [Preorder β] (T : MultisubadditiveMap α β) [Abs.IsModulus β] [DecidableEq ι]
  (Bₛ : ESeminorm β) [Bₛ.IsSolid] (f : (i : ι) → α i) (i : ι) (x y : α i) :
  ‖T (update f i (x + y))‖ₑ[Bₛ.toEQuasinorm] ≤
    ‖T (update f i x)‖ₑ[Bₛ.toEQuasinorm] + ‖T (update f i y)‖ₑ[Bₛ.toEQuasinorm]`enorm_update_add_le_mul` for an `ESeminorm`. 
  {ιType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {αι → Type u_2 : ιType u_1 → Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [(iι : ιType 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_2 iι)]
  {βType u_3 : Type u_3A 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_3] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) βType u_3]
  [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_3]
  (TMultisubadditiveMap α β : MultisubadditiveMapMultisubadditiveMap.{u_1, u_2, u_3} {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddMonoid (α i)] (β : Type u_3)
  [AddMonoid β] [Abs β] [Preorder β] : Type (max (max u_1 u_2) u_3)A map $f \colon ∏_i  α_i → β$ that is subadditive in the sense that forall $i \in ι$,
$$|f(a_1, \dots, a_i + b_i, \dots, a_k)| ≤
|f(a_1, \dots, a_i, \dots, a_k)| + |f(a_1, \dots, b_i, \dots, a_k)|.$$

For a function-valued $f$, this should be the pointwise absolute value, not
the norm of the function, and the inequality above lives in $β$.  αι → Type u_2 βType u_3)
  [Abs.IsModulusAbs.IsModulus.{u_1} (β : Type u_1) [AddMonoid β] [Preorder β] [Abs β] : Prop βType u_3] [DecidableEqDecidableEq.{u} (α : Sort u) : Sort (max 1 u)Propositional equality is `Decidable` for all elements of a type.

In other words, an instance of `DecidableEq α` is a means of deciding the proposition `a = b` is
for all `a b : α`.
 ιType u_1]
  (BₛESeminorm β : ESeminormESeminorm.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1An `ESeminorm` is an `EQuasinorm` such that $C = 1$.

This is `ESeminormedAddMonoid` as a structure, and without fixing a topology on 𝓐.  βType u_3) [BₛESeminorm β.IsSolidEQuasinorm.IsSolid.{u_1} {β : Type u_1} [AddMonoid β] [Abs β] [Preorder β] (B : EQuasinorm β) : Prop]
  (f(i : ι) → α i : (iι : ιType u_1) → αι → Type u_2 iι) (iι : ιType u_1)
  (xα i yα i : αι → Type u_2 iι) :
  ‖TMultisubadditiveMap α β
        (updateFunction.update.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
  β aReplacing the value of a function at a given point by a given value.  f(i : ι) → α i iι
          (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α i +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α i)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ₛESeminorm β.toEQuasinormESeminorm.toEQuasinorm.{u_1} {α : Type u_1} [AddMonoid α] (self : ESeminorm α) : EQuasinorm α] ≤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`.
    ‖TMultisubadditiveMap α β (updateFunction.update.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
  β aReplacing the value of a function at a given point by a given value.  f(i : ι) → α i iι xα i)‖ₑ[BₛESeminorm β.toEQuasinormESeminorm.toEQuasinorm.{u_1} {α : Type u_1} [AddMonoid α] (self : ESeminorm α) : EQuasinorm α] +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`.
      ‖TMultisubadditiveMap α β (updateFunction.update.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
  β aReplacing the value of a function at a given point by a given value.  f(i : ι) → α i iι yα i)‖ₑ[BₛESeminorm β.toEQuasinormESeminorm.toEQuasinorm.{u_1} {α : Type u_1} [AddMonoid α] (self : ESeminorm α) : EQuasinorm α]

theorem MultisubadditiveMap.isBoundedFor_iff_isBoundedFor_pow.{u_1,
    u_2, u_3}MultisubadditiveMap.isBoundedFor_iff_isBoundedFor_pow.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2}
  [(i : ι) → AddMonoid (α i)] {β : Type u_3} [AddMonoid β] [Abs β] [Preorder β] (T : MultisubadditiveMap α β)
  (A : (i : ι) → EQuasinorm (α i)) (B : EQuasinorm β) (C : ℝ≥0∞) {p : ℝ} :
  T.IsBoundedFor A B C ↔ T.IsBoundedFor (fun i ↦ (A i).pow p) (B.pow p) CThe operator $T$ is bounded if, and only if, it is bounded between the
same quasinorms raised to a common power. 
  {ιType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  ιType u_1]
  {αι → Type u_2 : ιType u_1 → Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [(iι : ιType 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_2 iι)]
  {βType u_3 : Type u_3A 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_3] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) βType u_3]
  [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_3]
  (TMultisubadditiveMap α β : MultisubadditiveMapMultisubadditiveMap.{u_1, u_2, u_3} {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddMonoid (α i)] (β : Type u_3)
  [AddMonoid β] [Abs β] [Preorder β] : Type (max (max u_1 u_2) u_3)A map $f \colon ∏_i  α_i → β$ that is subadditive in the sense that forall $i \in ι$,
$$|f(a_1, \dots, a_i + b_i, \dots, a_k)| ≤
|f(a_1, \dots, a_i, \dots, a_k)| + |f(a_1, \dots, b_i, \dots, a_k)|.$$

For a function-valued $f$, this should be the pointwise absolute value, not
the norm of the function, and the inequality above lives in $β$.  αι → Type u_2 βType u_3)
  (A(i : ι) → EQuasinorm (α i) : (iι : ιType u_1) → 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_2 iι))
  (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_3) (Cℝ≥0∞ : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ) {pℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } :
  TMultisubadditiveMap α β.IsBoundedForMultisubadditiveMap.IsBoundedFor.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2}
  [(i : ι) → AddMonoid (α i)] {β : Type u_3} [AddMonoid β] [Abs β] [Preorder β] (T : MultisubadditiveMap α β)
  (A : (i : ι) → EQuasinorm (α i)) (B : EQuasinorm β) (C : ℝ≥0∞) : PropA multisubadditive operator is bounded for quasinorms $A_i$, $B$ and a finite constant $C$ if
for all $x = (x_i)_{i ∈ ι}$,
$$\|T x\|_{B} ≤ C ∏_{i∈ ι} \|x_i\|_{A_i}$$.  A(i : ι) → EQuasinorm (α i) BEQuasinorm β Cℝ≥0∞ ↔Iff (a b : Prop) : PropIf and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`).
    TMultisubadditiveMap α β.IsBoundedForMultisubadditiveMap.IsBoundedFor.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2}
  [(i : ι) → AddMonoid (α i)] {β : Type u_3} [AddMonoid β] [Abs β] [Preorder β] (T : MultisubadditiveMap α β)
  (A : (i : ι) → EQuasinorm (α i)) (B : EQuasinorm β) (C : ℝ≥0∞) : PropA multisubadditive operator is bounded for quasinorms $A_i$, $B$ and a finite constant $C$ if
for all $x = (x_i)_{i ∈ ι}$,
$$\|T x\|_{B} ≤ C ∏_{i∈ ι} \|x_i\|_{A_i}$$.  (fun iι ↦ (A(i : ι) → EQuasinorm (α i) iι).powEQuasinorm.pow.{u_1} {α : Type u_1} [AddMonoid α] (A : EQuasinorm α) (p : ℝ) : EQuasinorm αThe quasinorm raised to a power $p$, as a quasinorm.  pℝ)
      (BEQuasinorm β.powEQuasinorm.pow.{u_1} {α : Type u_1} [AddMonoid α] (A : EQuasinorm α) (p : ℝ) : EQuasinorm αThe quasinorm raised to a power $p$, as a quasinorm.  pℝ) Cℝ≥0∞