Complex Integral of 1/z round the unit circle

Stream: Is there code for X?

[Kevin Buzzard]

I am giving a talk to Olympiad level schoolkids tomorrow and during it I would like to state in Lean the theorem that the integral $\int_{S^1}1/z=2\pi i$

[Kevin Buzzard]

Can we do this on some compiling commit of mathlib?

[Kevin Buzzard]

I don't need a proof but ideally I'd like to be able to present a term which contains as few symbols as possible other than the essential maths ones

[Mario Carneiro]

Are you okay with a parameterized curve?

[Kevin Buzzard]

I'm completely happy with def S\^1 : complex_path := <unreadable_thing>

[Kevin Buzzard]

I think a parameterised curve is fine

[Mario Carneiro]

I was thinking more along the lines of $\int_0^{2\pi}1/(e^{it})\frac{de^{it}}{dt}dt=2\pi i$

[Kevin Buzzard]

Anything which I can explain to a mathematician without having to go "enat: well ok there's thing called roption which is computer science"

[Mario Carneiro]

that might be halfway to solving the problem though

[Kevin Buzzard]

That would be a good start

[Kevin Buzzard]

Can we integrate complex-valued functions on $\R$?

[Mario Carneiro]

yeah

[Mario Carneiro]

bochner baby

[Mario Carneiro]

the domain can be any measurable space although it's specialized to $\Bbb R$, and the codomain can be any complete vector space including $\Bbb C$

[Mario Carneiro]

given what we know about derivatives, I think you could even do a proof of the theorem in your talk

[Mario Carneiro]

but stating it in terms of a contour integral is out of reach at the moment, unless you define a parameterized contour integral on the spot just so the statement looks nice

[Kevin Buzzard]

So is complex_integral (F : Icc 0 1 \to_<whatever> \C) : \C := ... accessible? Do we have the correct bundled morphism?

[Kevin Buzzard]

`(0 : \R) if you really must, but everyone knows the default Icc is $\R$.

[Kevin Buzzard]

I have learnt to live without the square bracket notation but we could define S^1 to be this

[Kevin Buzzard]

Why not? It's a model

[Kevin Buzzard]

It could be Carneiro's $S^1$ -- a convenient model.

[Kevin Buzzard]

You can create an instance of topological space later

[Mario Carneiro]

I managed this much:

import measure_theory.interval_integral

open_locale classical real
noncomputable theory

open set complex

def complex_path := { γ : ℝ → ℂ // differentiable ℝ γ }

instance : has_coe_to_fun complex_path := ⟨_, λ γ, γ.1⟩

lemma S1_deriv (t : ℝ) :
  has_deriv_at
    (λ x:ℝ, exp (2 * π * I * x))
    (2 * π * I * exp (2 * π * I * t)) t :=
sorry

def S1 : complex_path := ⟨λ t, exp (2 * π * I * t), λ t, ⟨_, S1_deriv t⟩⟩
notation `S¹` := S1

def contour_integral (γ : complex_path) (f : ℂ → ℂ) : ℂ :=
∫ t in 0..1, f (γ t) * deriv γ t

notation `∮` binders ` in ` γ `, ` f:(scoped:60 f, f) := contour_integral γ f

example : ∮ z in S¹, 1 / z = 2 * π * I :=
show ∫ (t:ℝ) in 0..1, (1 / exp (2 * π * I * t)) * deriv (λ x:ℝ, exp (2 * π * I * x)) t = 2 * π * I,
by simp [λ t, (S1_deriv t).deriv, mul_left_comm, exp_ne_zero]

The sorry looks easy but there is something missing about deriving real derivatives from complex ones

[Heather Macbeth]

Do you need to use a result from analysis.complex.real_deriv? (Just a hunch.)

[Mario Carneiro]

I noticed that file, but it seems to be about restricting the codomain, not the domain

[Mario Carneiro]

actually I take it back, they are doing both at once

[Mario Carneiro]

they are a little overspecific

[Heather Macbeth]

I think what's missing is the deriv (i.e., 1d) version of docs#has_fderiv_at.restrict_scalars.

[Heather Macbeth]

In its absence one has to convert to a multivariate version:

lemma S1_deriv (t : ℝ) :
  has_deriv_at
    (λ x:ℝ, exp (2 * π * I * x))
    (2 * π * I * exp (2 * π * I * t)) t :=
begin
  have h : has_fderiv_at (λ x : ℂ, exp (2 * π * I * x))
    ((2 * ↑π * I * exp (2 * π * I * t)) • continuous_linear_map.id ℂ ℂ) (of_real_clm t),
  { rw has_fderiv_at_iff_has_deriv_at,
    simpa [mul_comm] using ((has_deriv_at_id _).const_mul (2 * ↑π * I : ℂ)).cexp },
  simpa using ((h.restrict_scalars ℝ).comp t of_real_clm.has_fderiv_at).has_deriv_at,
end

[Johan Commelin]

Wow, I didn't expect that all of this would fit in ~ 35 lines!