Interpolated exponents in ℝ≥0∞

For exponents s₀, s₁ ∈ (0, ∞] and 0 ≤ θ ≤ 1, the interpolated exponent s is defined by 1 / s = (1 - θ) / s₀ + θ / s₁, written s⁻¹ = ofReal (1 - θ) * s₀⁻¹ + ofReal θ * s₁⁻¹. This is the exponent relation of complex and real interpolation of Lᵖ spaces (Riesz–Thorin, Marcinkiewicz). This file records its elementary arithmetic.

Main declarations

• TauCeti.inv_eq_ofReal_of_inv_eq: 1 / s is the real convex combination of 1 / s₀ and 1 / s₁.
• TauCeti.mem_uIcc_of_inv_eq: s lies between s₀ and s₁.
• TauCeti.exists_inv_eq_of_mem_Ioo: conversely, every s strictly between s₀ and s₁ is interpolated with some 0 < θ < 1.
• TauCeti.eq_top_iff_of_inv_eq: for 0 < θ < 1, s = ∞ exactly when s₀ = s₁ = ∞.
• TauCeti.one_le_of_inv_eq: interpolating exponents in [1, ∞] stays in [1, ∞].
• TauCeti.inv_conjExponent_eq_of_inv_eq: the conjugate exponents interpolate in the same way.
• TauCeti.exists_inv_eq_of_inv_lt_inv_add: an exponent q ≥ p with 1/p - 1/q < ν is interpolated, with θ < 1, between p and a finite s with 1/p - 1/s < ν.

theorem TauCeti.inv_eq_ofReal_of_inv_eq {s₀ s₁ s : ENNReal} {θ : ℝ} (hs₀ : s₀ ≠ 0) (hs₁ : s₁ ≠ 0) (hθ : θ ∈ Set.Icc 0 1) (hs : s⁻¹ = ENNReal.ofReal (1 - θ) * s₀⁻¹ + ENNReal.ofReal θ * s₁⁻¹) : s⁻¹ = ENNReal.ofReal ((1 - θ) * s₀⁻¹.toReal + θ * s₁⁻¹.toReal)

An interpolated exponent 1 / s = (1 - θ) / s₀ + θ / s₁ is the reciprocal of a real number in the closed interval between the reciprocals of the endpoints.

theorem TauCeti.mem_uIcc_of_inv_eq {s₀ s₁ s : ENNReal} {θ : ℝ} (hθ : θ ∈ Set.Icc 0 1) (hs : s⁻¹ = ENNReal.ofReal (1 - θ) * s₀⁻¹ + ENNReal.ofReal θ * s₁⁻¹) : s ∈ Set.uIcc s₀ s₁

An interpolated exponent lies between the two endpoint exponents.

theorem TauCeti.exists_inv_eq_of_mem_Ioo {s₀ s₁ s : ENNReal} (hs₀ : s₀ ≠ 0) (hs : s ∈ Set.Ioo s₀ s₁) : ∃ θ ∈ Set.Ioo 0 1, s⁻¹ = ENNReal.ofReal (1 - θ) * s₀⁻¹ + ENNReal.ofReal θ * s₁⁻¹

Every exponent strictly between s₀ ≠ 0 and s₁ is an interpolated exponent 1 / s = (1 - θ) / s₀ + θ / s₁ for some 0 < θ < 1.

theorem TauCeti.eq_top_iff_of_inv_eq {s₀ s₁ s : ENNReal} {θ : ℝ} (hθ : θ ∈ Set.Ioo 0 1) (hs : s⁻¹ = ENNReal.ofReal (1 - θ) * s₀⁻¹ + ENNReal.ofReal θ * s₁⁻¹) : s = ⊤ ↔ s₀ = ⊤ ∧ s₁ = ⊤

For 0 < θ < 1, an interpolated exponent is infinite exactly when both endpoint exponents are.

theorem TauCeti.one_le_of_inv_eq {s₀ s₁ s : ENNReal} {θ : ℝ} (hs₀ : 1 ≤ s₀) (hs₁ : 1 ≤ s₁) (hθ : θ ∈ Set.Icc 0 1) (hs : s⁻¹ = ENNReal.ofReal (1 - θ) * s₀⁻¹ + ENNReal.ofReal θ * s₁⁻¹) : 1 ≤ s

Interpolating between exponents in [1, ∞] gives an exponent in [1, ∞].

theorem TauCeti.inv_conjExponent_eq_of_inv_eq {s₀ s₁ s : ENNReal} {θ : ℝ} (hs₀ : 1 ≤ s₀) (hs₁ : 1 ≤ s₁) (hθ : θ ∈ Set.Icc 0 1) (hs : s⁻¹ = ENNReal.ofReal (1 - θ) * s₀⁻¹ + ENNReal.ofReal θ * s₁⁻¹) : s.conjExponent⁻¹ = ENNReal.ofReal (1 - θ) * s₀.conjExponent⁻¹ + ENNReal.ofReal θ * s₁.conjExponent⁻¹

Conjugate exponents interpolate in the same way as the exponents themselves.

theorem TauCeti.exists_inv_eq_of_inv_lt_inv_add {p q ν : ENNReal} (hq₁ : 1 ≤ q) (hq : q ≠ ⊤) (hν : ν ≠ ⊤) (hpq : p ≤ q) (h : p⁻¹ < q⁻¹ + ν) : ∃ (s : ENNReal) (θ : ℝ), 1 ≤ s ∧ s ≠ ⊤ ∧ p⁻¹ < s⁻¹ + ν ∧ 0 ≤ θ ∧ θ < 1 ∧ q⁻¹ = ENNReal.ofReal (1 - θ) * p⁻¹ + ENNReal.ofReal θ * s⁻¹

Let p ≤ q with 1 ≤ q < ∞, and let ν < ∞ with 1/p - 1/q < ν. Then q is interpolated between p and a larger finite exponent still in this range: there are a finite s ≥ 1 with 1/p - 1/s < ν and 0 ≤ θ < 1 with 1/q = (1 - θ)/p + θ/s. With ν = 1/n this chooses the auxiliary exponent for compactness of subcritical Sobolev embeddings by interpolation.