Zulip Chat Archive

Stream: maths

Topic: filters inf inf


view this post on Zulip Patrick Massot (Jun 16 2018 at 11:39):

@Johannes Hölzl I have difficulties setting up my uniform space structure on topological groups. Basically the trouble is the definition involves dependent nested infimum. I tried to mimick the metric space case where you wrote:

uniformity := ( ε>0, principal {p:α×α | dist p.1 p.2 < ε}),

(nested inf is somewhat hidden but still there). Question 1: would it be a good idea to rather use the subtype of positive real number as the indexing set?

view this post on Zulip Patrick Massot (Jun 16 2018 at 11:40):

So, in the context of a topological add group R, I wrote, with obvious notations:

uniformity  :=  U  nhd_zero R, principal {p : R×R | p.2 - p.1  U}

view this post on Zulip Patrick Massot (Jun 16 2018 at 11:41):

But again this is somewhat inconvenient to use.

view this post on Zulip Patrick Massot (Jun 16 2018 at 11:41):

I have the following lemma, which is a restatement of something already there:

view this post on Zulip Patrick Massot (Jun 16 2018 at 11:41):

lemma filter.mem_sets_of_mem_infi {α : Type*} {ι : Sort*} {f : ι  filter α} {A : set α}
  (h : directed () f) (ne : nonempty ι) : A  ( i,f i).sets   i, A  (f i).sets :=
begin
  intro H,
  finish [infi_sets_eq]
end

view this post on Zulip Patrick Massot (Jun 16 2018 at 11:42):

but already I'd like to deduced ne from existence of A

view this post on Zulip Patrick Massot (Jun 16 2018 at 11:43):

And then I need a version for dependent nested inf that, I think, would be something like:

lemma filter.mem_sets_of_mem_infi' {α : Type*} {ι : Sort*} {P : ι  Prop} {f : Π i, P i  filter α} {A : set α}
  (H : A  ( i,  h : P i, f i h).sets) :  i,  h : P i, A  (f i h).sets :=

but with some directedness assumption somewhere

view this post on Zulip Patrick Massot (Jun 16 2018 at 11:44):

Any help would be appreciated

view this post on Zulip Chris Hughes (Jun 16 2018 at 12:56):

I tried to prove it, but then realised it wasn't true.

import data.analysis.filter
open set list filter lattice

lemma filter.mem_sets_of_mem_infi' {α : Type*} {ι : Sort*} {P : ι  Prop} {f : Π i, P i  filter α} {A : set α}
  (H : A  ( i,  h : P i, f i h).sets) :  i,  h : P i, A  (f i h).sets := sorry

lemma proof_of_false : false :=
let x, hx := @filter.mem_sets_of_mem_infi'  empty empty.elim (λ i, i.elim) set.univ (by simp) in
x.elim

view this post on Zulip Chris Hughes (Jun 16 2018 at 12:57):

Not sure how helpful that is.

view this post on Zulip Chris Hughes (Jun 16 2018 at 13:11):

Probably need A ≠ univ, because univ is in every filter, but you might as well just have nonempty ι, which is implied by A ≠ univ,

view this post on Zulip Reid Barton (Jun 16 2018 at 13:17):

but already I'd like to deduced ne from existence of A

You should be deducing ne from the fact that f is directed, but I guess mathlib's definition leaves out that condition, oops.

view this post on Zulip Reid Barton (Jun 16 2018 at 13:32):

Apparently not assuming that a directed set is nonempty is a Bourbaki thing.

view this post on Zulip Reid Barton (Jun 16 2018 at 13:36):

@Patrick Massot There is

lemma infi_sets_eq' {f : β  filter α} {s : set β} (h : directed_on (λx y, f x  f y) s) (ne : i, i  s) :
  ( is, f i).sets = ( i  s, (f i).sets)

view this post on Zulip Johannes Hölzl (Jun 16 2018 at 15:27):

Hm, I think you don't need the infimum at all, it should be possible to use vmap and nhds_zero:
uniformity := vmap (fun p, p.1 - p.2) (nhds_zero R)

view this post on Zulip Patrick Massot (Jun 16 2018 at 19:27):

Oh. That's a completely different start

view this post on Zulip Patrick Massot (Jun 16 2018 at 19:27):

But maybe it's more natural

view this post on Zulip Patrick Massot (Jun 16 2018 at 19:27):

It means I need to learn a completely new set of lemmas

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:24):

It's worse than my original method

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:24):

I can't prove any single property

view this post on Zulip Mario Carneiro (Jun 16 2018 at 20:25):

like what?

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:41):

like principal id_rel ≤ vmap (λ (p : R × R), p.fst - p.snd) (nhds 0)

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:41):

and tendsto prod.swap (vmap (λ (p : R × R), p.fst - p.snd) (nhds 0)) (vmap (λ (p : R × R), p.fst - p.snd) (nhds 0))

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:42):

filter.lift' (vmap (λ (p : R × R), p.fst - p.snd) (nhds 0)) (λ (s : set (R × R)), comp_rel s s) ≤ vmap (λ (p : R × R), p.fst - p.snd) (nhds 0)

view this post on Zulip Mario Carneiro (Jun 16 2018 at 20:42):

I assume you know nhds_zero = nhds 0?

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:42):

and ∀ (s : set R), topological_space.is_open _inst_2 s ↔ ∀ (x : R), x ∈ s → {p : R × R | p.fst = x → p.snd ∈ s} ∈ (vmap (λ (p : R × R), p.fst - p.snd) (nhds 0)).sets

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:43):

Johannes suggestion doesn't use nhds_zero (which I defined earlier by def nhd_zero := (nhds (0 : R)).sets)

view this post on Zulip Mario Carneiro (Jun 16 2018 at 20:44):

What do you mean? I see nhds_zero in his post

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:44):

this is based on him incorrectly guessing my definition

view this post on Zulip Mario Carneiro (Jun 16 2018 at 20:45):

For the first one, you have tendsto_iff_vmap

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:45):

he probably thought I had def nhd_zero := nhds (0 : R)

view this post on Zulip Mario Carneiro (Jun 16 2018 at 20:45):

Well, nhds_zero has a special place in the theory of top groups

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:45):

Indeed the first thing I wrote is rw tendsto_vmap_iff

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:46):

I also tried rw tendsto_iff_vmap,

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:47):

but then I'm stuck

view this post on Zulip Mario Carneiro (Jun 16 2018 at 20:47):

then use that - is continuous

view this post on Zulip Mario Carneiro (Jun 16 2018 at 20:47):

continuous.tendsto

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:55):

I'd love to continue this discussion but I must leave at 6:30 tomorrow morning to get a plane to go to a conference in Cagliari

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:55):

so I should sleep

view this post on Zulip Patrick Massot (Jun 16 2018 at 20:55):

thank you very much for these hints

view this post on Zulip Johannes Hölzl (Jun 17 2018 at 14:15):

I guessed nhds_zero from your equation uniformity := ⨅ U ∈ nhd_zero R, principal {p : R×R | p.2 - p.1 ∈ U}.
(by the way: why is it okay to call the support type of a group R but not alpha?)

There are two important rules to convert between map and vmap: map_le_iff_le_vmap, and map_eq_vmap_of_inverse.

To prove the first rule use the rule map_le_iff_le_vmap to move the- to the left side, then using rewriting to end up with principal {a | a = 0} = pure 0 <= nhds 0.

The second rule (using prod.swap): use map_le_iff_le_vmap, and then map_comp the left side by (fun x, - x) o (fun p, p.1 - p.2) Then use tendsto_vmap (together with tendsto_comp).

And for the last one I guess we want to use vmap_eq_lift' (which essentially proofs that your and my definition are the equal)

view this post on Zulip Johannes Hölzl (Jun 17 2018 at 19:43):

https://gist.github.com/johoelzl/ca90562c46b49a1bbb1be36272ec3b1a
transitivity, i.e. the uniform_space.comp rule, is a little bit harder to show

view this post on Zulip Johannes Hölzl (Jun 17 2018 at 19:45):

Would you suggest any changes to this? if not I will just add this to mathlib


Last updated: May 09 2021 at 09:11 UTC