theorem MultisubadditiveMap.enorm_update_add_le_mul.{u_1,
    u_2, u_3, u_4}MultisubadditiveMap.enorm_update_add_le_mul.{u_1, u_2, u_3, u_4} {ι : Type u_1} {α : ι → Type u_2}
  [(i : ι) → AddCommMonoid (α i)] {β : Type u_3} [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M]
  [Modulus β M] (T : MultisubadditiveMap α β) (B : EQuasinorm β) [Modulus.IsDecomposable β M] [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_modulus_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) → AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 (αι → Type u_2 iι)]
  {βType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 βType u_3]
  {MType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 MType u_4]
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 MType u_4] [ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) βType u_3 MType u_4]
  (TMultisubadditiveMap α β : MultisubadditiveMapMultisubadditiveMap.{u_1, u_2, u_3, u_4} {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddCommMonoid (α i)]
  (β : Type u_3) {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M] : 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)|.$$

Here $|\cdot| \colon β → M$ is the modulus; for a function-valued $f$ it is pointwise, not
the norm of the function, and the inequality above lives in $M$.  αι → Type u_2 βType u_3)
  (BEQuasinorm β : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_3)
  [Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : Prop βType u_3 MType u_4]
  [DecidableEqDecidableEq.{u} (α : Sort u) : Sort (max 1 u) ιType u_1] [BEQuasinorm β.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (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 : α) :
  β a f(i : ι) → α i iι (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γxα i +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ yα i)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ)‖ₑ[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 α β γ] : α → β → γ‖TMultisubadditiveMap α β (updateFunction.update.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
  β a f(i : ι) → α i iι xα i)‖ₑ[BEQuasinorm β] +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ
        ‖TMultisubadditiveMap α β (updateFunction.update.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
  β a f(i : ι) → α i iι yα i)‖ₑ[BEQuasinorm β])HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ

theorem MultisubadditiveMap.enorm_update_add_le.{u_1,
    u_2, u_3, u_4}MultisubadditiveMap.enorm_update_add_le.{u_1, u_2, u_3, u_4} {ι : Type u_1} {α : ι → Type u_2}
  [(i : ι) → AddCommMonoid (α i)] {β : Type u_3} [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M]
  [Modulus β M] (T : MultisubadditiveMap α β) [Modulus.IsDecomposable β M] [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) → AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 (αι → Type u_2 iι)]
  {βType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 βType u_3]
  {MType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 MType u_4]
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 MType u_4] [ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) βType u_3 MType u_4]
  (TMultisubadditiveMap α β : MultisubadditiveMapMultisubadditiveMap.{u_1, u_2, u_3, u_4} {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddCommMonoid (α i)]
  (β : Type u_3) {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M] : 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)|.$$

Here $|\cdot| \colon β → M$ is the modulus; for a function-valued $f$ it is pointwise, not
the norm of the function, and the inequality above lives in $M$.  αι → Type u_2 βType u_3)
  [Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : Prop βType u_3 MType u_4]
  [DecidableEqDecidableEq.{u} (α : Sort u) : Sort (max 1 u) ιType u_1] (BₛESeminorm β : ESeminormESeminorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_3)
  [BₛESeminorm β.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (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 : α) :
  β a f(i : ι) → α i iι
          (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γxα i +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ yα i)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ)‖ₑ[BₛESeminorm β.toEQuasinormESeminorm.toEQuasinorm.{u_1} {α : Type u_1} [AddCommMonoid α] (self : ESeminorm α) : EQuasinorm α] ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop
    ‖TMultisubadditiveMap α β (updateFunction.update.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
  β a f(i : ι) → α i iι xα i)‖ₑ[BₛESeminorm β.toEQuasinormESeminorm.toEQuasinorm.{u_1} {α : Type u_1} [AddCommMonoid α] (self : ESeminorm α) : EQuasinorm α] +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ
      ‖TMultisubadditiveMap α β (updateFunction.update.{u, v} {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
  β a f(i : ι) → α i iι yα i)‖ₑ[BₛESeminorm β.toEQuasinormESeminorm.toEQuasinorm.{u_1} {α : Type u_1} [AddCommMonoid α] (self : ESeminorm α) : EQuasinorm α]

theorem MultisubadditiveMap.isBoundedForOn_iff_isBoundedForOn_pow.{u_1,
    u_2, u_3, u_4}MultisubadditiveMap.isBoundedForOn_iff_isBoundedForOn_pow.{u_1, u_2, u_3, u_4} {ι : Type u_1} [Fintype ι]
  {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] {β : Type u_3} [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M]
  [Preorder M] [Modulus β M] (T : MultisubadditiveMap α β) (A : (i : ι) → EQuasinorm (α i)) (B : EQuasinorm β)
  (C : ℝ≥0∞) {p : ℝ} (hp : 0 < p) (P : (i : ι) → α i → Prop) :
  T.IsBoundedForOn A B C P ↔ T.IsBoundedForOn (fun i ↦ (A i).pow hp) (B.pow hp) C PThe 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_3} (α : Type u_3) : Type u_3 ι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) → AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 (αι → Type u_2 iι)]
  {βType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 βType u_3]
  {MType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 MType u_4]
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 MType u_4] [ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) βType u_3 MType u_4]
  (TMultisubadditiveMap α β : MultisubadditiveMapMultisubadditiveMap.{u_1, u_2, u_3, u_4} {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddCommMonoid (α i)]
  (β : Type u_3) {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M] : 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)|.$$

Here $|\cdot| \colon β → M$ is the modulus; for a function-valued $f$ it is pointwise, not
the norm of the function, and the inequality above lives in $M$.  αι → Type u_2 βType u_3)
  (A(i : ι) → EQuasinorm (α i) : (iι : ιType u_1) → EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 (αι → Type u_2 iι))
  (BEQuasinorm β : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_3) (Cℝ≥0∞ : ℝ≥0∞ENNReal : Type) {pℝ : ℝReal : Type}
  (hp0 < p : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop pℝ)
  (P(i : ι) → α i → Prop : (iι : ιType u_1) → αι → Type u_2 iι → PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. ) :
  TMultisubadditiveMap α β.IsBoundedForOnMultisubadditiveMap.IsBoundedForOn.{u_1, u_2, u_3, u_4} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2}
  [(i : ι) → AddCommMonoid (α i)] {β : Type u_3} [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M]
  [Modulus β M] (T : MultisubadditiveMap α β) (A : (i : ι) → EQuasinorm (α i)) (B : EQuasinorm β) (C : ℝ≥0∞)
  (P : (i : ι) → α i → Prop) : PropA multisubadditive operator is bounded for quasinorms $A_i$, $B$ and a finite constant $C$ on
a predicate $P$ if for all $x = (x_i)_{i ∈ ι}$ with $P_i(x_i)$ for all $i$,
$$\|T x\|_{B} ≤ C ∏_{i∈ ι} \|x_i\|_{A_i}.$$
Since $0 · ∞ = 0$ in $[0,∞]$, one usually wants $P_i$ to imply $\|x_i\|_{A_i} < ∞$.  A(i : ι) → EQuasinorm (α i) BEQuasinorm β Cℝ≥0∞ P(i : ι) → α i → Prop ↔Iff (a b : Prop) : Prop
    TMultisubadditiveMap α β.IsBoundedForOnMultisubadditiveMap.IsBoundedForOn.{u_1, u_2, u_3, u_4} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2}
  [(i : ι) → AddCommMonoid (α i)] {β : Type u_3} [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M]
  [Modulus β M] (T : MultisubadditiveMap α β) (A : (i : ι) → EQuasinorm (α i)) (B : EQuasinorm β) (C : ℝ≥0∞)
  (P : (i : ι) → α i → Prop) : PropA multisubadditive operator is bounded for quasinorms $A_i$, $B$ and a finite constant $C$ on
a predicate $P$ if for all $x = (x_i)_{i ∈ ι}$ with $P_i(x_i)$ for all $i$,
$$\|T x\|_{B} ≤ C ∏_{i∈ ι} \|x_i\|_{A_i}.$$
Since $0 · ∞ = 0$ in $[0,∞]$, one usually wants $P_i$ to imply $\|x_i\|_{A_i} < ∞$. 
      (fun iι ↦ (A(i : ι) → EQuasinorm (α i) iι).powEQuasinorm.pow.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) {p : ℝ} (hp : 0 < p) : EQuasinorm α hp0 < p) (BEQuasinorm β.powEQuasinorm.pow.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) {p : ℝ} (hp : 0 < p) : EQuasinorm α hp0 < p) Cℝ≥0∞
      P(i : ι) → α i → Prop