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

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.

theorem Complex.circleTransformDeriv_periodic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (R : ℝ) (z w : ℂ) (f : ℂ → E) : Function.Periodic (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) : circleTransformDeriv R z w f = fun (θ : ℝ) => (circleMap z R θ - w)⁻¹ • 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, circleTransform R z w f θ = (2 * ↑Real.pi * 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 (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 (circleTransformDeriv R z w f)

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

A useful bound for circle integrals (with complex codomain)

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_norm_circleTransformBoundingFunction {R r : ℝ} (hr : r < R) (z : ℂ) : ContinuousOn ((fun (x : ℂ) => ‖x‖) ∘ circleTransformBoundingFunction R z) (Metric.closedBall z r ×ˢ Set.univ)

theorem Complex.norm_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))), ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖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 ε, ‖circleTransformDeriv R z y f t‖ ≤ B

The derivative of a circleTransform is locally bounded.