Theorems · Theorem · complex analysis

MeromorphicOn.circleIntegrable_posLog_norm_of_nonneg

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.sphere c R) → 0 ≤ R → CircleIntegrable (fun x => ‖f x‖.posLog) c R

Variant of MeromorphicOn.circleIntegrable_posLog_norm for non-negative radii.

Defined in: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Cited by: 1 results in Mathlib
Foundations: Depth 272 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup NormedSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
NormedSpacestatement and proof · cited by 12,499
Complexstatement and proof · cited by 5,565
Norm.normstatement · cited by 5,413
Metric.spherestatement and proof · cited by 371
abs_of_nonnegproof · cited by 279
MeromorphicOnstatement and proof · cited by 141
CircleIntegrablestatement · cited by 86
Real.posLogstatement · cited by 61
MeromorphicOn.circleIntegrable_posLog_normproof · cited by 7

Cited by1

Results whose statement or proof uses this declaration.

circleIntegrable_posLog_norm_meromorphicOn_of_nonnegproof · cited by 0