# Zulip Chat Archive

## Stream: maths

### Topic: analysis

#### James Palmer (Nov 12 2019 at 18:20):

Hi there, I was wondering if we had a proof formalised in Lean yet that the limit of (sin(x))/x is equal to 1. I looked over Mathlib and couldn't find anything of the sort.

#### Johan Commelin (Nov 12 2019 at 18:20):

I don't think we have. We have very little "concrete" results so far.

#### Johan Commelin (Nov 12 2019 at 18:21):

I also think it might be quite a challenge given current technology. But you might be able to reuse a whole bunch of computations that Chris used for the definition of pi

#### Kevin Buzzard (Nov 12 2019 at 18:23):

This is basically equivalent to proving that the derivative of sin is cos, which in my mind is a key missing thing. What I think we really need is that a power series is differentiable within its radius of convergence.

#### Kevin Buzzard (Nov 12 2019 at 18:30):

At school I was told that we would at some point prove that sin(x)/x tended to 1 as x tended to zero. We then used that fact to deduce that the derivative of sin was cos, and then later on after we'd drawn the graph of sin and had got thoroughly used to the fact that its derivative at 0 was cos(0)=1, the teacher told us that it was now obvious that sin(x)/x tended to 1 because cos(0)=1.

#### Chris Hughes (Nov 12 2019 at 18:39):

I think you actually want this more general result first. https://proofwiki.org/wiki/Derivative_of_Uniformly_Convergent_Series_of_Continuously_Differentiable_Functions

#### Kevin Buzzard (Nov 12 2019 at 23:49):

I've never taught this stuff so the last time I saw a proof of it was 30 years ago and I have no idea where to start.

#### Kevin Buzzard (Nov 12 2019 at 23:50):

You're right that it looks like a nice general statement though. Is it proved in 2nd year analysis at Imperial?

#### Chris Hughes (Nov 12 2019 at 23:53):

I think so.

#### Chris Hughes (Nov 12 2019 at 23:54):

I think there's something more general about sequences.

#### Chris Hughes (Nov 12 2019 at 23:58):

https://proofwiki.org/wiki/Derivative_of_Uniformly_Convergent_Sequence_of_Differentiable_Functions

#### Luca Seemungal (Nov 13 2019 at 08:18):

I guess the road map is to

- Define power series, with ROC, etc
- Define sine as some power series, prove that that power series converges (possibly before defining sine to be that power series)
- Do a similar thing for cosine
- Use the Fréchet derivative in mathlib to ge the univariate derivative.
- Prove some result like what Chris has mentioned about being able to differentiate inside the power series within the ROC or something else about uniform convergence
- Differentiate the sine power series, see that it is equal to the cosine power series
- Try to generalise to the complex numbers (shouldn't be too difficult, just replace a bunch of symbols and then fix things)
- Try to generalise even further to some sufficiently regular algebraic structure

#### Luca Seemungal (Nov 13 2019 at 08:19):

Oh and of course,

- Realise that the initial road map was completely changed after step 1

#### Johan Commelin (Nov 13 2019 at 08:19):

1a is done

#### Johan Commelin (Nov 13 2019 at 08:20):

As in, we have a definition of formal power series in mathlib. But nothing yet about ROC

#### Johan Commelin (Nov 13 2019 at 08:21):

Also, Chris's work on `exp`

, `sin`

and `pi`

was from before the definition of power series. So far these pieces of the library have not been glued together

#### Luca Seemungal (Nov 13 2019 at 08:35):

Oh, ok thanks. We'll have a look these things. Will we have to learn what a filter is?

#### Patrick Massot (Nov 13 2019 at 08:35):

Yes.

#### Johan Commelin (Nov 13 2019 at 08:35):

If you want to do things the mathlib way, then yes

#### Patrick Massot (Nov 13 2019 at 08:35):

If you are interested in anything related to analysis in mathlib you need to learn filters. And you'll be very happy in the end.

#### Luca Seemungal (Nov 13 2019 at 08:37):

Ok, great :joy::joy:

#### Johan Commelin (Nov 13 2019 at 08:39):

@Luca Seemungal Why don't you post your roadmap as an issue in the mathlib github? If you use `[ ]`

then we can even have checkboxes to tick off.

#### Kevin Buzzard (Nov 13 2019 at 08:53):

Yes please do this. If people want to change it later that's fine. I am interested in formalising parts of our undergraduate syllabus and the fact that the derivative of sin is cos is used from day 1 in the "methods" courses (without justification, because everyone was told it in high school and the methods courses continue with this tradition) so this sort of thing is a big roadblock to even beginning to formalise the problem sheets in these courses.

#### Mario Carneiro (Nov 13 2019 at 09:24):

I would suggest focusing on `exp`

for this roadmap. `sin`

and `cos`

should follow as algebraic combinations, not more power series

#### Mario Carneiro (Nov 13 2019 at 09:28):

I've also said this before, but the theory of power series and termwise differentiation is not required for `exp`

; you can take the derivative at zero by some elementary estimates, using the definition of the derivative

#### Mario Carneiro (Nov 13 2019 at 09:29):

Not that it wouldn't be useful to have the analytic theory of power series, but to me it's a high powered tool that isn't needed here

#### Luca Seemungal (Nov 13 2019 at 09:52):

Ah, yes this makes sense. I see that in `data/complex/exponential.lean`

we have that `exp`

is defined as a power series and `sin`

and `cos`

are algebraic combinations of `exp`

as you suggest.

#### Luca Seemungal (Nov 13 2019 at 09:52):

Right, of course - I can just guess the derivative of exp and then show it satisfies the definition of a Fréchet derivative. And I can also do the same with sin! Sorry, I was still in the "analysis 2" mindset where you don't know any multivariate calculus yet; at my university we proved all these derivative theorems by differentiating a power series term by term.

#### Luca Seemungal (Nov 13 2019 at 09:54):

I'll put a theory of power series as a different project some of us at Warwick will want to do after proving that the derivative of sine is cosine

#### Mario Carneiro (Nov 13 2019 at 09:57):

The trick with `exp`

is to prove that `exp' 0 = 1`

, and then `exp' a = (exp (a+x))' (x=0) = (exp a * exp x)' (0) = exp a * exp' 0 = exp a`

#### Mario Carneiro (Nov 13 2019 at 09:58):

in other words, you can exploit `exp (a+x) = exp a * exp x`

and the multiplication rule for differentiation to reduce the problem to calculating the derivative at zero

#### Luca Seemungal (Nov 13 2019 at 10:05):

This also makes sense, thanks!

#### Kevin Buzzard (Nov 13 2019 at 10:10):

But we need the theorem that a power series is differentiable within its radius of convergence to be a respectable maths library.

#### Mario Carneiro (Nov 13 2019 at 10:18):

Of course. But I like to have the developments follow the needs, when possible, and use the simplest tool for the job. In metamath I used a basic tail estimate to find the derivative of exp, and it wasn't until the lagrange formula for pi that I needed the actual theory of power series, to prove that Abel's theorem applies to the power series for the arctangent.

#### Kevin Buzzard (Nov 13 2019 at 10:19):

Then how come we ended up with the Bochner integral before the Riemann integral?

#### Mario Carneiro (Nov 13 2019 at 10:20):

'The job' involves a bunch of things that aren't going to be Riemann integrable

#### Mario Carneiro (Nov 13 2019 at 10:21):

It's possible that some of the power series work can be reused for the proof that exp is differentiable, but I think it is unlikely

#### Mario Carneiro (Nov 13 2019 at 10:22):

the direct elementary proof is pretty simple, it's hard to beat

#### Mario Carneiro (Nov 13 2019 at 10:22):

in order to apply the general theory you still need to know a bunch of things about the ROC that amount to the same tail estimates I'm talking about

#### Kevin Buzzard (Nov 13 2019 at 10:25):

fair do's

#### Mario Carneiro (Nov 13 2019 at 10:25):

To reiterate, I think that the general theory of power series is useful and we should put it on the todo list. But it's not blocking elementary calculus

#### Sebastien Gouezel (Nov 13 2019 at 13:04):

I just wanted to mention that the question whether `deriv ℝ sin = cos`

makes sense in mathlib since 20 minutes (i.e., the moment #1670 was merged). Thanks @Gabriel Ebner !

#### Luca Seemungal (Nov 15 2019 at 10:08):

What are good resources for learning about filters? Are filters "common knowledge" or are they a weird quirk? That is, if I ask one of my analysis professors about filters will they start talking about coffee or analysis?

#### Johan Commelin (Nov 15 2019 at 10:49):

Coffee

#### Johan Commelin (Nov 15 2019 at 10:50):

Filters are treated in Bourbaki. You can also read about them in any treatment on the Stone-Cech compactification, or compactness in model theory.

#### Luca Seemungal (Nov 15 2019 at 10:57):

Ok thanks

#### Mario Carneiro (Nov 15 2019 at 11:10):

Besides the wikipedia page, you can also look at Johannes's paper on filters for formalization of analysis: http://home.in.tum.de/~hoelzl/documents/hoelzl2013typeclasses.pdf

#### Kevin Buzzard (Nov 15 2019 at 14:28):

#### Luca Seemungal (Nov 15 2019 at 17:00):

Cheers!

What is `set.univ`

in the definition of a filter?

structure filter (α : Type*) := (sets : set (set α)) (univ_sets : set.univ ∈ sets) (sets_of_superset {x y} : x ∈ sets → x ⊆ y → y ∈ sets) (inter_sets {x y} : x ∈ sets → y ∈ sets → x ∩ y ∈ sets)

#### Chris Hughes (Nov 15 2019 at 17:07):

The set containing every element of `α`

. In normal maths it is `α`

, but in type theory `α`

is not a set.

#### Luca Seemungal (Nov 15 2019 at 17:26):

If you are interested in anything related to analysis in mathlib you need to learn filters. And you'll be very happy in the end.

wow - can confirm, filters are cool and are making me very happy

#### Yury G. Kudryashov (Nov 17 2019 at 04:37):

@Luca Seemungal @Johan Commelin About power series, `exp`

, `sin`

etc. Would be cool to have one-variable power series in non-commutative settings. I think of the exponent of a linear endomorphism. Though one can play a game like "restrict to the subalgebra generated by `A`

, compute in this subalgebra, come back". Maybe, it's easier.

#### Luca Seemungal (Nov 17 2019 at 09:53):

I don't know much algebra - what's the motivation for this?

#### Luca Seemungal (Nov 17 2019 at 10:02):

Given the spirit of mathlib, power series are probably going to end up being done with as much generality as possible. I don't know whether this includes noncommutative settings.

Currently, however, I personally am still at a fairly early stage; I've yet to fully understand the definition of the derivative because it's so general and it's written in lean.

#### Yury G. Kudryashov (Nov 17 2019 at 17:31):

@Luca Seemungal Then ignore my comment. I'd like to have a proof of $\frac{d}{dt} \exp(At)=\exp(At)$ in Lean for `A`

being a bounded linear endomorphism. This immediately leads to the formula $x(t)=\exp(At)x(0)$ for solutions of a linear ODE $\dot x=Ax$. As I said before, it's possible to work around non-commutativity even if most theorems are stated for commutative algebras.

#### Luca Seemungal (Nov 17 2019 at 19:13):

Sounds interesting. I've no idea :)

#### Luca Seemungal (Nov 22 2019 at 16:35):

what does the `L[𝕜] F`

in `analysis/calculus/fderiv.lean`

mean?

def has_fderiv_at_filter (f : E → F) (f' : E →L[𝕜] F) (x : E) (L : filter E) := is_o (λ x', f x' - f x - f' (x' - x)) (λ x', x' - x) L

#### Reid Barton (Nov 22 2019 at 16:36):

I think `→L[𝕜]`

means a continuous 𝕜-linear map. Jump to definition should help.

#### Luca Seemungal (Nov 22 2019 at 16:42):

Cheers! The thing is though, when I `git clone`

mathlib, and then I open it in vs-code, none of it seems to compile? Do I have to grab some binaries from somewhere? Do I have to just wait?

#### Patrick Massot (Nov 22 2019 at 16:43):

What are you doing? Are you contributing to mathlib or using mathlib?

#### Luca Seemungal (Nov 22 2019 at 16:44):

Contributing / messing about with it to understand it more

#### Patrick Massot (Nov 22 2019 at 16:45):

Ok, then git clone is a good first move. Then you need to checkout the `lean-3.4.2`

branch and call `cache-olean --fetch`

(assuming your installed the supporting tooling as described in mathlib install page).

#### Luca Seemungal (Nov 22 2019 at 16:47):

Thanks! This seems to be working a bit more. I now get errors like

file 'analysis/asymptotics' not found in the LEAN_PATH

#### Patrick Massot (Nov 22 2019 at 16:52):

Where are you seeing this? Did you restart the Lean server after fetching oleans?

#### Luca Seemungal (Nov 22 2019 at 16:56):

yes, I have restarted the lean server. Now I get issues like

could not resolve import: analysis.calculus.fderiv

#### Patrick Massot (Nov 22 2019 at 16:56):

Did you open the mathlib folder in VScode?

#### Patrick Massot (Nov 22 2019 at 16:57):

Or directly a file?

#### Patrick Massot (Nov 22 2019 at 16:57):

Or a subfolder of the mathlib folder?

#### Luca Seemungal (Nov 22 2019 at 16:58):

Ah, yes! I had opened `src`

. Everything is working fine now, thanks!

#### Patrick Massot (Nov 22 2019 at 17:00):

@Gabriel Ebner and @Bryan Gin-ge Chen it seems almost every beginner falls into this trap. Do you think the VScode extension could issue a warning if asked to work outside of a folder containing a leanpkg.path?

#### Bryan Gin-ge Chen (Nov 22 2019 at 18:02):

@Patrick Massot Yes, that's a great idea. The earliest I could look into this is probably next weekend, so if Gabriel or anyone else has some time before then they should go for it.

#### Luca Seemungal (Nov 22 2019 at 18:05):

Would a FAQ page be a good idea?

#### Bryan Gin-ge Chen (Nov 22 2019 at 18:07):

This particular issue with opening the project directory is mentioned in the "project" doc file. But a separate FAQ would probably be a good idea too.

#### Kevin Buzzard (Nov 22 2019 at 19:15):

I've seen students just click on Lean files and open them with VS Code. I would say that pointing people towards cloning Patrick's test repo and using update-mathlib was a better idea than getting them to clone mathlib directly and then have to switch branches before cache-olean works. I think cloning the test repo is the easiest way to get going. See #1728 (ooh, modular form number!)

#### Luca Seemungal (Nov 22 2019 at 19:46):

For me, mathlib defaulted to the lean-4.3.2 branch

#### Mario Carneiro (Nov 22 2019 at 19:49):

wow, that version doesn't even exist yet

#### Luca Seemungal (Nov 22 2019 at 20:16):

Oh, oops - I mean lean-4.2.1, or whatever!

#### Luca Seemungal (Nov 22 2019 at 20:17):

Oh wait

#### Luca Seemungal (Nov 22 2019 at 20:17):

3.4.2?

#### Luca Seemungal (Nov 23 2019 at 21:15):

I have a tactic state

1 goal y c : ℝ, hc : c > 0 ⊢ {x : ℝ | ∥sin x + (-sin y + -((x + -y) * cos y))∥ ≤ c * ∥x + -y∥} ∈ (nhds y).sets

In normal maths I would say

Let x ∈ ℝ such that ∥sin x + (-sin y + -((x + -y) * cos y))∥ ≤ c * ∥x + -y∥

So I feel like `intros x, hx`

should do what I want - but it doesn't work.

How do I deal with sets in lean?

Context below:

import analysis.calculus.deriv import data.complex.exponential open real example (y : ℝ): has_deriv_at sin (cos y) y := begin intro, intro hc, simp, sorry end

#### Sebastien Gouezel (Nov 23 2019 at 21:26):

Just to mention that this fact is proved in #1695, which is currently PRed to mathlib, so no need to work too hard on it. As for your question, you want to show that some set is a neighborhood of `y`

. In maths terms, you need to find some `epsilon`

such that your set contains the open interval `(y - epsilon, y + epsilon)`

, so a math proof would certainly not start with `Let x ∈ ℝ such that ∥sin x + (-sin y + -((x + -y) * cos y))∥ ≤ c * ∥x + -y∥`

. It would start with `let epsilon = c/10`

(or whatever you need). Let me show that, for any `x`

satisfying `|x - y| < epsilon`

, then `∥sin x + (-sin y + -((x + -y) * cos y))∥ ≤ c * ∥x + -y∥`

. The mathlib proof would definitely go this way, using additionally things like `filter.mem_sets_of_superset`

and `mem_nhds_sets`

(that say that a set containing a neighborhood of `y`

is itself a neighborhood of `y`

, and that an open set containing `y`

is a neighborhood of `y`

).

#### Luca Seemungal (Nov 23 2019 at 21:32):

Ah, thanks. I don't really understand what `nhds y`

is yet so I'll have to focus on that.

#### Patrick Massot (Nov 24 2019 at 08:22):

Sébastien's answer is right, but you may still have some difficulties to return to familiar grounds. You could study:

import analysis.calculus.deriv import data.complex.exponential open real open_locale topological_space example (y : ℝ): has_deriv_at sin (cos y) y := begin intro, intro hc, suffices : {x : ℝ | ∥sin x - sin y - (x - y) * cos y∥ ≤ c * ∥x - y∥} ∈ 𝓝 y, by simpa, rw metric.mem_nhds_iff, use [c/10, by linarith], intros x x_in, change abs(sin x - sin y - (x - y) * cos y) ≤ c * abs(x - y), rw [metric.mem_ball, real.dist_eq] at x_in, sorry end

Note how your non-terminal `simp`

with unwanted "simplification" (using the dreaded `sub_eq_add_neg`

) is replaced by something much more controled. The last two lines are controversial, you may be better off with general notions than trying to get down to earth with absolute value, but they illustrate the power of `change`

.

#### Luca Seemungal (Nov 24 2019 at 08:28):

Thanks! This is a helpful example to study

#### Patrick Massot (Nov 24 2019 at 08:29):

I forgot one piece of my message at the end: the last line could be replace by `change abs (x - y) < c / 10 at x_in,`

but I wanted to illustrate explicit rewriting of definitional equality vs `change`

.

#### Bryan Gin-ge Chen (Nov 24 2019 at 15:13):

Do you think the VScode extension could issue a warning if asked to work outside of a folder containing a leanpkg.path?

Gabriel has implemented this feature in the latest release! :tada:

Last updated: May 06 2021 at 19:30 UTC