Theorems · Theorem · complex analysis

ValueDistribution.characteristic_nonneg

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {a : WithTop E} {r : ℝ},
  1 ≤ r → 0 ≤ ValueDistribution.characteristic f a r

For 1 ≤ r, the characteristic function is non-negative.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace