Multilinear interpolation

5. Interpolation of multi-linear operators🔗

Definition5.1
Statement uses 1
Statement dependency previews
Preview
Definition 2.11
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 1
Reverse dependency previews
Preview
Theorem 5.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The norm \inf\Bigl\{\,\bigl\|\{r^{-\theta n}J(r^{n},a_{n},\bar{A}_{i})\}_{-N}^{N}\bigr\|_{\ell^{q}} : N<\infty \ \text{ and } \ \sum_{-N}^{N}a_{n}=a\,\Bigr\}.

Lean code for Definition5.1●1 definition
  • defdefined in MultilinearInterpolation/Janson.lean
    complete
    def jInfNorm.{u_1}jInfNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) (x : α) : ℝ≥0∞The norm
$$\inf\Bigl\{\,\bigl\|\{r^{-\theta n}J(r^{n},a_{n},\bar{A}_{i})\}_{-N}^{N}\bigr\|_{\ell^{q}}
 : N<\infty \ \text{ and } \ \sum_{-N}^{N}a_{n}=a\,\Bigr\}.$$  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u} (M : Type u) : Type uAn additive commutative monoid is an additive monoid with commutative `(+)`.  αType u_1] (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  α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. ) (xα : αType u_1) : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. 
    def jInfNorm.{u_1}jInfNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) (x : α) : ℝ≥0∞The norm
$$\inf\Bigl\{\,\bigl\|\{r^{-\theta n}J(r^{n},a_{n},\bar{A}_{i})\}_{-N}^{N}\bigr\|_{\ell^{q}}
 : N<\infty \ \text{ and } \ \sum_{-N}^{N}a_{n}=a\,\Bigr\}.$$  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommMonoidAddCommMonoid.{u} (M : Type u) : Type uAn additive commutative monoid is an additive monoid with commutative `(+)`.  αType u_1] (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  α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. ) (xα : αType u_1) : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure.

    The norm \inf\Bigl\{\,\bigl\|\{r^{-\theta n}J(r^{n},a_{n},\bar{A}_{i})\}_{-N}^{N}\bigr\|_{\ell^{q}} : N<\infty \ \text{ and } \ \sum_{-N}^{N}a_{n}=a\,\Bigr\}.

Theorem5.2
Statement uses 2
Statement dependency previews
Preview
Definition 5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 1
Reverse dependency previews
Preview
Theorem 1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
⚠L∃∀N

Lemma 1.

Lean code for Theorem5.2●1 theorem, incomplete
  • theoremdefined in MultilinearInterpolation/Janson.lean
    contains sorry
    theorem jInfNorm_le_kNorm.{u_1}jInfNorm_le_kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (hθ : θ ∈ Ioo 0 1) (q : ℝ≥0∞) :
  ∃ C < ∞, ∀ (x : α), jInfNorm A θ q x ≤ C * ‖x‖ₑ[A.kMethod θ q]Lemma 1.  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u} (M : Type u) : Type uAn additive commutative monoid is an additive monoid with commutative `(+)`.  αType u_1] (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  αType u_1)
  (θℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (hθθ ∈ Ioo 0 1 : θℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. IooSet.Ioo.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Ioo a b` is the left-open right-open interval $(a, b)$.  0 1) (qℝ≥0∞ : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ) :
  ∃ Cℝ≥0∞ < ∞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α : αType u_1), jInfNormjInfNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) (x : α) : ℝ≥0∞The norm
$$\inf\Bigl\{\,\bigl\|\{r^{-\theta n}J(r^{n},a_{n},\bar{A}_{i})\}_{-N}^{N}\bigr\|_{\ell^{q}}
 : N<\infty \ \text{ and } \ \sum_{-N}^{N}a_{n}=a\,\Bigr\}.$$  ACouple α θℝ qℝ≥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`. Cℝ≥0∞ *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α‖ₑ[ACouple α.kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α θℝ qℝ≥0∞]
    theorem jInfNorm_le_kNorm.{u_1}jInfNorm_le_kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (hθ : θ ∈ Ioo 0 1) (q : ℝ≥0∞) :
  ∃ C < ∞, ∀ (x : α), jInfNorm A θ q x ≤ C * ‖x‖ₑ[A.kMethod θ q]Lemma 1.  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommMonoidAddCommMonoid.{u} (M : Type u) : Type uAn additive commutative monoid is an additive monoid with commutative `(+)`.  αType u_1] (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  αType u_1) (θℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hθθ ∈ Ioo 0 1 : θℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. IooSet.Ioo.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α`Ioo a b` is the left-open right-open interval $(a, b)$.  0 1) (qℝ≥0∞ : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ) :
  ∃ Cℝ≥0∞ < ∞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α : αType u_1),
      jInfNormjInfNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) (x : α) : ℝ≥0∞The norm
$$\inf\Bigl\{\,\bigl\|\{r^{-\theta n}J(r^{n},a_{n},\bar{A}_{i})\}_{-N}^{N}\bigr\|_{\ell^{q}}
 : N<\infty \ \text{ and } \ \sum_{-N}^{N}a_{n}=a\,\Bigr\}.$$  ACouple α θℝ qℝ≥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`.
        Cℝ≥0∞ *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α‖ₑ[ACouple α.kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α θℝ qℝ≥0∞]

    Lemma 1.

Definition1.1
Statement uses 2
Statement dependency previews
Preview
Definition 3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Theorem 1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The set of ι-tuples \Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι : 0 \le θ₀ \le 1 \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\ \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i, \ \text{for some } q_i, q \in (0,\infty] \Bigr\}. The value of the parameters q,q_i are under an existential, and are not specified for the points of this set.

Lean code for Definition1.1●1 definition
  • defdefined in MultilinearInterpolation/Janson.lean
    complete
    def Ω.{u_1, u_2, u_3}Ω.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3} [AddMonoid β]
  [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι :
  0 \le θ₀ \le 1
  \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\
  \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i,
  \ \text{for some } q_i, q \in (0,\infty] \Bigr\}.$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set.
 {ι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) → AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) (αι → 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] [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]
  [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) β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 : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  βType u_3) (cα₀ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (cαι → ℝ : ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) : SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 (ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
    def Ω.{u_1, u_2, u_3}Ω.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3} [AddMonoid β]
  [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι :
  0 \le θ₀ \le 1
  \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\
  \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i,
  \ \text{for some } q_i, q \in (0,\infty] \Bigr\}.$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set.
 {ι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) → AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) (αι → 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]
  [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] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) β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 : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  βType u_3) (cα₀ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (cαι → ℝ : ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 (ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )

    The set of ι-tuples \Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι : 0 \le θ₀ \le 1 \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\ \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i, \ \text{for some } q_i, q \in (0,\infty] \Bigr\}. The value of the parameters q,q_i are under an existential, and are not specified for the points of this set.

Theorem5.3
Statement uses 3
Statement dependency previews
Preview
Definition 3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 1
Reverse dependency previews
Preview
Theorem 1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
⚠L∃∀N

Lemma 2, part 1.

Lean code for Theorem5.3●1 theorem, incomplete
  • theoremdefined in MultilinearInterpolation/Janson.lean
    contains sorry
    theorem mem_Ω_iff.{u_1, u_2, u_3}mem_Ω_iff.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3}
  [AddMonoid β] [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα θ : ι → ℝ) :
  θ ∈ Ω T A B cα₀ cα ↔
    have θ₀ := cα₀ + ∑ i, cα i;
    ∃ C < ∞,
      ∀ (a : (i : ι) → α i), ‖T a‖ₑ[B.kMethod θ₀ ∞] ≤ C * ∏ i, ‖a i‖ₑ[(A i).fst] ^ (1 - θ i) * ‖a i‖ₑ[(A i).snd] ^ θ iLemma 2, part 1.  {ι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) → AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) (αι → 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] [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]
  [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) β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 : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  βType u_3) (cα₀ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (cαι → ℝ θι → ℝ : ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  θι → ℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. ΩΩ.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3} [AddMonoid β]
  [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι :
  0 \le θ₀ \le 1
  \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\
  \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i,
  \ \text{for some } q_i, q \in (0,\infty] \Bigr\}.$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ ↔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 `<->`).
    have θ₀ℝ := cα₀ℝ +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`. ∑ iι, cαι → ℝ iι;
    ∃ Cℝ≥0∞ < ∞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`.,
      ∀ (a(i : ι) → α i : (iι : ιType u_1) → αι → Type u_2 iι),
        ‖TMultisubadditiveMap α β a(i : ι) → α i‖ₑ[BCouple β.kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α θ₀ℝ ∞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`.] ≤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`.
          Cℝ≥0∞ *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`.
            ∏ iι, ‖a(i : ι) → α i iι‖ₑ[(A(i : ι) → Couple (α i) iι).fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddMonoid α] (self : Couple α) : EQuasinorm αThe first quasinorm. ] ^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). θι → ℝ iι)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`. ‖a(i : ι) → α i iι‖ₑ[(A(i : ι) → Couple (α i) iι).sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddMonoid α] (self : Couple α) : EQuasinorm αThe second quasinorm. ] ^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`. θι → ℝ iι
    theorem mem_Ω_iff.{u_1, u_2, u_3}mem_Ω_iff.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3}
  [AddMonoid β] [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα θ : ι → ℝ) :
  θ ∈ Ω T A B cα₀ cα ↔
    have θ₀ := cα₀ + ∑ i, cα i;
    ∃ C < ∞,
      ∀ (a : (i : ι) → α i), ‖T a‖ₑ[B.kMethod θ₀ ∞] ≤ C * ∏ i, ‖a i‖ₑ[(A i).fst] ^ (1 - θ i) * ‖a i‖ₑ[(A i).snd] ^ θ iLemma 2, part 1.  {ι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) → AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) (αι → 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]
  [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] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) β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 : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  βType u_3) (cα₀ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (cαι → ℝ θι → ℝ : ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  θι → ℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. ΩΩ.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3} [AddMonoid β]
  [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι :
  0 \le θ₀ \le 1
  \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\
  \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i,
  \ \text{for some } q_i, q \in (0,\infty] \Bigr\}.$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ ↔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 `<->`).
    have θ₀ℝ := cα₀ℝ +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`. ∑ iι, cαι → ℝ iι;
    ∃ Cℝ≥0∞ < ∞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`.,
      ∀ (a(i : ι) → α i : (iι : ιType u_1) → αι → Type u_2 iι),
        ‖TMultisubadditiveMap α β a(i : ι) → α i‖ₑ[BCouple β.kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α θ₀ℝ ∞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`.] ≤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`.
          Cℝ≥0∞ *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`.
            ∏ iι,
              ‖a(i : ι) → α i iι‖ₑ[(A(i : ι) → Couple (α i) iι).fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddMonoid α] (self : Couple α) : EQuasinorm αThe first quasinorm. ] ^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). θι → ℝ iι)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`.
                ‖a(i : ι) → α i iι‖ₑ[(A(i : ι) → Couple (α i) iι).sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddMonoid α] (self : Couple α) : EQuasinorm αThe second quasinorm. ] ^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`. θι → ℝ iι

    Lemma 2, part 1.

Theorem5.4
Statement uses 3
Statement dependency previews
Preview
Definition 3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
⚠L∃∀N

Lemma 2, part 2.

Lean code for Theorem5.4●1 theorem, incomplete
  • theoremdefined in MultilinearInterpolation/Janson.lean
    contains sorry
    theorem knorm_of_mem_Ω.{u_1, u_2, u_3}knorm_of_mem_Ω.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3}
  [AddMonoid β] [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα θ : ι → ℝ) :
  θ ∈ Ω T A B cα₀ cα →
    have θ₀ := cα₀ + ∑ i, cα i;
    ∃ C < ∞,
      ∀ (t : ℝ≥0∞) (a : (i : ι) → α i),
        B.kNorm t (T a) ≤ C * t ^ cα₀ * ∏ i, ‖a i‖ₑ[(A i).fst] ^ (1 - θ i) * ‖a i‖ₑ[(A i).snd] ^ θ iLemma 2, part 2.  {ι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) → AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) (αι → 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] [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] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) β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 : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  (αι → Type u_2 iι)) (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  βType u_3) (cα₀ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (cαι → ℝ θι → ℝ : ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  θι → ℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. ΩΩ.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3} [AddMonoid β]
  [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι :
  0 \le θ₀ \le 1
  \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\
  \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i,
  \ \text{for some } q_i, q \in (0,\infty] \Bigr\}.$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ →
    have θ₀ℝ := cα₀ℝ +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`. ∑ iι, cαι → ℝ iι;
    ∃ Cℝ≥0∞ < ∞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`.,
      ∀ (tℝ≥0∞ : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ) (a(i : ι) → α i : (iι : ιType u_1) → αι → Type u_2 iι),
        BCouple β.kNormEQuasinorm.Couple.kNorm.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ tℝ≥0∞ (TMultisubadditiveMap α β a(i : ι) → α i) ≤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`.
          Cℝ≥0∞ *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`. 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`. cα₀ℝ *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`.
            ∏ iι, ‖a(i : ι) → α i iι‖ₑ[(A(i : ι) → Couple (α i) iι).fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddMonoid α] (self : Couple α) : EQuasinorm αThe first quasinorm. ] ^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). θι → ℝ iι)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`. ‖a(i : ι) → α i iι‖ₑ[(A(i : ι) → Couple (α i) iι).sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddMonoid α] (self : Couple α) : EQuasinorm αThe second quasinorm. ] ^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`. θι → ℝ iι
    theorem knorm_of_mem_Ω.{u_1, u_2, u_3}knorm_of_mem_Ω.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3}
  [AddMonoid β] [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα θ : ι → ℝ) :
  θ ∈ Ω T A B cα₀ cα →
    have θ₀ := cα₀ + ∑ i, cα i;
    ∃ C < ∞,
      ∀ (t : ℝ≥0∞) (a : (i : ι) → α i),
        B.kNorm t (T a) ≤ C * t ^ cα₀ * ∏ i, ‖a i‖ₑ[(A i).fst] ^ (1 - θ i) * ‖a i‖ₑ[(A i).snd] ^ θ iLemma 2, part 2. 
  {ι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) → AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) (αι → 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]
  [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] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) β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 : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  βType u_3) (cα₀ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (cαι → ℝ θι → ℝ : ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  θι → ℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. ΩΩ.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3} [AddMonoid β]
  [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι :
  0 \le θ₀ \le 1
  \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\
  \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i,
  \ \text{for some } q_i, q \in (0,\infty] \Bigr\}.$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ →
    have θ₀ℝ := cα₀ℝ +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`. ∑ iι, cαι → ℝ iι;
    ∃ Cℝ≥0∞ < ∞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`.,
      ∀ (tℝ≥0∞ : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ) (a(i : ι) → α i : (iι : ιType u_1) → αι → Type u_2 iι),
        BCouple β.kNormEQuasinorm.Couple.kNorm.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ tℝ≥0∞ (TMultisubadditiveMap α β a(i : ι) → α i) ≤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`.
          Cℝ≥0∞ *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`. 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`. cα₀ℝ *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`.
            ∏ iι,
              ‖a(i : ι) → α i iι‖ₑ[(A(i : ι) → Couple (α i) iι).fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddMonoid α] (self : Couple α) : EQuasinorm αThe first quasinorm. ] ^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). θι → ℝ iι)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`.
                ‖a(i : ι) → α i iι‖ₑ[(A(i : ι) → Couple (α i) iι).sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddMonoid α] (self : Couple α) : EQuasinorm αThe second quasinorm. ] ^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`. θι → ℝ iι

    Lemma 2, part 2.

Theorem1.2
Statement uses 3
Statement dependency previews
Preview
Definition 3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
⚠L∃∀N

The set Ω is convex. In particular, if we do not care about the choice of q_is, then T is bounded in the convex hull of the (θ_i)_is for which it is already known to be bounded.

Lean code for Theorem1.2●1 theorem, incomplete
  • theoremdefined in MultilinearInterpolation/Janson.lean
    contains sorry
    theorem convex_Ω.{u_1, u_2, u_3}convex_Ω.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3}
  [AddMonoid β] [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Convex ℝ (Ω T A B cα₀ cα)The set $Ω$ is convex. In particular, if we do not care about the choice of $q_i$s, then
$T$ is bounded in the convex hull of the $(θ_i)_i$s for which it is already known to be bounded.
 {ι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) → AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) (αι → 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] [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]
  [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) β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 : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  βType u_3) (cα₀ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (cαι → ℝ : ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) : ConvexConvex.{u_1, u_2} (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) :
  PropConvexity of sets.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (ΩΩ.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3} [AddMonoid β]
  [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι :
  0 \le θ₀ \le 1
  \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\
  \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i,
  \ \text{for some } q_i, q \in (0,\infty] \Bigr\}.$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ)
    theorem convex_Ω.{u_1, u_2, u_3}convex_Ω.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3}
  [AddMonoid β] [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Convex ℝ (Ω T A B cα₀ cα)The set $Ω$ is convex. In particular, if we do not care about the choice of $q_i$s, then
$T$ is bounded in the convex hull of the $(θ_i)_i$s for which it is already known to be bounded.
 {ι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) → AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) (αι → 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]
  [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] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) β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 : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  βType u_3) (cα₀ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (cαι → ℝ : ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  ConvexConvex.{u_1, u_2} (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) :
  PropConvexity of sets.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (ΩΩ.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3} [AddMonoid β]
  [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι :
  0 \le θ₀ \le 1
  \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\
  \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i,
  \ \text{for some } q_i, q \in (0,\infty] \Bigr\}.$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ)

    The set Ω is convex. In particular, if we do not care about the choice of q_is, then T is bounded in the convex hull of the (θ_i)_is for which it is already known to be bounded.

Theorem1.3
Statement uses 4
Statement dependency previews
Preview
Definition 3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
⚠L∃∀N

If (θ_i)_i is in the interior of Ω, then T \colon \prod_i (A_i)_{θ_i,q_i} \to B_{θ_0,q_0} is bounded for every choice of exponents with q_0^{-1} \le \sum_i q_i^{-1}. This is stronger than mere membership in Ω, where the q_i,q_0 are under an existential.

Lean code for Theorem1.3●1 theorem, incomplete
  • theoremdefined in MultilinearInterpolation/Janson.lean
    contains sorry
    theorem isBoundedOn_of_mem_interior_Ω.{u_1, u_2, u_3}isBoundedOn_of_mem_interior_Ω.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)]
  {β : Type u_3} [AddMonoid β] [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i))
  (B : Couple β) (cα₀ : ℝ) (cα θ : ι → ℝ) (hθ : θ ∈ interior (Ω T A B cα₀ cα)) :
  have θ₀ := cα₀ + ∑ i, cα i;
  ∀ (q₀ : ℝ≥0∞) (q : ι → ℝ≥0∞),
    q₀⁻¹ ≤ ∑ i, (q i)⁻¹ → ∃ C, T.IsBoundedFor (fun i ↦ (A i).kMethod (θ i) (q i)) (B.kMethod θ₀ q₀) CIf $(θ_i)_i$ is in the interior of $Ω$, then
$T \colon \prod_i (A_i)_{θ_i,q_i} \to B_{θ_0,q_0}$ is bounded for every choice of
exponents with $q_0^{-1} \le \sum_i q_i^{-1}$.
This is stronger than mere membership in $Ω$, where the $q_i,q_0$ are under an existential.
 {ι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) → AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) (αι → 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] [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] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) β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 : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  (αι → Type u_2 iι)) (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  βType u_3) (cα₀ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (cαι → ℝ θι → ℝ : ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hθθ ∈ interior (Ω T A B cα₀ cα) : θι → ℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. interiorinterior.{u} {X : Type u} [TopologicalSpace X] (s : Set X) : Set XThe interior of a set `s` is the largest open subset of `s`.  (ΩΩ.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3} [AddMonoid β]
  [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι :
  0 \le θ₀ \le 1
  \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\
  \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i,
  \ \text{for some } q_i, q \in (0,\infty] \Bigr\}.$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ)) :
  have θ₀ℝ := cα₀ℝ +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`. ∑ iι, cαι → ℝ iι;
  ∀ (q₀ℝ≥0∞ : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ) (qι → ℝ≥0∞ : ιType u_1 → ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ),
    q₀ℝ≥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`. ≤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`. ∑ iι, (qι → ℝ≥0∞ iι)⁻¹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`. →
      ∃ Cℝ≥0∞,
        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 : ι) → Couple (α i) iι).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α (θι → ℝ iι) (qι → ℝ≥0∞ iι))
          (BCouple β.kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α θ₀ℝ q₀ℝ≥0∞) Cℝ≥0∞
    theorem isBoundedOn_of_mem_interior_Ω.{u_1, u_2,
    u_3}isBoundedOn_of_mem_interior_Ω.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)]
  {β : Type u_3} [AddMonoid β] [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i))
  (B : Couple β) (cα₀ : ℝ) (cα θ : ι → ℝ) (hθ : θ ∈ interior (Ω T A B cα₀ cα)) :
  have θ₀ := cα₀ + ∑ i, cα i;
  ∀ (q₀ : ℝ≥0∞) (q : ι → ℝ≥0∞),
    q₀⁻¹ ≤ ∑ i, (q i)⁻¹ → ∃ C, T.IsBoundedFor (fun i ↦ (A i).kMethod (θ i) (q i)) (B.kMethod θ₀ q₀) CIf $(θ_i)_i$ is in the interior of $Ω$, then
$T \colon \prod_i (A_i)_{θ_i,q_i} \to B_{θ_0,q_0}$ is bounded for every choice of
exponents with $q_0^{-1} \le \sum_i q_i^{-1}$.
This is stronger than mere membership in $Ω$, where the $q_i,q_0$ are under an existential.

  {ι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) → AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) (αι → 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]
  [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] [AbsAbs.{u_2} (β : Sort u_2) : Sort (max 1 u_2) β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 : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A couple of two `EQuasinorm`s on the same `AddMonoid`.  βType u_3) (cα₀ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) (cαι → ℝ θι → ℝ : ιType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hθθ ∈ interior (Ω T A B cα₀ cα) : θι → ℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. interiorinterior.{u} {X : Type u} [TopologicalSpace X] (s : Set X) : Set XThe interior of a set `s` is the largest open subset of `s`.  (ΩΩ.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddGroup (α i)] {β : Type u_3} [AddMonoid β]
  [Preorder β] [Abs β] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ)
  (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\Omega = \Bigl\{ (θ_i)_{i ∈ ι} \in [0,1]^ι :
  0 \le θ₀ \le 1
  \ \text{ and }\ T \colon \prod_{i} (A_i)_{\theta_i,q_i} \to (B)_{\theta_0,q} \text{ is bounded},\\
  \ \text{with } \theta_0 = \alpha_0 + \sum_{i} \alpha_i \theta_i,
  \ \text{for some } q_i, q \in (0,\infty] \Bigr\}.$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ)) :
  have θ₀ℝ := cα₀ℝ +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`. ∑ iι, cαι → ℝ iι;
  ∀ (q₀ℝ≥0∞ : ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ) (qι → ℝ≥0∞ : ιType u_1 → ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure. ),
    q₀ℝ≥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`. ≤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`. ∑ iι, (qι → ℝ≥0∞ iι)⁻¹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`. →
      ∃ Cℝ≥0∞,
        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 : ι) → Couple (α i) iι).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α (θι → ℝ iι) (qι → ℝ≥0∞ iι))
          (BCouple β.kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α θ₀ℝ q₀ℝ≥0∞) Cℝ≥0∞

    If (θ_i)_i is in the interior of Ω, then T \colon \prod_i (A_i)_{θ_i,q_i} \to B_{θ_0,q_0} is bounded for every choice of exponents with q_0^{-1} \le \sum_i q_i^{-1}. This is stronger than mere membership in Ω, where the q_i,q_0 are under an existential.