Interpolating a high moment between a sup bound and a low moment

Proved

CircleMethod.holder_pow_interpolation

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorycircle-methodnumber-theorywaring-problem

The interpolation step of the circle method. If $\|f\|\le M$ pointwise on a measurable set $A$ and $m\le s$ , then

\int_A\|f\|^{s}\;\le\;M^{\,s-m}\int_A\|f\|^{m}.

Elementary, but it is the exact shape the minor-arc argument needs. Neither of the two available estimates suffices alone: the pointwise Weyl bound controls $\sup_A\|f\|$ but says nothing about the measure of the set where $f$ is large, while a mean value estimate such as Hua's inequality controls $\int\|f\|^{m}$ but not the maximum. Splitting $\|f\|^{s}=\|f\|^{s-m}\|f\|^{m}$ and applying the sup bound to the first factor combines them, and it is that combination which makes the minor arcs negligible.

Formalization Note. Stated for an arbitrary measure space and an arbitrary normed target, since nothing in the argument is specific to the circle; only measurability of $A$ and integrability of $\|f\|^{m}$ on $A$ are required.

Preamble

import Definitions.Def_CircleMethod_char
import Mathlib.MeasureTheory.Integral.Bochner.Set
open MeasureTheory

Formal statement

namespace CircleMethod

theorem holder_pow_interpolation {X E : Type*} [MeasurableSpace X] [NormedAddCommGroup E]
    {μ : Measure X} {A : Set X} (hA : MeasurableSet A) {f : X → E}
    {M : ℝ} (hM : ∀ x ∈ A, ‖f x‖ ≤ M) {m s : ℕ} (hms : m ≤ s)
    (hint : IntegrableOn (fun x => ‖f x‖ ^ m) A μ) :
    ∫ x in A, ‖f x‖ ^ s ∂μ ≤ M ^ (s - m) * ∫ x in A, ‖f x‖ ^ m ∂μ := by sorry

end CircleMethod

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 2 and Chapter 4 (the minor-arc treatment, where the pointwise Weyl bound and Hua's mean value estimate are interpolated).

View graph