Zulip Chat Archive

Stream: maths

Topic: analysis


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 12 2019 at 18:20):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Nov 12 2019 at 23:53):

I think so.

view this post on Zulip Chris Hughes (Nov 12 2019 at 23:54):

I think there's something more general about sequences.

view this post on Zulip Chris Hughes (Nov 12 2019 at 23:58):

https://proofwiki.org/wiki/Derivative_of_Uniformly_Convergent_Sequence_of_Differentiable_Functions

view this post on Zulip Luca Seemungal (Nov 13 2019 at 08:18):

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

view this post on Zulip Luca Seemungal (Nov 13 2019 at 08:19):

Oh and of course,

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

view this post on Zulip Johan Commelin (Nov 13 2019 at 08:19):

1a is done

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Nov 13 2019 at 08:35):

Yes.

view this post on Zulip Johan Commelin (Nov 13 2019 at 08:35):

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

view this post on Zulip 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.

view this post on Zulip Luca Seemungal (Nov 13 2019 at 08:37):

Ok, great :joy::joy:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Luca Seemungal (Nov 13 2019 at 10:05):

This also makes sense, thanks!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 13 2019 at 10:19):

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

view this post on Zulip Mario Carneiro (Nov 13 2019 at 10:20):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 13 2019 at 10:22):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 13 2019 at 10:25):

fair do's

view this post on Zulip 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

view this post on Zulip 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 !

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Nov 15 2019 at 10:49):

Coffee

view this post on Zulip 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.

view this post on Zulip Luca Seemungal (Nov 15 2019 at 10:57):

Ok thanks

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 14:28):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Luca Seemungal (Nov 17 2019 at 09:53):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Nov 17 2019 at 17:31):

@Luca Seemungal Then ignore my comment. I'd like to have a proof of ddtexp(At)=exp(At)\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)x(t)=\exp(At)x(0) for solutions of a linear ODE x˙=Ax\dot x=Ax. As I said before, it's possible to work around non-commutativity even if most theorems are stated for commutative algebras.

view this post on Zulip Luca Seemungal (Nov 17 2019 at 19:13):

Sounds interesting. I've no idea :)

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 22 2019 at 16:36):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Nov 22 2019 at 16:43):

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

view this post on Zulip Luca Seemungal (Nov 22 2019 at 16:44):

Contributing / messing about with it to understand it more

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 22 2019 at 16:52):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 22 2019 at 16:56):

Did you open the mathlib folder in VScode?

view this post on Zulip Patrick Massot (Nov 22 2019 at 16:57):

Or directly a file?

view this post on Zulip Patrick Massot (Nov 22 2019 at 16:57):

Or a subfolder of the mathlib folder?

view this post on Zulip Luca Seemungal (Nov 22 2019 at 16:58):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Luca Seemungal (Nov 22 2019 at 18:05):

Would a FAQ page be a good idea?

view this post on Zulip 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.

view this post on Zulip 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!)

view this post on Zulip Luca Seemungal (Nov 22 2019 at 19:46):

For me, mathlib defaulted to the lean-4.3.2 branch

view this post on Zulip Mario Carneiro (Nov 22 2019 at 19:49):

wow, that version doesn't even exist yet

view this post on Zulip Luca Seemungal (Nov 22 2019 at 20:16):

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

view this post on Zulip Luca Seemungal (Nov 22 2019 at 20:17):

Oh wait

view this post on Zulip Luca Seemungal (Nov 22 2019 at 20:17):

3.4.2?

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Luca Seemungal (Nov 24 2019 at 08:28):

Thanks! This is a helpful example to study

view this post on Zulip 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.

view this post on Zulip 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