Integrability of Functions Prominently Involving log⁺

Integrability for log⁺ of Meromorphic Functions

We establish integrability for functions of the form log⁺ ‖meromorphic‖. In the real setting, these functions are interval integrable over every interval of the real line. In the complex setting, the functions are circle integrable over every circle in the complex plane.

Interval Integrability for log⁺ of Real Meromorphic Functions

theorem MeromorphicOn.intervalIntegrable_posLog_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hf : MeromorphicOn f (Set.uIcc a b)) : IntervalIntegrable (fun (x : ℝ) => ‖f x‖.posLog) MeasureTheory.volume a b

If f is real-meromorphic on a compact interval, then log⁺ ‖f ·‖ is interval integrable on this interval.

Circle Integrability for log⁺ of Complex Meromorphic Functions

theorem MeromorphicOn.circleIntegrable_posLog_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E} (hf : MeromorphicOn f (Metric.sphere c |R|)) : CircleIntegrable (fun (x : ℂ) => ‖f x‖.posLog) c R

If f is complex meromorphic on a circle in the complex plane, then log⁺ ‖f ·‖ is circle integrable over that circle.

theorem MeromorphicOn.circleIntegrable_posLog_norm_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E} (hf : MeromorphicOn f (Metric.sphere c R)) (hR : 0 ≤ R) : CircleIntegrable (fun (x : ℂ) => ‖f x‖.posLog) c R

Variant of MeromorphicOn.circleIntegrable_posLog_norm for non-negative radii.