The Cauchy kernel $1/w$ on a disc lies in $L^q$ for $1\le q<2$

Proved

JHolomorphic.memLp_indicator_ball_inv_of_lt_two

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

complex-analysislp-spacesmeasure-theory

Let $1\le q<2$ and $r\in\mathbb R$ . The function $w\mapsto \mathbf 1_{B_r(0)}(w)\,w^{-1}$ on $\mathbb C$ belongs to $L^q(\mathbb C)$ with respect to Lebesgue measure. This is the integrability of the Cauchy kernel needed to define the Cauchy transform on $L^p$ data with $p>2$ .

Formalization Note Stated as MemLp ((ball (0 : ℂ) r).indicator fun w => w⁻¹) (ENNReal.ofReal q) volume. For $r\le0$ the ball is empty and the function is $0$ .

Preamble

import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
import Mathlib.MeasureTheory.Measure.Lebesgue.Complex
import Mathlib.Analysis.SpecialFunctions.Integrability.Basic
import Mathlib.Analysis.Complex.Basic

Formal statement

namespace JHolomorphic

open MeasureTheory Metric Filter Topology Set
open scoped ENNReal

/-- For `1 ≤ q < 2` and any radius `r`, the kernel `w ↦ w⁻¹` restricted to the disc `B_r(0) ⊆ ℂ` lies in `L^q(ℂ)`. -/
theorem memLp_indicator_ball_inv_of_lt_two {q : ℝ} (hq1 : 1 ≤ q) (hq2 : q < 2) (r : ℝ) :
    MemLp ((ball (0 : ℂ) r).indicator fun w : ℂ => w⁻¹) (ENNReal.ofReal q) volume := by
  sorry

end JHolomorphic

Source

Used for C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2, Lemma 2.24

View graph

The Cauchy kernel 1/w1/w1/w on a disc lies in LqL^qLq for 1≤q<21\le q<21≤q<2

The Cauchy kernel $1/w$ on a disc lies in $L^q$ for $1\le q<2$