Documentation

Mathlib.Analysis.SpecialFunctions.Integrability.PosLog

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 #

source
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.

source
@[deprecated MeromorphicOn.intervalIntegrable_posLog_norm (since := "2026-03-28")]
theorem MeromorphicOn.intervalIntegrable_posLog_norm_meromorphicOn {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

Alias of MeromorphicOn.intervalIntegrable_posLog_norm.

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 #

source
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.

source
@[deprecated MeromorphicOn.circleIntegrable_posLog_norm (since := "2026-03-28")]
theorem circleIntegrable_posLog_norm_meromorphicOn {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

Alias of MeromorphicOn.circleIntegrable_posLog_norm.

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

source
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.

source
@[deprecated MeromorphicOn.circleIntegrable_posLog_norm_of_nonneg (since := "2026-03-28")]
theorem circleIntegrable_posLog_norm_meromorphicOn_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

Alias of MeromorphicOn.circleIntegrable_posLog_norm_of_nonneg.

Variant of MeromorphicOn.circleIntegrable_posLog_norm for non-negative radii.