Already formalized in Mathlib, along with several variants.

 
If \(|\phi |\) is constant, everything holds trivially by setting \(M_0\) and \(M_1\) to be the value of \(|\phi |\) at a point. Assume \(|\phi |\) non-constant.

• Case 1: assume \(M_0=M_1=1\), and \(\sup _{0 \leq x \leq 1} | \phi (x+iy) | \to 0\) when \(|y| \to \infty \).
  Let \(M\) be the supremum of \(|\phi (z)|\) on \(\bar{S}\). Since the function is non-constant, we have \(M{\gt}0\).
  Let \(\{ z_n\} \) be a sequence of points in \(S\) such that \(|\phi (z_n)|\) converges to \(M\).
  Since we assumed the absolute value of \(\phi \) goes to zero as \(|y|\) goes to infinity, all points where \(|\phi (z)|{\gt}M-\epsilon \) must be in some rectangle around zero, i.e. the sequence \({z_n}\) must be bounded.
  Hence, there must be a converging subsequence of \({z_n}\) to a point \(z^* \in \bar{S}\).
  By maximum modulus principle, \(z^*\) must be on the boundary \(\delta S\), so it must have real part \(0\) or \(1\). Hence, by assumption, \(|\phi (z^*)|\leq 1\), and by construction \(|\phi (z)|\leq 1\) for all \(z \in \bar{S}\), which is what we wanted to show.

• Case 2: only assume \(M_0 = M_1 = 1\).
  For \(\epsilon {\gt}0\), define

  \[ \phi _{\epsilon } (z) = \phi (z) e^{\epsilon (z^2 - 1)} \]
  If the real part of \(z\) is \(0\), then \(z=iy\) and
  \[ | \phi _{\epsilon } (z) | = |\phi (z) e^{\epsilon (-y^2-1)}| \leq |\phi (z)| \cdot 1 \leq 1 \]
  If the real part of \(z\) is \(1\), then \(z=1+iy\) and
  \[ | \phi _{\epsilon } (z) | = |\phi (z) e^{\epsilon (1 -y^2 + 2iy -1)}| = |\phi (z) e^{\epsilon (-y^2 + 2iy)}| = |\phi (z) e^{\epsilon (-y^2)}| \leq |\phi (z)| \cdot 1 \leq 1 \]
  Moreover,
  \[ | \phi _{\epsilon } (x+iy)| \leq |\phi (x+iy)| \cdot |e^{\epsilon (z^2-1)}| = |\phi (x+iy)| \cdot |e^{\epsilon (x^2-1-y^2+2ixy)}| = |\phi (x+iy)| \cdot |e^{\epsilon (x^2-1-y^2)}| \]
  Hence, for \(0\leq x \leq 1\) and \(|y| \to \infty \), we have that both factors go to zero.
  Thus \(\phi _{\epsilon }\) satisfies the hypotheses of case 1, so \(|\phi _{\epsilon }| \leq 1\) on the whole strip.
  Now, we have pointwise that
  \[ \lim _{\epsilon \to 0} \phi _{\epsilon }(z) = \lim _{\epsilon \to 0} \phi (z) e^{\epsilon (z^2-1)} = \phi (z) \]
  Hence, for \(\epsilon \to 0\), we have \(|\phi _{\epsilon }(z)| \to |\phi (z)|\). Thus,
  \[ |\phi (z)| = \lim _{\epsilon \to 0} |\phi _{\epsilon }(z)| \leq 1 \]
  which is what we wanted to show.

• General case
  If \(M_0\) and \(M_1\) are any two positive real numbers, define

  \[ \tilde{\phi } (z) = M_0 ^{z-1} M_1^{-z} \phi (z) \]
  Recall that, for \(a\in \mathbb {R}\setminus \{ 0\} \), we have
  \[ |a^{b+ic}| = |a^b| \]
  Hence, if the real part of \(z\) is \(0\), we have
  \[ |\tilde{\phi } (z)| \leq |M_0^{-1}| \cdot |M_1^0| \cdot |\phi (z)| \leq \frac{1}{M_0} \cdot M_0 = 1 \]
  And if the real part of \(z\) is \(1\), we have
  \[ |\tilde{\phi } (z)| \leq |M_0^0| \cdot |M_1^{-1}| \cdot |\phi (z)| \leq \frac{1}{M_1} \cdot M_1 = 1 \]
  From the previous case, we obtain that for arbitrary \(z\) in the strip
  \[ |\tilde{\phi } (z)| \leq 1 \]
  Now, write \(z= t + iy\) and unroll the definition of \(\tilde{\phi }\) to obtain
  \[ |M_0^{t-1+y} M_1^{-t-iy} \phi (z)| \leq 1 \]
  The left-hand side is equal to
  \[ M_0^{t-1} M_1^{-t} |\phi (z)| \]
  So we obtain
  \[ |\phi (z)| \leq M_0^{1-t} M_1^t \]
  which is exactly what we wanted.

That

follows from Hölder’s inequality.

The other direction is trivial when \(\| f\| _{L^q}=0\). Suppose \(\| f\| _{L^q}\ne 0\). Set

Then \(\| g\| _{L^p} = 1\).

In (1) and (2), \(g_n\) is a monotone sequence of simple function approximating \(g\) from below, whose existence is basic real analysis.

That

follows from Hölder’s inequality.

Suppose \(M:= \sup _{\| g\| _{L^1} \leq 1, \ g \text{ simple}} \| fg \| _{L^1} {\lt} \| f\| _{L^\infty }\). Then \(\{ x | |f(x)| \ge M \} \) has positive measure. Since \(\mu \) is \(\sigma \)-finite, we have a subset \(B \subset \{ x | |f(x)| \ge M \} \) with finite positive measure by a classical lemma. Now set

Then we have

But \(\| h\| =1\) and \(h\) is simple, so \(\| fh\| _{L^1} \le M\), contradiction.

This is just a version of Hölder’s inequality, but in order to apply it, we should rule out some trivial cases.

First note that the assumption guarantees that \(0 {\lt} p_0 \le p \le p_1 \le \infty \) and \(0\le t \le 1\).

When \(t=0\) or \(t=1\), the inequality holds trivially. Hence we may assume \(t \ne 0\) and \(t \ne 1\). In this case \(p {\lt} p_1 \le \infty \).

Now we can rearrange the equality into

Using Hölder’s inequality, we have

For a valid choice of \(p,q\), note that we both need to show \(Tf\) is in \(L^q\) and a bound on the \(L^q\) norm of \(Tf\). Let \(q'\) be the conjugate exponent of \(q\). By Lemma ?? for \(Tf\), we need a bound of the form

• Case 1: assume \(p{\lt}\infty \) and \(q{\gt}1\), and let \(q', q_0^1, q_1'\) be the conjugate exponents of \(q, q_0, q_1\) respectively.

  • Subcase a: assume \(f=\sum _i a_i \chi _{E_i}\) is a simple function (finite sum with \(E_i\) disjoint of finite measure).
    Let \(g=\sum _j b_j \chi _{F_j}\) be a simple function. By writing \(f\) as \(||f||_{L^p} \cdot \frac{f}{||f||_{L^p}}\) and using linearity of \(T\) and integrals, it suffices to prove the above inequality when \(||f||_{L^p}=1\).
    We want to apply the three lines lemma to an appropriate function. Define

    \[ \gamma (z) = p \left(\frac{1-z}{p_0} + \frac{z}{p_1} \right) \qquad f_z = |f|^{\gamma (z)} \cdot \frac{f}{|f|} \]
    \[ \delta (z) = q' \left(\frac{1-z}{q'_0} + \frac{z}{q'_1} \right) \qquad g_z = |g|^{\delta (z)} \cdot \frac{g}{|g|} \]
    Observe that for \(t\) as in the statement of the theorem, we have by definition that \(\gamma (t)=1\), hence \(f_t=f\).
    Moreover, if \(\mathrm{Re}(z)=0\), we have that \(\mathrm{Re} (\gamma (z)) = \frac{p}{p_0}\), and hence
    \[ ||f_z||_{L^{p_0}} = \left(\int |f_z|^{p_0}\right)^{\frac{1}{p_0}} = \left(\int | |f|^{\gamma (z)} |^{p_0}\right)^{\frac{1}{p_0}} = \left(\int |f| ^{\frac{p}{p_0} \cdot p_0}\right)^{\frac{1}{p_0}} = \left(||f||_{L^p}^p\right)^{\frac{1}{p_0}} = 1^{\frac{1}{p_0}} = 1 \]
    If \(\mathrm{Re}(z)=1\), we have \(\mathrm{Re} (\gamma (z)) = \frac{p}{p_1}\), and the exact same computation replacing \(p_0\) with \(p_1\) now shows that \(||f_z||_{L^{p_1}}=1\).
    Similarly, one shows that
    \[ g_t=g \qquad ||g_z||_{L^{q'_0}} = 1 \text{ if } \mathrm{Re}(z)=0 \qquad ||g_z||_{L^{q'_1}} = 1 \text{ if } \mathrm{Re}(z)=1 \]
    Now, we want to apply the three lines lemma to the function
    \[ \phi (z) := \int (Tf_z) g_z \]
    Since \(f\) and \(g\) are simple and given by the expressions above, we can explicitly write \(f_z\) and \(g_z\) as
    \[ f_z=\sum _i |a_i|^{\gamma (z)} \frac{a_i}{|a_i|} \chi _{E_i} \qquad g_z=\sum _j |b_j|^{\delta (z)} \frac{b_j}{|b_j|} \chi _{F_j} \]
    (here, we use that the \(E_i\) (respectively \(F_j\)) are disjoint, so for every point in the domain there is at most one of the \(E_i\) covering it).
    So, expanding everything by linearity of \(T\) and integrals, we obtain
    \[ \phi (z) = \sum _{i,j} |a_i|^{\gamma (z)} \frac{a_i}{|a_i|} |b_j|^{\delta (z)} \frac{b_j}{|b_j|} \int T(\chi _{E_i}) \chi _{F_j} \]
    This only depends on \(z\) holomorphically in terms of the exponents of the \(|a_i|\) and \(|b_j|\), so it is a holomorphic function on the strip \(S\) in the three lines lemma and it is continuous on \(S\).
    It it also bounded on \(\bar{S}\). In fact, we wrote \(\phi \) as a finite sum, so we only need to show each summand is bounded. Since the real part of \(z\) is between \(0\) and \(1\), the terms \(|a_i|^{\gamma (z)}\) and \(|b_j|^{\delta (z)}\) have bounded norms. Finally, recall that Hölder’s inequality states that \(||fg||_1 \leq ||f||_p ||g||_1\) for conjugate exponents \(p,q\). Hence,
    \[ \left| \int T(\chi _{E_i}) \chi _{F_j} \right| \leq ||T(\chi _{E_i}) \chi _{F_j}||_{L^1} \leq ||T(\chi _{E_i})||_{L^{p_0}} \cdot ||\chi _{F_j}||_{p'_0} \leq M_0 \mu (E_i) \mu (F_j) \]
    which is bounded. Moreover, if \(\mathrm{Re}(z)=0\), since \(||f_z||_{L^{p_0}}=||g_z||_{L^{q'_0}}=1\), we have
    \[ | \phi (z) | \leq \int |(Tf_z) g_z| \leq ||Tf_z||_{L^{q_0}} \cdot ||g_z||_{L^{q'_0}} \leq M_0 \cdot ||g_z||_{L^{q'_0}} \leq M_0 \]
    Similarly, if \(\mathrm{Re}(z)=1\), we obtain
    \[ | \phi (z) | \leq \int |(Tf_z) g_z| \leq ||Tf_z||_{L^{q_1}} \cdot ||g_z||_{L^{q'_1}} \leq M_1 \cdot ||g_z||_{L^{q'_1}} \leq M_1 \]
    Thus, applying the three lines lemma to \(\phi (z)\) yields that
    \[ |\phi (t+yi)| \leq M_0^{1-t} M_1^t \]
    In particular, this holds for \(y=0\), but now
    \[ \phi (t) = \int (Tf_t) g_t = \int (Tf) g \]
    So we have
    \[ \left| \int (Tf) g \right| \leq M_0^{1-t} M_1^t \]
    which is exactly what we wanted to show.

  • Subcase b: Now, let \(f\) be any function in \(L^p\). By density of simple functions, approximate \(f\) by a sequence \({f_n}\) of simple functions with \(||f_n - f||_{L^p} \to 0\).
    By the previous case, we have \(||Tf_n||_{L^q} \leq M ||f_n||_{L^p}\). In particular, the sequence \(\{ Tf_n\} \) is Cauchy in \(L^q\), since

    \[ ||Tf_m - Tf_n||_{L^q} = ||T(f_m-f_n)||_{L^q} \leq M ||f_m - f_n||_{L^p} \]
    and the original sequence is Cauchy. By completeness, the \(\{ Tf_n\} \) converge in \(L^q\), in particular the \(L^q\) norm of the limit is the limit of the \(L^q\) norms, which is less than \(M ||f||_{L^p}\). Hence, it suffices to show that the sequence \(\{ Tf_n\} \) converges almost everywhere to \(Tf\).
    Write \(f= f^U + f^L\) with
    \[ f^U := \begin{cases} f(x) & \text{if } |f(x)|\geq 1 \\ 0 & \text{otherwise} \end{cases} \qquad f^L := \begin{cases} f(x) & \text{if } |f(x)|{\lt} 1 \\ 0 & \text{otherwise} \end{cases} \]
    and similarly \(f_n = f_n^U + f_n^L\).
    Modulo reordering them, assume \(p_0 \leq p_1\), so we have \(p_0 \leq p \leq p_1\). Since \(f\in L^p\), \(f^U\) must be in \(L^{p_0}\) and \(f^L\) in \(L^{p_1}\). Similarly, since \(f_n \to f\) in \(L^p\), we have \(f_n^U \to f^U\) in \(L^{p_0}\) and \(f_n^L \to f^L\) in \(L^{p_1}\).
    By the assumptions of boundedness of \(L\)
    \[ Tf_n^U \to Tf^U \ \text{ in } L^{q_0} \qquad Tf_n^L \to Tf^L \ \text{ in } L^{q_1} \]
    Modulo extracting subsequences, we can assume that the convergence is almost everywhere, so that almost everywhere
    \[ Tf_n (x) = Tf_n^U (x) + Tf_n^L(x) \to Tf^U (x) + Tf(x) = Tf (x) \]
    which is what we wanted to show.

• Case 2: \(p=\infty \) or \(q=1\).
  If \(p=\infty \), we must also have \(p_0=p_1=\infty \), thus we have

  \[ ||Tf||_{L^{q_0}} \leq M_0 ||f||_{L^{\infty }} \qquad ||Tf||_{L^{q_1}} \leq M_1 ||f||_{L^{\infty }} \]
  Applying Lemma 3.5 with \(Tf, q, q_0, q_1\), we obtain
  \[ ||Tf||_{L^q} \leq ||Tf||_{L^{q_0}}^{1-t} ||Tf||_{L^{q_1}}^{t} \leq M_0^{1-t} M_1^t ||f||_{L^{\infty }} \]
  which is what we wanted.
  
  If \(p{\lt}\infty \) and \(q=1\), then (since they must be at least \(1\) by definition of \(L^p\) spaces) we have that \(q_0\) and \(q_1\) must also both be \(1\) (for example, since \(\frac{1}{q}\) is a convex combination of the other two reciprocals, the largest one must be \(1\), and from that rearranging terms shows the other one is \(1\)). In this case, take \(g_z=g\) for all \(z\) and repeat the proof above (note:isn’t this what already happens if we do not consider this case separately?).

Observe that we may simply regard \(T\) as an operator \(L^1([0, 2\pi ]) \to L^{\infty }(\mathbb {Z})\) since \(L^2([0, 2\pi ]) \subseteq L^1([0, 2\pi ])\) (compact domain, bound with maximum), and \(L^2(\mathbb {Z}) \subseteq L^{\infty }(\mathbb {Z})\).
Note that the claim corresponds (unless \(q\) is infinity) to the inequality

For \(p_0=2\) (thus \(q_0=2\)), this is Parseval’s identity (see tsum_sq_fourierCoeff).
For \(p_1=1\) (thus \(q_1=\infty \)), we can check it directly. Since

we have

So

Applying Rietz-Thorin’s theorem, we obtain that the claim holds whenever we can find a \(t\in [0,1]\) such that

Substituting \(p_0=2\), \(p_1=1\), \(q_0=2\), \(q_1=\infty \),

Now

which for \(t\in [0,1]\) ranges from \(1\) to \(2\).
Moreover, we have

i.e., \(p\) and \(q\) are conjugate exponents.
This completes the proof.

This is similar to the previous corollary. Parseval’s identity gives the case \(p_0=q_0=2\).
For the case \(p_1=1\), \(q_1=\infty \), again

i.e.

As before, applying Rietz-Thorin’s interpolation theorem concludes the proof.