analysis

Stream: maths

[James Palmer]

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]

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

[Johan Commelin]

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]

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]

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]

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]

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]

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

[Chris Hughes]

I think so.

[Chris Hughes]

I think there's something more general about sequences.

[Chris Hughes]

https://proofwiki.org/wiki/Derivative_of_Uniformly_Convergent_Sequence_of_Differentiable_Functions

[Luca Seemungal]

I guess the road map is to

1. Define power series, with ROC, etc
2. Define sine as some power series, prove that that power series converges (possibly before defining sine to be that power series)
3. Do a similar thing for cosine
4. Use the Fréchet derivative in mathlib to ge the univariate derivative.
5. 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
6. Differentiate the sine power series, see that it is equal to the cosine power series
7. Try to generalise to the complex numbers (shouldn't be too difficult, just replace a bunch of symbols and then fix things)
8. Try to generalise even further to some sufficiently regular algebraic structure

[Luca Seemungal]

Oh and of course,

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

[Johan Commelin]

1a is done

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Patrick Massot]

Yes.

[Johan Commelin]

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

[Patrick Massot]

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]

Ok, great :joy::joy:

[Johan Commelin]

@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]

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]

I would suggest focusing on exp for this roadmap. sin and cos should follow as algebraic combinations, not more power series

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

This also makes sense, thanks!

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

fair do's

[Mario Carneiro]

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]

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]

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]

Coffee

[Johan Commelin]

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]

Ok thanks

[Mario Carneiro]

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]

https://xenaproject.wordpress.com/2018/08/04/what-is-a-filter-how-some-computer-scientists-think-about-limits/

[Luca Seemungal]

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]

The set containing every element of α. In normal maths it is α, but in type theory α is not a set.

[Luca Seemungal]

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]

@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]

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

[Luca Seemungal]

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]

@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]

Sounds interesting. I've no idea :)

[Luca Seemungal]

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]

I think →L[𝕜] means a continuous 𝕜-linear map. Jump to definition should help.

[Luca Seemungal]

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]

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

[Luca Seemungal]

Contributing / messing about with it to understand it more

[Patrick Massot]

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]

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]

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

[Luca Seemungal]

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

could not resolve import: analysis.calculus.fderiv

[Patrick Massot]

Did you open the mathlib folder in VScode?

[Patrick Massot]

Or directly a file?

[Patrick Massot]

Or a subfolder of the mathlib folder?

[Luca Seemungal]

Ah, yes! I had opened src. Everything is working fine now, thanks!

[Patrick Massot]

@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]

@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]

Would a FAQ page be a good idea?

[Bryan Gin-ge Chen]

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]

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]

For me, mathlib defaulted to the lean-4.3.2 branch

[Mario Carneiro]

wow, that version doesn't even exist yet

[Luca Seemungal]

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

[Luca Seemungal]

Oh wait

[Luca Seemungal]

3.4.2?

[Luca Seemungal]

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]

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]

Ah, thanks. I don't really understand what nhds y is yet so I'll have to focus on that.

[Patrick Massot]

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]

Thanks! This is a helpful example to study

[Patrick Massot]

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]

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: