Theorems · Theorem · complex analysis

CircleIntegrable.continuousOn_mul

∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [inst : NormedRing 𝕜] {f g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (g * f) c R

If g is continuous on the circle sphere c |R| and f is circle integrable, then g * f is circle integrable.

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedRing