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 must depend 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
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
Associated Lean declarations
-
Ω[complete]
Associated Lean declarations
-
Ω[complete]
-
defdefined in MultilinearInterpolation/Janson.leancomplete
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_2iι)] {β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_2iι)) (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_2iι)] {β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_2iι)) (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 parametersq,q_iare under an existential, and are not specified for the points of this set.
They proceed to show that the set \Omega is convex.
Theorem1.2
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
Associated Lean declarations
-
convex_Ω[sorry in proof]
Associated Lean declarations
-
convex_Ω[sorry in proof]
-
theoremdefined in MultilinearInterpolation/Janson.leancontains 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_2iι)] {β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_2iι)) (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_2iι)] {β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_2iι)) (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 ofq_is, thenTis 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
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
Associated Lean declarations
-
isBoundedOn_of_mem_interior_Ω[sorry in proof]
Associated Lean declarations
-
isBoundedOn_of_mem_interior_Ω[sorry in proof]
-
theoremdefined in MultilinearInterpolation/Janson.leancontains 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_2iι)] {β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_2iι)) (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_2iι)] {β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_2iι)) (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)_iis in the interior ofΩ, thenT \colon \prod_i (A_i)_{θ_i,q_i} \to B_{θ_0,q_0}is bounded for every choice of exponents withq_0^{-1} \le \sum_i q_i^{-1}. This is stronger than mere membership inΩ, where theq_i,q_0are under an existential.
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
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
Associated Lean declarations
-
EQuasinorm.eLorentz_equiv_kMethod_of_neq[sorry in proof]
Associated Lean declarations
-
EQuasinorm.eLorentz_equiv_kMethod_of_neq[sorry in proof]
-
theoremdefined in MultilinearInterpolation/ELorentz.leancontains 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 α) {β : Type u_2} [TopologicalSpace β] [ESeminormedAddMonoid β] [ContinuousAdd β] (p₀ q₀ p₁ q₁ q p : ℝ≥0∞) (hp₀₁ : p₀ ≠ p₁) (t : ℝ≥0) (hpos : 0 < p₀ ∧ 0 < p₁ ∧ 0 < q₀ ∧ 0 < q₁ ∧ 0 < q) (hp : p⁻¹ = (1 - ↑t) / p₀ + ↑t / p₁) : eLorentz μ β p q ≈ (eLorentzCouple μ β p₀ q₀ p₁ q₁).kMethod (↑t) qFor a Banach couple $A = (A_0,A_1)$ given by two Lorentz spaces $A_0 = L_{p_0,q_0}$ and $A_1 = L_{p_1,q_1}$ where $p_0,p_1,q_0,q_1 \in (0,\infty]$ with $p_0 \neq p_1$, for all $0 < \theta < 1$ and $q \in (0,\infty]$, the real interpolation space $(A)_{\theta,q}$ is the Lorentz space $L_{p,q}$ where $p^{-1} = (1 - \theta) p_0^{-1} + \theta p_1^{-1}$.{αType u_1: Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} [mαMeasurableSpace α: MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.αType u_1] (μMeasure α: MeasureMeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] : Type u_6A measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure. The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version is written `μ.real s`.αType u_1) {βType u_2: Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.βType u_2] [ESeminormedAddMonoidESeminormedAddMonoid.{u_8} (E : Type u_8) [TopologicalSpace E] : Type u_8An e-seminormed monoid is an additive monoid endowed with a continuous enorm. Note that we do not ask for the enorm to be positive definite: non-trivial elements may have enorm zero.βType u_2] [ContinuousAddContinuousAdd.{u_1} (M : Type u_1) [TopologicalSpace M] [Add M] : PropBasic hypothesis to talk about a topological additive monoid or a topological additive semigroup. A topological additive monoid over `M`, for example, is obtained by requiring both the instances `AddMonoid M` and `ContinuousAdd M`. Continuity in each argument separately can be stated using `SeparatelyContinuousAdd α`. If one wants only continuity in either the left or right argument, but not both one can use `ContinuousConstVAdd α α`/`ContinuousConstVAdd αᵐᵒᵖ α`.βType u_2] (p₀ℝ≥0∞q₀ℝ≥0∞p₁ℝ≥0∞q₁ℝ≥0∞qℝ≥0∞pℝ≥0∞: ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.) (hp₀₁p₀ ≠ p₁: p₀ℝ≥0∞≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`, and asserts that `a` and `b` are not equal. Conventions for notations in identifiers: * The recommended spelling of `≠` in identifiers is `ne`.p₁ℝ≥0∞) (tℝ≥0: ℝ≥0NNReal : TypeNonnegative real numbers, denoted as `ℝ≥0` within the NNReal namespace) (hpos0 < p₀ ∧ 0 < p₁ ∧ 0 < q₀ ∧ 0 < q₁ ∧ 0 < q: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.p₀ℝ≥0∞∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. Conventions for notations in identifiers: * The recommended spelling of `∧` in identifiers is `and`.0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.p₁ℝ≥0∞∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. Conventions for notations in identifiers: * The recommended spelling of `∧` in identifiers is `and`.0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.q₀ℝ≥0∞∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. Conventions for notations in identifiers: * The recommended spelling of `∧` in identifiers is `and`.0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.q₁ℝ≥0∞∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. Conventions for notations in identifiers: * The recommended spelling of `∧` in identifiers is `and`.0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.qℝ≥0∞) (hpp⁻¹ = (1 - ↑t) / p₀ + ↑t / p₁: pℝ≥0∞⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `⁻¹` in identifiers is `inv`.=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.(HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).1 -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).↑tℝ≥0)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator)./HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`. The meaning of this notation is type-dependent. * For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`. * For `Nat`, `a / b` rounds downwards. * For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative. It is implemented as `Int.ediv`, the unique function satisfying `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`. Other rounding conventions are available using the functions `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding). * For `Float`, `a / 0` follows the IEEE 754 semantics for division, usually resulting in `inf` or `nan`. Conventions for notations in identifiers: * The recommended spelling of `/` in identifiers is `div`.p₀ℝ≥0∞+HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `+` in identifiers is `add`.↑tℝ≥0/HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`. The meaning of this notation is type-dependent. * For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`. * For `Nat`, `a / b` rounds downwards. * For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative. It is implemented as `Int.ediv`, the unique function satisfying `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`. Other rounding conventions are available using the functions `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding). * For `Float`, `a / 0` follows the IEEE 754 semantics for division, usually resulting in `inf` or `nan`. Conventions for notations in identifiers: * The recommended spelling of `/` in identifiers is `div`.p₁ℝ≥0∞) : eLorentzEQuasinorm.eLorentz.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) (β : Type u_2) [TopologicalSpace β] [ESeminormedAddMonoid β] [ContinuousAdd β] (p q : ℝ≥0∞) : EQuasinorm (α → β)μMeasure αβType u_2pℝ≥0∞qℝ≥0∞≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v`x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass, the notion of equivalence is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `≈` in identifiers is `equiv`.(eLorentzCoupleEQuasinorm.eLorentzCouple.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) (β : Type u_2) [TopologicalSpace β] [ESeminormedAddMonoid β] [ContinuousAdd β] (p₀ p₁ q₀ q₁ : ℝ≥0∞) : Couple (α → β)μMeasure αβType u_2p₀ℝ≥0∞q₀ℝ≥0∞p₁ℝ≥0∞q₁ℝ≥0∞).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α(↑tℝ≥0) qℝ≥0∞theorem EQuasinorm.eLorentz_equiv_kMethod_of_neq.{u_1, u_2}
EQuasinorm.eLorentz_equiv_kMethod_of_neq.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) {β : Type u_2} [TopologicalSpace β] [ESeminormedAddMonoid β] [ContinuousAdd β] (p₀ q₀ p₁ q₁ q p : ℝ≥0∞) (hp₀₁ : p₀ ≠ p₁) (t : ℝ≥0) (hpos : 0 < p₀ ∧ 0 < p₁ ∧ 0 < q₀ ∧ 0 < q₁ ∧ 0 < q) (hp : p⁻¹ = (1 - ↑t) / p₀ + ↑t / p₁) : eLorentz μ β p q ≈ (eLorentzCouple μ β p₀ q₀ p₁ q₁).kMethod (↑t) qFor a Banach couple $A = (A_0,A_1)$ given by two Lorentz spaces $A_0 = L_{p_0,q_0}$ and $A_1 = L_{p_1,q_1}$ where $p_0,p_1,q_0,q_1 \in (0,\infty]$ with $p_0 \neq p_1$, for all $0 < \theta < 1$ and $q \in (0,\infty]$, the real interpolation space $(A)_{\theta,q}$ is the Lorentz space $L_{p,q}$ where $p^{-1} = (1 - \theta) p_0^{-1} + \theta p_1^{-1}$.{αType u_1: Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} [mαMeasurableSpace α: MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.αType u_1] (μMeasure α: MeasureMeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] : Type u_6A measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure. The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version is written `μ.real s`.αType u_1) {βType u_2: Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.βType u_2] [ESeminormedAddMonoidESeminormedAddMonoid.{u_8} (E : Type u_8) [TopologicalSpace E] : Type u_8An e-seminormed monoid is an additive monoid endowed with a continuous enorm. Note that we do not ask for the enorm to be positive definite: non-trivial elements may have enorm zero.βType u_2] [ContinuousAddContinuousAdd.{u_1} (M : Type u_1) [TopologicalSpace M] [Add M] : PropBasic hypothesis to talk about a topological additive monoid or a topological additive semigroup. A topological additive monoid over `M`, for example, is obtained by requiring both the instances `AddMonoid M` and `ContinuousAdd M`. Continuity in each argument separately can be stated using `SeparatelyContinuousAdd α`. If one wants only continuity in either the left or right argument, but not both one can use `ContinuousConstVAdd α α`/`ContinuousConstVAdd αᵐᵒᵖ α`.βType u_2] (p₀ℝ≥0∞q₀ℝ≥0∞p₁ℝ≥0∞q₁ℝ≥0∞qℝ≥0∞pℝ≥0∞: ℝ≥0∞ENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.) (hp₀₁p₀ ≠ p₁: p₀ℝ≥0∞≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`, and asserts that `a` and `b` are not equal. Conventions for notations in identifiers: * The recommended spelling of `≠` in identifiers is `ne`.p₁ℝ≥0∞) (tℝ≥0: ℝ≥0NNReal : TypeNonnegative real numbers, denoted as `ℝ≥0` within the NNReal namespace) (hpos0 < p₀ ∧ 0 < p₁ ∧ 0 < q₀ ∧ 0 < q₁ ∧ 0 < q: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.p₀ℝ≥0∞∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. Conventions for notations in identifiers: * The recommended spelling of `∧` in identifiers is `and`.0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.p₁ℝ≥0∞∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. Conventions for notations in identifiers: * The recommended spelling of `∧` in identifiers is `and`.0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.q₀ℝ≥0∞∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. Conventions for notations in identifiers: * The recommended spelling of `∧` in identifiers is `and`.0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.q₁ℝ≥0∞∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be constructed and destructed like a pair: if `ha : a` and `hb : b` then `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. Conventions for notations in identifiers: * The recommended spelling of `∧` in identifiers is `and`.0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.qℝ≥0∞) (hpp⁻¹ = (1 - ↑t) / p₀ + ↑t / p₁: pℝ≥0∞⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `⁻¹` in identifiers is `inv`.=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.(HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).1 -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).↑tℝ≥0)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator)./HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`. The meaning of this notation is type-dependent. * For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`. * For `Nat`, `a / b` rounds downwards. * For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative. It is implemented as `Int.ediv`, the unique function satisfying `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`. Other rounding conventions are available using the functions `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding). * For `Float`, `a / 0` follows the IEEE 754 semantics for division, usually resulting in `inf` or `nan`. Conventions for notations in identifiers: * The recommended spelling of `/` in identifiers is `div`.p₀ℝ≥0∞+HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `+` in identifiers is `add`.↑tℝ≥0/HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`. The meaning of this notation is type-dependent. * For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`. * For `Nat`, `a / b` rounds downwards. * For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative. It is implemented as `Int.ediv`, the unique function satisfying `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`. Other rounding conventions are available using the functions `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding). * For `Float`, `a / 0` follows the IEEE 754 semantics for division, usually resulting in `inf` or `nan`. Conventions for notations in identifiers: * The recommended spelling of `/` in identifiers is `div`.p₁ℝ≥0∞) : eLorentzEQuasinorm.eLorentz.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) (β : Type u_2) [TopologicalSpace β] [ESeminormedAddMonoid β] [ContinuousAdd β] (p q : ℝ≥0∞) : EQuasinorm (α → β)μMeasure αβType u_2pℝ≥0∞qℝ≥0∞≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v`x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass, the notion of equivalence is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `≈` in identifiers is `equiv`.(eLorentzCoupleEQuasinorm.eLorentzCouple.{u_1, u_2} {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) (β : Type u_2) [TopologicalSpace β] [ESeminormedAddMonoid β] [ContinuousAdd β] (p₀ p₁ q₀ q₁ : ℝ≥0∞) : Couple (α → β)μMeasure αβType u_2p₀ℝ≥0∞q₀ℝ≥0∞p₁ℝ≥0∞q₁ℝ≥0∞).kMethodEQuasinorm.Couple.kMethod.{u_1} {α : Type u_1} [AddMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) : EQuasinorm α(↑tℝ≥0) qℝ≥0∞For a Banach couple
A = (A_0,A_1)given by two Lorentz spacesA_0 = L_{p_0,q_0}andA_1 = L_{p_1,q_1}wherep_0,p_1,q_0,q_1 \in (0,\infty]withp_0 \neq p_1, for all0 < \theta < 1andq \in (0,\infty], the real interpolation space(A)_{\theta,q}is the Lorentz spaceL_{p,q}wherep^{-1} = (1 - \theta) p_0^{-1} + \theta p_1^{-1}.
This is a recipe for getting all the intermediate Lorentz spaces using interpolation.
Definition1.1.2
uses 0used by 0XL∃∀N
Lean status
- No associated Lean code or declarations.
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
Lean status
- No associated Lean code or declarations.
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
Lean code for Theorem1.2.1●1 theorem, incomplete
Associated Lean declarations
-
aokiRolewicz_pow_equiv_self[sorry in proof]
Associated Lean declarations
-
aokiRolewicz_pow_equiv_self[sorry in proof]
-
theoremdefined in MultilinearInterpolation/AokiRolewicz.leancontains sorry
theorem aokiRolewicz_pow_equiv_self.{u_1}
aokiRolewicz_pow_equiv_self.{u_1} {α : Type u_1} [AddCommMonoid α] {A : EQuasinorm α} {p : ℝ} (hp : (2 * A.C) ^ p = 2) : (A.aokiRolewicz p hp).pow p ≈ A{α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] {AEQuasinorm α: EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A quasinorm on a monoid $α$ is a function $α → [0,∞]$ and a finite constant $C$ that sends $0 : α$ to zero and is $C$-subadditive.αType u_1} {pℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (hp(2 * A.C) ^ p = 2: (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`.2 *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`.AEQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddMonoid α] (self : EQuasinorm α) : ℝ≥0∞The subadditivity constant.)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.^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`.pℝ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.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).powEQuasinorm.pow.{u_1} {α : Type u_1} [AddMonoid α] (A : EQuasinorm α) (p : ℝ) : EQuasinorm αThe quasinorm raised to a power $p$, as a quasinorm.pℝ≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v`x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass, the notion of equivalence is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `≈` in identifiers is `equiv`.AEQuasinorm αtheorem aokiRolewicz_pow_equiv_self.{u_1}
aokiRolewicz_pow_equiv_self.{u_1} {α : Type u_1} [AddCommMonoid α] {A : EQuasinorm α} {p : ℝ} (hp : (2 * A.C) ^ p = 2) : (A.aokiRolewicz p hp).pow p ≈ A{α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] {AEQuasinorm α: EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddMonoid α] : Type u_1A quasinorm on a monoid $α$ is a function $α → [0,∞]$ and a finite constant $C$ that sends $0 : α$ to zero and is $C$-subadditive.αType u_1} {pℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (hp(2 * A.C) ^ p = 2: (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`.2 *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`.AEQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddMonoid α] (self : EQuasinorm α) : ℝ≥0∞The subadditivity constant.)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.^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`.pℝ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.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).powEQuasinorm.pow.{u_1} {α : Type u_1} [AddMonoid α] (A : EQuasinorm α) (p : ℝ) : EQuasinorm αThe quasinorm raised to a power $p$, as a quasinorm.pℝ≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v`x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass, the notion of equivalence is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `≈` in identifiers is `equiv`.AEQuasinorm α