E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π))
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : CircleIntegrable f c R
⊢ IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
simp only [CircleIntegrable, deriv_circleMap, intervalIntegrable_iff] at *
case refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ AEStronglyMeasurable (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Measure.restrict volume (Ι 0 (2 * π)))

case refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ι 0 (2 * π)),
    ‖(circleMap 0 R a * I) • f (circleMap c R a)‖ ≤ Abs.abs R * ‖f (circleMap c R a)‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π))
refine' (hf.norm.const_mul (|R|)).mono' _ _
no goals
case refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ AEStronglyMeasurable (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Measure.restrict volume (Ι 0 (2 * π)))
exact ((continuous_circleMap _ _).aestronglyMeasurable.mul_const I).smul hf.aestronglyMeasurable
no goals
case refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π))
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ι 0 (2 * π)),
    ‖(circleMap 0 R a * I) • f (circleMap c R a)‖ ≤ Abs.abs R * ‖f (circleMap c R a)‖
simp [norm_smul]