# 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).

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

The derivative of circleTransform w.r.t w.

Equations
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 .., = (2 * * Complex.I)⁻¹ ∮ (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 (Metric.sphere z R)) (hw : w ) :
theorem Complex.continuous_circleTransformDeriv {E : Type u_1} [] {R : } (hR : 0 < R) {f : E} {z : } {w : } (hf : ContinuousOn f (Metric.sphere z R)) (hw : w ) :

A useful bound for circle integrals (with complex codomain)

Equations
Instances For
theorem Complex.continuousOn_prod_circle_transform_function {R : } {r : } (hr : r < R) {z : } :
ContinuousOn (fun (w : ) => (circleMap z R w.2 - w.1)⁻¹ ^ 2) ( ×ˢ Set.univ)
theorem Complex.abs_circleTransformBoundingFunction_le {R : } {r : } (hr : r < R) (hr' : 0 r) (z : ) :
∃ (x : ( ×ˢ Set.uIcc 0 (2 * Real.pi))), ∀ (y : ( ×ˢ Set.uIcc 0 (2 * Real.pi))), Complex.abs Complex.abs
theorem Complex.circleTransformDeriv_bound {R : } (hR : 0 < R) {z : } {x : } {f : } (hx : x ) (hf : ContinuousOn f (Metric.sphere z R)) :
∃ (B : ) (ε : ), 0 < ε ∀ (t : ), y, B

The derivative of a circleTransform is locally bounded.