1. Overview🔗

We want to formalize a version of interpolation for multisubadditive operators that starts with a set of points where the operator is known to have restricted weak type, and concludes that it has strong type in the interior of the convex hull of the points. For that, we use abstract K-theory and the results in Janson (1988) to get a general result stated in terms of abstract interpolation spaces, and then use isomorphisms between the abstract interpolation spaces and Lorentz spaces to transport that result to Lorentz spaces.

More concretely, fix a finite index set ι, a multisubadditive map T, couples of quasinorms A_i for i ∈ ι and an output quasinorm couple B. We are interested in knowing for which values of the parameters θ_0, \theta_i \in [0,1] and q_0, q_i ∈ (0, ∞] for i ∈ ι the map T is bounded as an operator between the K-interpolation spaces T : \prod_{i ∈ ι}(A_i)_{θ_i,p_i} → (B)_{θ_0,p_0}. It is known (see an example in Janson (1988)) that without further assumptions, we have a restriction \frac{1}{q_0} ≤ ∑_i \frac{1}{q_i} and the output parameter θ_0 depends linearly on the parameters \theta_i, in the sense that \theta_0 = α_0 + ∑_i α_i θ_i for some choice of coefficients (α_i)_{i ∈ ι} and α_0. In particular, if we start with |ι|+1 linearly independent combinations of θ_0 and (θ_i)_i for which the map is known to be bounded, then the coefficients uniquely determined.

Janson (1988) defines a set

Definition1.1

Statement uses 2

Statement dependency previews

Preview

Definition 2.18

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 6

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 \begin{aligned}\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\}.\end{aligned} The value of the parameters q,q_i are under an existential, and are not specified for the points of this set. Boundedness is only required on ∏_i (A_i)_0 ∩ (A_i)_1, where jInfNorm_le_discreteKMethod holds.

Lean code for Definition1.1●1 definition

defdefined in MultilinearInterpolation/Janson.lean

complete

def Ω.{u_1, u_2, u_3, u_4}Ω.{u_1, u_2, u_3, u_4} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddCommGroup (α i)] {β : Type u_3}
  [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M] (T : MultisubadditiveMap α β)
  (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ) (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\begin{aligned}\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\}.\end{aligned}$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set. Boundedness is only required on $∏_i (A_i)_0 ∩ (A_i)_1$, where
`jInfNorm_le_discreteKMethod` holds.
 {ι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) → AddCommGroupAddCommGroup.{u_2} (G : 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) αι → Type u_2 βType u_3) (A(i : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_3) (cα₀ℝ : ℝReal : Type) (cαι → ℝ : ιType u_1 → ℝReal : Type) : SetSet.{u} (α : Type u) : Type u (ιType u_1 → ℝReal : Type)

def Ω.{u_1, u_2, u_3, u_4}Ω.{u_1, u_2, u_3, u_4} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddCommGroup (α i)] {β : Type u_3}
  [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M] (T : MultisubadditiveMap α β)
  (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ) (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\begin{aligned}\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\}.\end{aligned}$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set. Boundedness is only required on $∏_i (A_i)_0 ∩ (A_i)_1$, where
`jInfNorm_le_discreteKMethod` holds.
 {ι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) → AddCommGroupAddCommGroup.{u_2} (G : 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) αι → Type u_2 βType u_3)
  (A(i : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_3) (cα₀ℝ : ℝReal : Type) (cαι → ℝ : ιType u_1 → ℝReal : Type) :
  SetSet.{u} (α : Type u) : Type u (ιType u_1 → ℝReal : Type)

They proceed to show that the set \Omega is convex.

Theorem1.2

Statement uses 5

Statement dependency previews

Preview

Modulus.IsDecomposable

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0⚠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, u_4, u_5}convex_Ω.{u_1, u_2, u_3, u_4, u_5} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddCommGroup (α i)]
  {β : Type u_3} [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M]
  (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ) (cα : ι → ℝ) {Mα : ι → Type u_5}
  [(i : ι) → AddCommMonoid (Mα i)] [(i : ι) → Preorder (Mα i)] [(i : ι) → Modulus (α i) (Mα i)]
  [hMα : ∀ (i : ι), Modulus.IsDecomposable (α i) (Mα i)] [hA₀ : ∀ (i : ι), (A i).fst.IsSolid]
  [hA₁ : ∀ (i : ι), (A i).snd.IsSolid] : 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_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) → AddCommGroupAddCommGroup.{u_2} (G : 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) αι → Type u_2 βType u_3)
  (A(i : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 (αι → Type u_2 iι)) (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_3) (cα₀ℝ : ℝReal : Type) (cαι → ℝ : ιType u_1 → ℝReal : Type)
  {Mαι → Type u_5 : ιType u_1 → Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [(iι : ιType u_1) → AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 (Mαι → Type u_5 iι)]
  [(iι : ιType u_1) → PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 (Mαι → Type u_5 iι)] [(iι : ιType u_1) → ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) (αι → Type u_2 iι) (Mαι → Type u_5 iι)]
  [hMα∀ (i : ι), Modulus.IsDecomposable (α i) (Mα i) : ∀ (iι : ιType u_1), Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : Prop (αι → Type u_2 iι) (Mαι → Type u_5 iι)]
  [hA₀∀ (i : ι), (A i).fst.IsSolid : ∀ (iι : ιType u_1), (A(i : ι) → Couple (α i) iι).fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop]
  [hA₁∀ (i : ι), (A i).snd.IsSolid : ∀ (iι : ιType u_1), (A(i : ι) → Couple (α i) iι).sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop] : ConvexConvex.{u_1, u_2} (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) :
  Prop ℝReal : Type (ΩΩ.{u_1, u_2, u_3, u_4} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddCommGroup (α i)] {β : Type u_3}
  [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M] (T : MultisubadditiveMap α β)
  (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ) (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\begin{aligned}\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\}.\end{aligned}$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set. Boundedness is only required on $∏_i (A_i)_0 ∩ (A_i)_1$, where
`jInfNorm_le_discreteKMethod` holds.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ)

theorem convex_Ω.{u_1, u_2, u_3, u_4, u_5}convex_Ω.{u_1, u_2, u_3, u_4, u_5} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddCommGroup (α i)]
  {β : Type u_3} [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M]
  (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ) (cα : ι → ℝ) {Mα : ι → Type u_5}
  [(i : ι) → AddCommMonoid (Mα i)] [(i : ι) → Preorder (Mα i)] [(i : ι) → Modulus (α i) (Mα i)]
  [hMα : ∀ (i : ι), Modulus.IsDecomposable (α i) (Mα i)] [hA₀ : ∀ (i : ι), (A i).fst.IsSolid]
  [hA₁ : ∀ (i : ι), (A i).snd.IsSolid] : 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_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) → AddCommGroupAddCommGroup.{u_2} (G : 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) αι → Type u_2 βType u_3)
  (A(i : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_3) (cα₀ℝ : ℝReal : Type) (cαι → ℝ : ιType u_1 → ℝReal : Type)
  {Mαι → Type u_5 : ιType u_1 → Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [(iι : ιType u_1) → AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 (Mαι → Type u_5 iι)]
  [(iι : ιType u_1) → PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 (Mαι → Type u_5 iι)]
  [(iι : ιType u_1) → ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) (αι → Type u_2 iι) (Mαι → Type u_5 iι)]
  [hMα∀ (i : ι), Modulus.IsDecomposable (α i) (Mα i) :
    ∀ (iι : ιType u_1),
      Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : Prop (αι → Type u_2 iι) (Mαι → Type u_5 iι)]
  [hA₀∀ (i : ι), (A i).fst.IsSolid : ∀ (iι : ιType u_1), (A(i : ι) → Couple (α i) iι).fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop]
  [hA₁∀ (i : ι), (A i).snd.IsSolid : ∀ (iι : ιType u_1), (A(i : ι) → Couple (α i) iι).sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop] :
  ConvexConvex.{u_1, u_2} (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) :
  Prop ℝReal : Type (ΩΩ.{u_1, u_2, u_3, u_4} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddCommGroup (α i)] {β : Type u_3}
  [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M] (T : MultisubadditiveMap α β)
  (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ) (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\begin{aligned}\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\}.\end{aligned}$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set. Boundedness is only required on $∏_i (A_i)_0 ∩ (A_i)_1$, where
`jInfNorm_le_discreteKMethod` holds.
 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.

As remarked in the statement above, this still does not handle particular choices of q_is, which is necessary for strong-type bounds, where we want the p and q of the Lorentz space L_{p,q} to be the same. This is finally handled in their Theorem 2 below.

Theorem1.3

Statement uses 8

Statement dependency previews

Preview

Modulus.IsDecomposable

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0⚠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. As in Ω, boundedness is on ∏_i (A_i)_0 ∩ (A_i)_1.

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, u_4, u_5}isBoundedOn_of_mem_interior_Ω.{u_1, u_2, u_3, u_4, u_5} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2}
  [(i : ι) → AddCommGroup (α i)] {β : Type u_3} [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M]
  [Modulus β M] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ) (cα : ι → ℝ)
  {Mα : ι → Type u_5} [(i : ι) → AddCommMonoid (Mα i)] [(i : ι) → Preorder (Mα i)] [(i : ι) → Modulus (α i) (Mα i)]
  [hMα : ∀ (i : ι), Modulus.IsDecomposable (α i) (Mα i)] [hA₀ : ∀ (i : ι), (A i).fst.IsSolid]
  [hA₁ : ∀ (i : ι), (A i).snd.IsSolid] (θ : ι → ℝ) (hθ : θ ∈ interior (Ω T A B cα₀ cα)) :
  have θ₀ := cα₀ + ∑ i, cα i * θ i;
  ∀ (q₀ : ℝ≥0∞) (q : ι → ℝ≥0∞),
    q₀⁻¹ ≤ ∑ i, (q i)⁻¹ →
      ∃ C,
        T.IsBoundedForOn (fun i ↦ (A i).kMethod (θ i) (q i)) (B.kMethod θ₀ q₀) C fun i x ↦
          x ∈ (A i).inf.finiteLocus ∧ ‖x‖ₑ[(A i).kMethod (θ i) (q i)] < ∞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.
As in $Ω$, boundedness is on $∏_i (A_i)_0 ∩ (A_i)_1$.
 {ι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) → AddCommGroupAddCommGroup.{u_2} (G : 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) αι → Type u_2 βType u_3)
  (A(i : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 (αι → Type u_2 iι)) (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_3) (cα₀ℝ : ℝReal : Type) (cαι → ℝ : ιType u_1 → ℝReal : Type)
  {Mαι → Type u_5 : ιType u_1 → Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [(iι : ιType u_1) → AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 (Mαι → Type u_5 iι)]
  [(iι : ιType u_1) → PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 (Mαι → Type u_5 iι)] [(iι : ιType u_1) → ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) (αι → Type u_2 iι) (Mαι → Type u_5 iι)]
  [hMα∀ (i : ι), Modulus.IsDecomposable (α i) (Mα i) : ∀ (iι : ιType u_1), Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : Prop (αι → Type u_2 iι) (Mαι → Type u_5 iι)]
  [hA₀∀ (i : ι), (A i).fst.IsSolid : ∀ (iι : ιType u_1), (A(i : ι) → Couple (α i) iι).fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop]
  [hA₁∀ (i : ι), (A i).snd.IsSolid : ∀ (iι : ιType u_1), (A(i : ι) → Couple (α i) iι).sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop] (θι → ℝ : ιType u_1 → ℝReal : Type)
  (hθθ ∈ interior (Ω T A B cα₀ cα) : θι → ℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → Prop interiorinterior.{u} {X : Type u} [TopologicalSpace X] (s : Set X) : Set X (ΩΩ.{u_1, u_2, u_3, u_4} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddCommGroup (α i)] {β : Type u_3}
  [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M] (T : MultisubadditiveMap α β)
  (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ) (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\begin{aligned}\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\}.\end{aligned}$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set. Boundedness is only required on $∏_i (A_i)_0 ∩ (A_i)_1$, where
`jInfNorm_le_discreteKMethod` holds.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ)) :
  have θ₀ℝ := cα₀ℝ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ ∑ iι, cαι → ℝ iι *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ θι → ℝ iι;
  ∀ (q₀ℝ≥0∞ : ℝ≥0∞ENNReal : Type) (qι → ℝ≥0∞ : ιType u_1 → ℝ≥0∞ENNReal : Type),
    q₀ℝ≥0∞⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop ∑ iι, (qι → ℝ≥0∞ iι)⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α →
      ∃ Cℝ≥0∞,
        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) : Prop (fun iι ↦ (A(i : ι) → Couple (α i) iι).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α (θι → ℝ iι) (qι → ℝ≥0∞ iι))
          (BCouple β.kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α θ₀ℝ q₀ℝ≥0∞) Cℝ≥0∞ fun iι xα i ↦
          xα i ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → Prop (A(i : ι) → Couple (α i) iι).infEQuasinorm.Couple.inf.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) : EQuasinorm α.finiteLocusEQuasinorm.finiteLocus.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) : AddSubmonoid α ∧And (a b : Prop) : Prop
            ‖xα i‖ₑ[(A(i : ι) → Couple (α i) iι).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α (θι → ℝ iι) (qι → ℝ≥0∞ iι)] <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop ∞Top.top.{u_1} {α : Type u_1} [self : Top α] : α

theorem isBoundedOn_of_mem_interior_Ω.{u_1, u_2,
    u_3, u_4, u_5}isBoundedOn_of_mem_interior_Ω.{u_1, u_2, u_3, u_4, u_5} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2}
  [(i : ι) → AddCommGroup (α i)] {β : Type u_3} [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M]
  [Modulus β M] (T : MultisubadditiveMap α β) (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ) (cα : ι → ℝ)
  {Mα : ι → Type u_5} [(i : ι) → AddCommMonoid (Mα i)] [(i : ι) → Preorder (Mα i)] [(i : ι) → Modulus (α i) (Mα i)]
  [hMα : ∀ (i : ι), Modulus.IsDecomposable (α i) (Mα i)] [hA₀ : ∀ (i : ι), (A i).fst.IsSolid]
  [hA₁ : ∀ (i : ι), (A i).snd.IsSolid] (θ : ι → ℝ) (hθ : θ ∈ interior (Ω T A B cα₀ cα)) :
  have θ₀ := cα₀ + ∑ i, cα i * θ i;
  ∀ (q₀ : ℝ≥0∞) (q : ι → ℝ≥0∞),
    q₀⁻¹ ≤ ∑ i, (q i)⁻¹ →
      ∃ C,
        T.IsBoundedForOn (fun i ↦ (A i).kMethod (θ i) (q i)) (B.kMethod θ₀ q₀) C fun i x ↦
          x ∈ (A i).inf.finiteLocus ∧ ‖x‖ₑ[(A i).kMethod (θ i) (q i)] < ∞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.
As in $Ω$, boundedness is on $∏_i (A_i)_0 ∩ (A_i)_1$.

  {ι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) → AddCommGroupAddCommGroup.{u_2} (G : 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) αι → Type u_2 βType u_3)
  (A(i : ι) → Couple (α i) : (iι : ιType u_1) → CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 (αι → Type u_2 iι))
  (BCouple β : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 βType u_3) (cα₀ℝ : ℝReal : Type) (cαι → ℝ : ιType u_1 → ℝReal : Type)
  {Mαι → Type u_5 : ιType u_1 → Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [(iι : ιType u_1) → AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 (Mαι → Type u_5 iι)]
  [(iι : ιType u_1) → PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 (Mαι → Type u_5 iι)]
  [(iι : ιType u_1) → ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) (αι → Type u_2 iι) (Mαι → Type u_5 iι)]
  [hMα∀ (i : ι), Modulus.IsDecomposable (α i) (Mα i) :
    ∀ (iι : ιType u_1),
      Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : Prop (αι → Type u_2 iι) (Mαι → Type u_5 iι)]
  [hA₀∀ (i : ι), (A i).fst.IsSolid : ∀ (iι : ιType u_1), (A(i : ι) → Couple (α i) iι).fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop]
  [hA₁∀ (i : ι), (A i).snd.IsSolid : ∀ (iι : ιType u_1), (A(i : ι) → Couple (α i) iι).sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop]
  (θι → ℝ : ιType u_1 → ℝReal : Type)
  (hθθ ∈ interior (Ω T A B cα₀ cα) : θι → ℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → Prop interiorinterior.{u} {X : Type u} [TopologicalSpace X] (s : Set X) : Set X (ΩΩ.{u_1, u_2, u_3, u_4} {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → AddCommGroup (α i)] {β : Type u_3}
  [AddCommMonoid β] {M : Type u_4} [AddCommMonoid M] [Preorder M] [Modulus β M] (T : MultisubadditiveMap α β)
  (A : (i : ι) → Couple (α i)) (B : Couple β) (cα₀ : ℝ) (cα : ι → ℝ) : Set (ι → ℝ)The set of $ι$-tuples
$$\begin{aligned}\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\}.\end{aligned}$$
The value of the parameters $q,q_i$ are under an existential, and are not specified
for the points of this set. Boundedness is only required on $∏_i (A_i)_0 ∩ (A_i)_1$, where
`jInfNorm_le_discreteKMethod` holds.
 TMultisubadditiveMap α β A(i : ι) → Couple (α i) BCouple β cα₀ℝ cαι → ℝ)) :
  have θ₀ℝ := cα₀ℝ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ ∑ iι, cαι → ℝ iι *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ θι → ℝ iι;
  ∀ (q₀ℝ≥0∞ : ℝ≥0∞ENNReal : Type) (qι → ℝ≥0∞ : ιType u_1 → ℝ≥0∞ENNReal : Type),
    q₀ℝ≥0∞⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop ∑ iι, (qι → ℝ≥0∞ iι)⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α →
      ∃ Cℝ≥0∞,
        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) : Prop
          (fun iι ↦
            (A(i : ι) → Couple (α i) iι).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α (θι → ℝ iι) (qι → ℝ≥0∞ iι))
          (BCouple β.kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α θ₀ℝ q₀ℝ≥0∞) Cℝ≥0∞ fun iι xα i ↦
          xα i ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → Prop (A(i : ι) → Couple (α i) iι).infEQuasinorm.Couple.inf.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) : EQuasinorm α.finiteLocusEQuasinorm.finiteLocus.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) : AddSubmonoid α ∧And (a b : Prop) : Prop
            ‖xα i‖ₑ[(A(i : ι) → Couple (α i) iι).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α (θι → ℝ iι)
                  (qι → ℝ≥0∞ iι)] <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop
              ∞Top.top.{u_1} {α : Type u_1} [self : Top α] : α

There are three important caveats, and they will be addressed in the sections below. First, we must relate the abstract statement above with the concrete Lorentz spaces. Second, the proofs in Janson (1988) are written for seminorms (a quasinorm with subadditivity constant 1), and the adaptation to quasinorms requires an extra step. And finally, the proofs in the paper assume that we work with all the different norms inside the restricted spaces given by the intersection of the elements of the couples, and then have the conclusion extended to the whole space. This is generally possible to do in L_{p,q} for q ≠ ∞ because the intersections contain simple functions of finite integral, which are dense.

1.1. From restricted weak type to strong type in the interior🔗

To get the result about restricted weak type and strong type mentioned in the introduction, we make use of the following result.

Theorem1.1.1

Statement uses 5

Statement dependency previews

Preview

Definition 2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0⚠L∃∀N

For a Banach couple A = (A_0,A_1) given by two Lorentz spaces A_0 = L_{p_0,q_0} and A_1 = L_{p_1,q_1} where p_0,p_1,q_0,q_1 \in (0,\infty] with p_0 \neq p_1, for all 0 < \theta < 1 and q \in (0,\infty], the real interpolation space (A)_{\theta,q} is the Lorentz space L_{p,q} where p^{-1} = (1 - \theta) p_0^{-1} + \theta p_1^{-1}.

Lean code for Theorem1.1.1●1 theorem, incomplete

theoremdefined in MultilinearInterpolation/ELorentz.lean

contains sorry

theorem EQuasinorm.eLorentz_equiv_kMethod_of_neq.{u_1, u_2}EQuasinorm.eLorentz_equiv_kMethod_of_neq.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α)
  [SigmaFinite μ] {β : Type u_2} [TopologicalSpace β] [ESeminormedAddCommMonoid β] [ContinuousAdd β]
  (p₀ q₀ p₁ q₁ q p : ℝ≥0∞) (hp₀₁ : p₀ ≠ p₁) (t : ℝ≥0) (hpos : 0 < p₀ ∧ 0 < p₁ ∧ 0 < q₀ ∧ 0 < q₁ ∧ 0 < q)
  (hp : p⁻¹ = (1 - ↑t) / p₀ + ↑t / p₁) : eLorentz μ β p q ≈ (eLorentzCouple μ β p₀ q₀ p₁ q₁).kMethod (↑t) qFor a Banach couple $A = (A_0,A_1)$ given by two Lorentz spaces
$A_0 = L_{p_0,q_0}$ and $A_1 = L_{p_1,q_1}$ where $p_0,p_1,q_0,q_1 \in (0,\infty]$ with
$p_0 \neq p_1$, for all $0 < \theta < 1$ and $q \in (0,\infty]$, the real interpolation space
$(A)_{\theta,q}$ is the Lorentz space $L_{p,q}$ where
$p^{-1} = (1 - \theta) p_0^{-1} + \theta p_1^{-1}$.
 {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [mαMeasurableSpace α : MeasurableSpaceMeasurableSpace.{u_6} (α : Type u_6) : Type u_6 αType u_1] (μMeasure α : MeasureMeasureTheory.Measure.{u_5} (α : Type u_5) [MeasurableSpace α] : Type u_5 αType u_1) [SigmaFiniteMeasureTheory.SigmaFinite.{u_1} {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) : Prop μMeasure α]
  {βType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type u βType u_2] [ESeminormedAddCommMonoidESeminormedAddCommMonoid.{u_4} (E : Type u_4) [TopologicalSpace E] : Type u_4 βType u_2]
  [ContinuousAddContinuousAdd.{u_1} (M : Type u_1) [TopologicalSpace M] [Add M] : Prop βType u_2] (p₀ℝ≥0∞ q₀ℝ≥0∞ p₁ℝ≥0∞ q₁ℝ≥0∞ qℝ≥0∞ pℝ≥0∞ : ℝ≥0∞ENNReal : Type) (hp₀₁p₀ ≠ p₁ : p₀ℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop p₁ℝ≥0∞) (tℝ≥0 : ℝ≥0NNReal : Type)
  (hpos0 < p₀ ∧ 0 < p₁ ∧ 0 < q₀ ∧ 0 < q₁ ∧ 0 < q : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop p₀ℝ≥0∞ ∧And (a b : Prop) : Prop 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop p₁ℝ≥0∞ ∧And (a b : Prop) : Prop 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop q₀ℝ≥0∞ ∧And (a b : Prop) : Prop 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop q₁ℝ≥0∞ ∧And (a b : Prop) : Prop 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop qℝ≥0∞)
  (hpp⁻¹ = (1 - ↑t) / p₀ + ↑t / p₁ : pℝ≥0∞⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α =Eq.{u_1} {α : Sort u_1} : α → α → Prop (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ1 -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ ↑tℝ≥0)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ p₀ℝ≥0∞ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ ↑tℝ≥0 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ p₁ℝ≥0∞) :
  eLorentzEQuasinorm.eLorentz.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) [SigmaFinite μ] (β : Type u_2)
  [TopologicalSpace β] [ESeminormedAddCommMonoid β] [ContinuousAdd β] (p q : ℝ≥0∞) : EQuasinorm (α → β) μMeasure α βType u_2 pℝ≥0∞ qℝ≥0∞ ≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v (eLorentzCoupleEQuasinorm.eLorentzCouple.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) [SigmaFinite μ]
  (β : Type u_2) [TopologicalSpace β] [ESeminormedAddCommMonoid β] [ContinuousAdd β] (p₀ p₁ q₀ q₁ : ℝ≥0∞) :
  Couple (α → β) μMeasure α βType u_2 p₀ℝ≥0∞ q₀ℝ≥0∞ p₁ℝ≥0∞ q₁ℝ≥0∞).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α (↑tℝ≥0) qℝ≥0∞

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

  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [mαMeasurableSpace α : MeasurableSpaceMeasurableSpace.{u_6} (α : Type u_6) : Type u_6 αType u_1]
  (μMeasure α : MeasureMeasureTheory.Measure.{u_5} (α : Type u_5) [MeasurableSpace α] : Type u_5 αType u_1) [SigmaFiniteMeasureTheory.SigmaFinite.{u_1} {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) : Prop μMeasure α]
  {βType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type u βType u_2]
  [ESeminormedAddCommMonoidESeminormedAddCommMonoid.{u_4} (E : Type u_4) [TopologicalSpace E] : Type u_4 βType u_2]
  [ContinuousAddContinuousAdd.{u_1} (M : Type u_1) [TopologicalSpace M] [Add M] : Prop βType u_2]
  (p₀ℝ≥0∞ q₀ℝ≥0∞ p₁ℝ≥0∞ q₁ℝ≥0∞ qℝ≥0∞ pℝ≥0∞ : ℝ≥0∞ENNReal : Type)
  (hp₀₁p₀ ≠ p₁ : p₀ℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop p₁ℝ≥0∞) (tℝ≥0 : ℝ≥0NNReal : Type)
  (hpos0 < p₀ ∧ 0 < p₁ ∧ 0 < q₀ ∧ 0 < q₁ ∧ 0 < q :
    0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop p₀ℝ≥0∞ ∧And (a b : Prop) : Prop
      0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop p₁ℝ≥0∞ ∧And (a b : Prop) : Prop 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop q₀ℝ≥0∞ ∧And (a b : Prop) : Prop 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop q₁ℝ≥0∞ ∧And (a b : Prop) : Prop 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop qℝ≥0∞)
  (hpp⁻¹ = (1 - ↑t) / p₀ + ↑t / p₁ : pℝ≥0∞⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α =Eq.{u_1} {α : Sort u_1} : α → α → Prop (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ1 -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ ↑tℝ≥0)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ p₀ℝ≥0∞ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ ↑tℝ≥0 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ p₁ℝ≥0∞) :
  eLorentzEQuasinorm.eLorentz.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) [SigmaFinite μ] (β : Type u_2)
  [TopologicalSpace β] [ESeminormedAddCommMonoid β] [ContinuousAdd β] (p q : ℝ≥0∞) : EQuasinorm (α → β) μMeasure α βType u_2 pℝ≥0∞ qℝ≥0∞ ≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v
    (eLorentzCoupleEQuasinorm.eLorentzCouple.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) [SigmaFinite μ]
  (β : Type u_2) [TopologicalSpace β] [ESeminormedAddCommMonoid β] [ContinuousAdd β] (p₀ p₁ q₀ q₁ : ℝ≥0∞) :
  Couple (α → β) μMeasure α βType u_2 p₀ℝ≥0∞ q₀ℝ≥0∞ p₁ℝ≥0∞
          q₁ℝ≥0∞).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α
      (↑tℝ≥0) qℝ≥0∞

This is a recipe for getting all the intermediate Lorentz spaces using interpolation.

Definition1.1.2

uses 0used by 0XL∃∀N

We say that a multisubadditive map T has restricted weak type for p_0, p_i ∈ (0,∞] and i ∈ ι if it is bounded as an operator T : ∏_{i ∈ ι}L_{p_i,1} \to L_{p_0,\infty}.

Definition1.1.3

uses 0used by 0XL∃∀N

We say that a multisubadditive map T has strong type for p_0, p_i ∈ (0,∞] and i ∈ ι if it is bounded as an operator T : ∏_{i ∈ ι}L_{p_i} \to L_{p_0}, where L_{p}=L_{p,p}.

Suppose now that we have |ι|+1 linearly independent tuples \big(p_0^{(j)}, (p_i^{(j)})_{i∈ ι}\big) for 1 ≤ j ≤ |ι| + 1 and the operator is known to have restricted weak type for each tuple.

We want to conclude that T has strong type in the interior of the convex hull (p_i^{(j)})_{i∈ ι}, where output parameter p_0 is linearly determined by the input (p_i)_{i∈ ι}. For that, let p_i^{\text{min}}=\min_{j}p_i^{(j)} and p_0^{\text{min}}=\min_{j}p_0^{(j)} and define the couples

A_i = (L_{p_i^{\text{min}},1}, L_{∞,∞}), \quad B = (L_{p_0^{\text{min}},1}, L_{∞,∞}).

Therefore, the "cube" formed by the possible interpolation spaces ∏_i(A_i)_{\theta_i,1} contains the initial tuples. And as remarked before, the choice of couples and the linear independence of the tuples also uniquely define coefficients α_0 and (\alpha_i)_i so that Ω contains the initial tuples.

Applying Theorem 1.3, we get the desired strong type bounds for any point in the interior of \Omega, as long as p_0⁻¹ ≤ ∑_i p_i⁻¹.

1.2. Dealing with quasinorms🔗

The argument in Janson (1988) uses seminorms, which are the special case of quasinorms when the constant C = 1. It's a theorem that every C-quasinorm is equivalent to a seminorm raised to the power p such that (2 C) ^ p = 2.

Theorem1.2.1

Statement uses 4

Statement dependency previews

Preview

Definition 2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0⚠L∃∀N

Lean code for Theorem1.2.1●1 theorem, incomplete

theoremdefined in MultilinearInterpolation/AokiRolewicz.lean

contains sorry

theorem aokiRolewicz_equiv_pow.{u_1}aokiRolewicz_equiv_pow.{u_1} {α : Type u_1} [AddCommMonoid α] {A : EQuasinorm α} {p : ℝ} (hp : (2 * A.C) ^ p = 2) :
  (A.aokiRolewicz p hp).toEQuasinorm ≈ A.pow ⋯ {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  {AEQuasinorm α : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1} {pℝ : ℝReal : Type} (hp(2 * A.C) ^ p = 2 : (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ2 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ AEQuasinorm α.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 α β γ] : α → β → γ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ pℝ =Eq.{u_1} {α : Sort u_1} : α → α → Prop 2) :
  (AEQuasinorm α.aokiRolewiczEQuasinorm.aokiRolewicz.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) (p : ℝ) (hp : (2 * A.C) ^ p = 2) :
  ESeminorm α pℝ hp(2 * A.C) ^ p = 2).toEQuasinormESeminorm.toEQuasinorm.{u_1} {α : Type u_1} [AddCommMonoid α] (self : ESeminorm α) : EQuasinorm α ≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v AEQuasinorm α.powEQuasinorm.pow.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) {p : ℝ} (hp : 0 < p) : EQuasinorm α ⋯

theorem aokiRolewicz_equiv_pow.{u_1}aokiRolewicz_equiv_pow.{u_1} {α : Type u_1} [AddCommMonoid α] {A : EQuasinorm α} {p : ℝ} (hp : (2 * A.C) ^ p = 2) :
  (A.aokiRolewicz p hp).toEQuasinorm ≈ A.pow ⋯
  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  {AEQuasinorm α : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1} {pℝ : ℝReal : Type}
  (hp(2 * A.C) ^ p = 2 : (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ2 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ AEQuasinorm α.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 α β γ] : α → β → γ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ pℝ =Eq.{u_1} {α : Sort u_1} : α → α → Prop 2) :
  (AEQuasinorm α.aokiRolewiczEQuasinorm.aokiRolewicz.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) (p : ℝ) (hp : (2 * A.C) ^ p = 2) :
  ESeminorm α pℝ hp(2 * A.C) ^ p = 2).toEQuasinormESeminorm.toEQuasinorm.{u_1} {α : Type u_1} [AddCommMonoid α] (self : ESeminorm α) : EQuasinorm α ≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v
    AEQuasinorm α.powEQuasinorm.pow.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) {p : ℝ} (hp : 0 < p) : EQuasinorm α ⋯

Multilinear interpolation

1. Overview🔗

1.1. From restricted weak type to strong type in the interior🔗

1.2. Dealing with quasinorms🔗

1.3. Extending from the intersection to the closure🔗