Contribution to mathlib with the Ostrowski theorem

Stream: new members

[Ryan Lahfa]

Hello, I'm a beginner in Lean and I want to create my first contribution to mathlib with the Ostrowski theorem: https://en.wikipedia.org/wiki/Ostrowski%27s_theorem — I read that I should try to inform the community first and discuss regarding new contributions, so here I am. I also use this post to ask about the topological equivalence between metrics, I looked through the API doc for some "equiv", "metric equivalence" but didn't found anything.

So my guess is either it does not exist yet, it exists under a name that I do not know, it can be trivially created from the data.equiv module (?).

Thank you in advance and thank you for this awesome thing!

[Yury G. Kudryashov]

Which equivalence relation are you talking about? The Wiki page doesn't state it in the header, and I don't want to read the proof.

[Ryan Lahfa]

@Yury G. Kudryashov Topological equivalence (metrics induces the same topology), I can see topological_space_eq and uniform_space_eq but what about metric_space_eq ?

[Yury G. Kudryashov]

So you want to say that the identity is a homeomorphism.

[Ryan Lahfa]

@Yury G. Kudryashov Right.

[Yury G. Kudryashov]

Then define a homeomorph between two metric spaces with to_fun = id and inv_fun = id.

[Yury G. Kudryashov]

Note that we use typeclasses for norms so you'll need something like def rat_with_norm (norm : has_norm rat) := rat, or maybe a more general version.

[Ryan Lahfa]

Alright, understood @ topological equivalence in metric spaces! That's super clear.

But, I'm not sure why I would need to define rat_with_norm for now?

[Yury G. Kudryashov]

When you write rat, Lean tries to find the norm associated with this type. If you want to deal with two norms on the same space, you need to fool Lean into treating them as to different types.

[Patrick Massot]

I don't think you need such wrapper.

[Ryan Lahfa]

@Yury G. Kudryashov Oh, makes sense.

Also, I'm trying to make general definitions of metric_space_eq like this:

definition metric_space_eq {α : Type u} {β : Type u} [metric_space α] [metric_space β] :=
    ({continuous_to_fun := id _, continuous_inv_fun := id _} : homeomorph α β)

And I have a lot of errors, but I guess I'm doing something super wrong, I defined some universe u before and imported everything I needed:

ostrowski.lean:19:5: error
invalid structure value { ... }, field 'to_fun' was not provided
ostrowski.lean:19:5: error
invalid structure value { ... }, field 'inv_fun' was not provided
ostrowski.lean:19:5: error
invalid structure value { ... }, field 'left_inv' was not provided
ostrowski.lean:19:5: error
invalid structure value { ... }, field 'right_inv' was not provided

When I use to_fun and inv_fun, it says that continuous ones are missing.

[Patrick Massot]

Also, Ryan, you should have a look at the data/padics in mathlib

[Ryan Lahfa]

@Patrick Massot Yes I'm reusing most of the stuff that I can that is in there.

[Patrick Massot]

In particular I don't think it uses doesn't analysis/normed_space

[Yury G. Kudryashov]

You should reuse equiv.refl for many fields. Sorry, I have to go.

[Ryan Lahfa]

@Yury G. Kudryashov It's alright, thank you, I'll try to figure it out!

[Yury G. Kudryashov]

Anyway the main lemma should state that id is continuous. Once you prove this, packing into homeomorph will be easy.

[Yury G. Kudryashov]

I mean, id from rat with one norm to rat with standard norm.

[Yury G. Kudryashov]

And the same for reversed id.

[Patrick Massot]

Ryan, could you clarify what you want about "equivalent metrics"? I mean the math meaning, not Lean code.

[Ryan Lahfa]

@Patrick Massot Topological equivalence

[Patrick Massot]

Of what?

[Patrick Massot]

Two metric structure on the same type?

[Patrick Massot]

Or different types?

[Patrick Massot]

Do you want to define a predicate or something containing data?

[Ryan Lahfa]

@Patrick Massot Mathematically, what I want is something that @Yury G. Kudryashov said: I want that id : (E, d_1) → (E, d_2) is an homemorphism, implying that (E, d_1) and (E, d_2) have the same opens (so topological equivalence of topological spaces?)

[Patrick Massot]

So you want a predicate with input E, d_1 and d_2, right?

[Ryan Lahfa]

Indeed, what I defined earlier takes two metric spaces which is not what I want in fact

[Kevin Buzzard]

Ostrowski can be formalised without any mention of topology. The guts of it is a purely algebraic statement. There is an independent fact that two norms on a field are equivalent (|.|_1=|.|_2^d) if and only if they induce the same topology, but this is somehow an independent thing.

[Patrick Massot]

Yes, this is what I fond confusing.

[Patrick Massot]

What you ask for is then:

def metric_space_eqv {α : Type*} (d d' : metric_space α) : Prop :=
d.to_uniform_space.to_topological_space = d'.to_uniform_space.to_topological_space

[Patrick Massot]

I was answering Ryan, not Kevin.

[Ryan Lahfa]

@Kevin Buzzard I agree with this, I just want to port the entire theorem, it's also a way for me to get better at Lean and understand more ; though I think I'll try to isolate the algebraic statement from the topological one.

[Patrick Massot]

What Kevin says is more specific. In general there is no nice algebraic criterion for topological equivalence between metrics (for instance asking that Id is bilipschitz is much stronger).

[Kevin Buzzard]

Yes, this is specific to fields, but Ostrowski is about $\mathbb{Q}$ so this topology talk is perhaps misleading.

[Kevin Buzzard]

The work is checking that every norm is one of the ones we know already. There's a proof in Cassels' book on local fields which might be pleasant to formalise.

[Patrick Massot]

Indeed, this is why I suggested reading data/padics instead of anything living under topology or analysis.

[Kevin Buzzard]

Cassels' proof involves taking a limit though, it might be quite an interesting project to do in Lean.

[Ryan Lahfa]

That sounds super interesting, I'm going to get the proof and study it, if I have any further issue, I'll try to come back ; BTW, are limits available in Lean?

[Kevin Buzzard]

sure, I just thought it was interesting that things like limits and logs were involved when the statement feels quite algebraic.

[Patrick Massot]

Sure, we have a lot about limits in mathlib.

[Ryan Lahfa]

Awesome :)

[Patrick Massot]

Search for tendsto.

[Patrick Massot]

You can use the search at https://leanprover-community.github.io/mathlib_docs/

[Ryan Lahfa]

@Patrick Massot Yes, it has been super useful so far

[Kevin Buzzard]

[I just clicked on the link you posted and it looks to me like it's the same proof as in Cassels]

[Ryan Lahfa]

I come back with plenty of questions:
— let's say I want to prove that a finite product of M non-negative rationals such that the result is < 1 contains at least a term such that it is < 1, should I use the list type for this?
I have a lemma like this:

lemma product_of_nonnegative_rat_le_one_contains_at_least_one_le_one_factor (L : list ℚ)  (H: ∀ a : ℚ, a ∈ L → a ≥ 0) (J: list.prod L ≤ 1)
    : ∃ a : ℚ, a ∈ L ∧ a ≤ 1 := sorry

bonus: should I design it so that it rather show the existence of j such that nth L j ≤ 1 (that's better I suppose).

— next is, I have an n0 ≥ 2, I want to apply the absolute value on its prime factor decomposition, so naively, I do have afactors := list.map abv (nat.factors n0) and I get a list of Q, but I have this hypothesis on n0 which is abv n0 <= 1 and I want to transmit it to list.prod afactors, so I guess I have to use the fact that list.prod (nat.factors n0) = n0 to getlist.prod (list.map abv nat.factors n0) = abv n0.
Maybe I don't know enough about the mathlib to perform this easily.

Thank you!

[Alex J. Best]

Hello, I'm a beginner in Lean and I want to create my first contribution to mathlib with the Ostrowski theorem: https://en.wikipedia.org/wiki/Ostrowski%27s_theorem — I read that I should try to inform the community first and discuss regarding new contributions, so here I am. I also use this post to ask about the topological equivalence between metrics, I looked through the API doc for some "equiv", "metric equivalence" but didn't found anything.

So my guess is either it does not exist yet, it exists under a name that I do not know, it can be trivially created from the data.equiv module (?).

I took a crack at Ostrowski at one point (see the attached file). Its a complete work in progress and it needs a lot of cleanup, but some of the key steps were there. I was hindered a bit by the fact that I didn't really develop the theory of equivalences, or expressing different numbers in different bases before I began, and I didn't really have a mathematical reference in mind before I started. The most succinct math proof I have seen is due to Artin and combines a lot of the steps in quite a neat way, so I'd probably try and reformat it to follow that more if I did it again or restarted. You are more than welcome to take bits of this or completely ignore it of course ;): ostrowski.lean

[Kevin Buzzard]

I think people usually use finset.prod, which has the best interface

[Kevin Buzzard]

The lemma that you need about applying a group hom to a finite product being equal to the product of the factors will surely be there for finset products

[Kevin Buzzard]

Note that the finset isn't the set of factors, it is an auxiliary finite set equipped with a map to the factors

[Johan Commelin]

In other words... one option is to use a family of elements, indexed by some index type \iota. This is how the finset.prod stuff works.

[Johan Commelin]

Using lists is in principle a good idea. It's just not the way it's been done in mathlib. Not sure if that is silly on our side, though...

[Ryan Lahfa]

Hello, I'm a beginner in Lean and I want to create my first contribution to mathlib with the Ostrowski theorem: https://en.wikipedia.org/wiki/Ostrowski%27s_theorem — I read that I should try to inform the community first and discuss regarding new contributions, so here I am. I also use this post to ask about the topological equivalence between metrics, I looked through the API doc for some "equiv", "metric equivalence" but didn't found anything.

So my guess is either it does not exist yet, it exists under a name that I do not know, it can be trivially created from the data.equiv module (?).

I took a crack at Ostrowski at one point (see the attached file). Its a complete work in progress and it needs a lot of cleanup, but some of the key steps were there. I was hindered a bit by the fact that I didn't really develop the theory of equivalences, or expressing different numbers in different bases before I began, and I didn't really have a mathematical reference in mind before I started. The most succinct math proof I have seen is due to Artin and combines a lot of the steps in quite a neat way, so I'd probably try and reformat it to follow that more if I did it again or restarted. You are more than welcome to take bits of this or completely ignore it of course ;): ostrowski.lean

That's super helpful, I want to read a lot of Lean to understand more :)

[Ryan Lahfa]

In other words... one option is to use a family of elements, indexed by some index type \iota. This is how the finset.prod stuff works.

I understand ; but isnat.factors compatible with finset?

[Johan Commelin]

Maybe not as compatible as we would like :wink:

[Johan Commelin]

This might be an argument to go with lists

[Johan Commelin]

Here's a question: can you state Ostrowski in Lean? Or is that impossible with current state of the library?

[Johan Commelin]

(And then I mean a relatively clean statement. I'm sure we can get some unreadable thing that is some form of Ostrowski.)

[Ryan Lahfa]

State as in: says that if some absolute value over Q is not the trivial absolute value (in terms of pointwise equality), then (Q, |⋅|) is topologically equivalent as topological spaces to (Q, |⋅|_p) or (Q, |⋅|_inf) for some p prime ; right?

Or in terms of proof?

[Johan Commelin]

No, I mean

theorem Ostrowski : _fill_this_in_ :=
sorry

[Johan Commelin]

So, you can leave the sorry there, for now.

[Ryan Lahfa]

No, I mean

theorem Ostrowski : _fill_this_in_ :=
sorry

This is what I understood, don't worry ;

(abv : \Q \to \Q) [is_absolute_value abv] (H\_1: \not (abv \eq trivial_abs)) : (\exists p : nat.primes, …) \or (…))

Where … is something about the topological equivalence regarding padic.padic_norm and standard absolute value which I think is possible based on what @Patrick Massot and @Yury G. Kudryashov told me.

I might be wrong though and this could be wishful thinking.

[Johan Commelin]

That's why I'm asking :smiley: I think it would be good to have a version that Lean is happy with.

[Johan Commelin]

@Ryan Lahfa Is is_absolute_value something that Lean know about? Or is this something that still has to be written?

[Patrick Massot]

https://leanprover-community.github.io/mathlib_docs/data/real/cau_seq.html#is_absolute_value

[Johan Commelin]

thanks

[Patrick Massot]

It's nice to see you've been able to use padics in mathlib without knowing this file. It proves the API is good.

[Yury G. Kudryashov]

BTW, I'd prefer to see p-adics defined as sequences of digits, maybe using some generic algebraic construction. This way Lean will be able to actually do finite precision computations in p-adics.

[Yury G. Kudryashov]

Then we can prove that they form a complete_space w.r.t. the p-adic norm.

[Yury G. Kudryashov]

All of this needs a ring (probably with some additional properties), a prime ideal, and something equivalent to the quotient (used for computations).

[Kevin Buzzard]

The p-adic numbers are an example of a nonarchimedean local field and I'd prefer to see a general theory of these set up.

[Ryan Lahfa]

I tried to look for equality of functions but I'm not sure I found something in mathlib, I got overwhelmed by the amount of equiv modules ; I have the feeling that abv \neq trivial_abv is stronger than saying that \forall x \in F, abv x \neq trivial_abv x, but is there a way to not write this?

[Patrick Massot]

It's not stronger.

[Alex J. Best]

Yeah one problem my ostrowski formulation I had was my absolute values mapped from $\Q \to \Q$ instead of $\Q \to \R$, I chose this as the usual absolute value function and p-adic valuation for rationals defaults to maps like this iirc. But really you want the stronger statement that any $\Q \to \R$ is one of $|\cdot |$ or $|\cdot|_p$.

[Alex J. Best]

So my notion of equivalence was a weird hack where you extend to $\R$ then ask that one be a power of the other.

[Ryan Lahfa]

It's not stronger.

So abv = trivial_abv is exactly \forall x : some domain, abv x = trivial_abv x (?)

[Ryan Lahfa]

Yeah one problem my ostrowski formulation I had was my absolute values mapped from $\Q \to \Q$ instead of $\Q \to \R$, I chose this as the usual absolute value function and p-adic valuation for rationals defaults to maps like this iirc. But really you want the stronger statement that any $\Q \to \R$ is one of $|\cdot |$ or $|\cdot|_p$.

Exact, I've read and thanks to your code, I moved faster than I expected, I learnt a lot about how to do some simple stuff (product of terms, etc.)

[Alex J. Best]

Yes the principle that functions are equal when their values are is called function extensionality. A tactic to use this is called funext. If you apply this to a goal f=g you'll get a value x and have to prove f x =g X

[Patrick Massot]

A more complete answer is: for mathematicians, the equivalence is trivial. Because Lean is also used for software verification, this triviality is not an base axiom, but you have it anyway.

[Kevin Buzzard]

It's just something that computer scientists make a fuss about for some reason ;-)

[Ryan Lahfa]

I agree with the facts it was trivial for mathematicians, and for Lean, it requires some base axiom, my underlying question was: is this axiom there? I have my answer now :)

[Patrick Massot]

Also forget what Alex wrote about funext, this is a historical accident. This tactic is subsumed by the more general ext tactic.

[Alex J. Best]

The only time one needs to use funext is in a conv block right?

[Patrick Massot]

Oh maybe yes. Maybe ext has no conv version.

[Ryan Lahfa]

Here's new questions!

I'm trying to figure out how to instantiate some fields and stuff and I often run into "failed to synthesize type class instance for […]", for example, if I try to do #check \Q_[3] it'll fail, I guess I have to prove that 3 is prime but I'm unsure how to inject this information? It seems like apply_instance is what I want but once I'm not sure how to use it.

[Ryan Lahfa]

Also, what's the difference between writing \exists p : nat.primes, … and \exists (p), [hp: nat.prime p], … ?

[Yury G. Kudryashov]

In the first case p is a structure with two fields: p.val is a number and p.property says that p.val is prime. In the latter case p is a number and hp says that it is prime.

[Ryan Lahfa]

@Yury G. Kudryashov Okay, makes sense, thank you!

[Ryan Lahfa]

New question, so if I have some absolute value |⋅| and I want to induce some metric_space using it over \Q ; like @Yury G. Kudryashov said earlier, I have to define some rat_with_abv to create a new type and then I can define as an instance of metric_space for example, right? I don't think I can avoid it ; but curious question, is there a technical limitation for why we could not have:

def field_with_abv {a: Type*} (abv: a \to a) [normed_field a] [is_absolute_value abv]: normed_field a := [build generally the normed_field using abv over a]

I'm not exactly sure that a must be a discrete_field, but whatever it has to be.

And this way we could swap absolute values (or norm) for all normed fields I guess (?).

[Ryan Lahfa]

I suppose I could use the Cauchy completion by showing that from all absolute values, we can derive some norms?

[Johan Commelin]

It's just something that computer scientists make a fuss about for some reason ;-)

@Kevin Buzzard How many different ways are there to sort a list?

[Kevin Buzzard]

Just the one

[Kevin Buzzard]

It's called "WLOG the elements are in increasing order"

[Kevin Buzzard]

unless of course it's not WLOG, in which case sorting it would be non-canonical.

[Patrick Massot]

Ryan, you don't have to create an instance if you don't want to use it through type class inference. This instance stuff is all about Lean figuring out what you don't write. You always keep the possibility of not asking Lean but telling it.

[Patrick Massot]

Maybe this discussion is too abstract. Let me write some code:

import topology.metric_space.basic

noncomputable theory

open is_absolute_value

variables {α : Type*} [ring α]

def metric_space_of_real_abv (abv: α → ℝ) [is_absolute_value abv] : metric_space α :=
{ dist := λ x y, abv $ x - y,
  dist_self := λ x, show abv (x-x) = 0, by simp[abv_zero abv],
  eq_of_dist_eq_zero := λ x y h, eq_of_sub_eq_zero $ (abv_eq_zero abv).mp h,
  dist_comm := abv_sub abv,
  dist_triangle := λ x y z, begin
    change abv (x-z) ≤ abv (x-y) + abv (y-z),
    rw show x - z = (x - y) + (y - z), by abel,
    apply abv_add,
  end}

def topology_of_real_abv (abv: α → ℝ) [is_absolute_value abv] : topological_space α :=
(metric_space_of_real_abv abv).to_uniform_space.to_topological_space

def abv_top_eqv (abv₁ abv₂ : α → ℝ) [is_absolute_value abv₁] [is_absolute_value abv₂] : Prop :=
topology_of_real_abv abv₁ = topology_of_real_abv abv₂

[Patrick Massot]

Is this what you want? This is still going toward a very weak version of the conclusion of Ostrowski.

[Ryan Lahfa]

It makes a lot of sense now, regarding the instance. Thank you!

[Ryan Lahfa]

Is this what you want? This is still going toward a very weak version of the conclusion of Ostrowski.

What's the strong version of Ostrowski? IMHO, I was under the assumption it was a statement of the form: for all absolute values over Q, either it is equivalent to the real absolute value, or there is some prime p such that the absolute value is equivalent to the padic one.

It appears to me that I need the metric_space_of_real_abv to have:

theorem rat_abs_val_p_adic_or_real (abv: ℚ → ℚ)
    [habv: is_absolute_value abv]
    (hnontriv: abv ≠ trivial_abs):
    (metric_space_eq
        (metric_rat_with_abv abv)
        (rat.metric_space))
    ∨
    (∃ (p) [hp: nat.prime p],
        (metric_space_eq
            (metric_rat_with_abv abv)
            (padic.metric_space p)))

Something like this.

[Ryan Lahfa]

But sure, that might be better to just prove that there is directly some relation between the absolute values themselves.

[Johan Commelin]

I think the stronger form would be saying that the two absolute values differ by a power

[Ryan Lahfa]

I think the stronger form would be saying that the two absolute values differ by a power

Ah ; but I was going to derive the weak form (same topology) by the strong form (absolute values differ by a power).

So yes I agree that it might be better to expose the stronger form as a theorem and derive the weak form through a lemma.

[Johan Commelin]

Also, it's good to see that you have a Lean statement now. Does it already typecheck?

[Johan Commelin]

Could you post a self-contained piece of code that we can copy-paste (including the necessary import and variable statements etc...)

[Ryan Lahfa]

Could you post a self-contained piece of code that we can copy-paste (including the necessary import and variable statements etc...)

For now, it's still somewhat a scratch file with a lot of code / sorry, but next time I post something, I'll try to give a minimal example, sure.

[Ryan Lahfa]

Also, it's good to see that you have a Lean statement now. Does it already typecheck?

I did a lot of changes and it does not typecheck anymore :D

[Ryan Lahfa]

New question, when I have, let's say I have:

import data.nat.prime
import data.real.basic
import data.real.cau_seq
import tactic.apply
import tactic.apply_fun

section

open_locale classical real
open list option
open nat

-- absolute values are monoid homemorphisms.
def hom_of_abv {α: Type*} [hlifield: linear_ordered_field α] (abv: α → ℝ) [habv: is_absolute_value abv]: monoid_hom α ℝ :=
{
    to_fun := abv,
    map_one' := is_absolute_value.abv_one abv,
    map_mul' := is_absolute_value.abv_mul abv
}


example (z : ℕ) (f: ℚ → ℝ) [is_absolute_value f]:
    list.prod (list.map (hom_of_abv f) (list.map (coe : ℕ → ℚ) (factors z))) = f (list.prod (list.map (coe : ℕ → ℚ) (factors z))) :=
begin
    exact prod_hom (list.map (coe :ℕ → ℚ) (factors z)) (hom_of_abv f)
end

example (z : ℕ) (f: ℚ → ℚ) [is_absolute_value f]: prod (map (f ∘ (coe : ℕ → ℚ)) (factors z)) = f ↑(list.prod (factors z)) :=
    begin
    exact prod_hom (factors z) (f ∘ (coe :ℕ → ℚ))
end

end

The second example is failing because f is not an unbundled monoid homomorphism (under the assumption that there is something which implements is_monoid_hom for f \circ g), but while reading the documentation, I see that those are deprecated and being slowed removed from mathlib.

Does that mean I have to use bundled monoid homomorphism?

In this example, I can trivially have a hom_of_abv which gives me a monoid_hom Q Q (or whatever) and then, I can use prod_hom on it and have a close result except that it has this upper arrow which I suppose says this is a bundled homomorphism.

But, can I lift those to rewrite the unbundled version of the homomorphism?

Better, I'd like to prod_hom with (f \circ (coe : N → Q)) but unsure how that's feasible w/o having something which takes (f, g), bundle the composition. How does that scale to f_1 \circ … \circ f_n ? It does not sound general enough…

[Johan Commelin]

Tip: if you write

```lean
code here
```

then you even get syntax highlighting

[Ryan Lahfa]

Thank you @Johan Commelin — now I add regarding my last question that I know I could merge the map map using list.map_map,

but then, I'm stuck with this coe_fn in front of all my abv functions ; I'm not super strong with the coercion thing, I understand most of it, but I'm not sure how I can lift it in the context? I tried: simp, push_cast, norm_cast and all of them failed.

[Johan Commelin]

If they fail, that might also be because of missing simp-lemmas in the library...

[Johan Commelin]

@Ryan Lahfa To fix the second example, you should add an instance that shows that is_absolute_value f implies is_monoid_hom f.

[Johan Commelin]

Apparently that one is missing

[Ryan Lahfa]

If they fail, that might also be because of missing simp-lemmas in the library...

AFAIK, according to this, should not this be enough: https://leanprover-community.github.io/mathlib_docs/algebra/group/hom.html#monoid_hom.has_coe_to_fun ?

[Ryan Lahfa]

Ryan Lahfa To fix the second example, you should add an instance that shows that is_absolute_value f implies is_monoid_hom f.

Sure, I could do this, but the docs say it is deprecated to use is_monoid_hom f so I'm not sure what's the situation, I prefer to avoid introducing stuff that will have to be rewritten :P

[Johan Commelin]

Well... that means that absolute values should be refactored, and replaced with bundled versions...

[Johan Commelin]

That's a lot of work for a first PR, so I wouldn't advice it

[Mario Carneiro]

unbundled homs are deprecated, but that really only means that we are starting to use them in new stuff. Because bundled homs are not entirely supported yet, we can't just delete the unbundled homs, and some proofs will require both

[Johan Commelin]

@Mario Carneiro Ryan is concerned about adding new instances of is_monoid_hom to mathlib in a PR on Ostrowski.

[Johan Commelin]

I think adding such instances is indeed "discouraged". But we might also make some exceptions.

[Mario Carneiro]

That seems fine to me, especially if the bundled version is included as well

[Johan Commelin]

How would that look like?

[Johan Commelin]

We have unbundled absolute values. Those are monoid homs, but Lean doesn't know this.

[Johan Commelin]

I don't expect such a PR to introduce bundled absolute values.

[Mario Carneiro]

Actually, it makes a lot of sense to have bundled absolute values for ostrowski, since it is about characterizing this space

[Mario Carneiro]

you can define an equivalence relation on the type absolute_value which is "differs by a power", and then define the real and p-adic and trivial absolute values, and then it is easy to state the theorem

[Johan Commelin]

That makes sense. (And then later derive an unbundled statement? In case someone actually wants to apply Ostrowski at some point? Although by that time we'll hopefully want and have a version for number fields.)

[Ryan Lahfa]

Alright, it makes sense, so I should wrap all abv into bundled hom and work with them, this I can do.

At some point, statement about bundled hom abv can be made into statement about unbundled abv; this I don't see how to do, but I can believe that someone will figure out, right?

[Johan Commelin]

Sure, that last step is not so hard: no maths involved, just shuffling some data around in Lean.

[Ryan Lahfa]

you can define an equivalence relation on the type absolute_value which is "differs by a power", and then define the real and p-adic and trivial absolute values, and then it is easy to state the theorem

@Alex J. Best already done it in its version of Ostrowski and I'm reusing this. The only thing is that we have not defined this equiv relation on the monoid_hom Q R which implements is_absolute_value but rather on Q → R which implements is_absolute_value, right?

[Johan Commelin]

For an idea of how to define absolute_value, see: https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/valuation/basic.lean#L58

[Ryan Lahfa]

But do we agree this require a change from:

class is_absolute_value {α} [discrete_linear_ordered_field α]
  {β} [ring β] (f : β → α) : Prop :=
(abv_nonneg : ∀ x, 0 ≤ f x)
(abv_eq_zero : ∀ {x}, f x = 0 ↔ x = 0)
(abv_add : ∀ x y, f (x + y) ≤ f x + f y)
(abv_mul : ∀ x y, f (x * y) = f x * f y)

to

class is_absolute_value {α} [discrete_linear_ordered_field α]
  {β} [ring β] (f : monoid_hom β α) : Prop :=
(abv_nonneg : ∀ x, 0 ≤ f x)
(abv_eq_zero : ∀ {x}, f x = 0 ↔ x = 0)
(abv_add : ∀ x y, f (x + y) ≤ f x + f y)

I guess abv_mul is now trivial due to monoid_hom.map_mul', so not required to implement it. It also looks better IMHO, because it makes sense to say that an absolute value is a monoid homomorphism which implements additional stuff.
Also, abv_one becomes trivial too.

[Ryan Lahfa]

@Johan Commelin Shouldn't we change the is_absolute_value definition coming from Cauchy completion?

[Ryan Lahfa]

But that also requires changes in the padic.padic_norm definition and the real absolute value definition (right?)

[Johan Commelin]

I understand your confusion. But you should ignore all the existing stuff (for now).

[Johan Commelin]

In the end, we'll have both bundled and unbundled versions. And Mario says that's ok.

[Johan Commelin]

Don't worry about refactoring things.

[Johan Commelin]

Just introduce a new thing absolute_value that extends mul_hom, like in the example I linked to.

[Johan Commelin]

After that, define some coercions and prove some trivial simp-lemmas, like we did for valuations.

[Johan Commelin]

After that, define some examples, like real.abs_val and padic.abs_val, and here you will reuse the unbundled versions. Defining these examples is not hard.

[Johan Commelin]

Also, define an equivalence relation.

[Johan Commelin]

And then you are good to go to get a nice statement for Ostrowski.

[Ryan Lahfa]

Alright, that works for me :)

[Mario Carneiro]

We don't need to change is_absolute_value itself, but absolute_value := {abv // is_absolute_value abv} is easy enough to define

[Mario Carneiro]

I would prefer that the monoid hom thing be proven rather than assumed (it's not immediate from the definition that f 1 = 1, for example, and we wouldn't want to require that to be proven too)

[Mario Carneiro]

The usage of is_absolute_value in the definition of real is somewhat foundational, so it's okay if it's not completely in line with conventions

[Ryan Lahfa]

I would prefer that the monoid hom thing be proven rather than assumed (it's not immediate from the definition that f 1 = 1, for example, and we wouldn't want to require that to be proven too)

Do you mean to prove that absolute_value are monoid hom by proving that abv 1 = 1?

Under which assumptions should we define absolute_value? Like for real, discrete linear ordered fields?

[Mario Carneiro]

The reason is_absolute_value in cau_seq requires a discrete_linear_ordered_field is because I needed it on Q and R

[Mario Carneiro]

The statement only needs an ordered ring afaik

[Mario Carneiro]

But I think Ostrowski works in the context of a real-valued absolute value

[Ryan Lahfa]

But I think Ostrowski works in the context of a real-valued absolute value

We can always specialize it afterwards, but I guess we want a general is_absolute_value right?

[Ryan Lahfa]

New questions:
I'm trying to do some real power algebra, and I have a real in my exponent, so I'm trying to find some theorems to manipulate them, I expected most of the theorems to be there or in group power:

https://leanprover-community.github.io/mathlib_docs/algebra/field_power.html

But I'm lacking something akin to (a ^ n) ^ m = a ^ (n*m) for m n : R, which would be some fpow_mul I guess.
At the same time, I guess that real pow are more analysis than true algebra, making sense for why those theorems would not be in field power.

I looked in analysis, found nothing. I tried the custom search but it is not super reliable. I guess I could do some PR or something to improve the search and replacing it by some full text search using JavaScript. This is a parallel idea but it would be awesome to have a Hoogle-like search for Lean, just give it some types and it'll give you what you want, this could be a project I would be super proficient in I think.

[Johan Commelin]

fpow_mul would be for powers by integers

[Johan Commelin]

There is rpow.* I think

[Johan Commelin]

Or was it real_pow.*?

[Ryan Lahfa]

@Johan Commelin I searched for rpow and real_pow and found nothing :/

[Patrick Massot]

real.rpow

[Ryan Lahfa]

https://leanprover-community.github.io/mathlib_docs/analysis/complex/exponential.html#real.rpow Indeed… I was supposing that complex had nothing to do with what I wanted.

[Patrick Massot]

I found it by running mk_all.sh and then inside all.lean:

def rpo : ℝ → ℝ → ℝ :=
begin
  suggest,
  sorry
end

[Ryan Lahfa]

@Patrick Massot Thank you for the tip!

[Ryan Lahfa]

ostrowski-ext.lean
I have a more difficult question, if you load the file I provide here.
And go line 312, for some reason, I cannot close the goal "prime p" by using a hypothesis which is "prime p", I guess it has to do with implicit contexts, but unsure how to debug, nor solve this. I guess I'm too newbie in coe stuff.

[Johan Commelin]

Hmm, I currently don't have Lean available. what happens if you convert this?

[Patrick Massot]

My guess: _root_.prime and nat.prime are fighting over this proof.

[Ryan Lahfa]

Hmm, I currently don't have Lean available. what happens if you convert this?

it becomes prime p = prime p and refl does not end it.

[Ryan Lahfa]

My guess: _root_.prime and nat.prime are fighting over this proof.

What's the difference?

[Ryan Lahfa]

You're right, I think it's that. When I replaced apply prime.ne_zero by apply nat.prime.ne_zero and nat.mem_factors it worked!

[Patrick Massot]

Does anyone know why we still have nat.prime?

[Mario Carneiro]

I'm not sure I like replacing the obvious definition with a complicated one

[Ryan Lahfa]

I'm not sure I like replacing the obvious definition with a complicated one

Which definition?

[Mario Carneiro]

the abstract algebra definition

[Mario Carneiro]

that's _root_.prime

[Patrick Massot]

You can still keep the same API for nat.

[Mario Carneiro]

we should at least make sure that the definition of _root_.prime does not have high dependencies

[Mario Carneiro]

and move the proof of (the equivalent of) prime n <-> nat.prime n as early as possible

[Patrick Massot]

Ryan, if you really need this, the lemma is nat.prime_iff_prime in algebra.gcd_domain

[Ryan Lahfa]

I can do just fine by being explicit and I never manipulate abstract prime concepts, so I'm fine with explicit nat.prime everywhere! Thank you :)

[Ryan Lahfa]

I'm continuing my work on power manipulation and I am trying the abv_nonneg property of my real_padic_norm, so here is an example which is perfectly working:

import data.nat.prime
import data.real.basic
import data.real.cau_seq
import analysis.complex.exponential
import tactic.apply
import tactic.apply_fun
import data.padics

section

open_locale classical real
open list option
open nat

def real_padic_norm (p: ℕ): ℚ → ℝ := λ x : ℚ, real.of_rat (padic_norm p x)

instance (p: ℕ) [hp: nat.prime p]: is_absolute_value (real_padic_norm p) :=
{
    abv_nonneg := sorry,
    abv_eq_zero := sorry,
    abv_add := sorry,
    abv_mul := sorry
}

example (p: ℕ) [hp: nat.prime p]: ∀ x : ℚ, ∀ y z : ℝ, ((real_padic_norm p) x) ^ (y * z) = (((real_padic_norm p) x) ^ y) ^ z := begin
    intros x y z,
    rw real.rpow_mul (is_absolute_value.abv_nonneg (real_padic_norm p) _),
end

end

But when I do more or less the same in the attached file, line 394, excerpt:

      conv_rhs at this {
          congr, skip,
          rw real.rpow_mul (is_absolute_value.abv_nonneg (real_padic_norm p) _),
      },

It fails to synthesize type classes and fails, unsure what's the difference with the minimal case below and this one. ostrowski-ext.lean

[Ryan Lahfa]

Also, is there any way to solve this kind of problems:

type mismatch at application
  is_unit_int.mp a
term
  a
has type
  @is_unit ℤ
    (@ring.to_monoid ℤ
       (@domain.to_ring ℤ (@integral_domain.to_domain ℤ (@principal_ideal_domain.to_integral_domain ℤ _inst))))
    x_2
but is expected to have type
  @is_unit ℤ int.monoid x_2
state:
abv : ℚ → ℝ,
habv : is_absolute_value abv,
hnontriv : abv ≠ trivial_abv,
B : ℚ,
int_lt_B : ∀ (z : ℕ), abv ↑z ≤ ↑B,
all_nat_le_one : ∀ (z : ℕ), abv ↑z ≤ 1,
all_int_le_one : ∀ (z : ℤ), abv ↑z ≤ 1,
z : ℕ+,
hz : abv ↑z < 1,
p : ℕ,
p_fact : p ∈ factors ↑z,
abv_p_lt_one : abv ↑p < 1,
this : ∀ (q : ℕ), coprime p q → abv ↑q = 1,
hp : prime p,
α : ℝ := abv ↑p,
this : 0 < -(real.log α / real.log ↑p),
x : ℚ,
x_1 : ℤ,
_inst : principal_ideal_domain ℤ,
_inst_1 : unique_factorization_domain ℤ,
x_2 : ℤ,
a : is_unit x_2
⊢ abv ↑x_2 = real_padic_norm p ↑x_2 ^ -(real.log α / real.log ↑p)

More difficult, I guess, I see that is_unit_int provides int.nat_abs x_2 = 1, but this notion of absolute value is incompatible with absolute values in general I suppose.

Knowing that int.nat_abs x_2 = 1 do not give me abv (coe x_2) = int.nat_abs in general AFAIK. So I guess I have to work more to interface nat_abs with absolute values.

[Kevin Buzzard]

For your first question, first a side comment. In the attachment you have by infer_instance and infer_instance isn't a tactic -- you would want to put by apply_instance or infer_instance. Another side comment is that this proof is gigantic and you might seriously want to consider breaking it up into smaller pieces if possible.

The reason that rw real.rpow_mul (is_absolute_value.abv_nonneg (real_padic_norm p) _) is failing is that type class inference can't find an instance of is_absolute_value (real_padic_norm p). The reason it won't use the instance on line 184 is that this only applies when type class inference can find an instance of nat.prime p and it seems to me that typeclass inference can't find an instance of that. If I insert haveI : nat.prime p := by apply_instance, in line 392 of your attached file, it fails. Conversely, if I write haveI : nat.prime p := sorry on line 392 then things work again -- although it takes a few seconds on my machine to do anything after any line is changed, and this is I guess because the proof is so long.

[Kevin Buzzard]

For your second question, I guess I need more context. It seems to me that a is a proof that x_2 is a unit wrt one monoid structure on the integers, and you want it to be a proof that x_2 is a unit wrt another one. If these two monoid structures are definitionally equal then Lean would not be complaining. I tried to reproduce what you did but I can't:

import data.real.basic
import data.padics.padic_norm
import ring_theory.principal_ideal_domain
import data.real.cau_seq
import analysis.complex.exponential
import tactic.apply
import tactic.apply_fun

instance I : principal_ideal_domain ℤ := by apply_instance
def M1 : monoid ℤ := by apply_instance
def M2 : monoid ℤ := (@ring.to_monoid ℤ
       (@domain.to_ring ℤ (@integral_domain.to_domain ℤ (@principal_ideal_domain.to_integral_domain ℤ I))))

example : M1 = M2 := rfl

So I am totally confused by this one. Did you write [principal_ideal_domain ℤ] at some point? This would be bad because it means "let the integers have the structure of a principal ideal domain in a way which I am not going to tell you anything about, and in particular the underlying addition and multiplication might be completely random".

[Kevin Buzzard]

You seem to have a diamond and there should be no diamonds in mathlib.

[Ryan Lahfa]

For your first question, first a side comment. In the attachment you have by infer_instance and infer_instance isn't a tactic -- you would want to put by apply_instance or infer_instance. Another side comment is that this proof is gigantic and you might seriously want to consider breaking it up into smaller pieces if possible.

The reason that rw real.rpow_mul (is_absolute_value.abv_nonneg (real_padic_norm p) _) is failing is that type class inference can't find an instance of is_absolute_value (real_padic_norm p). The reason it won't use the instance on line 184 is that this only applies when type class inference can find an instance of nat.prime p and it seems to me that typeclass inference can't find an instance of that. If I insert haveI : nat.prime p := by apply_instance, in line 392 of your attached file, it fails. Conversely, if I write haveI : nat.prime p := sorry on line 392 then things work again -- although it takes a few seconds on my machine to do anything after any line is changed, and this is I guess because the proof is so long.

Thank you for looking for a so long time, I totally agree on the fact that the proof is too big and I will refactor it soon.

It makes a lot more sense to me now.

[Ryan Lahfa]

For your second question, I guess I need more context. It seems to me that a is a proof that x_2 is a unit wrt one monoid structure on the integers, and you want it to be a proof that x_2 is a unit wrt another one. If these two monoid structures are definitionally equal then Lean would not be complaining. I tried to reproduce what you did but I can't:

import data.real.basic
import data.padics.padic_norm
import ring_theory.principal_ideal_domain
import data.real.cau_seq
import analysis.complex.exponential
import tactic.apply
import tactic.apply_fun

instance I : principal_ideal_domain ℤ := by apply_instance
def M1 : monoid ℤ := by apply_instance
def M2 : monoid ℤ := (@ring.to_monoid ℤ
       (@domain.to_ring ℤ (@integral_domain.to_domain ℤ (@principal_ideal_domain.to_integral_domain ℤ I))))

example : M1 = M2 := rfl

So I am totally confused by this one. Did you write [principal_ideal_domain ℤ] at some point? This would be bad because it means "let the integers have the structure of a principal ideal domain in a way which I am not going to tell you anything about, and in particular the underlying addition and multiplication might be completely random".

The reason must be the one you pointed, I wrote principal_ideal_domain Zat some point. Is there any way to add more details on the PID I'm looking at?

[Kevin Buzzard]

Lean knows that the integers are a PID, you don't have to type [principal_ideal_domain ℤ] (which inserts a new instance of this fact into the type class inference machine) -- the instance is there already as you can see with instance : principal_ideal_domain ℤ := by apply_instance

[Kevin Buzzard]

If you type [principal_ideal_domain ℤ] then you just made the set of integers (or more precisely the type of integers) into a principal ideal domain by choosing a completely random integer and saying "this one is the 0", another completely random integer and saying "this one is the 1", choosing a random binary function and saying "this can be +" etc.

[Kevin Buzzard]

Your inst_1 is not my I, I suspect.

[Kevin Buzzard]

so then you get problems later on because now you have two different concepts of unit on the set of integers.

[Ryan Lahfa]

I discussed with my math advisor who told me that it might be interesting to rework a bit the absolute value, valuations stuff to do a complete classification of all valuations over a field (according to Artin, Algebraic Numbers & Algebraic Functions), Artin makes super satisfying proofs IMHO, its proof of Ostrowski is quite the same of the Cassels' one, except he's able to make it a lot more compact by doing some work beforehand on the base $b$ expansions.

So I think it makes sense to create a concept of valuations, derive the fact that valuations are always equivalent to one with triangular inequality, then I can have Ostrowski with kind of the same proof (shortened maybe) I have. Modulo base expansions.

BTW, is there any plan regarding decimal/bases expansions in mathlib?

[Kevin Buzzard]

I'm not sure there is any sensible classification of all valuations over a general field?

[Ryan Lahfa]

Lean knows that the integers are a PID, you don't have to type [principal_ideal_domain ℤ] (which inserts a new instance of this fact into the type class inference machine) -- the instance is there already as you can see with instance : principal_ideal_domain ℤ := by apply_instance

It makes sense to me, but when I do this, I still have the same issue:

haveI : principal_ideal_domain ℤ := by apply_instance,
haveI : unique_factorization_domain ℤ := by apply_instance,
apply unique_factorization_domain.induction_on_prime x_1,
 {sorry,},
{intros, have abs_x2_eq_one: int.nat_abs x_2 = 1 := is_unit_int.1 a},
{ sorry },

where x_1 : \Z.

Am I still doing something wrong?

[Kevin Buzzard]

I only know of classifications over number fields (and I can believe that there will be a classification for global fields). Anything beyond that gets hairy very quickly.

[Kevin Buzzard]

I can't answer your question about instances unless you post complete working code.

[Kevin Buzzard]

I am explicitly asking you whether you have any [principal_ideal_domain ℤ] with the rectangular brackets in your code. If you don't, the problem is elsewhere.

[Ryan Lahfa]

I'm not sure there is any sensible classification of all valuations over a general field?

AFAIK, Artin provides some results regarding archimedean/non-archimedean.

[Ryan Lahfa]

ostrowski-ext.lean
Here's the long file, because whenever I extract it into a minimal case, it works, so I don't understand what's the difference, sorry for the long proof. You'll see line 414 the issue.

[Kevin Buzzard]

I can't really comment on the Artin results because I am not sure what precisely you're talking about.

[Ryan Lahfa]

Not sure I can link a PDF for a book here, I suppose. But the exact reference is "Artin, Algebraic Numbers & Algebraic Functions", chapter 1, section 3, "Classifications of Valuations"

[Ryan Lahfa]

He proves a necessary & sufficient condition for a field to be non-archimedean based on the boundness of the values of the rationals integers for the valuation if I read well.

My advisor told me that it'd be interested to go this way in order to develop https://en.wikipedia.org/wiki/Berkovich_space in Lean.

[Kevin Buzzard]

Commelin, Massot and me already developed adic spaces in Lean, probably what we did would be of some help if you wanted to do Berkovich spaces.

[Kevin Buzzard]

It's not in mathlib though.

[Ryan Lahfa]

It's not in mathlib though.

Is it in the perfectoid repository?

[Kevin Buzzard]

Right.

[Ryan Lahfa]

That's something I'm interested in, thanks, I'll take a look to the repo then.

[Kevin Buzzard]

I am now beginning to think that the problem with your code is unique_factorization_domain.induction_on_prime

[Kevin Buzzard]

unique_factorization_domain.induction_on_prime :
  ∀ {α : Type u_2} [_inst_1 : integral_domain α] [_inst_2 : unique_factorization_domain α] {P : α → Prop}
  (a : α),
    P 0 → (∀ (x : α), is_unit x → P x) → (∀ (a p : α), a ≠ 0 → prime p → P a → P (p * a)) → P a

[Kevin Buzzard]

no I'm wrong, this looks fine; unique_factorization_domain doesn't extend integral_domain

[Kevin Buzzard]

Oh! I am a twit. It shouldn't be haveI -- you need to change them to letI.

[Ryan Lahfa]

Oh! I am a twit. It shouldn't be haveI -- you need to change them to letI.

Is there some docs on what's the difference between them?

[Ryan Lahfa]

And it worked! :D

[Kevin Buzzard]

you use let to define data and have to define proofs.

[Kevin Buzzard]

Because principal_ideal_domain extends integral_domain, it's data.

[Kevin Buzzard]

The term of type principal_ideal_domain int contains all the data of the multiplication etc.

[Ryan Lahfa]

Okay I got it!

[Patrick Massot]

My advisor told me that it'd be interested to go this way in order to develop https://en.wikipedia.org/wiki/Berkovich_space in Lean.

Who is your advisor? Antoine?

[Ryan Lahfa]

My advisor told me that it'd be interested to go this way in order to develop https://en.wikipedia.org/wiki/Berkovich_space in Lean.

Who is your advisor? Antoine?

Frédéric Paugam (I'm not in PhD)

[Patrick Massot]

I didn't know Frédéric was interested in Lean!

[Patrick Massot]

Are you a M2 student?

[Ryan Lahfa]

Are you a M2 student?

I'm in L3 :D…

[Patrick Massot]

Doing Berkovich spaces? Interesting...

[Ryan Lahfa]

I didn't know Frédéric was interested in Lean!

Frédéric Le Roux is also working on metric spaces in Lean IIRC, he wants to redo limits/etc without using uniform spaces so that it can be closer to what students know AFAIK.

[Ryan Lahfa]

Doing Berkovich spaces? Interesting...

Too much free time… :D

[Patrick Massot]

Yes, I know that Frédéric is interested in Lean, I didn't know about Paugam.

[Patrick Massot]

Lean is very good software for students who have too much free time.

[Ryan Lahfa]

Definitely agreed!