Theorems · Theorem · complex analysis

CircleIntegrable.smul_continuousOn

∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → 𝕜} {g : ℂ → F},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (f • g) c R

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

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedRingNormedAddCommGroupModuleNormSMulClass