Integrals of translates along a segment over a disc are bounded by the integral over the enlarged disc

Proved

JHolomorphic.lintegral_ball_segment_le

by Mazecto · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

lebesgue-integrationmeasure-theory

Let $H:\mathbb{C}\to[0,\infty]$ be measurable, let $a,c\in\mathbb{C}$ and $r\in\mathbb{R}$ . Then

\int_{B(c,r)}\int_{(0,1]} H(z+ta)\,dt\,dz\;\le\;\int_{B(c,r+|a|)} H(w)\,dw.

This is the integrated form of the statement that averaging over the segments $z+[0,1]a$ moves mass from the disc $B(c,r)$ only into the larger disc $B(c,r+|a|)$ ; it is used for $L^q$ bounds of such averages.

Formalization Note The integrals are lower Lebesgue integrals (∫⁻) for Lebesgue measure on $\mathbb{C}$ restricted to the open disc ball c r, Lebesgue measure on $\mathbb{R}$ restricted to Set.Ioc 0 1, and Lebesgue measure on $\mathbb{C}$ restricted to ball c (r + ‖a‖). If $r\le 0$ the left side is $0$ .

Preamble

import Mathlib.MeasureTheory.Measure.Lebesgue.Complex
import Mathlib.MeasureTheory.Group.LIntegral
import Mathlib.MeasureTheory.Measure.Prod

Formal statement

namespace JHolomorphic

open MeasureTheory Metric
open scoped ENNReal

/-- For a measurable `H : ℂ → [0, ∞]`, `a, c ∈ ℂ` and `r ∈ ℝ`, the integral over `z ∈ B(c, r)` of the
integral over `t ∈ (0, 1]` of `H (z + t a)` is at most the integral of `H` over `B(c, r + ‖a‖)`. -/
theorem lintegral_ball_segment_le (H : ℂ → ℝ≥0∞) (hH : Measurable H) (a c : ℂ) (r : ℝ) :
    ∫⁻ z in ball c r, ∫⁻ t in Set.Ioc (0:ℝ) 1, H (z + (t:ℂ) * a) ≤
      ∫⁻ w in ball c (r + ‖a‖), H w := by
  sorry

end JHolomorphic

Source

Standard (Lebesgue integration, translation invariance).

View graph