mathlib documentation

measure_theory.integral.circle_transform

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.

noncomputable def complex.circle_transform {E : Type} [normed_add_comm_group E] [normed_space 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} [normed_add_comm_group E] [normed_space E] (R : ) (z w : ) (f : E) (θ : ) :
E

The derivative of circle_transform w.r.t w.

Equations
theorem complex.continuous_circle_transform {E : Type} [normed_add_comm_group E] [normed_space E] {R : } (hR : 0 < R) {f : E} {z w : } (hf : continuous_on f (metric.sphere z R)) (hw : w metric.ball z R) :
noncomputable def complex.circle_transform_bounding_function (R : ) (z : ) (w : × ) :

A useful bound for circle integrals (with complex codomain)

Equations
theorem complex.circle_transform_deriv_bound {R : } (hR : 0 < R) {z x : } {f : } (hx : x metric.ball z R) (hf : continuous_on f (metric.sphere z R)) :
(B ε : ), 0 < ε metric.ball x ε metric.ball z R (t : ) (y : ), y metric.ball x ε complex.circle_transform_deriv R z y f t B

The derivative of a circle_transform is locally bounded.