Nonstandard analysis

Stream: new members

[Michael OConnor]

Hi all!

I found this place by watching the YouTube video of Jeremy Avigad's talk at the Topos Institute, this looks like a wonderful community!

I was thinking about what I could contribute, and was wondering if anyone either already has or would be interested in a nonstandard analysis library?

Looking around mathlib, I see that both first-order languages and ultrafilters are already defined. I suspect that the most straightforward approach would be the ultrapower approach, where you prove a "transfer principle" saying that the ultrapower of (say) R has the same first order properties as R (but also has infinitesimals).

But in order to make that practically usable for other arguments in Lean, I think you'd need a tactic: something like "use_transfer at h" which would do something like: examine the type of some hypothesis (or goal) h to observe that it does have the form of a first-order statement over R and then transform it to a first-order statement over the ultrapower of R.

I think this would have to be a tactic rather than a theorem, since it depends on the structure of the type of h. But I'm not 100% sure of that (or really anything else I'm saying).

Does any of that sound reasonable/plausible? (Also, I'm not sure if or how many Wikipedia links I should have provided for the things I said above; let me know if anything needs further clarification.)

Thanks!

[Kevin Buzzard]

It was an undergrad at Imperial who started off with the ultraproducts and they were motivated by doing some non-standard analysis, but as you point out there was a missing tactic, and so he didn't take it any further. I have an MSc student @Joseph Hua doing some model theory right now; he is working towards Ax-Grothendieck via model theory but we'll have a good time whether or not we get there.

[Kevin Buzzard]

I don't think anyone's working on nonstandard analysis right now though. It would be an interesting project! But quite a challenging one for a first project I guess.

[Michael OConnor]

Ah, thanks for the background!

Yeah, I do agree it'd be a challenging first project. That's why I was thinking to first prove a transfer theorem without adding a new tactic (unless it's implicit in the existing ultrafilter code; I haven't actually read it yet). That seems a bit more manageable than jumping in with metaprogramming from the start.

[Reid Barton]

Part of my o-minimal structures project is a tactic to prove that expressions are definable in a certain first-order structure--which is similar to but maybe not exactly the same as what you want

[Reid Barton]

Because I just need to know whether a formula (typically in one free variable) is definable or not, not to translate it into a formula about another structure.

[Michael OConnor]

Thank you!