circleIntegral.integral_eq_zero_of_hasDerivWithinAt
theorem circleIntegral.integral_eq_zero_of_hasDerivWithinAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {f f' : ℂ → E}
{c : ℂ} {R : ℝ},
0 ≤ R →
(∀ z ∈ Metric.sphere c R, HasDerivWithinAt f (f' z) (Metric.sphere c R) z) → (∮ (z : ℂ) in C(c, R), f' z) = 0
The theorem states that if `f' : ℂ → E` is a derivative of a complex differentiable function on the circle defined by the metric sphere `Metric.sphere c R`, then the complex line integral of `f'` around the circle `C(c, R)` equals zero. This holds for all functions `f` and `f'` from the complex numbers to a normed additive commutative group `E` that is also a complex normed space and a complete space, for all complex numbers `c`, and for all real numbers `R` greater than or equal to zero.
More concisely: If `f : ℂ → E` is complex differentiable on the metric sphere `Metric.sphere c R` in a complex normed space and complete group `E`, then the complex line integral of `f'` around the circle `C(c, R)` equals zero.
|
circleIntegral.integral_sub_inv_of_mem_ball
theorem circleIntegral.integral_sub_inv_of_mem_ball :
∀ {c w : ℂ} {R : ℝ}, w ∈ Metric.ball c R → (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑Real.pi * Complex.I
The theorem `circleIntegral.integral_sub_inv_of_mem_ball` states that for any complex numbers `c` and `w`, and any real number `R`, if `w` is in the open ball centered at `c` with radius `R` (i.e., the distance from `w` to `c` is less than `R`), then the contour integral over the circle centered at `c` with radius `R`, of the function `1/(z-w)` with respect to `z`, equals `2πi` (where `π` is the mathematical constant Pi and `i` is the imaginary unit). This theorem is a key result in complex analysis related to Cauchy's integral formula.
More concisely: For any complex numbers `c` and `w` with `|z-c|
|
circleMap_sub_center
theorem circleMap_sub_center : ∀ (c : ℂ) (R θ : ℝ), circleMap c R θ - c = circleMap 0 R θ
This theorem states that for any complex number 'c' and real numbers 'R' and 'θ', the difference between the result of applying the 'circleMap' function to 'c', 'R', and 'θ' and 'c' itself, is equal to the result of applying the 'circleMap' function to 0, 'R', and 'θ'. In other words, if we shift the center of the circular map from 'c' to the origin (0), the mapped values will also shift by the same amount 'c'. This can be thought of as a property of the shift invariance of the circular map in the complex plane.
More concisely: For any complex number 'c' and real numbers 'R' and 'θ', the circular map of 'c' with radius 'R' and angle 'θ' is equal to the circular map of the origin with the same radius and angle, translated by 'c'.
|
differentiable_circleMap
theorem differentiable_circleMap : ∀ (c : ℂ) (R : ℝ), Differentiable ℝ (circleMap c R)
The theorem `differentiable_circleMap` states that for any complex number `c` and any real number `R`, the function `circleMap` is differentiable with respect to the real numbers. The `circleMap` function represents the exponential map in the complex plane, mapping a real number `θ` to a point on a circle with center `c` and radius `|R|`. The differentiability of this function is fundamental to understanding the behavior of the function's output as the input `θ` changes infinitesimally.
More concisely: The exponential map in the complex plane, represented by the `circleMap` function with center `c` and radius `R`, is differentiable as a function from the real numbers to the complex numbers.
|
hasSum_cauchyPowerSeries_integral
theorem hasSum_cauchyPowerSeries_integral :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ},
CircleIntegrable f c R →
Complex.abs w < R →
HasSum (fun n => (cauchyPowerSeries f c R n) fun x => w)
((2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
This theorem states that for any circle-integrable function `f`, the Cauchy power series `cauchyPowerSeries f c R`, where `R` is greater than 0, converges to the Cauchy integral `(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z` within the open disc `Metric.ball c R`, where `I` is the imaginary unit, `π` is the mathematical constant pi and `∮` is the contour integral. This rule applies for any complex number `w` that has an absolute value less than `R`. Here, `c` is the center of the circle, `R` is the radius, `f` is the function being integrated and `w` is the point of evaluation.
More concisely: For any circle-integrable function `f`, the Cauchy power series of `f` converges to the value of the Cauchy integral of `(z - w)⁻¹ * f(z) dz` around the circle centered at `c` with radius `R`, where `w` has an absolute value less than `R`.
|
circleIntegral.integral_sub_zpow_of_ne
theorem circleIntegral.integral_sub_zpow_of_ne :
∀ {n : ℤ}, n ≠ -1 → ∀ (c w : ℂ) (R : ℝ), (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
The theorem states that for any integer `n` that is not equal to -1, and for any complex numbers `c` and `w`, and any real number `R`, the integral of `(z - w) ^ n` over a circle centered at `c` with radius `R` is equal to zero. This integral is computed over complex numbers `z` along the circle.
More concisely: For any complex number `c`, real number `R` (`R` > 0), and integer `n` (!= -1, `\mathbb{Z}`), the integral of `(z - c) ^ n` over a circle of radius `R` centered at `c` is equal to zero.
|
hasFPowerSeriesOn_cauchy_integral
theorem hasFPowerSeriesOn_cauchy_integral :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : NNReal},
CircleIntegrable f c ↑R →
0 < R →
HasFPowerSeriesOnBall (fun w => (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z)
(cauchyPowerSeries f c ↑R) c ↑R
This theorem states that, for any circle-integrable function `f` from the complex numbers to a normed space `E`, given a complex number `c` and a positive nonnegative real number `R`, the Cauchy power series `cauchyPowerSeries f c R` converges to the Cauchy integral `(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z` on the open disc `Metric.ball c R`. This means that the series representation of the Cauchy integral of the function `f` within the circle with center `c` and radius `R` is given by the `cauchyPowerSeries` of `f` at `c` and `R`.
Here, `CircleIntegrable f c R` means that the function `f` is integrable over the circle with center `c` and radius `R`, and `HasFPowerSeriesOnBall` means that a function has a formal power series on a ball in the complex plane.
In more mathematical terms, it's expressing the relation between the Cauchy integral formula and power series representation of holomorphic functions on the complex plane.
More concisely: For a circle-integrable function `f` from the complex numbers to a normed space, the Cauchy power series `cauchyPowerSeries f c R` of `f` at `c` with radius `R` converges to the Cauchy integral of `f` on the open disc `Metric.ball c R`.
|
circleMap_zero_radius
theorem circleMap_zero_radius : ∀ (c : ℂ), circleMap c 0 = Function.const ℝ c
This theorem states that for any complex number `c`, if we apply the function `circleMap` with `c` as the center and zero as the radius, we will obtain a constant function that always returns `c`. In other words, when the radius of the circle in the complex plane is zero, the `circleMap` function reduces to a singleton point at the center `c`.
More concisely: For any complex number `c`, the `circleMap` function with `c` as the center and radius 0 is the constant function equal to `c`.
|
circleIntegrable_sub_zpow_iff
theorem circleIntegrable_sub_zpow_iff :
∀ {c w : ℂ} {R : ℝ} {n : ℤ},
CircleIntegrable (fun z => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ Metric.sphere c |R|
The theorem `circleIntegrable_sub_zpow_iff` states that for any complex numbers `c` and `w`, any real number `R`, and any integer `n`, the function `fun z ↦ (z - w) ^ n` is circle integrable on the circle with center `c` and radius `|R|` if and only if either `R` equals zero, `n` is nonnegative, or `w` does not belong to the circle defined by the center `c` and radius `|R|`. In mathematical terms, it states that the function $(z - w)^n$ can be integrated around the circle with radius $|R|$ and center at $c$ if and only if $R=0$, $n$ is nonnegative, or $w$ does not lie on the said circle.
More concisely: The theorem `circleIntegrable_sub_zpow_iff` in Lean 4 states that a complex function of the form `z ↦ (z - w) ^ n` is circle integrable on a circle with center `c` and radius `|R|` if and only if `R = 0`, `n` is nonnegative, or `w` is not on the circle with center `c` and radius `|R|`.
|
periodic_circleMap
theorem periodic_circleMap : ∀ (c : ℂ) (R : ℝ), Function.Periodic (circleMap c R) (2 * Real.pi)
The theorem `periodic_circleMap` states that the function `circleMap`, which maps a complex number `c`, a real number `R`, and an angle `θ` to a point on the complex plane representing a circle with center `c` and radius `|R|`, is periodic with period `2π`. This means for any complex number `c` and real number `R`, for all `θ`, `circleMap` of `θ + 2π` is equal to `circleMap` of `θ`. Essentially, this is saying that once you've rotated `2π` radians (a full circle) around the circle, you end up in the same place where you started.
More concisely: The `circleMap` function, which maps a complex number `c`, a real number `R`, and an angle `θ` to a point on the complex plane representing a circle with center `c` and radius `|R|`, is a periodic function with period `2π`.
|
circleMap_mem_sphere'
theorem circleMap_mem_sphere' : ∀ (c : ℂ) (R θ : ℝ), circleMap c R θ ∈ Metric.sphere c |R|
This theorem states that for any complex number `c`, and any real numbers `R` and `θ`, the output of the function `circleMap` with inputs `c`, `R`, and `θ`, is a member of the sphere centered at `c` with radius `|R|`. In other words, the exponential map, which maps the real number `θ` to the complex number `c + Re^{θi}`, produces a point on the complex plane that lies on the circle with center `c` and radius `|R|`.
More concisely: For any complex number `c` and real numbers `R` and `θ`, the point `c + R * exp iθ` lies on the circle centered at `c` with radius `|R|` in the complex plane.
|
abs_circleMap_zero
theorem abs_circleMap_zero : ∀ (R θ : ℝ), Complex.abs (circleMap 0 R θ) = |R|
The theorem `abs_circleMap_zero` states that for all real numbers `R` and `θ`, the complex absolute value (or modulus) of the result of mapping `θ` to the circle in the complex plane with center at 0 and radius `R` using the `circleMap` function, is equal to the absolute value of `R`. In other words, the distance from the origin to any point on the circle mapped by `circleMap` with center 0 and radius `R` is precisely the absolute value of `R`, regardless of the angle `θ`.
More concisely: For all real numbers R and angles θ, the absolute value of the complex number obtained by mapping θ to the complex plane with center at 0 and radius R using the `circleMap` function, equals R.
|
hasSum_two_pi_I_cauchyPowerSeries_integral
theorem hasSum_two_pi_I_cauchyPowerSeries_integral :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ},
CircleIntegrable f c R →
Complex.abs w < R →
HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
(∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
The theorem `hasSum_two_pi_I_cauchyPowerSeries_integral` establishes a relationship between a power series and a circle integral in the field of complex analysis. Specifically, for a given circle integrable function `f`, a complex number `c`, a real number `R`, and a complex number `w` with its complex absolute value less than `R`, the power series formed by the integral of `f` around a circle centered at `c` with radius `R`, with each term multiplied by `(w / (z - c)) ^ n` and `(z - c)⁻¹`, converges to the integral of `f` around the same circle, but with each term multiplied by `(z - (c + w))⁻¹`. This result plays a crucial role in the study of analytic functions in complex analysis.
More concisely: For a circle integrable function `f` and complex number `c`, the power series formed by integrating `f` around a circle centered at `c` using a specific transformation converges to the original circle integral.
|
circleIntegral.integral_radius_zero
theorem circleIntegral.integral_radius_zero :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c : ℂ),
(∮ (z : ℂ) in C(c, 0), f z) = 0
This theorem states that for any complex-valued function `f` and any complex number `c`, the contour (or line) integral of `f` around the circle centered at `c` with radius 0 is always 0. More formally, `∮ (z : ℂ) in C(c, 0), f z = 0`, where `C(c, 0)` is the circle centered at `c` with radius 0, `ℂ` denotes the set of complex numbers, and `E` is any normed add-commutative group that is also a normed space over the complex numbers.
More concisely: The contour integral of any complex-valued function `f` over the circle centered at `c` with radius 0 is equal to 0.
|
image_circleMap_Ioc
theorem image_circleMap_Ioc : ∀ (c : ℂ) (R : ℝ), circleMap c R '' Set.Ioc 0 (2 * Real.pi) = Metric.sphere c |R| := by
sorry
The theorem `image_circleMap_Ioc` states that for any complex number `c` and any real number `R`, the image of the interval `(0, 2π]` under the function `circleMap c R` is exactly the circle with center `c` and radius `|R|`. In other words, if we map each real number `θ` in the interval `(0, 2π]` to the complex number `c + R e^{θi}`, we obtain all and only the points on the complex plane that are a distance `|R|` away from `c`, forming a circle.
More concisely: The image of the interval (0, 2π] under the complex function `circleMap c R (x => c + R * exp (I * x))` is the circle with center `c` and radius `|R|` in the complex plane.
|
sum_cauchyPowerSeries_eq_integral
theorem sum_cauchyPowerSeries_eq_integral :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ},
CircleIntegrable f c R →
Complex.abs w < R →
(cauchyPowerSeries f c R).sum w =
(2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z
This theorem states that for any circle-integrable function `f` and a given complex number `c`, real number `R` such that `R > 0`, the Cauchy power series `cauchyPowerSeries f c R` converges to the Cauchy integral `(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z` within the open disk `Metric.ball c R`. This holds provided that the absolute value of a complex number `w` is less than `R`. Essentially, it's a statement about the behavior of power series and their relationship to complex integration, where the integral is taken around a circle of radius `R` centered at a complex point `c`.
More concisely: For any circle-integrable function `f`, the Cauchy power series `cauchyPowerSeries f c R` converges to the value of the Cauchy integral `(2 * π * I : ℂ)⁻¹ • ∫(z : C(c, R)) dz [(z - w)⁻¹ * f z]` within the open disk `Metric.ball c R`, where `w` is a complex number with smaller absolute value than `R`.
|
circleIntegral.integral_sub_zpow_of_undef
theorem circleIntegral.integral_sub_zpow_of_undef :
∀ {n : ℤ} {c w : ℂ} {R : ℝ}, n < 0 → w ∈ Metric.sphere c |R| → (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
This theorem states that for any integer `n`, complex numbers `c` and `w`, and a real number `R`, if `n` is less than zero and `w` lies on the sphere with center `c` and radius `|R|` (i.e., the distance from `w` to `c` equals `|R|`), then the complex line integral of `(z - w) ^ n` over the circle `C(c, R)` is equal to zero. In other words, the integral of the function `(z - w) ^ n` with respect to `z` along the circular path centered at `c` with radius `R` is zero under these conditions.
More concisely: For any complex number `c`, real number `R`, integer `n` with `n < 0`, and complex number `w` on the sphere with center `c` and radius `|R|`, the complex line integral of `(z - w) ^ n` over the circle `C(c, R)` equals zero.
|
range_circleMap
theorem range_circleMap : ∀ (c : ℂ) (R : ℝ), Set.range (circleMap c R) = Metric.sphere c |R|
The theorem `range_circleMap` states that for any complex number `c` and any real number `R`, the range of the function `circleMap` with parameters `c` and `R` is equal to the sphere centered at `c` with radius equal to the absolute value of `R`. In other words, when the function `circleMap` maps any real number to a complex number, it maps to a point on a circle in the complex plane, with `c` as the center and `|R|` as the radius.
More concisely: The range of the function `circleMap` with complex number parameter `c` and real number parameter `R` is the sphere in the complex plane with center `c` and radius `|R|`.
|
circleIntegral.norm_integral_lt_of_norm_le_const_of_lt
theorem circleIntegral.norm_integral_lt_of_norm_le_const_of_lt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R C : ℝ},
0 < R →
ContinuousOn f (Metric.sphere c R) →
(∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) →
(∃ z ∈ Metric.sphere c R, ‖f z‖ < C) → ‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * Real.pi * R * C
The theorem states that if we have a function `f` that is continuous on a circle in the complex plane centered at `c` with radius `R` greater than 0, and if the norm of `f(z)` is less than or equal to a constant `C` for all points `z` on the circle, and the norm of `f(z)` is strictly less than `C` for at least one point `z` on the circle, then the norm of the complex line integral of `f(z)` around the circle is strictly less than `2πRC`. For this theorem to hold, `f` must be a function from complex numbers to a normed additive commutative group `E` that also forms a normed space over the complex numbers.
More concisely: If `f: ℂ → E` is a continuous, norm-preserving function on a circle in the complex plane of radius `R` centered at `c`, with `∥f(z)∥ ≤ C` for all `z` on the circle and `∥f(z0)∥ < C` for some `z0`, then `∥∫(dz) f(z)∥ < 2πRC`.
|
circleIntegral.integral_eq_zero_of_hasDerivWithinAt'
theorem circleIntegral.integral_eq_zero_of_hasDerivWithinAt' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {f f' : ℂ → E}
{c : ℂ} {R : ℝ},
(∀ z ∈ Metric.sphere c |R|, HasDerivWithinAt f (f' z) (Metric.sphere c |R|) z) →
(∮ (z : ℂ) in C(c, R), f' z) = 0
This theorem states that if `f' : ℂ → E` is the derivative of a complex differentiable function `f` on a circle described by `Metric.sphere c |R|`, where `c` is the center of the circle and `|R|` is the radius, then the complex line (circle) integral of `f'` around the circle `C(c, R)` equals zero. The circle is understood in the complex plane. This holds for any normed additive commutative group `E` that is a complete normed space over the complex numbers. The condition on the derivative is that for every point `z` on the circle, `f` has a derivative `f'(z)` at `z` within the circle.
More concisely: If `f : ℂ → E` is complex differentiable on a circle `C(c, R)` in the complex plane, where `c` is the center and `R` is the radius, then the complex line integral of `f'` around `C(c, R)` equals zero in any complete normed space `E` over the complex numbers.
|
circleMap_mem_sphere
theorem circleMap_mem_sphere : ∀ (c : ℂ) {R : ℝ}, 0 ≤ R → ∀ (θ : ℝ), circleMap c R θ ∈ Metric.sphere c R
The theorem `circleMap_mem_sphere` states that for any complex number `c`, any real number `R` that is greater than or equal to zero, and any real number `θ`, the result of the `circleMap` with parameters `c`, `R`, and `θ` is an element of the sphere with center `c` and radius `R`. In other words, the complex number generated by the exponential map (where `c` is the center and `R` is the radius of the circle) is always on the sphere centered at `c` with radius equal to `R` in the complex plane.
More concisely: For any complex number `c`, real number `R` ≥ 0, and real angle `θ`, the output of the `circleMap` function with parameters `c`, `R`, and `θ` is an element of the complex sphere with center `c` and radius `R`.
|
continuous_circleMap
theorem continuous_circleMap : ∀ (c : ℂ) (R : ℝ), Continuous (circleMap c R)
The theorem `continuous_circleMap` states that for any given complex number `c` and real number `R`, the function `circleMap` with fixed parameters `c` and `R` is continuous. In mathematical terms, this means that for every complex number `c` and real number `R`, the exponential map `θ ↦ c + Re^{θi}`, which maps a real number `θ` to a point on the circle in the complex plane with center `c` and radius `|R|`, is a continuous function.
More concisely: The exponential map `θ ↦ c + Re^(θi)` is a continuous function from the real numbers to the complex plane for any complex number `c` and real number `R`.
|
CircleIntegrable.out
theorem CircleIntegrable.out :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ} [inst_1 : NormedSpace ℂ E],
CircleIntegrable f c R →
IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) MeasureTheory.volume 0
(2 * Real.pi)
This theorem states that for any function `f` from complex numbers to a normed addition group `E`, given a complex number `c` and a real number `R`, if `f` is circle integrable - which means that it can be integrated over a circle in the complex plane with center `c` and radius `R` - then the function that we actually integrate over the interval `[0, 2π]` in the definition of `circleIntegral` is interval integrable. Specifically, this function is the derivative of the `circleMap` (which maps a given angle to a point on the circle) at each angle `θ`, scaled by the function `f` evaluated at the point on the circle corresponding to `θ`. Here, "interval integrable" means that this function is integrable over the intervals `(0, 2π]` and `(2π, 0]` with respect to the Lebesgue measure, where the latter interval is always empty, so it's equivalent to being integrable over `(0, 2π]`.
More concisely: If a complex-valued function `f` is circle integrable over a circle in the complex plane with center `c` and radius `R`, then the derivative of the `circleMap` scaled by `f` is interval integrable over `[0, 2π]` with respect to the Lebesgue measure.
|
deriv_circleMap
theorem deriv_circleMap : ∀ (c : ℂ) (R θ : ℝ), deriv (circleMap c R) θ = circleMap 0 R θ * Complex.I
This theorem states that for any complex number `c` and real numbers `R` and `θ`, the derivative of the circle map function at `θ` is equal to the result of the circle map function evaluated at `0`, `R` and `θ` multiplied by the imaginary unit. The `circleMap` function here represents the exponential map that maps `θ` to `c + Re^{θi}`. The output of this function is a point on the complex plane forming a circle around `c` with radius `|R|`. The theorem essentially describes how changes in `θ` affect the point on the circle.
More concisely: The derivative of the complex exponential function (circle map) at a real angle `θ` is equal to `R * i` times the result of the function evaluated at `θ`, where `c` is the center of the circle and `R` is the radius.
|