Documentation

Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Integrability for Logarithms 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. This implies in particular that logarithms of trigonometric functions are interval integrable. In the complex setting, the functions are circle integrable over every circle in the complex plane.

Interval Integrability for Logarithms of Real Meromorphic Functions #

source
theorem MeromorphicOn.intervalIntegrable_log_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hf : MeromorphicOn f (Set.uIcc a b)) :
IntervalIntegrable (fun (x : ℝ) => Real.log ‖f x‖) 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_log_norm (since := "2026-03-28")]
theorem intervalIntegrable_log_norm_meromorphicOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hf : MeromorphicOn f (Set.uIcc a b)) :
IntervalIntegrable (fun (x : ℝ) => Real.log ‖f x‖) MeasureTheory.volume a b

Alias of MeromorphicOn.intervalIntegrable_log_norm.

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

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.

source
theorem MeromorphicOn.intervalIntegrable_log {a b : ℝ} {f : ℝ → ℝ} (hf : MeromorphicOn f (Set.uIcc a b)) :
IntervalIntegrable (Real.log ∘ f) MeasureTheory.volume a b

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

source
theorem intervalIntegrable_log_sin {a b : ℝ} :
IntervalIntegrable (Real.log ∘ Real.sin) MeasureTheory.volume a b

Special case of MeromorphicOn.intervalIntegrable_log: The function log ∘ sin is interval integrable over every interval.

source
theorem intervalIntegrable_log_cos {a b : ℝ} :
IntervalIntegrable (Real.log ∘ Real.cos) MeasureTheory.volume a b

Special case of MeromorphicOn.intervalIntegrable_log: The function log ∘ cos is interval integrable over every interval.

Circle Integrability for Logarithms of Complex Meromorphic Functions #

source
theorem MeromorphicOn.circleIntegrable_log_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E} (hf : MeromorphicOn f (Metric.sphere c |R|)) :
CircleIntegrable (fun (x : ℂ) => Real.log ‖f x‖) 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_log_norm (since := "2026-03-28")]
theorem circleIntegrable_log_norm_meromorphicOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E} (hf : MeromorphicOn f (Metric.sphere c |R|)) :
CircleIntegrable (fun (x : ℂ) => Real.log ‖f x‖) c R

Alias of MeromorphicOn.circleIntegrable_log_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_log_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 : ℂ) => Real.log ‖f x‖) c R

Variant of MeromorphicOn.circleIntegrable_log_norm for non-negative radii.

source
@[deprecated MeromorphicOn.circleIntegrable_log_norm_of_nonneg (since := "2026-03-28")]
theorem circleIntegrable_log_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 : ℂ) => Real.log ‖f x‖) c R

Alias of MeromorphicOn.circleIntegrable_log_norm_of_nonneg.

Variant of MeromorphicOn.circleIntegrable_log_norm for non-negative radii.

source
theorem circleIntegrable_log_norm_factorizedRational {R : ℝ} {c : ℂ} (D : ℂ → ℤ) :
CircleIntegrable (∑ᶠ (u : ℂ), fun (x : ℂ) => ↑(D u) * Real.log ‖x - u‖) c R

Variant of MeromorphicOn.circleIntegrable_log_norm for factorized rational 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.