Circle averages of log⁺ ‖f‖⁻¹ and a Fatou bound

For f meromorphic on a circle, log⁺ ‖f‖⁻¹ = log⁺ ‖f‖ - log ‖f‖ is circle integrable, and its circle average is the difference of the circle averages of log⁺ ‖f‖ and of log ‖f‖. This is the identity ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage of Nevanlinna theory, for a function meromorphic only on the circle and a circle with arbitrary centre. Since the integrand is nonnegative, the same identity also computes the lower Lebesgue integral of log⁺ ‖f‖⁻¹ over one period. Fatou's lemma then bounds the measure of angles where values on a sequence of circles approach zero through nonzero values; this last result only needs circle integrability.

Main results

• MeromorphicOn.circleIntegrable_posLog_inv_norm — log⁺ ‖f‖⁻¹ is circle integrable.
• ContinuousOn.circleIntegrable_posLog_norm — log⁺ ‖f‖ is circle integrable when f is continuous on the circle.
• DifferentiableOn.circleIntegrable_posLog_norm — log⁺ ‖f‖ is circle integrable on every circle inside a disc on which f is holomorphic.
• CircleIntegrable.circleAverage_posLog_norm_sub_const_le — circle averages of log⁺ ‖f - a‖ are at most those of log⁺ ‖f‖ plus log⁺ ‖a‖ + log 2.
• MeromorphicOn.circleAverage_posLog_inv_norm — the circle average of log⁺ ‖f‖⁻¹ is the difference of the circle averages of log⁺ ‖f‖ and of log ‖f‖.
• MeromorphicOn.lintegral_ofReal_posLog_inv_norm_circleMap — the lower Lebesgue integral of log⁺ ‖f‖⁻¹ over one period of the circle is 2π times that difference.
• TauCeti.volume_setOf_tendsto_circleMap_nhdsNE_zero — bounded circle averages of log⁺ ‖f‖⁻¹ force the angles with nonzero radial values tending to zero to be null.

theorem ContinuousOn.circleIntegrable_posLog_norm {c : ℂ} {r : ℝ} {E : Type u_1} [SeminormedAddCommGroup E] {f : ℂ → E} (hf : ContinuousOn f (Metric.sphere c |r|)) : CircleIntegrable (fun (z : ℂ) => ‖f z‖.posLog) c r

log⁺ ‖f‖ is circle integrable if f is continuous on the circle.

theorem DifferentiableOn.circleIntegrable_posLog_norm {f : ℂ → ℂ} {c : ℂ} {r R : ℝ} (hf : DifferentiableOn ℂ f (Metric.ball c R)) (hr : r ∈ Set.Ioo 0 R) : CircleIntegrable (fun (z : ℂ) => ‖f z‖.posLog) c r

log⁺ ‖f‖ is circle integrable over every circle inside a disc on which f is holomorphic.

theorem CircleIntegrable.circleAverage_posLog_norm_sub_const_le {c : ℂ} {r : ℝ} {E : Type u_1} [SeminormedAddCommGroup E] {f : ℂ → E} (hf : CircleIntegrable (fun (z : ℂ) => ‖f z‖.posLog) c r) (a : E) (hfa : CircleIntegrable (fun (z : ℂ) => ‖f z - a‖.posLog) c r) : Real.circleAverage (fun (z : ℂ) => ‖f z - a‖.posLog) c r ≤ Real.circleAverage (fun (z : ℂ) => ‖f z‖.posLog) c r + (‖a‖.posLog + Real.log 2)

Circle averages of log⁺ ‖f - a‖ are at most those of log⁺ ‖f‖ plus log⁺ ‖a‖ + log 2, whenever both integrands are circle integrable.

theorem MeromorphicOn.circleIntegrable_posLog_inv_norm {f : ℂ → ℂ} {c : ℂ} {r : ℝ} (hf : MeromorphicOn f (Metric.sphere c |r|)) : CircleIntegrable (fun (z : ℂ) => ‖f z‖⁻¹.posLog) c r

If f is meromorphic on a circle, then log⁺ ‖f‖⁻¹ is circle integrable there.

theorem MeromorphicOn.circleAverage_posLog_inv_norm {f : ℂ → ℂ} {c : ℂ} {r : ℝ} (hf : MeromorphicOn f (Metric.sphere c |r|)) : Real.circleAverage (fun (z : ℂ) => ‖f z‖⁻¹.posLog) c r = Real.circleAverage (fun (z : ℂ) => ‖f z‖.posLog) c r - Real.circleAverage (fun (z : ℂ) => Real.log ‖f z‖) c r

If f is meromorphic on a circle, then the circle average of log⁺ ‖f‖⁻¹ is the difference of the circle averages of log⁺ ‖f‖ and of log ‖f‖.

theorem MeromorphicOn.lintegral_ofReal_posLog_inv_norm_circleMap {f : ℂ → ℂ} {c : ℂ} {r : ℝ} (hf : MeromorphicOn f (Metric.sphere c |r|)) : ∫⁻ (θ : ℝ) in Set.Ioc 0 (2 * Real.pi), ENNReal.ofReal ‖f (circleMap c r θ)‖⁻¹.posLog = ENNReal.ofReal (2 * Real.pi * (Real.circleAverage (fun (z : ℂ) => ‖f z‖.posLog) c r - Real.circleAverage (fun (z : ℂ) => Real.log ‖f z‖) c r))

If f is meromorphic on a circle, then the lower Lebesgue integral of log⁺ ‖f‖⁻¹ over one period (0, 2π] of the circle is 2π times the difference of the circle averages of log⁺ ‖f‖ and of log ‖f‖.

theorem TauCeti.volume_setOf_tendsto_circleMap_nhdsNE_zero {f : ℂ → ℂ} {c : ℂ} {ρ : ℕ → ℝ} {B : ℝ} (hf : ∀ (n : ℕ), CircleIntegrable (fun (z : ℂ) => ‖f z‖⁻¹.posLog) c (ρ n)) (hB : ∀ (n : ℕ), Real.circleAverage (fun (z : ℂ) => ‖f z‖⁻¹.posLog) c (ρ n) ≤ B) : MeasureTheory.volume {θ : ℝ | θ ∈ Set.Ioc 0 (2 * Real.pi) ∧ Filter.Tendsto (fun (n : ℕ) => f (circleMap c (ρ n) θ)) Filter.atTop (nhdsWithin 0 {0}ᶜ)} = 0

Fatou's lemma on circles. If log⁺ ‖f‖⁻¹ is integrable on the circles about c of radii ρ n, and its circle averages there are at most B, then the angles in one period along which f (circleMap c (ρ n) θ) tends to 0 through nonzero values form a null set.