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} [NormedAddCommGroup E] [NormedSpace ℂ E] (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

• Complex.circleTransform R z w f θ = (2 * ↑Real.pi * Complex.I)⁻¹ • deriv (circleMap z R) θ • (circleMap z R θ - w)⁻¹ • f (circleMap z R θ)

def Complex.circleTransformDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (R : ℝ) (z : ℂ) (w : ℂ) (f : ℂ → E) (θ : ℝ) : E

The derivative of circleTransform w.r.t w.

Equations

• Complex.circleTransformDeriv R z w f θ = (2 * ↑Real.pi * Complex.I)⁻¹ • deriv (circleMap z R) θ • ((circleMap z R θ - w) ^ 2)⁻¹ • f (circleMap z R θ)

theorem Complex.circleTransformDeriv_periodic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (R : ℝ) (z : ℂ) (w : ℂ) (f : ℂ → E) : Function.Periodic (Complex.circleTransformDeriv R z w f) (2 * Real.pi)

theorem Complex.circleTransformDeriv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (R : ℝ) (z : ℂ) (w : ℂ) (f : ℂ → E) : Complex.circleTransformDeriv R z w f = fun (θ : ℝ) => (circleMap z R θ - w)⁻¹ • Complex.circleTransform R z w f θ

theorem Complex.integral_circleTransform {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (R : ℝ) (z : ℂ) (w : ℂ) (f : ℂ → E) : ∫ (θ : ℝ) in 0 ..2 * Real.pi, Complex.circleTransform R z w f θ = (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z

theorem Complex.continuous_circleTransform {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {R : ℝ} (hR : 0 < R) {f : ℂ → E} {z : ℂ} {w : ℂ} (hf : ContinuousOn f (Metric.sphere z R)) (hw : w ∈ Metric.ball z R) : Continuous (Complex.circleTransform R z w f)

theorem Complex.continuous_circleTransformDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {R : ℝ} (hR : 0 < R) {f : ℂ → E} {z : ℂ} {w : ℂ} (hf : ContinuousOn f (Metric.sphere z R)) (hw : w ∈ Metric.ball z R) : Continuous (Complex.circleTransformDeriv R z w f)

def Complex.circleTransformBoundingFunction (R : ℝ) (z : ℂ) (w : ℂ × ℝ) : ℂ

A useful bound for circle integrals (with complex codomain)

Equations

• Complex.circleTransformBoundingFunction R z w = Complex.circleTransformDeriv R z w.1 (fun (x : ℂ) => 1) w.2

theorem Complex.continuousOn_prod_circle_transform_function {R : ℝ} {r : ℝ} (hr : r < R) {z : ℂ} : ContinuousOn (fun (w : ℂ × ℝ) => (circleMap z R w.2 - w.1)⁻¹ ^ 2) (Metric.closedBall z r ×ˢ Set.univ)

theorem Complex.continuousOn_abs_circleTransformBoundingFunction {R : ℝ} {r : ℝ} (hr : r < R) (z : ℂ) : ContinuousOn (⇑Complex.abs ∘ Complex.circleTransformBoundingFunction R z) (Metric.closedBall z r ×ˢ Set.univ)

theorem Complex.abs_circleTransformBoundingFunction_le {R : ℝ} {r : ℝ} (hr : r < R) (hr' : 0 ≤ r) (z : ℂ) : ∃ (x : ↑(Metric.closedBall z r ×ˢ Set.uIcc 0 (2 * Real.pi))), ∀ (y : ↑(Metric.closedBall z r ×ˢ Set.uIcc 0 (2 * Real.pi))), Complex.abs (Complex.circleTransformBoundingFunction R z ↑y) ≤ Complex.abs (Complex.circleTransformBoundingFunction R z ↑x)

theorem Complex.circleTransformDeriv_bound {R : ℝ} (hR : 0 < R) {z : ℂ} {x : ℂ} {f : ℂ → ℂ} (hx : x ∈ Metric.ball z R) (hf : ContinuousOn f (Metric.sphere z R)) : ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ Metric.ball x ε ⊆ Metric.ball z R ∧ ∀ (t : ℝ), ∀ y ∈ Metric.ball x ε, ‖Complex.circleTransformDeriv R z y f t‖ ≤ B

The derivative of a circleTransform is locally bounded.