# Documentation

Mathlib.MeasureTheory.Integral.CircleTransform

# Circle integral transform #

In this file we define the circle integral transform of a function f with complex domain. This is defined as $(2πi)^{-1}\frac{f(x)}{x-w}$ where x moves along a circle. We then prove some basic facts about these functions.

These results are useful for proving that the uniform limit of a sequence of holomorphic functions is holomorphic.

def Complex.circleTransform {E : Type u_1} [] (R : ) (z : ) (w : ) (f : E) (θ : ) :
E

Given a function f : ℂ → E, circleTransform R z w f is the function mapping θ to (2 * ↑π * I)⁻¹ • deriv (circleMap z R) θ • ((circleMap z R θ) - w)⁻¹ • f (circleMap z R θ).

If f is differentiable and w is in the interior of the ball, then the integral from 0 to 2 * π of this gives the value f(w).

Instances For
def Complex.circleTransformDeriv {E : Type u_1} [] (R : ) (z : ) (w : ) (f : E) (θ : ) :
E

The derivative of circleTransform w.r.t w.

Instances For
theorem Complex.circleTransformDeriv_periodic {E : Type u_1} [] (R : ) (z : ) (w : ) (f : E) :
theorem Complex.circleTransformDeriv_eq {E : Type u_1} [] (R : ) (z : ) (w : ) (f : E) :
= fun θ => (circleMap z R θ - w)⁻¹
theorem Complex.integral_circleTransform {E : Type u_1} [] (R : ) (z : ) (w : ) (f : E) :
∫ (θ : ) in 0 .., = ()⁻¹ ∮ (z : ) in C(z, R), (z - w)⁻¹ f z
theorem Complex.continuous_circleTransform {E : Type u_1} [] {R : } (hR : 0 < R) {f : E} {z : } {w : } (hf : ContinuousOn f ()) (hw : w ) :
theorem Complex.continuous_circleTransformDeriv {E : Type u_1} [] {R : } (hR : 0 < R) {f : E} {z : } {w : } (hf : ContinuousOn f ()) (hw : w ) :

A useful bound for circle integrals (with complex codomain)

Instances For
theorem Complex.continuousOn_prod_circle_transform_function {R : } {r : } (hr : r < R) {z : } :
ContinuousOn (fun w => (circleMap z R w.snd - w.fst)⁻¹ ^ 2) ( ×ˢ Set.univ)
theorem Complex.continuousOn_abs_circleTransformBoundingFunction {R : } {r : } (hr : r < R) (z : ) :
ContinuousOn ( fun t => ) ( ×ˢ Set.univ)
theorem Complex.abs_circleTransformBoundingFunction_le {R : } {r : } (hr : r < R) (hr' : 0 r) (z : ) :
x, ∀ (y : ↑( ×ˢ Set.uIcc 0 ())),
theorem Complex.circleTransformDeriv_bound {R : } (hR : 0 < R) {z : } {x : } {f : } (hx : x ) (hf : ContinuousOn f ()) :
B ε, 0 < ε ∀ (t : ) (y : ), y B

The derivative of a circleTransform is locally bounded.