filters inf inf

Stream: maths

[Patrick Massot]

@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?

[Patrick Massot]

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}

[Patrick Massot]

But again this is somewhat inconvenient to use.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

Any help would be appreciated

[Chris Hughes]

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

[Chris Hughes]

Not sure how helpful that is.

[Chris Hughes]

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

[Reid Barton]

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.

[Reid Barton]

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

[Reid Barton]

@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) :
  (⨅ i∈s, f i).sets = (⋃ i ∈ s, (f i).sets)

[Johannes Hölzl]

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)

[Patrick Massot]

Oh. That's a completely different start

[Patrick Massot]

But maybe it's more natural

[Patrick Massot]

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

[Patrick Massot]

It's worse than my original method

[Patrick Massot]

I can't prove any single property

[Mario Carneiro]

like what?

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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)

[Mario Carneiro]

I assume you know nhds_zero = nhds 0?

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

What do you mean? I see nhds_zero in his post

[Patrick Massot]

this is based on him incorrectly guessing my definition

[Mario Carneiro]

For the first one, you have tendsto_iff_vmap

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

Indeed the first thing I wrote is rw tendsto_vmap_iff

[Patrick Massot]

I also tried rw tendsto_iff_vmap,

[Patrick Massot]

but then I'm stuck

[Mario Carneiro]

then use that - is continuous

[Mario Carneiro]

continuous.tendsto

[Patrick Massot]

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

[Patrick Massot]

so I should sleep

[Patrick Massot]

thank you very much for these hints

[Johannes Hölzl]

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)

[Johannes Hölzl]

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

[Johannes Hölzl]

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