Borsuk Ulam theorem

Stream: new members

[Nguyen Duc Hoan]

Hello, I am trying to formulate Borsuk-Ulam theorem (the theorem in this link: https://en.wikipedia.org/wiki/Borsuk%E2%80%93Ulam_theorem) but I have some questions. Could you please help me?
1. In my code, why do I need two properties has_mem ↥(sphere_Sn n r) (set (fin (n + 1) → ℝ)) and has_neg ↥(sphere_Sn n r) in the theorem?
2. In my code, I use the theorem mem_sphere_Sn to define what is member of sphere_Sn. Moreover, the theorem sym_sphere_Sn defines if p ∈ sphere_Sn then (-p) ∈ sphere_Sn. However, LEAN could not use that properties in the Borsuk_Ulam_theorem. So how to use two theorems mem_sphere_Sn and sym_sphere_Sn into Borsuk_Ulam_theorem?
This is my code

variable n:nat
variable r:real
variable p: fin (n+1) → ℝ

variable [metric_space (fin (n+1) → ℝ)]
variable [vector_space ℝ (fin (n+1) → ℝ)]

def sphere_Sn (n:ℕ) (r:ℝ) : set (fin (n + 1) → ℝ) :=
{y | dist y (0:fin (n+1) → ℝ) = r}


theorem mem_sphere_Sn : p ∈ sphere_Sn n r ↔ dist p (0:fin (n+1) → ℝ) = r := iff.rfl

theorem sym_sphere_Sn : p ∈ sphere_Sn n r ↔ -p ∈ sphere_Sn n r :=sorry

theorem Borsuk_Ulam_theorem (n:ℕ) (r:ℝ) [has_mem ↥(sphere_Sn n r) (set (fin (n + 1) → ℝ))] [has_neg ↥(sphere_Sn n r)]
(f: sphere_Sn n r → (fin n → ℝ)) (h1: continuous f) : ∃ p ∈ sphere_Sn n r, f (-p) = f p
:=sorry

[Kevin Buzzard]

You have a variable p ∈ sphere_Sn n r and you talk about -p, so Lean wants to know what -p means.

[Kevin Buzzard]

Because -p is short for has_neg.neg p Lean comes up with this rather elaborate error about has_neg.

[Kevin Buzzard]

But you cannot solve the problem correctly with [has_neg ↥(sphere_Sn n r)]. That line means "let's just assume we have a completely random function has_neg.neg sending p to -p, about which we know absolutely nothing".

[Kevin Buzzard]

I would imagine that you have a certain function in mind, and you need to tell Lean to use that function.

[Bryan Gin-ge Chen]

This section on inferring notation in TPiL may help.

[Kevin Buzzard]

Every occurrence of [...] in your code is very suspicious to me. They all mean "let's assume we have a random function". For example variable [vector_space ℝ (fin (n+1) → ℝ)] means "Let's assume that the space of functions from fin (n+1) to the reals has a completely arbitrary vector space structure, about which we know nothing at all, other than the fact that it satisfies the axioms of a vector space". We do not even know that the map sending everything to zero will be the zero of the vector space -- we know literally nothing about this structure. What you almost certainly want to do is to tell Lean to use the obvious vector space structure on this type.

[Kevin Buzzard]

Let's start at the beginning. I should say now that I have never used vector spaces in Lean, so I don't know the answer to this question: Is the vector space ℝ^n already built in Lean? I suspect it is, and you should use Lean's pre-built one, which will have the correct vector space structure on it, rather than trying to build your own (which is of course possible, you can define addition and scalar multiplication on (fin (n+1) → ℝ) and then prove all the axioms yourself).

[Kevin Buzzard]

The theory of modules over a ring (and hence vector spaces over a field) changed only a few weeks ago. Are you completely up to date with Lean 3.4.2 release and the current version of mathlib?

[Nguyen Duc Hoan]

yes, I were up to date with Lean 3.4.2 release and the current version mathlib

[Kevin Buzzard]

import data.real.basic algebra.pi_instances algebra.module

variable n : ℕ
definition is_it_there_already : vector_space ℝ (fin (n+1) → ℝ) :=
by apply_instance -- fails

Instead of [vector_space ℝ (fin (n+1) → ℝ)] (which means "put an arbitrary real vector space structure on (fin (n+1) → ℝ)) about which we know nothing"), I am trying to get Lean to guess what vector space structure we want. But I am failing.

[Kevin Buzzard]

So I think we need to start there.

[Kevin Buzzard]

Once we get this right, Lean will know the correct vector space structure on (fin (n+1) → ℝ).

[Nguyen Duc Hoan]

So I need to build vector space structure on (fin (n+1) \to \R)?

[Rob Lewis]

Kevin, either you're missing an import, or this will be added soon. I just tried it in the repo Johannes and I are working on and we have that instance.

[Patrick Massot]

He is missing an import, this has been there forever

[Kevin Buzzard]

I knew for sure that it was there before the module refactor.

[Kevin Buzzard]

@Nguyen Duc Hoan it's OK, the vector space structure is there already, I just appear to have mislaid it.

[Rob Lewis]

Ah, this is the magic instance.

instance discrete_field.to_vector_space {α : Type*} [discrete_field α] : vector_space α α :=
{ .. ring.to_module }

[Kevin Buzzard]

Is this in mathlib?

[Kevin Buzzard]

@Nguyen Duc Hoan we've nearly found it.

[Rob Lewis]

Apparently not, but it will be before long.

[Kevin Buzzard]

Aah, apparently it's too cutting edge :-)

[Kevin Buzzard]

@Patrick Massot :P

[Kevin Buzzard]

;-)

[Kevin Buzzard]

We are finally there!

import data.real.basic algebra.pi_instances algebra.module

instance discrete_field.to_vector_space {α : Type*} [discrete_field α] : vector_space α α :=
{ .. ring.to_module }

variable n : ℕ
noncomputable definition is_it_there_already : vector_space ℝ (fin (n+1) → ℝ) :=
by apply_instance

So you don't need to write the line defining is_it_there_already : this line is just a test to see that Lean can guess that (fin (n+1) → ℝ) is a vector space. But you do need this funny instance line above. I think Patrick is right, this maybe was there before, but there have been a lot of changes to rings and modules recently and maybe this stopped working.

[Kevin Buzzard]

But the point is that you can now remove the line [vector_space ℝ (fin (n+1) → ℝ)] because Lean knows the right vector space structure now.

[Kevin Buzzard]

[you need to add the funny instance line instead -- and in a few weeks' time mathlib will perhaps give you an error on this line with message "this is defined already" and then you can just remove it]

[Kevin Buzzard]

The same story is true with variable [metric_space (fin (n+1) → ℝ)]. This cannot be right, because this means "put a random metric space structure on (fin (n+1) → ℝ). I might use this in the following setting: variables (X : Type) [metric space X] -- this is how you tell Lean "let $X$ be a metric space". It means "let $X$ be a random set, and then put a random metric space structure on $X$". In that context you can see it's the right thing to do -- but in your context you have a very concrete set (fin (n+1) → ℝ) and you almost certainly want the "standard" metric space on that. Now actually here is where we do need @Patrick Massot -- do we have the metric space structure on this set Patrick, or will Nguyen have to build it himself?

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/master/src/topology/metric_space/basic.lean#L915

[Kevin Buzzard]

doh that's there already. So Lean already knows fin (n+1) → ℝ is a metric space. Sorry Patrick, I just assumed that because it had been added as a variable Lean was complaining that it didn't know.

[Sebastien Gouezel]

Warning: the default distance is the sup distance, not the euclidean one.

[Kevin Buzzard]

Oh dear, so we have instead defined the unit cube or something.

[Kevin Buzzard]

OK so @Nguyen Duc Hoan the metric on a product of metric spaces is not the usual Euclidean one, so now you have some decisions to make :-) Will you redefine your sphere, will you use cubes instead (they are homeomorphic to spheres after all) or will you define the usual metric on R^n? Mathlib's inbuilt metric on R^n is not the usual one.

[Kevin Buzzard]

It might be an interesting exercise to define the usual Euclidean metric on R^n, but it might be tricky, and you are also faced with the problem that mathlib already has a metric on R^n and some wise guy made metric_space a class not a structure, meaning that every type is supposed to have at most one metric on it.

[Patrick Massot]

It doesn't matter for Borsuk-Ulam, which is a topological result

[Nguyen Duc Hoan]

OK so @Nguyen Duc Hoan the metric on a product of metric spaces is not the usual Euclidean one, so now you have some decisions to make :-) Will you redefine your sphere, will you use cubes instead (they are homeomorphic to spheres after all) or will you define the usual metric on R^n? Mathlib's inbuilt metric on R^n is not the usual one.

I think I need to redefine the sphere S^n because Lean understand sphere_Sn in function (f : sphere_Sn n r → (fin n → ℝ)) as a Type not as a set. :(

[Kevin Buzzard]

Everything is a type in type theory. You can't really work with sets, they are terms. But a set and the corresponding subtype are exactly the same data.

I was thinking about Patrick's comment. I am not sure that this is a valid way of doing things. I mean, Borsuk-Ulam is a theorem about spheres. You could formalise it as a theorem about hollow cubes, because cubes are spheres topologically, but if you don't formalise the proof of this statement as well then one could argue that you have not formalised Borsuk-Ulam in the sense that you have not formalised something which is provably, in Lean, equivalent. The problem with formalising something which "mathematicians can prove is equivalent" is that you could formalise it as true, which is mathematically equivalent to Borsuk-Ulam because mathematicians can prove that Borsuk-Ulam is true.

On the other hand I'm not sure you need to prove that R^n is a metric space. Why not just define S^n to be the points in R^{n+1} such that the sum of the squares of the coefficients is 1?

[Nguyen Duc Hoan]

Actually, I don't know how to get the coefficients of a point in R^n?

[Johan Commelin]

It is a function... so you evaluate it on i : fin n

[Nguyen Duc Hoan]

Moreover, I want to read more about fin n → ℝ. could you please suggest me which files I should read?

[Johan Commelin]

Hmmm... what would you want to know precisely?

[Johan Commelin]

There is data/fin.lean.

[Nguyen Duc Hoan]

It is a function... so you evaluate it on i : fin n

I mean I want to get x(i) with i = 1..n in x : fin n → ℝ.

[Johan Commelin]

fin n "=" 0 .. (n-1). So you write (i : fin n) in your hypotheses; and then you can just use x(i) later on.

[Nguyen Duc Hoan]

fin n "=" 0 .. (n-1). So you write (i : fin n) in your hypotheses; and then you can just use x(i) later on.

Thank you! I got it! :D

[Nguyen Duc Hoan]

Everything is a type in type theory. You can't really work with sets, they are terms. But a set and the corresponding subtype are exactly the same data.

I was thinking about Patrick's comment. I am not sure that this is a valid way of doing things. I mean, Borsuk-Ulam is a theorem about spheres. You could formalise it as a theorem about hollow cubes, because cubes are spheres topologically, but if you don't formalise the proof of this statement as well then one could argue that you have not formalised Borsuk-Ulam in the sense that you have not formalised something which is provably, in Lean, equivalent. The problem with formalising something which "mathematicians can prove is equivalent" is that you could formalise it as true, which is mathematically equivalent to Borsuk-Ulam because mathematicians can prove that Borsuk-Ulam is true.

On the other hand I'm not sure you need to prove that R^n is a metric space. Why not just define S^n to be the points in R^{n+1} such that the sum of the squares of the coefficients is 1?

I tried to write the function of sum of squares the coefficients of R^{n+1}. However I got many errors, could you please give me some advice?

def sum_of_square_coeff (n : ℕ) {x: fin n → ℝ} [has_zero (fin n)] : ℝ
| 0 := x(0)*x(0)
| (succ n) := (sum_coeff1 (n-1) (x: fin (n-1) → ℝ))*(sum_coeff1 (n-1) (x: fin (n-1) → ℝ))  + (x(n))*x((n))

[Johan Commelin]

@Nguyen Duc Hoan What exactly do you want to do? In math language, do you want: $\sum_{i=0}^{n-1} f(i)^2$? If so, you can use something like

def sum_of_square_coeff (n : ℕ) {x: fin n → ℝ} : ℝ := finset.sum univ (\lam i, f(i)^2)

[Johan Commelin]

Note that you need to fix the \lam into a proper lambda. This code depends on finset.sum which is in mathlib. If you don't want to depend on mathlib, then you can try to roll your own definition using recursion, like you did above. But it will be somewhat ugly, because you have to restrict f to fin (n-1), but of course this isn't really a restriction, because it doesn't make sense in type theory to say that fin (n-1) is a subset of fin n.

[Nguyen Duc Hoan]

I want to compute $x_0^2 + x_1^2 +...+x_n^2$ where $X \in R^n \text{ and } X = (x_0, x_1,...,x_{n-1})^T$

[Kevin Buzzard]

You have an undefined $x_n$ there :-) Doesn't Johan's code do what you want though?

[Nguyen Duc Hoan]

I don't understand the function "finset.sum". Where can I find the function "finset.sum" in mathlib? I couldn't find :(

[Johan Commelin]

@Nguyen Duc Hoan Voila: https://github.com/leanprover-community/mathlib/blob/master/src/algebra/big_operators.lean#L28

[Kevin Buzzard]

import data.real.basic

open finset

def sum_of_square_coeff (n : ℕ) {x: fin n → ℝ} : ℝ :=
sum univ (λ i, (x i)^2)

[Nguyen Duc Hoan]

Yes, that is what I want. Thank you! :grinning_face_with_smiling_eyes:

[Nguyen Duc Hoan]

Hello again, I defined the sphere S^n in Lean. I used the theorem mem_sphere_Sn to define what is member of sphere S^n, and the theorem sym_sphere_Sn to define if x ∈ sphere_Sn then (-x) ∈ sphere_Sn. However, I got some problems with these theorems. Could you please help me?

import init.data.nat data.real.basic

open finset

variable (n: nat)

def sum_of_square_coeff {n:ℕ} (x: fin n → ℝ) : ℝ :=
sum univ (λ i, (x i)^2)

def sphere_Sn (n:ℕ) : set (fin (n+1)→ ℝ) := {x| sum_of_square_coeff x = 1}

variable x: fin (n+1) → ℝ

theorem mem_sphere_Sn :  ∀ x ∈ sphere_Sn n ↔ (sum_of_square_coeff x = 1) := sorry

theorem sym_sphere_Sn : ∀ x ∈ sphere_Sn n ↔ (-x) ∈  sphere_Sn n :=sorry

[Rob Lewis]

There are a few issues. Luckily they're easy to fix. Instead of writing ∀ x ∈ sphere_Sn n ↔ (sum_of_square_coeff x = 1), you should write ∀ x, x ∈ sphere_Sn n ↔ (sum_of_square_coeff x = 1). (You could also move the x to the left of the :.) Also, with the imports you have, Lean doesn't know what -x means. You need to include something from mathlib that adds the right instance. import algebra.pi_instances will work.

[Rob Lewis]

Your first theorem has a very easy proof.

theorem mem_sphere_Sn :  ∀ x, x ∈ sphere_Sn n ↔ (sum_of_square_coeff x = 1) :=
λ x, iff.refl _

The second one will take you slightly more work.

[Nguyen Duc Hoan]

Thank you! Let me try to prove the second theorem.

[Nguyen Duc Hoan]

Hello again,
I tried to prove a theorem that is x : fin n→ ℝ and sum_of_square_coeff x = 1 then sum_of_square_coeff (-x) = 1. To prove that I tried to find relationship between x and -x in file data/fintype.lean but I could not find anything. Then I had no ideas for proving. Could you please give some hints?
This is my code

import analysis.exponential topology.algebra.infinite_sum
import init.data.nat data.real.basic
import algebra.pi_instances
open finset

variable (n: nat)

def sum_of_square_coeff {n:ℕ} (x: fin n → ℝ) : ℝ :=
sum univ (λ i, (x i)^2)


theorem sum_of_square_coeff_neg_x (x: fin n→ ℝ) (h: sum_of_square_coeff x = 1) : sum_of_square_coeff (-x) = 1 :=
begin

end

[Sebastien Gouezel]

You need to use the fact that the square of -a is the same as the square of a. I asked library_search, and it told me that this is called neg_square. Then you can do a proof by hand. However, it is much more efficient to let the simplifier do the work for you. Just help it a little by telling it that it should expand sum_of_square_coeff, and then it can do everything.

by simpa [sum_of_square_coeff]

The a in simpa tells it to simplify as much as it can, and then try to use some assumption (i.e., some information that is already available in the context) to prove the theorem.

[Kevin Buzzard]

[cue @Mario Carneiro pointing out that this is is not quite what simpa does, even though it's what people always say it's what it does]

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#simpa

[Sebastien Gouezel]

In the version without using or this, it does just use assumption to close the goal, as I said, if I understand the docs. Otherwise, it is more clever.

[Kevin Buzzard]

example (a : ℤ) (this : -(-a) = 5) : a = 5 := by simpa
example (a : ℤ) (that : -(-a) = 5) : a = 5 := by simpa -- fails

Even without mentioning this explicitly, the behaviour of simpa changes if there is a this in the context

[Sebastien Gouezel]

You are right. I did not understand the docs. I read "if present" as "if you provide it in the list of things to simplify", not as "in the context".

[Kevin Buzzard]

I think it's because Mario got sick of typing suffices : blah, simpa using [this]

[Nguyen Duc Hoan]

You need to use the fact that the square of -a is the same as the square of a. I asked library_search, and it told me that this is called neg_square. Then you can do a proof by hand. However, it is much more efficient to let the simplifier do the work for you. Just help it a little by telling it that it should expand sum_of_square_coeff, and then it can do everything.

by simpa [sum_of_square_coeff]

The a in simpa tells it to simplify as much as it can, and then try to use some assumption (i.e., some information that is already available in the context) to prove the theorem.

Did you mean this?

@[simp] def sum_of_square_coeff {n:ℕ} (x: fin n → ℝ) : ℝ :=
sum univ (λ i, (x i)^2)

theorem sum_of_square_coeff_neg_x (x: fin n→ ℝ) (h: sum_of_square_coeff x = 1) : sum_of_square_coeff (-x) = 1 :=
by simpa [sum_of_square_coeff]

I tried but it looks like the problem is not solved. There is no error but lean say that

n : ℕ,
x : fin n → ℝ,
h : sum_of_square_coeff x = 1
⊢ sum_of_square_coeff (-x) = 1

[Johan Commelin]

I don't think you want the @[simp] in front of your def. Unless you always want simp to unfold that definition. In that case you don't have to pass it to simpa in the theorem.

[Kevin Buzzard]

import analysis.exponential topology.algebra.infinite_sum
import init.data.nat data.real.basic
import algebra.pi_instances
open finset

variable (n: nat)

def sum_of_square_coeff {n:ℕ} (x: fin n → ℝ) : ℝ :=
sum univ (λ i, (x i)^2)


theorem sum_of_square_coeff_neg_x (x: fin n→ ℝ) (h: sum_of_square_coeff x = 1) : sum_of_square_coeff (-x) = 1 :=
by simpa [sum_of_square_coeff]

[Kevin Buzzard]

@Nguyen Duc Hoan What you wrote also works. Are you sure you are understanding Lean correctly? If there is no error then everything has worked. Whatever Lean "says" just depends on where you put the cursor.