Zulip Chat Archive

Stream: new members

Topic: WIP: metric spaces tutorial


view this post on Zulip Kevin Buzzard (Apr 06 2020 at 18:13):

I've spent a few hours today trying to knock a metric spaces tutorial into shape because @Ryan Lahfa , @Jason KY. and @Kevin Doran were all independently formalising stuff like this. But I ran into trouble when I got to open sets because to manipulate open sets you need to be able to manipulate sets. So I think we need to roll back a bit and do a basic tutorial about working with sets. Here's how far I got with metric spaces (but as I say we need another tutorial first I think).

--import data.set
--import data.set.finite
import data.real.basic
--import data.finset
--import order.conditionally_complete_lattice
import topology.opens -- remove when finished checking types of things.
-- note: we don't import topology.metric_space.basic, which is
-- mathlib's version of metric spaces

/-! -/
--open_locale classical

open set


/-- A metric space is a set/type X equipped with a real-valued distance function
    satisfying the usual axioms -/
class metric_space (X : Type) :=
(dist : X  X  )
(dist_self :  x : X, dist x x = 0)
(eq_of_dist_eq_zero :  {x y : X}, dist x y = 0  x = y)
(dist_comm :  x y : X, dist x y = dist y x)
(dist_triangle :  x y z : X, dist x z  dist x y + dist y z)

-- Exercise: compare with the definition in all the maths books.
-- Did we leave something out?

-- theorems that we are about to prove about metric spaces go in the metric space namespace
namespace metric_space

-- let X be a metric space
variables {X : Type} [metric_space X]

/-! # Learning to use `linarith`

We left out the axiom that ∀ x y : X, dist x y ≥ 0 in our metric space,
because it can be deduced from the triangle inequality and symmetry!
Let's prove it now, using `linarith`. The `linarith` tactic proves
many "obvious" results involving inequalities as long as the expressions
involved have degree 1. It looks at the hypotheses and tries to prove
the goal. For example if `h : 0 ≤ a + a` is a hypothesis, and the goal
is `⊢ 0 ≤ a`, then `linarith` will close the goal.

Other useful tactics :

`have h := dist_triangle x y x` will create a new hypothesis `h`.

`push_neg` will move `¬` as far to the right as it can, and possibly
remove it. For example if `h : ¬ (a ≤ b)` then `push_neg at h` will change `h` to `b < a`.

`by_contra h` will create a hypothesis `h` saying that the goal is false, and
will replace the goal with `false`. Note that `linarith` can even prove a goal `false` if
the hypotheses are contradictory.

Let's prove some basic things about distances using `linarith`.

-/

theorem dist_nonneg :  (x y : X), 0  dist x y :=
begin
  --replace with sorry in tutorial
  intros x y,
  have h := dist_triangle x y x,
  rw dist_self at h,
  rw dist_comm y x at h,
  linarith,
end

theorem dist_le_zero {x y : X} : dist x y  0  x = y :=
begin
  --replace with sorry in tutorial
  split,
  { intro h,
    have h2 := dist_nonneg x y,
    apply eq_of_dist_eq_zero,
    linarith,
  },
  { intro h,
    rw h,
    rw dist_self,
  }
end

theorem dist_pos {x y : X} : 0 < dist x y  x  y :=
begin
  --replace with sorry in tutorial
  split,
  { intro h,
    intro hxy,
    rw dist_le_zero at hxy,
    linarith,
  },
  { intro h,
    by_contra h2,
    push_neg at h2,
    rw dist_le_zero at h2,
    contradiction,

  }
end

/-! ### Open balls

We define `ball x ε` to be the open ball centre `x` and radius `ε`. Note that we do not
require `ε > 0`! That hypothesis shows up later in the theorems, not in the definition.


-/

variables {x y z : X} {ε ε₁ ε₂ : } {s : set X}

/-- `ball x ε` is the set of all points `y` with `dist y x < ε` -/
def ball (x : X) (ε : ) : set X := {y | dist y x < ε}

-- Let's tag this lemma with the `simp` tag, so the `simp` tactic will use it.
@[simp] theorem mem_ball : y  ball x ε  dist y x < ε := iff.rfl -- true by definition

-- Now we get this proof for free:
theorem mem_ball_comm : x  ball y ε  y  ball x ε :=
begin
  simp [dist_comm]
end

-- Let's tag `dist_self` with the `simp` tag too:

attribute [simp] dist_self

-- Can you find a proof of this? And then can you find a one-line proof using `simp`?
theorem mem_ball_self (h : 0 < ε) : x  ball x ε :=
begin
  --replace with sorry
  rw mem_ball,
  rw dist_self,
  exact h,
end

/- Top tip: `rw mem_ball at hy ⊢` will rewrite `mem_ball` at both the hypothesis `hy` and the goal.
  Get `⊢` in VS Code with `\|-`

-/
theorem ball_mono (h : ε₁  ε₂) : ball x ε₁  ball x ε₂ :=
begin
  -- delete me
  intros y hy,
  rw mem_ball at hy ,
  linarith,
end


/-! # Open sets.

A subset of a metric space is open if for every element `s` in the subset, there's some open
ball `ball s ε`, with ε > 0, entirely contained with `S`.
-/

/-- A subset U of a metric space is open if every s ∈ U there's an open ball centre s within U -/
def is_open (U : set X) :=  s  U,  (ε : ) ( : 0 < ε), ball s ε  U

-- Note that `is_open` is a Proposition. Things like `is_open_Union` below are proofs.

-- Let's start with two easy facts about open sets -- the empty set and the whole space is open.
theorem is_open_empty : is_open ( : set X) :=
begin
  intro x,
  intro hx,
  cases hx,-- too hard for a beginner. Need to get a contradiction from `h : x ∈ ∅`
end

theorem is_open_univ : is_open (univ : set X) :=
begin
  intro x,
  intro hx,
  use 37,
  split,
    norm_num,
  -- need subset_univ
  simp,
end

-- An arbitrary union of open sets is open. The union is indexed over an auxiliary type ι

-- TODO: I don't think this is any good, people need to know about set.subset.trans,
-- set.subset.Union etc. Should do something on sets first?

theorem is_open_Union (ι : Type) (f : ι  set X) (hf :  (i : ι), is_open (f i)) :
  is_open ( (i : ι), f i) :=
begin
  intro x,
  intro hx,
  rcases hx with U, i, rfl, hxU,
  have h := hf i x hxU,
  rcases h with ε, , hxε,
  use ε,
  split, use ,
  refine set.subset.trans hxε _,
  apply set.subset_Union,
end

theorem is_open_inter {U V : set X}  (hU : is_open U) (hV : is_open V) : is_open (U  V) := sorry




/- A subset S of a metric space is closed if its complement is open -/
def is_closed (S : set X) := is_open (-S)

end metric_space

#exit

-- the lemmas from 274 to 300:
theorem closed_ball_subset_closed_ball {α : Type u} [metric_space α] {ε₁ ε₂ : } {x : α} (h : ε₁  ε₂) :
  closed_ball x ε₁  closed_ball x ε₂ :=
λ y (yx : _  ε₁), le_trans yx h

theorem ball_disjoint (h : ε₁ + ε₂  dist x y) : ball x ε₁  ball y ε₂ =  :=
eq_empty_iff_forall_not_mem.2 $ λ z h₁, h₂,
not_lt_of_le (dist_triangle_left x y z)
  (lt_of_lt_of_le (add_lt_add h₁ h₂) h)

theorem ball_disjoint_same (h : ε  dist x y / 2) : ball x ε  ball y ε =  :=
ball_disjoint $ by rwa [ two_mul,  le_div_iff' two_pos]

theorem ball_subset (h : dist x y  ε₂ - ε₁) : ball x ε₁  ball y ε₂ :=
λ z zx, by rw  add_sub_cancel'_right ε₁ ε₂; exact
lt_of_le_of_lt (dist_triangle z x y) (add_lt_add_of_lt_of_le zx h)

theorem ball_half_subset (y) (h : y  ball x (ε / 2)) : ball y (ε / 2)  ball x ε :=
ball_subset $ by rw sub_self_div_two; exact le_of_lt h

theorem exists_ball_subset_ball (h : y  ball x ε) :  ε' > 0, ball y ε'  ball x ε :=
⟨_, sub_pos.2 h, ball_subset $ by rw sub_sub_self

theorem ball_eq_empty_iff_nonpos : ε  0  ball x ε =  :=
(eq_empty_iff_forall_not_mem.trans
⟨λ h, le_of_not_gt $ λ ε0, h _ $ mem_ball_self ε0,
 λ ε0 y h, not_lt_of_le ε0 $ pos_of_mem_ball h).symm

@[simp] lemma ball_zero : ball x 0 =  :=
by rw [ metric.ball_eq_empty_iff_nonpos]

--

-- Do we want this?
theorem eq_of_forall_dist_le {x y : α} (h : ε, ε > 0  dist x y  ε) : x = y :=
eq_of_dist_eq_zero (eq_of_le_of_forall_le_of_dense dist_nonneg h)

/-- The triangle (polygon) inequality for sequences of points; `finset.range` version. -/
lemma dist_le_range_sum_dist (f :   α) (n : ) :
  dist (f 0) (f n)  (finset.range n).sum (λ i, dist (f i) (f (i + 1))) :=
finset.Ico.zero_bot n  dist_le_Ico_sum_dist f (nat.zero_le n)

-- From mathlib
https://github.com/leanprover-community/mathlib/blob/17632202cdf9682cea972e86437d32ac20c91b06/src/topology/basic.lean#L262-L319

def closure (s : set α) : set α := ⋂₀ {t | is_closed t  s  t}

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 18:15):

My plan was to prove that closure was a Galois insertion. This comes out quite nicely.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:16):

@Kevin Buzzard Wow! Didn't know about the ⊢ trick!

But definitely, a set tutorial would be awesome, I do some stuff which might not be considered optimal by Lean seniors :)

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 18:16):

But others might want to try other things. Perhaps one should do a series of three things: first a basic thing on sets, and then something on open and closed sets including def of metric space, and then a third one on basic stuff with limits of sequences perhaps, or stick to the real numbers or whatever.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:18):

Kevin Buzzard said:

But others might want to try other things. Perhaps one should do a series of three things: first a basic thing on sets, and then something on open and closed sets including def of metric space, and then a third one on basic stuff with limits of sequences perhaps, or stick to the real numbers or whatever.

Proving Bolzano-Weierstrass as a final result would quite awesome I think, it's one of the most powerful & non-trivial theorems you first learn as an undergraduate in real analysis (in France, at least AFAIK).
(well, there is also Heine theorem on uniform continuity over closed bounded intervals, i.e. compacts)

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:19):

But that would require sticking to real numbers, and this is still possible to revisit the result in a 4th section if even necessary

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:20):

@Kevin Buzzard Could we help you to write the tutorial?

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 18:32):

Sure, that's why I posted here.

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 18:33):

Ideally we would push them all to the tutorial project. Building up to something like BW would be very cool and of course it's possible to do in Lean, but a beginner wouldn't be able to do it without some help.

view this post on Zulip Patrick Massot (Apr 06 2020 at 18:35):

You can push to branch in the tutorial repository (if you don't have enough access we can investigate).

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 18:35):

oh so it's like mathlib for someone like me?

view this post on Zulip Patrick Massot (Apr 06 2020 at 18:36):

As I wrote yesterday, I plan do to the same thing with my first year course, which focuses entirely on real numbers. So I think you should keep it at metric space level, with special emphasis on:

  • using structures and classes
  • setting up a theory, including simp lemmas

neither of those points are covered in my first year stuff.

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 18:37):

OK. What about handling sets in general, e.g. subset_union or whatever?

view this post on Zulip Patrick Massot (Apr 06 2020 at 18:38):

I don't have any of that.

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 18:38):

OK so for now I'll think about basic stuff with subsets, and then general metric spaces.

view this post on Zulip Patrick Massot (Apr 06 2020 at 18:38):

My part will be about handling logical connective and various kinds of reasonning

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:41):

Kevin Buzzard said:

OK so for now I'll think about basic stuff with subsets, and then general metric spaces.

It might be hard to do, but a classical final boss of set theory is Cantor-Bernstein-Schröder, it requires some help though for a beginner

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:41):

(but it'd need to introduce injective, surjective, bijective stuff… Unsure if it is wise.)

view this post on Zulip Patrick Massot (Apr 06 2020 at 18:52):

I'm not sure that would teach much Lean at that point.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:54):

Well, there is also mathlib API to learn too

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:54):

Documentation is pretty great (there are few pain points) so I'm not sure if that's necessary at all

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 19:01):

If we're doing open sets then we need to show the users how to prove the axioms for a topology, and these proofs seem to rely on a basic understanding of how to manipulate sets

view this post on Zulip Patrick Massot (Apr 06 2020 at 19:05):

Yes, sure. I was specifically referring to Cantor-Bernstein.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 19:10):

Patrick Massot said:

Yes, sure. I was specifically referring to Cantor-Bernstein.

BTW, is Cantor Bernstein in mathlib?

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 19:10):

(docs would benefit if we could search by alternative names of big theorems or look for a theorem and get its generalization, I should open an issue)

view this post on Zulip Patrick Massot (Apr 06 2020 at 19:13):

Did you really search?

view this post on Zulip Patrick Massot (Apr 06 2020 at 19:13):

There is a file name giving you a hint...

view this post on Zulip Johan Commelin (Apr 06 2020 at 19:13):

@Ryan Lahfa PRs that add alternative names to docstrings are very welcome! (And they will usually get merged before you can reload your page :wink:)

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 19:14):

Patrick Massot said:

Did you really search?

I definitely searched for "Cantor" and "Cantor-Bernstein", but I should have searched for something else, I suppose, in set_theory and cardinals (?)

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 19:15):

Johan Commelin said:

Ryan Lahfa PRs that add alternative names to docstrings are very welcome! (And they will usually get merged before you can reload your page :wink:)

Sounds something I can do :)

view this post on Zulip Patrick Massot (Apr 06 2020 at 19:16):

https://leanprover-community.github.io/mathlib_docs/set_theory/schroeder_bernstein.html

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 19:16):

Ryan Lahfa said:

Patrick Massot said:

Did you really search?

I definitely searched for "Cantor" and "Cantor-Bernstein", but I should have searched for something else, I suppose, in set_theory and cardinals (?)

→ schroeder_bernstein :D — I should have searched for bernstein I guess ; in France, we call it Cantor-Bernstein

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 19:18):

If I wanted to see where is Banach-Tarski-Hausdorff paradox, where would I expect to find it?

view this post on Zulip Johan Commelin (Apr 06 2020 at 19:29):

I don't think it's there yet. But I guess it would be somewhere in measure_theory/

view this post on Zulip Patrick Massot (Apr 06 2020 at 19:31):

That could be a fun project for you.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 19:38):

Patrick Massot said:

That could be a fun project for you.

Definitely :-)

view this post on Zulip David Wärn (Apr 06 2020 at 19:55):

Is there something like the Vitali set to show that not every set of reals is measurable?

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 20:11):

Highly unlikely

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 20:11):

They're not into examples in mathlib

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 20:15):

git grep -i Vitali

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 20:16):

It is in measure_theory/lebesgue_measure but it is in a comment, so possibly it doesn't work with current mathlib.

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 20:17):

You can move it to examples and PR

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 20:17):

Then move it back if you'll need it for some proof.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 20:31):

Johan Commelin said:

I don't think it's there yet. But I guess it would be somewhere in measure_theory/

I will need some isometry stuff, I see metric_space/isometry, but, is there any notion of orientation (direct/indirect) isometries?
I tried to grep for direct in the file but no result.

view this post on Zulip Johan Commelin (Apr 06 2020 at 20:39):

I don't know anything about this kind of maths

view this post on Zulip Johan Commelin (Apr 06 2020 at 20:40):

What is a direct/indirect isometry?

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 20:45):

Johan Commelin said:

What is a direct/indirect isometry?

Oh, sorry, if f:ABf : A \to B is an isometry between euclidean affine spaces, we say that ff is direct when the linear part of ff is of determinant 1, IIRC.

Basically, ff preserves the orientation of the space.

view this post on Zulip Johan Commelin (Apr 06 2020 at 20:45):

Aah, ok. In that case I knew the concept :lol:

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 20:47):

Probably you'll need to define SO(n)

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 20:48):

We have SL(n) in linear_algebra/special_linear_group

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 20:53):

Johan Commelin said:

Aah, ok. In that case I knew the concept :lol:

I attempted the dangerous game of direct (without pun) translation from French to English :D

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 20:53):

Yury G. Kudryashov said:

Probably you'll need to define SO(n)

Yes, I'll definitely need SOn\mathrm{SO}_n

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 21:03):

Then you'll deal with SOnSO_n, not isometry.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 21:09):

Yury G. Kudryashov said:

Then you'll deal with SOnSO_n, not isometry.

Definitely, but I need to glue SOnSO_n and isometry, right? At least, I just need to know that an element of OnO_n is an isometry.

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 21:09):

Yes, but you don't have to define "orientation preserving" for isometries.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 21:11):

Agreed

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 21:11):

BTW, you'll need to redefine euclidean_space. Right now it is define somewhere in geometry/ to help defining manifolds, and it has sup-norm instead of an inner_product_space structure.

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 21:15):

Something like instance [fintype n] : has_inner (n → real) := ⟨λ a b, finset.univ.sum (λ i, a i * b i)⟩.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 21:17):

Makes sense

view this post on Zulip Kevin Doran (Apr 06 2020 at 22:35):

As a token learner, I just thought I'd mention that a set tutorial would be much appreciated; I quickly ran into trouble trying to use sets of sets and I didn't find it obvious how to work with them by looking at mathlib etc.

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 23:06):

I pushed some stuff onto a branch of the tutorial project. I need to do other things tomorrow/Wed but hopefully I'll get back to it Thurs. Feel free to help out with some examples or exercises. I thought it was worth figuring out exactly which tactics are needed to prove the set stuff, because the moment we're into metric spaces we're using linarith etc.


Last updated: May 14 2021 at 13:24 UTC