Theorems · Theorem · complex analysis

ValueDistribution.Cartan.integrableOn_intervalIntegral_cartanKernel_right

∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    MeasureTheory.IntegrableOn (fun x => ∫ (β : ℝ) in 0..2 * Real.pi, ValueDistribution.Cartan.cartanKernel f R x β)
      (Set.Ioc 0 (2 * Real.pi)) MeasureTheory.volume

Corollary of integrableOn_cartanKernel: If f : ℂ → ℂ is meromorphic, then the function α ↦ ∫ β in 0..2 * π, Cartan.cartanKernel f R α β is integrable.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Cited by

1 results in Mathlib

Foundations

Depth 296 from the axioms · uses propext, Classical.choice, Quot.sound