Complex.circleTransformDeriv_bound

theorem Complex.circleTransformDeriv_bound : ∀ {R : ℝ}, 0 < R → ∀ {z x : ℂ} {f : ℂ → ℂ}, x ∈ Metric.ball z R → 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

This theorem states that for any positive real number `R`, complex numbers `z` and `x`, and a function `f` mapping complex numbers to complex numbers, if `x` is inside the ball centered at `z` with radius `R` and `f` is continuous on the boundary of this ball (the sphere centered at `z` with radius `R`), then there exists a positive real number `ε` and a bound `B` such that the ball centered at `x` with radius `ε` is contained within the ball centered at `z` with radius `R` and for every real number `t` and every point `y` inside the ball centered at `x` with radius `ε`, the norm of the derivative of the circle transform of `f` at `y` with respect to `t` is less than or equal to `B`.

More concisely: Given a positive real number `R`, a complex number `z`, a complex function `f` continuous on the boundary of the complex ball centered at `z` with radius `R`, and any complex number `x` inside this ball, there exist a positive real number `ε` and a bound `B` such that the open ball centered at `x` with radius `ε` is contained in the ball centered at `z` with radius `R`, and for all `t` and `y` in the ball centered at `x` with radius `ε`, the norm of the derivative of the circle transform of `f` at `y` with respect to `t` is less than or equal to `B`.