Source indexedlemma · leanprover/lean4:v4.32.0

cauchy_formula_deriv

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:100 to 120

Source documentation

This upstreamed from https://github.com/math-inc/strongpnt/tree/main

Exact Lean statement

@[blueprint "cauchy_formula_deriv"
  (title := "cauchy-formula-deriv")
  (statement := /--
    Let $f$ be analytic on $|z|\leq R$. For any $z$ with $|z|\leq r$ and any $r'$
    with $0 < r < r' < R$ we have
    $$f'(z)=\frac{1}{2\pi i}\oint_{|w|=r'}\frac{f(w)}{(w-z)^2}\,dw=\frac{1}{2\pi}
    \int_0^{2\pi}\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\,dt.$$
  -/)
  (proof := /--
    This is just Cauchy's integral formula for derivatives.
  -/)
  (latexEnv := "lemma")]
lemma cauchy_formula_deriv {r r' R : ℝ} {f : ℂ → ℂ} {z : ℂ}
    (r_lt_r' : r < r') (r'_lt_R : r' < R)
    (hf_on_ball : DifferentiableOn ℂ f (Metric.ball 0 R))
    (hz : z ∈ Metric.closedBall 0 r) :
    deriv f z = (1 / (2 * Real.pi * I)) • ∮ w in C(0, r'), (w - z)⁻¹ ^ 2 • f w

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint "cauchy_formula_deriv"  (title := "cauchy-formula-deriv")  (statement := /--    Let $f$ be analytic on $|z|\leq R$. For any $z$ with $|z|\leq r$ and any $r'$    with $0 < r < r' < R$ we have    $$f'(z)=\frac{1}{2\pi i}\oint_{|w|=r'}\frac{f(w)}{(w-z)^2}\,dw=\frac{1}{2\pi}    \int_0^{2\pi}\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\,dt.$$  -/)  (proof := /--    This is just Cauchy's integral formula for derivatives.  -/)  (latexEnv := "lemma")]lemma cauchy_formula_deriv {r r' R : ℝ} {f : ℂ → ℂ} {z : ℂ}    (r_lt_r' : r < r') (r'_lt_R : r' < R)    (hf_on_ball : DifferentiableOn ℂ f (Metric.ball 0 R))    (hz : z ∈ Metric.closedBall 0 r) :    deriv f z = (1 / (2 * Real.pi * I)) • ∮ w in C(0, r'), (w - z)⁻¹ ^ 2 • f w := by  have hz_in_ball : z ∈ Metric.ball 0 r' :=    Metric.mem_ball.mpr <| (Metric.mem_closedBall.mp hz).trans_lt r_lt_r'  simp [← Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable      Metric.isOpen_ball (Metric.closedBall_subset_ball r'_lt_R) hf_on_ball hz_in_ball]