E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R : ℝ
z w : ℂ
inst✝ : CompleteSpace E
f : ℂ → E
⊢ (∫ (θ : ℝ) in 0 ..2 * π,
      (2 * ↑π * I)⁻¹ • ((0 + ↑R * exp (↑θ * I)) * I) • (z + ↑R * exp (↑θ * I) - w)⁻¹ • f (z + ↑R * exp (↑θ * I))) =
    (2 * ↑π * I)⁻¹ •
      ∫ (θ : ℝ) in 0 ..2 * π, ((0 + ↑R * exp (↑θ * I)) * I) • (z + ↑R * exp (↑θ * I) - w)⁻¹ • f (z + ↑R * exp (↑θ * I))
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R : ℝ
z w : ℂ
inst✝ : CompleteSpace E
f : ℂ → E
⊢ (∫ (θ : ℝ) in 0 ..2 * π, circleTransform R z w f θ) = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z
simp_rw [circleTransform, circleIntegral, deriv_circleMap, circleMap]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R : ℝ
z w : ℂ
inst✝ : CompleteSpace E
f : ℂ → E
⊢ (∫ (θ : ℝ) in 0 ..2 * π,
      (2 * ↑π * I)⁻¹ • ((0 + ↑R * exp (↑θ * I)) * I) • (z + ↑R * exp (↑θ * I) - w)⁻¹ • f (z + ↑R * exp (↑θ * I))) =
    (2 * ↑π * I)⁻¹ •
      ∫ (θ : ℝ) in 0 ..2 * π, ((0 + ↑R * exp (↑θ * I)) * I) • (z + ↑R * exp (↑θ * I) - w)⁻¹ • f (z + ↑R * exp (↑θ * I))
simp