member of cartesian product of sets

Stream: new members

[Ashwin Iyengar]

I'm struggling to understand why this (contrived example) doesn't compile, I don't understand how sets work really:

import analysis.normed_space.basic

variables (S R : Type*) [normed_ring R]

lemma x (f : S → R) (r : set S × S) : true :=
begin
  have : ∃ x ∈ r, ∥f x.1∥ = ∥f x.2∥ := sorry
end

[Kevin Buzzard]

I think this is just the Lean 3 parser giving up on you rather than any misunderstanding on your part.

[Johan Commelin]

lemma x (f : S → R) (r : set (S × S)) : true :=
begin
  have : ∃ (x : S × S) (hx : x ∈ r), ∥f x.1∥ = ∥f x.2∥ := sorry
end

[Johan Commelin]

Note that you had another problem. Lean parses the type of r as (set S) × S

[Ashwin Iyengar]

Oh I see, so the point is that membership is a proposition?

[Johan Commelin]

yes

[Ashwin Iyengar]

Cool thanks

[Kevin Buzzard]

#print notation × -- _ `×`:35 _:34 := prod #1 #0 -- \times has a meagre binding power of 35, and set is a function so has a binding power of something like 1000.

[Ashwin Iyengar]

Hm okay does this nonarchimedean_normed_ring.ultrametric look like a reasonable statement then? It compiles but I'm not sure I'm using everything correctly.

import analysis.normed_space.basic
import ring_theory.power_series.basic

open filter

noncomputable theory
open_locale big_operators

class nonarchimedean_normed_ring (R : Type*) extends normed_ring R :=
(ultrametric_inequality : ∀ x y : R, ∥x + y∥ ≤ (max ∥x∥ ∥y∥))

variables {R : Type*} [normed_ring R]

lemma nonarchimedean_normed_ring.ultrametric {S : set R} {t : finset S} {n : nonempty S} (m: S → R) :
  ∃ x : S, ∥∑ p in t, m p∥ ≤ ∥m x∥ ∧ ∀ y : S, ∥m y∥ ≤ ∥m x∥ :=
begin
  sorry
end

[Kevin Buzzard]

Functions seem to have binding power 1024 by the way:

variables (f : ℕ → ℤ) (a b : ℕ)

def moo : ℕ → ℕ → ℕ := λ a b, 0

notation a `★`:1025 b := moo a b -- will fail if you lower this to 1024

#check f a ★ b -- works

[Johan Commelin]

For exactly this reason of binding powers, you shouldn't need () around max here:

(ultrametric_inequality : ∀ x y : R, ∥x + y∥ ≤ (max ∥x∥ ∥y∥))

[Johan Commelin]

The lemma statement looks a bit non-idiomatic too me...

[Johan Commelin]

I would replace {S : set R} by {S : Type*}

[Johan Commelin]

And use [nonempty S]

[Kevin Buzzard]

I'm not sure it's true as it stands. What about if S is infinite, m is unbounded, and t is empty?

[Kevin Buzzard]

And also what Johan says -- S doesn't need to be anything to do with R. I think you want that t is nonempty.

[Ashwin Iyengar]

Sorry I'm confused, basically there should only be S, I wanted t to be a proof that S is finite, but I think I'm misinterpreting what a finset is

[Kevin Buzzard]

t : finset S means t is a finite subset of S. Maybe you want hS : S.finite then

[Kevin Buzzard]

except that because you don't even need S to be a set, you maybe want a random nonempty finite type S.

[Kevin Buzzard]

lemma nonarchimedean_normed_ring.ultrametric {ι : Type*} [fintype ι]
[nonempty ι] (m: ι → R) :
  ∃ x : ι, ∥∑ p, m p∥ ≤ ∥m x∥ ∧ ∀ y : ι, ∥m y∥ ≤ ∥m x∥ :=
begin
  sorry
end

hopefully that's true.

[Johan Commelin]

But actually, the version with s : finset \iota will probably be more useful in practice.

[Kevin Buzzard]

set S is the type of subsets of S, finset S is the type of finite subsets of S, set.finite is a predicate on set S saying "I am finite", fintype is a predicate on Type saying "I am finite".

[Johan Commelin]

So the I would drop the [fintype \iota], replace [nonempty \iota] by (hs : s.nonempty) and \ex x : \iota by \ex x \in s.

[Kevin Buzzard]

with s : finset iota

[Kevin Buzzard]

I totally agree that this is confusing and that there is no obvious reference to point to.

[Ashwin Iyengar]

Thanks that clarifies things! Then this gives an error still

lemma nonarchimedean_normed_ring.ultrametric {ι : Type*} {S : finset ι} (hS : S.nonempty) (m : S → R) :
  ∃ x ∈ S, ∥∑ p, m p∥ ≤ ∥m x∥ ∧ ∀ y ∈ S, ∥m y∥ ≤ ∥m x∥ :=
begin
  sorry
end

[Ashwin Iyengar]

Apparently I can't make a map out of a finset... I guess it's not a type

[Kevin Buzzard]

Maybe you want m : iota -> R

[Ashwin Iyengar]

But then presumably m has to be defined on all of \iota, when I would just want it to be defined on S

[Kevin Buzzard]

S : finset iota is a term not a type, it has type finset iota. Types have type Type. But clearly you sometimes want to think of S as a type in itself, the type of elements of S, so there is a way to coerce it into a type, but it involves up-arrows because nobody fixed it yet.

[Kevin Buzzard]

If you only want m to be defined on S then you could go with my [fintype iota] suggestion. But Johan's point is that actually if you think you have a map defined only on S, you might well find that Lean will happily let it be defined on all of iota, even if it involves things like division by 0, because this is some type theory philosophy that maps should be defined on all of a type and return junk values away from the domain of interest.

[Kevin Buzzard]

If you really only want m defined on S then there's no point having iota.

[Kevin Buzzard]

1/0=0, sup of the naturals in the reals is 0, as is sup of the empty set etc.

[Kevin Buzzard]

if you're foolish enough to give a set to the real.sup function which isn't non-empty and bounded, you'll get a junk answer rather than an error.

[Johan Commelin]

Ashwin Iyengar said:

Apparently I can't make a map out of a finset... I guess it's not a type

S : finset \iota means that S has type finset \iota. S : Type means that S has type Type. The latter means "S is a type". So indeed, finsets aren't types.
It takes a bit of time to get used to, but really everything only has 1 type.

[Kevin Buzzard]

so similarly here you might think that m is only defined on S but probably it will make sense on all of iota.

[Johan Commelin]

@Ashwin Iyengar for proofs it will be extremely convenient to have m defined on all of \iota, but also have s around as finset.

[Johan Commelin]

It means that you can restrict the sum to a smaller finset, or do induction on the size of the finset, and all the while m : \iota \to R doesn't change.

[Johan Commelin]

Thousands of lines of code about \sum x in s, m s have shown that this model is extremely convenient to work with in practice.

[Ashwin Iyengar]

Okay thanks. Final question, do you imagine that

lemma nonarchimedean_normed_ring.ultrametric {S : finset R} (hS : S.nonempty):
  ∃ x ∈ S, ∥∑ p in S, p∥ ≤ ∥x∥ ∧ ∀ y ∈ S, ∥y∥ ≤ ∥x∥

would be less useful than

lemma nonarchimedean_normed_ring.ultrametric {ι : Type*} {S : finset ι} (hS : S.nonempty) (m : ι → R) :
  ∃ x ∈ S, ∥∑ p in S, m p∥ ≤ ∥m x∥ ∧ ∀ y ∈ S, ∥m y∥ ≤ ∥m x∥

[Kevin Buzzard]

sure

[Kevin Buzzard]

the first is a trivial special case of the second, where two random types are being randomly decreed to be equal despite having nothing to do with each other.

[Kevin Buzzard]

Even if you have a type which you are convinced is equal to R (e.g. a type canonically isomorphic to R), Lean might not let you prove that it's equal to R.

[Kevin Buzzard]

Oh I see, you removed m too.

[Johan Commelin]

I would certainly go for the second version

[Kevin Buzzard]

I would still prove the second.

[Johan Commelin]

The proof will be just as long as that of the first, but it will be much easier to apply the second version

[Ashwin Iyengar]

Okay thanks, maybe to convince myself I'll compare how hard it is to apply the first one vs the second one in my proof that you can multiply restricted power series

[Johan Commelin]

(Note that when you apply the second version, usually lean will figure out automatically what \iota and m are. But with the first version you will hit situations quickly where you want to apply it, but lean will say "nope")

[Kevin Buzzard]

Ashwin, if you think that $R[1/fg]=R[1/f][1/g]$ then your notion of what equality is is not the same as Lean's. If you think you have elements of $R$ and they're actually elements of a ring canonically isomorphic to $R$ then you need the map. Experience has shown us that having an index type is a powerful level of abstraction which covers essentially all use cases.

[Kevin Buzzard]

If you really are in the situation where your map is not defined on all of iota, which does occasionally happen, then you just promote S to a type and continue anyway.

[Ashwin Iyengar]

Johan Commelin said:

For exactly this reason of binding powers, you shouldn't need () around max here:

(ultrametric_inequality : ∀ x y : R, ∥x + y∥ ≤ (max ∥x∥ ∥y∥))

Oh btw it doesn't work without the () for some reason

[Ashwin Iyengar]

≤ seems to take priority over the application of max or something

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/parsing.20question.20about.20.60.E2.88.A5x.E2.88.A5.60/near/226744899

[Johan Commelin]

@Ashwin Iyengar ypu, you are right. sorry for making a false claim