Complex.circleIntegral_eq_of_differentiable_on_annulus_off_countable
theorem Complex.circleIntegral_eq_of_differentiable_on_annulus_off_countable :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {c : ℂ}
{r R : ℝ},
0 < r →
r ≤ R →
∀ {f : ℂ → E} {s : Set ℂ},
s.Countable →
ContinuousOn f (Metric.closedBall c R \ Metric.ball c r) →
(∀ z ∈ (Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt ℂ f z) →
(∮ (z : ℂ) in C(c, R), f z) = ∮ (z : ℂ) in C(c, r), f z
The **Cauchy-Goursat theorem** for an annulus states that if a function `f : ℂ → E` is continuous on a closed annulus defined by `r ≤ ‖z - c‖ ≤ R`, where `0 < r ≤ R`, and the function is complex differentiable at all points within this annulus except for a countable number of points, then the integrals of `f` over two circles, with radii `r` and `R` respectively and centered at `c`, are equal. In other words, the line integral of `f` along these two circles give the same value.
More concisely: If a complex-differentiable function `f : ℂ → E` on the closed annulus `{z : ℂ | r ≤ ‖z - c‖ ≤ R}` has a countable number of exceptions, then the integrals of `f` over the circles centered at `c` with radii `r` and `R` are equal.
|
Differentiable.contDiff
theorem Differentiable.contDiff :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {f : ℂ → E},
Differentiable ℂ f → ∀ {n : ℕ∞}, ContDiff ℂ n f
The theorem `Differentiable.contDiff` states that for any complex-valued function `f` that maps from the field of complex numbers `ℂ` to a normed additive commutative group `E` (which is also a normed space over `ℂ` and a complete space), if `f` is differentiable at every point (as defined by `Differentiable ℂ f`), then `f` is continuously differentiable at every point for any natural number `n` or infinity (`ℕ∞`). In other words, a function that is differentiable everywhere in the complex plane is also continuously differentiable everywhere.
More concisely: If `f` is a complex-valued function differentiable at every point in the complex numbers `ℂ`, then `f` is continuously differentiable at every point.
|
Differentiable.hasFPowerSeriesOnBall
theorem Differentiable.hasFPowerSeriesOnBall :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {f : ℂ → E},
Differentiable ℂ f → ∀ (z : ℂ) {R : NNReal}, 0 < R → HasFPowerSeriesOnBall f (cauchyPowerSeries f z ↑R) z ⊤
The theorem `Differentiable.hasFPowerSeriesOnBall` states that for any complex-valued function `f` that is differentiable everywhere, for any complex number `z` and for any non-negative real number `R` where `R` is greater than zero, there exists a power series `cauchyPowerSeries f z ↑R` centered at `z` that represents `f` on the entire complex plane, regardless of the value of `R`. This theorem essentially shows that differentiable complex functions can be represented as a power series.
More concisely: For any complex-valued differentiable function `f` and complex number `z` with non-negative real `R` > 0, there exists a power series `cauchyPowerSeries f z R` that represents `f` on the entire complex plane.
|
Complex.integral_boundary_rect_eq_zero_of_differentiableOn
theorem Complex.integral_boundary_rect_eq_zero_of_differentiableOn :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] (f : ℂ → E)
(z w : ℂ),
DifferentiableOn ℂ f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
0
The **Cauchy-Goursat theorem** for a rectangle states that the integral of a complex differentiable function over the boundary of a rectangle equals zero. More specifically, if we have a function `f` that is complex differentiable on a closed rectangle defined by complex numbers `z` and `w`, the integral of `f` over the boundary of this rectangle equals zero. The boundary integral is computed as the sum of four integrals, each corresponding to one side of the rectangle, with the sides parallel to the imaginary axis being multiplied by the imaginary unit `Complex.I`.
More concisely: The Cauchy-Goursat theorem asserts that the integral of a complex differentiable function over the boundary of a rectangle equals zero.
|
Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
theorem Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : ℝ} {c w : ℂ}
{f : ℂ → E} {s : Set ℂ},
s.Countable →
w ∈ Metric.ball c R →
ContinuousOn f (Metric.closedBall c R) →
(∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x) →
((2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
The **Cauchy integral formula** theorem states that if we have a complex-valued function `f` that is continuous on a closed disc of radius `R` centered at a complex number `c`, and is differentiable at all but countably many points within the interior of this disc, then for any complex number `w` in the interior of this disc, the integral around the circle of radius `R` centered at `c` of `(z-w)^{-1}f(z)` multiplied by `1/(2πi)` is equal to `f(w)`. The set `s` in the statement is the set of exceptions where `f` might not be differentiable.
More concisely: For complex-valued functions `f` continuous on a closed disc and differentiable at all but countably many points in its interior, the integral of `(z-w)^{-1}f(z)` over the circle of radius `R` centered at `c` equals `f(w) / (2πi)`.
|
Complex.integral_boundary_rect_of_differentiableOn_real
theorem Complex.integral_boundary_rect_of_differentiableOn_real :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] (f : ℂ → E)
(z w : ℂ),
DifferentiableOn ℝ f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
MeasureTheory.IntegrableOn (fun z => Complex.I • (fderiv ℝ f z) 1 - (fderiv ℝ f z) Complex.I)
(Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) MeasureTheory.volume →
(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) -
∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
∫ (x : ℝ) in z.re..w.re,
∫ (y : ℝ) in z.im..w.im,
Complex.I • (fderiv ℝ f (↑x + ↑y * Complex.I)) 1 - (fderiv ℝ f (↑x + ↑y * Complex.I)) Complex.I
This theorem states that if we have a complex-valued function `f` that is real differentiable on a closed rectangle defined by the complex numbers `z` and `w`, and if the derivative of `f` with respect to the conjugate of `z` is integrable over this rectangle, then the integral of `f` over the boundary of the rectangle equals the integral of `(2i * derivative of f with respect to the conjugate of z) = (i * derivative of f with respect to x) - (derivative of f with respect to y)` over the rectangle. In the statement of the theorem, `fderiv ℝ f z` represents the derivative of `f` at point `z`, `Complex.I` is the imaginary unit, and `∫` represents the integral over the specified range.
More concisely: If a complex-valued function `f` is real differentiable on a closed rectangle and its derivative with respect to the conjugate is integrable, then the integral of `f` over the rectangle's boundary equals the integral of `(2i * (∂f/∂ conj(z))` ) over the rectangle, where `i` is the imaginary unit and `z` is a point in the rectangle.
|
Complex.circleIntegral_div_sub_of_differentiable_on_off_countable
theorem Complex.circleIntegral_div_sub_of_differentiable_on_off_countable :
∀ {R : ℝ} {c w : ℂ} {s : Set ℂ},
s.Countable →
w ∈ Metric.ball c R →
∀ {f : ℂ → ℂ},
ContinuousOn f (Metric.closedBall c R) →
(∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) →
(∮ (z : ℂ) in C(c, R), f z / (z - w)) = 2 * ↑Real.pi * Complex.I * f w
This is the **Cauchy integral formula**: Given a complex-valued function `f`, a set `s` of complex numbers, and complex numbers `c`, `w`, as well as a real number `R`, if `s` is countable, `w` is in the open disk of radius `R` centered at `c`, `f` is continuous on the closed disk of radius `R` centered at `c`, and `f` is differentiable at all points in the open disk of radius `R` centered at `c` except possibly for those in `s`, then the contour integral of `f(z)/(z-w)` over the circle of radius `R` centered at `c`, equals `2 * π * i * f(w)`, where `π` is the mathematical constant Pi and `i` is the imaginary unit. The contour integral is denoted by `∮ (z : ℂ) in C(c, R), f z / (z - w)`. This theorem is a central result in complex analysis, relating the values of a complex function inside a disk to the values on the boundary.
More concisely: If a complex-valued function `f` is continuous on the closed disk of radius `R` centered at `c`, differentiable on the open disk except for at most countable points, then `∮ (z : ℂ) in C(c, R), f z / (z - w) = 2 * π * i * f(w)`, where `w` is in the open disk and `i` is the imaginary unit.
|
Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable
theorem Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {c : ℂ}
{r R : ℝ},
0 < r →
r ≤ R →
∀ {f : ℂ → E} {s : Set ℂ},
s.Countable →
ContinuousOn f (Metric.closedBall c R \ Metric.ball c r) →
(∀ z ∈ (Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt ℂ f z) →
(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z
The theorem `Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable` states that given a complex-valued function `f` which is continuous on a closed annulus defined by `r ≤ ‖z - c‖ ≤ R` (where `0 < r ≤ R`), and is differentiable at all but countably many points in its interior, the integrals of `f z / (z - c)` over the circles determined by `‖z - c‖ = r` and `‖z - c‖ = R` are equal. The theorem requires that the points where `f` is not differentiable form a countable set. The continuous function `f` maps from the complex numbers to a complete normed space `E`. The integral is taken over the function `(z - c)⁻¹ • f z`, where `•` denotes scalar multiplication.
More concisely: Given a complex-valued function `f` continuous on the annulus `{z : ∣∣z - c∣∣ ≤ R and ∣∣z - c∣∣ ≥ r}` with a countable set of non-differentiable points in its interior, the integral of `(z - c)⁻¹ • f z` over the circles `{z : ∣∣z - c∣∣ = r}` and `{z : ∣∣z - c∣∣ = R}` are equal.
|
DifferentiableOn.circleIntegral_sub_inv_smul
theorem DifferentiableOn.circleIntegral_sub_inv_smul :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : ℝ} {c w : ℂ}
{f : ℂ → E},
DifferentiableOn ℂ f (Metric.closedBall c R) →
w ∈ Metric.ball c R → (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑Real.pi * Complex.I) • f w
The theorem is stating the **Cauchy integral formula** in the field of complex analysis. According to the theorem, let `f` be a complex function mapping from complex numbers to a complete normed add commutative group `E`. If `f` is complex differentiable on a closed disc with center `c` and radius `R` (defined as `Metric.closedBall c R`), then for any complex number `w` in the interior of this disc (defined as `Metric.ball c R`), the line integral of `(z-w)⁻¹ • f z` along the boundary of the disc (`C(c, R)`) is equal to `2 * π * i * f(w)`, where `π` is the mathematical constant Pi, `i` is the imaginary unit, and `•` indicates scalar multiplication.
More concisely: If a complex function `f` is complex differentiable on the closed disc with center `c` and radius `R`, then for `w` in the disc's interior, the line integral of `(z-w)⁻¹ • f z` around the boundary equals `2πi * f(w)`.
|
DifferentiableOn.contDiffOn
theorem DifferentiableOn.contDiffOn :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {s : Set ℂ}
{f : ℂ → E} {n : ℕ}, DifferentiableOn ℂ f s → IsOpen s → ContDiffOn ℂ (↑n) f s
The theorem `DifferentiableOn.contDiffOn` states that if a function `f` from the complex numbers to a normed additive commutative group `E` is complex differentiable on some open set `s`, then it is continuously differentiable on `s`. Here, `E` is a complete normed space over the complex numbers, and the degree of continuous differentiability is represented by a natural number `n`. The open set `s` is defined in the topological space of complex numbers. The condition of the set being open is crucial for this theorem.
More concisely: If a complex-valued function `f` is complex differentiable on an open set `s` in the complex numbers, then it is continuously differentiable on `s`.
|
DifferentiableOn.analyticAt
theorem DifferentiableOn.analyticAt :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {s : Set ℂ}
{f : ℂ → E} {z : ℂ}, DifferentiableOn ℂ f s → s ∈ nhds z → AnalyticAt ℂ f z
The theorem `DifferentiableOn.analyticAt` states that if a function `f` from the complex numbers to a certain type `E`, which forms a complete normed add commutative group and normed space over the complex numbers, is complex differentiable on a set `s`, then it is analytic at any point `z` such that `s` is in the neighborhood of `z`. Equivalently, it says that if `f` is complex differentiable on `s`, then `f` is analytic at any point `z` lying in the interior of `s`. Being analytic at `z` means that the function `f` admits a power series expansion that converges to `f` in a neighborhood of `z`.
More concisely: If a complex-valued function `f` is complex differentiable on a complex open set `s`, then it is analytic at every point `z` in the interior of `s`.
|
Complex.integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn
theorem Complex.integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] (f : ℂ → E)
(z w : ℂ),
ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
DifferentiableOn ℂ f (Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im)) →
(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) -
∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
0
The Cauchy-Goursat theorem for a rectangle states that the integral of a complex differentiable function over the boundary of a rectangle equals zero. In more technical terms, if we have a function `f` from complex numbers to some vector space `E` that is continuous on a closed rectangle, and complex differentiable on the open rectangle formed by the same two points, then the sum of four integrals along the boundary of the rectangle equals zero. These four integrals correspond to integrating `f` over each of the four sides of the rectangle.
More concisely: If a complex differentiable function on an open rectangle is continuous on the closed rectangle, then the integral of the function over the boundary of the rectangle equals zero.
|
Differentiable.analyticAt
theorem Differentiable.analyticAt :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {f : ℂ → E},
Differentiable ℂ f → ∀ (z : ℂ), AnalyticAt ℂ f z
The theorem `Differentiable.analyticAt` states that for any complex differentiable function `f` mapping from the complex numbers `ℂ` to a normed additive commutative group `E` (which is also a complex normed space and a complete space), the function `f` is analytic at every point in its domain. In simpler terms, it asserts that any function that is differentiable when viewed as a function over complex numbers is also analytic at every point, meaning it can be expressed as a convergent power series around each point.
More concisely: A complex differentiable function from the complex numbers to a complex normed space is analytic at every point in its domain.
|
DiffContOnCl.hasFPowerSeriesOnBall
theorem DiffContOnCl.hasFPowerSeriesOnBall :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : NNReal}
{c : ℂ} {f : ℂ → E},
DiffContOnCl ℂ f (Metric.ball c ↑R) → 0 < R → HasFPowerSeriesOnBall f (cauchyPowerSeries f c ↑R) c ↑R
The theorem `DiffContOnCl.hasFPowerSeriesOnBall` states that if we have a function `f` that maps from the set of complex numbers to a normed add-commutative group `E` that also is a normed space over the complex numbers and is a complete space. If this function `f` is complex differentiable on an open disc of positive radius and is continuous on the boundary of this disc, then the function is analytic on the open disc. Here, the open disc is defined as a set of all points with distance from the center `c` less than the radius `R`. Also, the coefficients of the power series that represents the function `f` on this open disc are given by the Cauchy integral formulas.
More concisely: If a complex differentiable and continuous function `f : ℂ → E` on the open disc `{z ∈ ℂ : |z - c| < R}` in a complete, normed space `E` over the complex numbers has coefficients for its power series given by Cauchy integral formulas, then `f` is analytic on the open disc.
|
Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
theorem Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : ℝ} {c w : ℂ}
{f : ℂ → E} {s : Set ℂ},
s.Countable →
w ∈ Metric.ball c R →
ContinuousOn f (Metric.closedBall c R) →
(∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x) →
(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑Real.pi * Complex.I) • f w
This is the **Cauchy Integral Formula**: Given a complex function `f` that is continuous on a closed disc of radius `R` and is complex differentiable at all but countably many points in the interior of this disc, for any point `w` within this disc, the line integral of `(z-w)^{-1}f(z)` along the boundary of the disc equals `2πi f(w)`.
More specifically, for a complex valued function `f`, a complex number `c` representing the center of the disc, a real number `R` representing the radius of the disc, a complex number `w` within the open disc, and a set `s` of countably many points in the open disc where `f` might not be differentiable, if `f` is continuous on the closed disc and differentiable at all points in the open disc not in `s`, then the integral of `(z-w)^{-1}f(z)` along the circle of radius `R` centered at `c` equals `2πi f(w)`.
More concisely: If a complex function `f` is continuous on a disc's closure and complex differentiable at all but countably many points in its interior, then the line integral of `(z-w)^{-1}f(z)` around the disc's boundary equals `2πi f(w)`.
|
Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable
theorem Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : NNReal}
{c : ℂ} {f : ℂ → E} {s : Set ℂ},
s.Countable →
ContinuousOn f (Metric.closedBall c ↑R) →
(∀ z ∈ Metric.ball c ↑R \ s, DifferentiableAt ℂ f z) →
0 < R → HasFPowerSeriesOnBall f (cauchyPowerSeries f c ↑R) c ↑R
The theorem `Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable` states that if we have a function `f` that maps complex numbers to a complete normed space `E`, and this function is continuous on a closed ball (the set of all points at a distance less than or equal to a given positive radius `R` from a central point `c`), and differentiable at every point in the open ball (the set of all points at a distance strictly less than `R` from `c`) except for a countable set `s`, then `f` is analytic on the open ball. This means it can be represented by a power series, where the coefficients of the power series are given by the Cauchy integral formulas.
In other words, under these conditions, the function `f` behaves locally like a power series, which is a fundamental feature of analytic functions. Analyticity is a stronger property than differentiability and implies that the function is infinitely differentiable and equal to its Taylor series.
More concisely: If a continuous function `f : Complex → E` on the closed ball centered at `c` with radius `R` is differentiable on the open ball except for a countable set of points, then `f` is analytic on the open ball.
|
Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux
theorem Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : ℝ} {c w : ℂ}
{f : ℂ → E} {s : Set ℂ},
s.Countable →
w ∈ Metric.ball c R \ s →
ContinuousOn f (Metric.closedBall c R) →
(∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x) →
(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑Real.pi * Complex.I) • f w
This theorem states that for a complex function `f` that is continuous on a closed ball and differentiable in the open ball, where both balls are centered at `c` with radius `R`, and excluding a countable set `s` that does not contain a complex number `w`, the line integral of the function `f` multiplied by the inverse of `(z - w)`, around the circumference of the circle `C(c, R)`, is equal to `2πi` times `f(w)`. This theorem assumes `w` does not belong to the set `s`, while the main theorem associated with this auxiliary lemma relaxes this assumption.
More concisely: For a complex function `f` that is continuous on the closed ball `C(c, R)` and differentiable on the open ball `int(C(c, R))`, excluding a countable set `s`, the line integral of `f(z) * (1 / (z - w)) dz` over `C(c, R)`, where `w ∈ ℂ \ s`, is equal to `2πi * f(w)`.
|
DiffContOnCl.circleIntegral_sub_inv_smul
theorem DiffContOnCl.circleIntegral_sub_inv_smul :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : ℝ} {c w : ℂ}
{f : ℂ → E},
DiffContOnCl ℂ f (Metric.ball c R) →
w ∈ Metric.ball c R → (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑Real.pi * Complex.I) • f w
This Lean theorem states the **Cauchy integral formula**. Given a function `f` from the complex numbers to a normed and complete additive commutative group `E`, if `f` is differentiable and continuous within an open disc (defined by metric ball `Metric.ball c R` with center `c` and radius `R`) and its closure, then for any complex number `w` within this same open disc, the line integral around the circle `C(c, R)` of the function `(z - w)⁻¹` multiplied by `f(z)` with respect to `z` equals `2πi` multiplied by `f(w)`. Here, `2πi` is represented as `2 * ↑Real.pi * Complex.I` in Lean 4, where `Real.pi` represents the mathematical constant π and `Complex.I` represents the imaginary unit i.
More concisely: If a function `f` is differentiable and continuous within the open disc and its closure, then the line integral of `(z - w)⁻¹ * f(z)` around the circle `C(c, R)` equals `2πi * f(w)`.
|
DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul
theorem DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : ℝ} {c w : ℂ}
{f : ℂ → E},
DiffContOnCl ℂ f (Metric.ball c R) →
w ∈ Metric.ball c R → ((2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
This theorem is a statement of the **Cauchy integral formula** in the context of complex analysis. It states that if we have a function `f`, which maps from the complex numbers to a specific type `E` where `E` is a complete normed vector space over the complex numbers, then under certain conditions, the value of `f` at any point `w` inside a given disc is equal to a certain complex contour integral around the boundary of that disc. The conditions are that `f` should be continuously differentiable within the open disc and continuous on its closure. The disc is defined by a center `c` and radius `R`. The contour integral is scaled by the inverse of `2πi` (where `i` is the imaginary unit and `π` is the mathematical constant pi), and it involves the integrand `(z - w)⁻¹ • f z`, where `z` traces out the boundary of the disc, `w` is the point inside the disc, and `•` denotes scalar multiplication.
More concisely: If `f` is a continuously differentiable complex-valued function on an open disc in the complex plane and is continuous on its closure, then for any point `w` inside the disc, `f(w)` equals the value of the contour integral of `(z - w)⁻¹ • f(z)` over the boundary of the disc, scaled by `1 / (2πi)`.
|
DifferentiableOn.hasFPowerSeriesOnBall
theorem DifferentiableOn.hasFPowerSeriesOnBall :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : NNReal}
{c : ℂ} {f : ℂ → E},
DifferentiableOn ℂ f (Metric.closedBall c ↑R) → 0 < R → HasFPowerSeriesOnBall f (cauchyPowerSeries f c ↑R) c ↑R
This theorem states that if a function `f` from the complex numbers to a normed additive commutative group `E`, which is a complete space, is differentiable on a closed disc (which in the metric space of complex numbers is the set of all points at a distance less than or equal to a certain number `R` from a fixed complex number `c`), then `f` is also analytic on the corresponding open disc. Here, to be analytic means that `f` is represented by a power series. Furthermore, the coefficients of this power series are given by the Cauchy integral formulas. The theorem requires that the radius `R` of the disc is positive. There is a related theorem with weaker assumptions: `Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable`.
More concisely: If a complex function `f` is differentiable on the closed disc of radius `R` centered at `c`, then `f` has a power series representation and is analytic on the open disc of radius `R` around `c`.
|
Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto
theorem Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {c : ℂ} {R : ℝ},
0 < R →
∀ {f : ℂ → E} {y : E} {s : Set ℂ},
s.Countable →
ContinuousOn f (Metric.closedBall c R \ {c}) →
(∀ z ∈ (Metric.ball c R \ {c}) \ s, DifferentiableAt ℂ f z) →
Filter.Tendsto f (nhdsWithin c {c}ᶜ) (nhds y) →
(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑Real.pi * Complex.I) • y
The **Cauchy Integral Formula** for the value at the center of a disc is described by this theorem. Given a punctured closed disc of radius `R` with center at a complex number `c`, suppose `f` is a complex-valued function that is continuous on the disc (excluding the center), differentiable at all but countably many points in the interior of this disc, and has a limit `y` at the center of the disc. Then, the complex line integral of `f(z)/(z-c)` over the boundary of the disc (where `z` is a complex number on the boundary) is equal to `2πiy`. This essentially says that the value of this complex line integral only depends on the behavior of the function near the center of the disc, and not on its behavior elsewhere.
More concisely: The Cauchy Integral Formula asserts that the complex line integral of a differentiable function, except at countably many points, over the boundary of a punctured closed disc equals `2πi` times the value of the function at the disc's center.
|
Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable
theorem Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : ℝ},
0 < R →
∀ {f : ℂ → E} {c : ℂ} {s : Set ℂ},
s.Countable →
ContinuousOn f (Metric.closedBall c R) →
(∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) →
(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑Real.pi * Complex.I) • f c
This theorem is known as the **Cauchy integral formula** for the value at the center of a disc. It states that if we have a function `f : ℂ → E`, which is continuous on a closed disc of radius `R`, and is complex differentiable at all but countably many points of the interior of this disc, then the line integral around the boundary of the disc, where the integrand is the function `f(z)` divided by `z-c` (where `c` is the center of the disc), is equal to `2πiy`, where `y` is the value of `f` at the center of the disc. In other words, the value of the function at the center of the disc can be computed from its values on the boundary of the disc. This theorem is a fundamental result in complex analysis.
More concisely: If a complex function `f : ℂ → E` is continuous on a disc's closure and complex differentiable at all but countably many of its interior points, then `∫ₕₖ f(z)/(z-c) dz = 2πiy`, where `c` is the disc's center, implies `f(c) = y`.
|
Complex.circleIntegral_eq_zero_of_differentiable_on_off_countable
theorem Complex.circleIntegral_eq_zero_of_differentiable_on_off_countable :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] {R : ℝ},
0 ≤ R →
∀ {f : ℂ → E} {c : ℂ} {s : Set ℂ},
s.Countable →
ContinuousOn f (Metric.closedBall c R) →
(∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) → (∮ (z : ℂ) in C(c, R), f z) = 0
The **Cauchy-Goursat theorem** for a disk states the following: given a continuous function `f` from complex numbers to a normed additive commutative group `E`, a complex number `c`, a radius `R` (where `R` is greater than or equal to zero), and a countable set `s` of complex numbers, if `f` is continuous on the closed disk `{z | ‖z - c‖ ≤ R}` and is differentiable at all points in the open disk `{z | ‖z - c‖ < R}` except for those in the set `s`, then the complex line integral of `f` over the circle with center `c` and radius `R` is equal to zero. This is represented mathematically as $\oint_{|z-c|=R}f(z)\,dz = 0$.
More concisely: If a continuous complex-valued function `f` is differentiable at all points in the open disk excluding a countable set, then its complex line integral over the boundary of that disk is zero.
|
Complex.integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real
theorem Complex.integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] (f : ℂ → E)
(f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ),
ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
(∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im),
HasFDerivAt f (f' x) x) →
MeasureTheory.IntegrableOn (fun z => Complex.I • (f' z) 1 - (f' z) Complex.I)
(Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) MeasureTheory.volume →
(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) -
∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
∫ (x : ℝ) in z.re..w.re,
∫ (y : ℝ) in z.im..w.im,
Complex.I • (f' (↑x + ↑y * Complex.I)) 1 - (f' (↑x + ↑y * Complex.I)) Complex.I
This theorem states that if we have a function `f` from the complex numbers to a complete normed space `E`, which is continuous on a closed rectangle defined by the complex numbers `z` and `w`, and is real differentiable on the corresponding open rectangle. Also, the derivative of `f` with respect to the conjugate of `z` is integrable on this rectangle. Then, the integral of `f` over the boundary of the rectangle is equal to the integral of the expression `2i * derivative of f with respect to conjugate of z` which can also be written as `i * derivative of f with respect to x - derivative of f with respect to y` over the rectangle. This theorem is a complex analysis result analogous to the Green's theorem in real analysis.
More concisely: If a complex-valued function `f` is continuous on a closed rectangle, real differentiable on the interior, and has integrable derivative with respect to the conjugate variable, then the integral of `f` over the rectangle's boundary equals the integral of `2i * df/d(conj(z))` over the rectangle.
|
Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable
theorem Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : CompleteSpace E] (f : ℂ → E)
(z w : ℂ) (s : Set ℂ),
s.Countable →
ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
(∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ s,
DifferentiableAt ℂ f x) →
(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) -
∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
0
This theorem is the Cauchy-Goursat theorem for a rectangle. It states that for a function `f` mapping complex numbers to an element of a complete normed additive commutative group `E`, if `f` is continuous on a closed rectangle defined by complex points `z` and `w` and differentiable at all but a countable number of points on the corresponding open rectangle (excluding a set `s`), then the integral of `f` around the boundary of the rectangle equals zero. The boundary integral is computed as the sum and difference of integrals over the real intervals from `z.re` to `w.re` and `z.im` to `w.im` with appropriate complex shifts and scaling by the imaginary unit `Complex.I`.
More concisely: If a complex-valued function `f` is continuous on the closure and differentiable at all but a countable number of points in the open rectangle defined by `z` and `w`, then the integral of `f` around the boundary of the rectangle is zero.
|