Complex.dist_le_dist_of_mapsTo_ball_self
theorem Complex.dist_le_dist_of_mapsTo_ball_self :
∀ {f : ℂ → ℂ} {c z : ℂ} {R : ℝ},
DifferentiableOn ℂ f (Metric.ball c R) →
Set.MapsTo f (Metric.ball c R) (Metric.ball c R) → f c = c → z ∈ Metric.ball c R → dist (f z) c ≤ dist z c
The Schwarz Lemma states that if a complex function `f` maps an open disk to itself and the center `c` of this disk to itself, then for any point `z` in this disk, the distance from `f(z)` to `c` is less than or equal to the distance from `z` to `c`. More specifically, given a complex function `f`, a center `c`, a point `z`, and a real number `R`, if `f` is differentiable on the open disk centered at `c` with radius `R` and `f` maps this open disk to itself, and if `f(c)` equals `c` and `z` is an element of this open disk, then the distance from `f(z)` to `c` is less than or equal to the distance from `z` to `c`.
More concisely: If `f` is a complex function that maps an open disk centered at `c` to itself, is differentiable on this disk, and satisfies `f(c) = c`, then for all `z` in the disk, `|f(z) - c| <= |z - c|`.
|
Complex.schwarz_aux
theorem Complex.schwarz_aux :
∀ {R₁ R₂ : ℝ} {c z : ℂ} {f : ℂ → ℂ},
DifferentiableOn ℂ f (Metric.ball c R₁) →
Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂) → z ∈ Metric.ball c R₁ → ‖dslope f c z‖ ≤ R₂ / R₁
The theorem `Complex.schwarz_aux` states that for all real numbers `R₁` and `R₂`, complex numbers `c` and `z`, and a function `f` from the complex numbers to the complex numbers, if `f` is differentiable on the open ball centered at `c` with radius `R₁` and the image of the open ball under `f` is contained within the open ball centered at `f(c)` with radius `R₂`, and `z` is an element in the open ball centered at `c` with radius `R₁`, then the norm of the directional derivative of `f` at `c` in the direction of `z` is less than or equal to the ratio `R₂ / R₁`. This theorem is used as an auxiliary lemma in the proof of `Complex.norm_dslope_le_div_of_mapsTo_ball`.
More concisely: Given a differentiable complex function $f$, if the image of the open ball centered at $c$ with radius $R\_1$ under $f$ is contained in the open ball centered at $f(c)$ with radius $R\_2$, then for any $z$ in the open ball centered at $c$ with radius $R\_1$, the norm of the directional derivative of $f$ at $c$ in the direction of $z$ is less than or equal to $R\_2 / R\_1$.
|
Complex.abs_le_abs_of_mapsTo_ball_self
theorem Complex.abs_le_abs_of_mapsTo_ball_self :
∀ {f : ℂ → ℂ} {z : ℂ} {R : ℝ},
DifferentiableOn ℂ f (Metric.ball 0 R) →
Set.MapsTo f (Metric.ball 0 R) (Metric.ball 0 R) →
f 0 = 0 → Complex.abs z < R → Complex.abs (f z) ≤ Complex.abs z
This is the **Schwarz Lemma** from complex analysis, stated in terms of Lean 4's formal mathematics language. The Lemma says that if we have a complex-valued function `f` which is differentiable on an open disk centered at `0` (with some radius `R`) and maps this disk to itself, then for any point `z` within this disk, the absolute value of `f(z)` is less than or equal to the absolute value of `z`. It is also required that `f(0) = 0`. In mathematical terms, for all `f : ℂ → ℂ`, `z : ℂ`, and `R : ℝ`, given that `f` is differentiable on the disk `D(0, R)` and maps `D(0, R)` to itself, and `f(0) = 0`, if `|z| < R` then `|f(z)| ≤ |z|`.
More concisely: If `f` is a complex-valued differentiable function that maps an open disk centered at 0 to itself and has `f(0) = 0`, then for any point `z` within the disk, `|f(z)| ≤ |z|`.
|
Complex.dist_le_div_mul_dist_of_mapsTo_ball
theorem Complex.dist_le_div_mul_dist_of_mapsTo_ball :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z : ℂ},
DifferentiableOn ℂ f (Metric.ball c R₁) →
Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂) →
z ∈ Metric.ball c R₁ → dist (f z) (f c) ≤ R₂ / R₁ * dist z c
The **Schwarz Lemma** states that given a function `f` mapping from complex numbers to a normed additive commutative group `E`, and given two real numbers `R₁` and `R₂`, if `f` is differentiable on an open disk with center at a complex number `c` and radius `R₁`, and if the image of this disk under `f` is contained within an open ball with center at `f(c)` and radius `R₂`, then for any complex number `z` within the original disk, the distance between `f(z)` and `f(c)` is less than or equal to the ratio `R₂ / R₁` times the distance between `z` and `c`.
More concisely: Given a differentiable function `f` from complex numbers to a normed additive commutative group with an open disk around `c` as its domain, if the image of this disk is contained within a smaller open ball around `f(c)`, then for any `z` in the disk, `|f(z) - f(c)| ≤ |z - c| * (R₂ / R₁)`, where `|.|` denotes the norm and `R₁` is the radius of the disk, `R₂` the radius of the smaller ball.
|
Complex.abs_deriv_le_one_of_mapsTo_ball
theorem Complex.abs_deriv_le_one_of_mapsTo_ball :
∀ {f : ℂ → ℂ} {c : ℂ} {R : ℝ},
DifferentiableOn ℂ f (Metric.ball c R) →
Set.MapsTo f (Metric.ball c R) (Metric.ball c R) → f c = c → 0 < R → Complex.abs (deriv f c) ≤ 1
The **Schwarz Lemma** states that if a complex function `f` maps an open disk of positive radius to itself and the center of this disk to itself, then the absolute value of the derivative of `f` at the center of this disk is at most `1`. In more formal terms, for any complex function `f`, complex number `c`, and real number radius `R`, if `f` is differentiable on the open disk centered at `c` with radius `R`, `f` maps each point in this disk back into the disk, and `f(c) = c`, with `R > 0`, then the complex absolute value of the derivative of `f` at `c` is less than or equal to `1`.
More concisely: If `f` is a complex differentiable function mapping an open disk centered at `c` with positive radius to itself, then the absolute value of `f'(c)` is at most 1.
|
Complex.abs_deriv_le_div_of_mapsTo_ball
theorem Complex.abs_deriv_le_div_of_mapsTo_ball :
∀ {f : ℂ → ℂ} {c : ℂ} {R₁ R₂ : ℝ},
DifferentiableOn ℂ f (Metric.ball c R₁) →
Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂) → 0 < R₁ → Complex.abs (deriv f c) ≤ R₂ / R₁
The theorem is known as the Schwarz Lemma. It states that for a function `f` mapping complex numbers to complex numbers, if `f` maps an open disk with center `c` and a positive radius `R₁` to another open disk with center `f(c)` and radius `R₂`, then the absolute value of the derivative of `f` at `c` is at most the ratio `R₂ / R₁`. This theorem assumes that `f` is differentiable on the first disk and that the radius `R₁` is positive.
More concisely: If a differentiable complex function maps an open disk to another with the same center and smaller radius, then the absolute value of its derivative at the center is less than or equal to the ratio of the radii.
|
Complex.norm_deriv_le_div_of_mapsTo_ball
theorem Complex.norm_deriv_le_div_of_mapsTo_ball :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c : ℂ},
DifferentiableOn ℂ f (Metric.ball c R₁) →
Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂) → 0 < R₁ → ‖deriv f c‖ ≤ R₂ / R₁
The Schwarz Lemma states that if we have a function `f` mapping from the complex numbers to a normed space `E`, which sends an open disk with center `c` and a positive radius `R₁` to an open ball with center `f(c)` and radius `R₂`, then the absolute value of the derivative of `f` at `c` is at most the ratio `R₂ / R₁`. In other words, if `f` is differentiable within the disk and the image of the disk under `f` is contained within the ball, and if `R₁` is positive, then the norm of the derivative of `f` at `c` is less than or equal to `R₂ / R₁`.
More concisely: If `f: ℂ → E` is a differentiable function, `c ∈ ℂ`, `R₁ > 0`, and the image of the open disk `{z : ℂ | |z - c| < R₁}` under `f` is contained in the open ball `{x : E | ||x - f(c)|| < R₂}`, then `||f'(c)|| ≤ R₂ / R₁`, where `||.||` denotes the norm in `E` and `f'` is the derivative of `f`.
|
Complex.norm_dslope_le_div_of_mapsTo_ball
theorem Complex.norm_dslope_le_div_of_mapsTo_ball :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z : ℂ},
DifferentiableOn ℂ f (Metric.ball c R₁) →
Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂) → z ∈ Metric.ball c R₁ → ‖dslope f c z‖ ≤ R₂ / R₁
The Schwarz Lemma theorem in complex analysis states that for certain given conditions, the magnitude of the derivative of a complex-valued function is bounded above by the ratio of two real numbers. More specifically, if a complex-valued function `f` is differentiable on a ball of radius `R₁` centered at a complex number `c`, and the image of this ball under `f` is contained within a ball of radius `R₂` centered at `f(c)`, then for any complex number `z` in the first ball, the norm of the derivative of `f` at `z` (as given by `dslope f c z`) is less than or equal to the ratio `R₂ / R₁`.
More concisely: If a complex-valued function is differentiable on a disk and its image is contained in a smaller disk, then the magnitude of its derivative is bounded by the ratio of the radii of the disks.
|
Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div
theorem Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z₀ : ℂ}
[inst_2 : CompleteSpace E] [inst_3 : StrictConvexSpace ℝ E],
DifferentiableOn ℂ f (Metric.ball c R₁) →
Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂) →
z₀ ∈ Metric.ball c R₁ →
‖dslope f c z₀‖ = R₂ / R₁ → Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (Metric.ball c R₁)
In the context of complex vector spaces, this theorem is an equality case in the Schwarz Lemma. Given a function `f` from complex numbers to a normed additive commutative group `E` that is differentiable on a ball of radius `R₁` centered at `c`, and such that all the images of points from this ball lie within another ball of radius `R₂` centered at `f(c)`, if we can find a point `z₀` in the first ball such that the norm of the derivative of the slope of `f` at `z₀` equals `R₂ / R₁`, then `f` is an affine function on the first ball. More precisely, for each `z` in the first ball, `f(z)` equals `f(c)` plus the product of `z - c` and the derivative of the slope of `f` at `z₀`.
More concisely: If a differentiable function `f` from complex numbers to a complex normed vector space, whose images lie in a smaller ball centered at `f(c)`, has a derivative norm equal to the ratio of the smaller and larger ball radii at some point in the larger ball, then `f` is an affine function on the larger ball.
|