The function $1/t$ is locally integrable on $\mathbb C$

Proved

JHolomorphic.locallyIntegrable_inv_complex_volume

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

complex-analysismeasure-theory

The function $t\mapsto t^{-1}$ (with $0^{-1}=0$ ) is locally integrable on $\mathbb C$ with respect to two-dimensional Lebesgue measure.

Formalization Note LocallyIntegrable (fun t : ℂ => t⁻¹) volume; Lean's convention 0⁻¹ = 0 fixes the value at the origin, which is a null set.

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

/-- The function `t ↦ t⁻¹` on `ℂ` is locally integrable for Lebesgue measure. -/
theorem locallyIntegrable_inv_complex_volume :
    LocallyIntegrable (fun t : ℂ => t⁻¹) 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 function 1/t1/t1/t is locally integrable on C\mathbb CC

The function $1/t$ is locally integrable on $\mathbb C$