Higher integrability from a 1/|z| bound and power decay of the L² mass

Proved

FiniteEnergyPlane.lintegral_rpow_lt_top_of_norm_mul_le

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

elliptic-regularityreal-analysissobolev-spaces

Let $r>0$ , $\mu>0$ , and let $g\ge 0$ be a measurable function on the disc $B_r=\{|z|<r\}\subset\mathbb{C}$ such that

|z|\,g(z)\le C\quad(0<|z|<r),\qquad \int_{|z|<s}g^2\,dz\le K\,s^{2\mu}\quad(0<s\le r).

Then

\int_{B_r}g^p\,dz<\infty\qquad\text{for every }2\le p<2+2\mu .

A function with a $1/|z|$ bound whose $L^2$ mass on small discs decays like a power of the radius has strictly better than square integrability. This is used for derivatives of maps near a puncture.

Formalization Note The integrals are lower integrals in ℝ≥0∞ of ENNReal.ofReal (g z ^ 2) and ENNReal.ofReal (g z ^ p) with real powers; g is AEMeasurable for the restriction of Lebesgue measure to ball 0 r.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Higher integrability from a `1/|z|` bound and power decay of the `L²` mass. Let `g ≥ 0` be
measurable on the disc of radius `r > 0` about `0`, with `|z| g(z) ≤ C` for `0 < |z| < r` and
`∫_{|z| < s} g² ≤ K s^{2μ}` for `0 < s ≤ r`, where `μ > 0`. Then `∫_{|z| < r} g^p < ∞` for every
`2 ≤ p < 2 + 2μ`. -/
theorem lintegral_rpow_lt_top_of_norm_mul_le (g : ℂ → ℝ) {r C K μ : ℝ} (hr : 0 < r)
    (hμ : 0 < μ) (hg0 : ∀ z, 0 ≤ g z) (hg : AEMeasurable g (volume.restrict (ball 0 r)))
    (hbd : ∀ z : ℂ, z ≠ 0 → ‖z‖ < r → ‖z‖ * g z ≤ C)
    (hdec : ∀ s : ℝ, 0 < s → s ≤ r →
      ∫⁻ z in ball 0 s, ENNReal.ofReal (g z ^ 2) ≤ ENNReal.ofReal (K * s ^ (2 * μ)))
    (p : ℝ) (hp2 : 2 ≤ p) (hp : p < 2 + 2 * μ) :
    ∫⁻ z in ball 0 r, ENNReal.ofReal (g z ^ p) < ⊤ := by
  sorry

end FiniteEnergyPlane

Source

A. Zinger, Notes on J-holomorphic maps, arXiv:1706.00331, proof of Proposition 4.8

View graph