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

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

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

theorem 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

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

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.

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.

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

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

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

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

Variant of circleIntegrable_log_norm_meromorphicOn for non-negative radii.

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

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

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

Variant of circleIntegrable_posLog_norm_meromorphicOn for non-negative radii.