Theorems · Theorem · complex analysis
ValueDistribution.Cartan.integrableOn_cartanKernel
∀ {f : ℂ → ℂ} {R : ℝ},
Meromorphic f →
MeasureTheory.IntegrableOn (fun p => ValueDistribution.Cartan.cartanKernel f R p.1 p.2)
(Set.uIoc 0 (2 * Real.pi) ×ˢ Set.uIoc 0 (2 * Real.pi)) MeasureTheory.volumeIf f : ℂ → ℂ is meromorphic, then the Cartan kernel of integration is integrable as a function in
the two variables α and β.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 295 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- MeasureTheory.Measureproof · cited by 10,939
- Complexstatement and proof · cited by 5,565
- LT.lt.leproof · cited by 2,189
- Real.pistatement and proof · cited by 1,774
- SProd.sprodstatement and proof · cited by 1,750
- MeasureTheory.Measure.restrictproof · cited by 1,646
- Measurableproof · cited by 1,499
- MeasureTheory.Integrableproof · cited by 1,367
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- MeasureTheory.IntegrableOnstatement · cited by 548
Cited by3
Results whose statement or proof uses this declaration.
- ValueDistribution.circleAverage_circleAverage_eq_proximity_topproof · cited by 1
- ValueDistribution.Cartan.integrableOn_intervalIntegral_cartanKernel_leftproof · cited by 0