Riesz–Thorin interpolation theorem

TheoremRiesz–Thorin interpolation on finite sets, auxiliary form#✓fully proved

Let \(\iota\) and \(\kappa\) be finite sets, each with a σ-algebra in which singletons are measurable and with the counting measure, and write \(\|g\|_r \in [0, \infty]\) for the \(\ell^r\) norm of \(g\) with respect to the counting measure. Let \(p_0, p_1, p, q_0, q_1, q \in [1, \infty]\) and \(\theta \in [0, 1]\) satisfy \(1/p = (1-\theta)/p_0 + \theta/p_1\) and \(1/q = (1-\theta)/q_0 + \theta/q_1\), where \(1/\infty = 0\). Let \(M_0, M_1 \in [0, \infty]\) and let \(T : \mathbb{C}^\iota \to \mathbb{C}^\kappa\) be a \(\mathbb{C}\)-linear map with \(\|Tf\|_{q_0} \le M_0 \|f\|_{p_0}\) and \(\|Tf\|_{q_1} \le M_1 \|f\|_{p_1}\) for all \(f \in \mathbb{C}^\iota\). Then \(\|Tf\|_q \le M_0^{1-\theta} M_1^{\theta} \|f\|_p\) for all \(f \in \mathbb{C}^\iota\), where products and powers are computed in \([0, \infty]\) with \(0 \cdot \infty = 0\) and \(c^0 = 1\).

This is the Riesz–Thorin interpolation theorem on finite sets with finiteness assumed as a property rather than given by an explicit enumeration of the elements; that theorem is derived from this one.

MathlibExt.Analysis.FunctionalAnalysis.RieszThorinWanted.riesz_thorin_finite · 21 lines

theorem riesz_thorin_finite
    {ι κ : Type*} [Finite ι] [Finite κ]
    [MeasurableSpace ι] [MeasurableSpace κ]
    [MeasurableSingletonClass ι] [MeasurableSingletonClass κ]
    {p₀ p₁ q₀ q₁ p q : ENNReal}
    {θ : ℝ} (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1)
    (hp₀ : 1 ≤ p₀) (hp₁ : 1 ≤ p₁) (hp : 1 ≤ p)
    (hq₀ : 1 ≤ q₀) (hq₁ : 1 ≤ q₁) (hq : 1 ≤ q)
    (hp_eq : p⁻¹ = ENNReal.ofReal (1 - θ) * p₀⁻¹ + ENNReal.ofReal θ * p₁⁻¹)
    (hq_eq : q⁻¹ = ENNReal.ofReal (1 - θ) * q₀⁻¹ + ENNReal.ofReal θ * q₁⁻¹)
    {M₀ M₁ : ENNReal}
    (T : (ι → Complex) →ₗ[Complex] (κ → Complex))
    (h₀ : ∀ f : ι → Complex,
      eLpNorm (T f) q₀ (Measure.count : Measure κ) ≤
        M₀ * eLpNorm f p₀ (Measure.count : Measure ι))
    (h₁ : ∀ f : ι → Complex,
      eLpNorm (T f) q₁ (Measure.count : Measure κ) ≤
        M₁ * eLpNorm f p₁ (Measure.count : Measure ι)) :
    ∀ f : ι → Complex,
      eLpNorm (T f) q (Measure.count : Measure κ) ≤
        (M₀ ^ (1 - θ) * M₁ ^ θ) * eLpNorm f p (Measure.count : Measure ι)

Used by 1

Used byRiesz–Thorin interpolation theorem on finite sets

TheoremRiesz–Thorin interpolation theorem on finite sets#✓fully proved

Let \(\iota\) and \(\kappa\) be finite sets, each with a σ-algebra in which singletons are measurable and with the counting measure, and write \(\|g\|_r \in [0, \infty]\) for the \(\ell^r\) norm of \(g\) with respect to the counting measure. Let \(p_0, p_1, p, q_0, q_1, q \in [1, \infty]\) and \(\theta \in [0, 1]\) satisfy \(1/p = (1-\theta)/p_0 + \theta/p_1\) and \(1/q = (1-\theta)/q_0 + \theta/q_1\), where \(1/\infty = 0\). Let \(M_0, M_1 \in [0, \infty]\) and let \(T : \mathbb{C}^\iota \to \mathbb{C}^\kappa\) be a \(\mathbb{C}\)-linear map with \(\|Tf\|_{q_0} \le M_0 \|f\|_{p_0}\) and \(\|Tf\|_{q_1} \le M_1 \|f\|_{p_1}\) for all \(f \in \mathbb{C}^\iota\). Then \(\|Tf\|_q \le M_0^{1-\theta} M_1^{\theta} \|f\|_p\) for all \(f \in \mathbb{C}^\iota\), where products and powers are computed in \([0, \infty]\) with \(0 \cdot \infty = 0\) and \(c^0 = 1\).

MathlibExt.Analysis.FunctionalAnalysis.RieszThorinWanted.riesz_thorin · 21 lines

theorem riesz_thorin
    {ι κ : Type*} [Fintype ι] [Fintype κ]
    [MeasurableSpace ι] [MeasurableSpace κ]
    [MeasurableSingletonClass ι] [MeasurableSingletonClass κ]
    {p₀ p₁ q₀ q₁ p q : ENNReal}
    {θ : ℝ} (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1)
    (hp₀ : 1 ≤ p₀) (hp₁ : 1 ≤ p₁) (hp : 1 ≤ p)
    (hq₀ : 1 ≤ q₀) (hq₁ : 1 ≤ q₁) (hq : 1 ≤ q)
    (hp_eq : p⁻¹ = ENNReal.ofReal (1 - θ) * p₀⁻¹ + ENNReal.ofReal θ * p₁⁻¹)
    (hq_eq : q⁻¹ = ENNReal.ofReal (1 - θ) * q₀⁻¹ + ENNReal.ofReal θ * q₁⁻¹)
    {M₀ M₁ : ENNReal}
    (T : (ι → Complex) →ₗ[Complex] (κ → Complex))
    (h₀ : ∀ f : ι → Complex,
      eLpNorm (T f) q₀ (Measure.count : Measure κ) ≤
        M₀ * eLpNorm f p₀ (Measure.count : Measure ι))
    (h₁ : ∀ f : ι → Complex,
      eLpNorm (T f) q₁ (Measure.count : Measure κ) ≤
        M₁ * eLpNorm f p₁ (Measure.count : Measure ι)) :
    ∀ f : ι → Complex,
      eLpNorm (T f) q (Measure.count : Measure κ) ≤
        (M₀ ^ (1 - θ) * M₁ ^ θ) * eLpNorm f p (Measure.count : Measure ι)

Sources

• M. Riesz, Sur les maxima des formes bilinéaires et sur les fonctionnelles linéaires, Acta Math. 49 (1927), 465–497, DOI 10.1007/BF02564121; and G. O. Thorin, Convexity theorems generalizing those of M. Riesz and Hadamard with some applications, Comm. Sem. Math. Univ. Lund 9 (1948), 1–58, Riesz-Thorin interpolation theorem; Stein-Shakarchi Complex interpolation; Lean states finite counting-measure complex →ₗ[ℂ] form with explicit interpolation identities p⁻¹=(1-θ)p₀⁻¹+θp₁⁻¹ and bound M₀^(1-θ)M₁^θ.

Uses 1 · Used by 1

Proof usesRiesz–Thorin interpolation on finite sets, auxiliary form

Used byHausdorff–Young inequality on a finite abelian group

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.