mathlib3 documentation

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.

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

The derivative of circle_transform w.r.t w.

Equations
source
theorem complex.circle_transform_deriv_periodic {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] (R : ℝ) (z w : ℂ) (f : ℂ → E) :
function.periodic (complex.circle_transform_deriv R z w f) (2 * real.pi)
source
theorem complex.circle_transform_deriv_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] (R : ℝ) (z w : ℂ) (f : ℂ → E) :
complex.circle_transform_deriv R z w f = λ (θ : ℝ), (circle_map z R θ - w)⁻¹ • complex.circle_transform R z w f θ
source
theorem complex.integral_circle_transform {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] (R : ℝ) (z w : ℂ) [complete_space E] (f : ℂ → E) :
∫ (θ : ℝ) in 0..2 * real.pi, complex.circle_transform R z w f θ = (2 * ↑real.pi * complex.I)⁻¹ • ∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z
source
theorem complex.continuous_circle_transform {E : Type u_1} [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) :
continuous (complex.circle_transform R z w f)
source
theorem complex.continuous_circle_transform_deriv {E : Type u_1} [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) :
continuous (complex.circle_transform_deriv R z w f)
source
noncomputable def complex.circle_transform_bounding_function (R : ℝ) (z : ℂ) (w : ℂ × ℝ) :
ℂ

A useful bound for circle integrals (with complex codomain)

Equations
source
theorem complex.continuous_on_prod_circle_transform_function {R r : ℝ} (hr : r < R) {z : ℂ} :
continuous_on (λ (w : ℂ × ℝ), (circle_map z R w.snd - w.fst)⁻¹ ^ 2) (metric.closed_ball z r ×ˢ set.univ)
source
theorem complex.continuous_on_abs_circle_transform_bounding_function {R r : ℝ} (hr : r < R) (z : ℂ) :
continuous_on (⇑complex.abs ∘ λ (t : ℂ × ℝ), complex.circle_transform_bounding_function R z t) (metric.closed_ball z r ×ˢ set.univ)
source
theorem complex.abs_circle_transform_bounding_function_le {R r : ℝ} (hr : r < R) (hr' : 0 ≤ r) (z : ℂ) :
∃ (x : ↥(metric.closed_ball z r ×ˢ set.uIcc 0 (2 * real.pi))), ∀ (y : ↥(metric.closed_ball z r ×ˢ set.uIcc 0 (2 * real.pi))), ⇑complex.abs (complex.circle_transform_bounding_function R z ↑y) ≤ ⇑complex.abs (complex.circle_transform_bounding_function R z ↑x)
source
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.