English
If f is CircleIntegrable, then the integral with the weight deriv(circleMap(c,R)θ) is Lebesgue-integrable on [0,2π].
Русский
Если f CircleIntegrable, то взвешенная производнойCircleMap интегрируемая на [0,2π].
LaTeX
$$$\text{out}\_{hf} : \text{IntervalIntegrable}(\theta \mapsto \operatorname{deriv}(\circleMap(c,R))(\theta) \cdot f(\circleMap(c,R,\theta)), \; \text{volume}, 0, 2\pi).$$$
Lean4
/-- The function we actually integrate over `[0, 2π]` in the definition of `circleIntegral` is
integrable. -/
theorem out [NormedSpace ℂ E] (hf : CircleIntegrable f c R) :
IntervalIntegrable (fun θ : ℝ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π) :=
by
simp only [CircleIntegrable, deriv_circleMap, intervalIntegrable_iff] at *
refine (hf.norm.const_mul |R|).mono' ?_ ?_
· exact ((continuous_circleMap _ _).aestronglyMeasurable.mul_const I).smul hf.aestronglyMeasurable
· simp [norm_smul]
