feat(order/filter/filter_product): build hyperreals

[abhimanyupallavisudhir]

Construction of "filter products" (ultraproducts on a general filter), ultraproducts, some instances, hyperreal numbers. Not sure if it belongs in another folder.

[sgouezel]

Comments on the form:

• You should add a header, with the license details and so on, but also explaining what is in the file, with motivations, math explanations, and references to the literature.
• Add docstrings to most of the definitions
• You should use namespaces: put the first definitions in the filter namespace, and the instances maybe in filter.bigly_equal.

Otherwise, the maths look good (except that you are missing a field instance when your filter is a ultrafilter).

[johoelzl]

Hi @abhimanyupallavisudhir,
the formalization looks really nice. I have a couple of style comments and requests for changes.

[avigad]

@abhimanyupallavisudhir I already made the fix and checked compilation on my machine. I am just waiting for the Travis check to finish, and then I'll merge.

[abhimanyupallavisudhir]

@abhimanyupallavisudhir I already made the fix and checked compilation on my machine. I am just waiting for the Travis check to finish, and then I'll merge.

Isn't making f implicit a better fix?

[jcommelin]

I realise I'm a bit late with these comments, as @avigad was already talking about merging this. I don't mind if you ignore these comments... they're not that important.

I should stress that I think this is a cool PR!

[avigad]

@abhimanyupallavisudhir I didn't even see your change. I think we pushed them at the same time. Could you make the argument implicit again and adapt @jcommelin's suggestions as you see fit? Then I'll merge right away.

[abhimanyupallavisudhir]

Ok, all done.