Operations on uniform limits

Stream: Is there code for X?

[Vincent Beffara]

Do we have this somewhere where I didn't find it? docs#tendsto_uniformly_on.mul is for uniform groups.

variables {ι α 𝕜 : Type*} [normed_field 𝕜] {p : filter ι} [ne_bot p] {K s : set α} {m mf mg : ℝ}
  {F G : ι → α → 𝕜} {f g : α → 𝕜}

lemma tendsto_uniformly_on.inv_of_le (hF : tendsto_uniformly_on F f p s)
  (hm : 0 < m) (hf : ∀ x ∈ s, m ≤ ∥f x∥) :
  tendsto_uniformly_on F⁻¹ f⁻¹ p s := sorry

lemma tendsto_uniformly_on.mul_of_le
  (hF : tendsto_uniformly_on F f p s) (hG : tendsto_uniformly_on G g p s)
  (hf : ∀ᶠ i in p, ∀ x ∈ s, ∥F i x∥ ≤ mf) (hg : ∀ᶠ i in p, ∀ x ∈ s, ∥G i x∥ ≤ mg) :
  tendsto_uniformly_on (F * G) (f * g) p s := sorry

lemma tendsto_uniformly_on.mul_of_bound
  (hF : tendsto_uniformly_on F f p s) (hG : tendsto_uniformly_on G g p s)
  (hf : ∀ x ∈ s, ∥f x∥ ≤ mf) (hg : ∀ x ∈ s, ∥g x∥ ≤ mg) :
  tendsto_uniformly_on (F * G) (f * g) p s := sorry

I have proofs but they are too ugly to be displayed in public :sweat_smile:

[Patrick Massot]

I'm not surprised this isn't there yet. I'm not even sure we have the statement that inversion in a topological field is uniformly continuous on a set whose closure doesn't contain zero.

[Patrick Massot]

Probably you would even need something like: if p and q are filters on $𝕜$ such that p ⊓ 𝓝 0 = ⊥ and q ⊓ 𝓝 0 = ⊥ then map (λ x : 𝕜 × 𝕜, (x.1⁻¹, x.2 ⁻¹)) (𝓤 𝕜 ⊓ (p ×ᶠ q)) ≤ 𝓤 𝕜.

[Patrick Massot]

Note this is totally untested and I didn't think very hard. It simply looks good and the kind of thing that would help in writing a nice proof of your first lemma.

[Patrick Massot]

This inequality would be meant to be used with the one appearing in docs#tendsto_uniformly_on_iff_tendsto

[Vincent Beffara]

p ⊓ 𝓝 0 = ⊥ as in "eventually bounded below" ?

[Patrick Massot]

I was thinking of p and q as 𝓟 (f '' s) and 𝓝ˢ (f '' s) (or the other way around)

[Vincent Beffara]

Here is what I have for step 1:

variables {ι α 𝕜 : Type*} [normed_field 𝕜] {p : filter ι} [ne_bot p] {K s : set α} {m mf mg : ℝ}
  {F G : ι → α → 𝕜} {f g : α → 𝕜} {x y : 𝕜} {η η' : ℝ}

lemma toto (hη : 0 < η) (hη' : 0 < η') (hx : x ∉ ball (0:𝕜) η) (hy : y ∉ ball (0:𝕜) η') :
  dist x⁻¹ y⁻¹ ≤ dist x y / (η * η') :=
begin
  have h1 : x ≠ 0 := λ h, by simpa [h, hη] using hx,
  have h2 : y ≠ 0 := λ h, by simpa [h, hη'] using hy,
  simp [dist_eq_norm] at hx hy,
  rw [dist_eq_norm, inv_sub_inv h1 h2, norm_div, norm_mul, dist_comm, dist_eq_norm],
  exact div_le_div (norm_nonneg _) le_rfl (mul_pos hη hη') (mul_le_mul hx hy hη'.le (norm_nonneg _))
end

lemma titi {p q : filter 𝕜} (hp : p ⊓ 𝓝 0 = ⊥) (hq : q ⊓ 𝓝 0 = ⊥) :
  map (λ x : 𝕜 × 𝕜, (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ (p ×ᶠ q)) ≤ 𝓤 𝕜 :=
begin
  obtain ⟨U, hU, V, hV, hUV⟩ := inf_eq_bot_iff.mp hp,
  obtain ⟨U', hU', V', hV', hUV'⟩ := inf_eq_bot_iff.mp hq,
  obtain ⟨η, hη, hV⟩ := metric.mem_nhds_iff.mp hV,
  obtain ⟨η', hη', hV'⟩ := metric.mem_nhds_iff.mp hV',
  have hηη' : 0 < η * η' := mul_pos hη hη',
  rintro u hu,
  obtain ⟨ε, hε, hu⟩ := mem_uniformity_dist.mp hu,
  rw mem_map_iff_exists_image,
  refine ⟨_, inter_mem_inf (dist_mem_uniformity (mul_pos hε hηη')) (prod_mem_prod hU hU'), _⟩,
  rintro z ⟨x, ⟨hx1, hx2⟩, rfl⟩,
  have hx'1 : x.1 ∉ ball (0 : 𝕜) η,
  from λ h, (nonempty_of_mem (mem_inter hx2.1 (hV h))).ne_empty hUV,
  have hx'2 : x.2 ∉ ball (0 : 𝕜) η',
  from λ h, (nonempty_of_mem (mem_inter hx2.2 (hV' h))).ne_empty hUV',
  refine hu ((toto hη hη' hx'1 hx'2).trans_lt _),
  convert (div_lt_div_right hηη').mpr hx1,
  field_simp [hη.lt.ne.symm, hη'.lt.ne.symm]; ring
end

[Vincent Beffara]

example (hη : 0 < η) : uniform_continuous_on (λ x, x⁻¹) (ball (0 : 𝕜) η)ᶜ :=
begin
  rw [uniform_continuous_on, tendsto, ← prod_principal_principal],
  refine titi (inf_eq_bot_iff.mpr _) (inf_eq_bot_iff.mpr _);
  exact ⟨(ball 0 η)ᶜ, mem_principal_self _, ball 0 η, ball_mem_nhds _ hη, compl_inter_self _⟩
end

[Vincent Beffara]

I mean,

example {s : set 𝕜} (hs : 𝓟 s ⊓ 𝓝 0 = ⊥) : uniform_continuous_on (λ x, x⁻¹) s :=
by simpa only [uniform_continuous_on, tendsto, ← prod_principal_principal] using titi hs hs

[Vincent Beffara]

@Patrick Massot I seem to be stuck at this point writing the proof that at the moment feels natural:

example (hF : tendsto_uniformly_on F f p s) (hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥) :
  tendsto_uniformly_on F⁻¹ f⁻¹ p s :=
begin
  rw [tendsto_uniformly_on_iff_tendsto, tendsto] at hF ⊢,
  have h1 : map (λ (q : ι × α), (f q.snd, F q.fst q.snd)) (p ×ᶠ 𝓟 s) ≤ 𝓟 (f '' s) ×ᶠ 𝓝ˢ (f '' s),
  { sorry },
  have h2 := le_inf hF h1,
  have h3 : monotone (filter.map (λ (x : 𝕜 × 𝕜), ((x.fst)⁻¹, (x.snd)⁻¹))) := filter.map_mono,
  have h4 : 𝓝ˢ (f '' s) ⊓ 𝓝 0 = ⊥, sorry, -- but this should work
  exact (h3 h2).trans (titi hf h4)
end

(with titi as above). h1 fits very well with the rest, but I'm not sure it is true; I also have trouble proving the simpler map (λ (q : ι × α), F q.1 q.2) (p ×ᶠ 𝓟 s) ≤ 𝓝ˢ (f '' s). I somehow convinced myself that it is not true and one should replace 𝓝ˢ (f '' s) with a uniform version to be able to exploit hypothesis hF so that the same element of p works everywhere. Is that completely off?

[Patrick Massot]

Indeed that suggestion was probably a bit too optimistic. There is clearly a notion of uniform neighborhood of a set in a uniform space, but I'm not sure how to phrase it nicely, and we clearly don't have it in mathlib.

[Junyan Xu]

This topic is about uniform neighborhoods right?

[Vincent Beffara]

So ⋃ x ∈ A, ball x V for V ∈ 𝓤 α is the uniform neighborhood I was looking for

[Patrick Massot]

It is a basis for the filter you were asking for

[Vincent Beffara]

Like this?

def uniform_thickening (s : set α) (u : set (α × α)) : set α :=
⋃ x ∈ s, uniform_space.ball x u

def uniform_nhds_set [uniform_space α] (s : set α) : filter (set α) :=
filter.generate ((λ u, {t | uniform_thickening s u ⊆ t}) '' (𝓤 α).sets)

[Anatole Dedecker]

Yes, but the goal is to make it less readable more easy to apply the API to by defining it in terms of all the filter operations we have (e.g the usual infimum, supremum, pushforward and pullback, but also docs#filter.lift or docs#filter.lift')

[Anatole Dedecker]

(I'm not sure that's possible, I didn't find anything like this for the uniformity generating the topology of uniform convergence, so it's completely possible we don't have a nice way to do it, but I'm mentioning it because it's worth thinking about)

[Patrick Massot]

Yes, there should be a nice description but I don't immediately see it (and I'm really late with many things so I should really really resist the temptation to spend the evening thinking about this).

[Vincent Beffara]

def uniform_nhds_set [uniform_space α] (s : set α) : filter (set α) :=
⨅ u ∈ 𝓤 α, 𝓟 {t | uniform_thickening s u ⊆ t}

[Vincent Beffara]

def uniform_nhds_set [uniform_space α] (s : set α) : filter (set α) :=
(𝓤 α).lift' (λ u, {t | uniform_thickening s u ⊆ t})

[Vincent Beffara]

Not sure which one is "more easy to apply the API to"

[Vincent Beffara]

Ah, actually this makes more sense probably:

def uniform_nhds_set [uniform_space α] (s : set α) : filter α :=
(𝓤 α).lift' (uniform_thickening s)

[Anatole Dedecker]

Oh indeed I didn't realize your first suggestion didn't have the good type (as in, not the same as docs#nhds_set)

[Vincent Beffara]

The definition above is quite workable:

def uniform_thickening (s : set α) (u : set (α × α)) : set α :=
⋃ x ∈ s, uniform_space.ball x u

lemma monotone_uniform_thickening {s : set α} : monotone (uniform_thickening s) :=
λ u v huv, Union₂_mono (λ i hi, by simpa [uniform_space.ball] using preimage_mono huv)

def uniform_nhds_set [uniform_space α] (s : set α) : filter α :=
(𝓤 α).lift' (uniform_thickening s)

lemma lemma1 (hF : tendsto_uniformly_on F f p s) (hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥) :
  map (λ (q : ι × α), (f q.2, F q.1 q.2)) (p ×ᶠ 𝓟 s) ≤ 𝓟 (f '' s) ×ᶠ uniform_nhds_set (f '' s) :=
begin
  rintro u hu,
  obtain ⟨t1, ht1, t2, ht2, h⟩ := filter.mem_prod_iff.mp hu,
  simp only [uniform_nhds_set, mem_lift'_sets monotone_uniform_thickening, exists_prop] at ht2,
  obtain ⟨v, hv1, hv2⟩ := ht2,
  rw mem_map_iff_exists_image,
  refine ⟨_ ×ˢ s, prod_mem_prod (hF v hv1) (mem_principal_self s), subset.trans _ h⟩,
  rintro ⟨x1, x2⟩ ⟨⟨i, a⟩, ⟨h1, h2⟩, h3⟩,
  replace h1 : ∃ b ∈ s, (f b, F i a) ∈ v := ⟨a, h2, by simp [h1 a h2]⟩,
  rcases prod.mk.inj_iff.mp h3 with ⟨rfl, rfl⟩,
  simp [mem_principal.mp ht1 (mem_image_of_mem f h2), prod_mk_mem_set_prod_eq, true_and],
  refine hv2 _,
  simpa [uniform_space.ball, uniform_thickening] using h1
end

lemma lemma2 {t : set 𝕜} (hf : 𝓟 t ⊓ 𝓝 0 = ⊥) : (uniform_nhds_set t) ⊓ 𝓝 0 = ⊥ :=
sorry

(the proof of lemma1 is a bit clumsy but it works well enough for now). @Anatole Dedecker what is your feeling about the separation lemma lemma2 here? I can prove it in a metric space but the whole point is to work in a uniform space, where some additional assumption could be needed.

[Anatole Dedecker]

I think this is true. You can certainly prove it as a direct consequence of docs#disjoint.exists_uniform_thickening applied to the compact {0} and to the closed set closure t (which 0 does not belong to by the hypothesis)

[Anatole Dedecker]

That said a direct proof would work well too and maybe it is more “morally satisfying”: you take a U ball around 0 that does not meet t, split it in half using docs#comp_mem_uniformity_sets, and with the V you get, you have that the V ball around 0 does not meet the V uniform thickening of t

[Anatole Dedecker]

There’s also a more practical reason why this second proof is better, which is that we definitely want to rewrite some things using this uniform_nhds_set filter, like we have rewritten a lot of things using nhds_set (e.g in separation axioms). I need to look more at the current library to get a better feel of how it would fit the best, but at least it suggests that using “high level” results about uniform space is not a good choice

[Vincent Beffara]

Ah, this is what I did in a metric space but comp_mem_uniformity_sets is what I did not find (the name is difficult to guess ...) so thanks! I will try to use it and see what happens.

[Anatole Dedecker]

For example, I’d argue docs#uniform_space.regular_space should be proven using your lemma2 (or a variation of it), first because it feels more “mathlib”-y than the current proof, and because anyone looking at the proof would easily find your uniform version of regularity, which is arguably more useful and intuitive than closed entourages being a basis of uniformity

[Vincent Beffara]

𝓝ᵘ s as a notation?

[Anatole Dedecker]

Ah yes, this is the key fact that makes uniform spaces nice: you have an “epsilon/2” principle

[Patrick Massot]

I'm sure the proof of lemma1 can be made nicer, but I really don't have time so I'll let Anatole handle it. He will probably start with removing the hf argument that looks like a copy-paste mistake

[Vincent Beffara]

I will work further on that proof

[Anatole Dedecker]

Sorry, I couldn't resist working on it anyway :sweat_smile: There are probably a dozen more way to do it, so feel free to work on it too, we will almost surely learn something by comparing the versions.

lemma lemma0 : tendsto (snd : α × α → α) (𝓤 α ⊓ comap fst (𝓟 s)) (uniform_nhds_set s) :=
begin
  simp_rw [comap_principal, uniform_nhds_set, tendsto_lift', eventually_inf_principal],
  exact λ U hU, mem_of_superset hU (λ ⟨x, y⟩ hxy hx, mem_bUnion hx hxy)
end

lemma lemma1 (hF : tendsto_uniformly_on F f p s) :
  map (λ (q : ι × α), (f q.2, F q.1 q.2)) (p ×ᶠ 𝓟 s) ≤ 𝓟 (f '' s) ×ᶠ uniform_nhds_set (f '' s) :=
begin
  rw [tendsto_uniformly_on_iff_tendsto] at hF,
  rw [← tendsto, tendsto_prod_iff'],
  have : tendsto (f ∘ snd) (p ×ᶠ 𝓟 s) (𝓟 (f '' s)) :=
    (tendsto_principal_principal.mpr $ λ a, mem_image_of_mem f).comp tendsto_snd,
  exact ⟨this, tendsto.comp lemma0 (tendsto_inf.mpr ⟨hF, tendsto_comap_iff.mpr this⟩)⟩,
end

[Vincent Beffara]

Here is what I have for now for the uniform separation lemma, together with a bit of API around uniform neighborhoods of sets:

import topology.uniform_space.uniform_convergence

open set filter uniform_space
open_locale filter uniformity topological_space

variables {ι α β : Type*} {a : α} {s t : set α} {u v : set (α × α)}

lemma comp_symm_of_uniformity' [uniform_space α] (hu : u ∈ 𝓤 α) :
  ∃ t ∈ 𝓤 α, symmetric_rel t ∧ t ○ t ⊆ u :=
let ⟨v, hv, hvu, hu⟩ := comp_symm_of_uniformity hu in ⟨v, hv, by { ext ⟨_,_⟩, exact ⟨hvu,hvu⟩ }, hu⟩

-----------------------------------------------------------------------------

namespace uniform_space -- uniform thickening

def thickening (s : set α) (u : set (α × α)) : set α :=
⋃ x ∈ s, ball x u

@[simp] lemma thickening_singleton : thickening {a} = ball a :=
by { ext, simp [thickening] }

@[simp] lemma monotone_thickening : monotone (thickening s) :=
λ u v huv, Union₂_mono (λ i hi, by simpa [ball] using preimage_mono huv)

lemma thickening_mono (h : s ⊆ t) : thickening s ≤ thickening t :=
pi.le_def.mpr (λ u, Union₂_mono' (λ a ha, ⟨a, h ha, subset_rfl⟩))

@[simp] lemma thickening_comp : thickening (thickening s u) v = thickening s (u ○ v) :=
by { ext, simp [thickening, ball] }

lemma disjoint_ball_iff : disjoint (ball a u) t ↔ ∀ b ∈ t, (a, b) ∉ u :=
by { rw [← compl_compl (ball a u), disjoint_compl_left_iff_subset]; refl }

lemma thickening_inter_eq_empty : thickening s u ∩ t = ∅ ↔ ∀ (a ∈ s) (b ∈ t), (a, b) ∉ u :=
by simp [thickening, ← disjoint_iff_inter_eq_empty, disjoint_ball_iff]

lemma thickening_inter_eq_empty_comm (hu : symmetric_rel u) :
  thickening s u ∩ t = ∅ ↔ s ∩ thickening t u = ∅ :=
begin
  simp [thickening_inter_eq_empty, inter_comm s],
  split; exact λ h a ha b hb hab, h b hb a ha (hu.mk_mem_comm.mp hab)
end

lemma thickening_inter_thickening_eq_empty_of_comp (hv : symmetric_rel v) (hvu : v ○ v ⊆ u)
  (hST : thickening s u ∩ t = ∅) :
  thickening s v ∩ thickening t v = ∅ :=
begin
  simp [← thickening_inter_eq_empty_comm hv],
  exact subset_empty_iff.mp (hST ▸ inter_subset_inter_left t (monotone_thickening hvu))
end

end uniform_space

-----------------------------------------------------------------------------

def uniform_nhds_set [uniform_space α] (s : set α) : filter α :=
(𝓤 α).lift' (uniform_space.thickening s)

localized "notation (name := uniform_nhds_set) `𝓝ᵘ` := uniform_nhds_set" in uniformity

namespace uniform_space -- uniform_nhds_set

variables [uniform_space α]

lemma uniform_nhds_set_mono (h : s ⊆ t) : 𝓝ᵘ s ≤ 𝓝ᵘ t :=
lift'_mono le_rfl (thickening_mono h)

lemma uniform_nhds_set_singleton : 𝓝ᵘ {a} = 𝓝 a :=
by simp [nhds_eq_uniformity, uniform_nhds_set]

lemma mem_uniform_nhds_set_iff : s ∈ 𝓝ᵘ t ↔ ∃ u ∈ 𝓤 α, thickening t u ⊆ s :=
by simp [uniform_nhds_set, mem_lift'_sets]

lemma nhds_le_uniform_nhds_set (ha : a ∈ s) : 𝓝 a ≤ 𝓝ᵘ s :=
by simpa [← uniform_nhds_set_singleton] using uniform_nhds_set_mono (singleton_subset_iff.mpr ha)

lemma nhds_set_le_uniform_nhds_set : 𝓝ˢ s ≤ 𝓝ᵘ s :=
by simpa [nhds_set] using λ a, nhds_le_uniform_nhds_set

lemma uniform_nhds_inf_uniform_nhds_eq_bot (h : 𝓝ᵘ s ⊓ 𝓟 t = ⊥) : 𝓝ᵘ s ⊓ 𝓝ᵘ t = ⊥ :=
begin
  simp_rw [inf_principal_eq_bot, inf_eq_bot_iff, mem_uniform_nhds_set_iff] at h ⊢,
  obtain ⟨u, hu, hsu⟩ := h,
  obtain ⟨v, hv, hvs, hvu⟩ := comp_symm_of_uniformity' hu,
  refine ⟨_, ⟨v, hv, subset_rfl⟩, _, ⟨v, hv, subset_rfl⟩, _⟩,
  refine thickening_inter_thickening_eq_empty_of_comp hvs hvu _,
  exact (subset_compl_iff_disjoint_right.mp hsu).inter_eq,
end

lemma nhds_inf_uniform_nhds_eq_bot (hf : 𝓝 a ⊓ 𝓟 s = ⊥) : 𝓝 a ⊓ 𝓝ᵘ s = ⊥ :=
by { rw [← uniform_nhds_set_singleton] at hf ⊢; exact uniform_nhds_inf_uniform_nhds_eq_bot hf }

end uniform_space

[Anatole Dedecker]

If you add

@[simp] lemma lift'_inter {f : filter α} {g h : set α → set β} :
  f.lift' (λx, g x ∩ h x) = f.lift' g ⊓ f.lift' h :=
calc f.lift' (λx, g x ∩ h x)
    = f.lift (λx, (𝓟 $ g x) ⊓ (𝓟 $ h x)) : by simp [filter.lift']
... = f.lift' g ⊓ f.lift' h : lift_inf

lemma lift_eq_bot_iff {f : filter α} {g : set α → filter β} (hm : monotone g) :
  f.lift g = ⊥ ↔ ∃ s ∈ f, g s = ⊥ :=
by simp only [← empty_mem_iff_bot, mem_lift_sets hm]

lemma lift'_eq_bot_iff {f : filter α} {g : set α → set β} (hm : monotone g) :
  f.lift' g = ⊥ ↔ ∃ s ∈ f, g s = ∅ :=
by simp_rw [filter.lift', lift_eq_bot_iff (monotone_principal.comp hm),
  ← principal_empty, principal_eq_iff_eq]

You can do:

lemma uniform_nhds_inf_uniform_nhds_eq_bot (h : 𝓝ᵘ s ⊓ 𝓟 t = ⊥) : 𝓝ᵘ s ⊓ 𝓝ᵘ t = ⊥ :=
begin
  simp only [uniform_nhds_set, lift'_inf_principal_eq, ← lift'_inter, lift'_eq_bot_iff,
              monotone_thickening.inter monotone_const,
              monotone_thickening.inter monotone_thickening] at h ⊢,
  obtain ⟨u, hu, hsu⟩ := h,
  obtain ⟨v, hv, hvs, hvu⟩ := comp_symm_of_uniformity' hu,
  exact ⟨v, hv, thickening_inter_thickening_eq_empty_of_comp hvs hvu hsu⟩
end

It's not really shorter so you can keep your version, I just really wanted to give it a try :sweat_smile:

[Anatole Dedecker]

But the whole thing is quite nice, I'd say you can open a PR with what you have right now (unless you want to do more things with it first of course)

[Vincent Beffara]

I want to add that the uniform neighborhood of a compact is its set neighborhood. (If it is true.) But first I have to go teach...

[Anatole Dedecker]

Is it true and we do have it! You just have to rephrase docs#is_compact.nhds_set_basis_uniformity as 𝓝ᵘ K = 𝓝ˢ K but that should be straightforward

[Anatole Dedecker]

But if you think you can shorten the proof using API then you should absolutely go for that!

[Vincent Beffara]

Also I wanted to swap the arguments of uniform_space.thickening to match metric.thickening

[Patrick Massot]

This is still abusing dot notation to obfuscate code. It is especially confusing when $f$ is a filter and $g$ and $h$ are maps...

[Vincent Beffara]

Patrick Massot said:

This is still abusing dot notation to obfuscate code. It is especially confusing when $f$ is a filter and $g$ and $h$ are maps...

Which part exactly is abusing dot notation?

[Patrick Massot]

Lines like f.lift' (λx, g x ∩ h x) = f.lift' g ⊓ f.lift' h

[Vincent Beffara]

Also here then?

def uniform_nhds_set [uniform_space α] (s : set α) : filter α :=
(𝓤 α).lift' (uniform_space.thickening s)

[Vincent Beffara]

lemma lemma3 (hs : is_compact s) : 𝓝ˢ s = 𝓝ᵘ s :=
(hs.nhds_set_basis_uniformity (basis_sets _)).eq_of_same_basis ⟨λ t, mem_uniform_nhds_set_iff⟩