# mathlib3documentation

measure_theory.integral.circle_transform

# Circle integral transform #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

noncomputable def complex.circle_transform {E : Type u_1} [ E] (R : ) (z w : ) (f : E) (θ : ) :
E

Given a function f : ℂ → E, circle_transform R z w f is the functions mapping θ to (2 * ↑π * I)⁻¹ • deriv (circle_map z R) θ • ((circle_map z R θ) - w)⁻¹ • f (circle_map 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
noncomputable def complex.circle_transform_deriv {E : Type u_1} [ E] (R : ) (z w : ) (f : E) (θ : ) :
E

The derivative of circle_transform w.r.t w.

Equations
theorem complex.circle_transform_deriv_periodic {E : Type u_1} [ E] (R : ) (z w : ) (f : E) :
(2 * real.pi)
theorem complex.circle_transform_deriv_eq {E : Type u_1} [ E] (R : ) (z w : ) (f : E) :
= λ (θ : ), R θ - w)⁻¹ f θ
theorem complex.integral_circle_transform {E : Type u_1} [ E] (R : ) (z w : ) (f : E) :
(θ : ) in 0.., f θ = * complex.I)⁻¹ (z : ) in C(z, R), (z - w)⁻¹ f z
theorem complex.continuous_circle_transform {E : Type u_1} [ E] {R : } (hR : 0 < R) {f : E} {z w : } (hf : R)) (hw : w R) :
theorem complex.continuous_circle_transform_deriv {E : Type u_1} [ E] {R : } (hR : 0 < R) {f : E} {z w : } (hf : R)) (hw : w R) :
noncomputable def complex.circle_transform_bounding_function (R : ) (z : ) (w : × ) :

A useful bound for circle integrals (with complex codomain)

Equations
theorem complex.continuous_on_prod_circle_transform_function {R r : } (hr : r < R) {z : } :
continuous_on (λ (w : × ), R w.snd - w.fst)⁻¹ ^ 2)
theorem complex.abs_circle_transform_bounding_function_le {R r : } (hr : r < R) (hr' : 0 r) (z : ) :
(x : ×ˢ (2 * real.pi))), (y : ×ˢ (2 * real.pi))),
theorem complex.circle_transform_deriv_bound {R : } (hR : 0 < R) {z x : } {f : } (hx : x R) (hf : R)) :
(B ε : ), 0 < ε ε R (t : ) (y : ), y ε t B

The derivative of a circle_transform is locally bounded.