UniformContinuous + TendstoUniformly -> UniformContinuous

Stream: Is there code for X?

[Weiyi Wang]

Mathlib has docs#TendstoUniformly.continuous for Uniform limit theorem. On the wikipedia page, there is also a note "The uniform limit theorem also holds if continuity is replaced by uniform continuity". Does mathlib have this or tools to quickly prove this?

Tentative statements that I don't know if is correct

import Mathlib
variable {α β ι : Type*} [UniformSpace α] [UniformSpace β]
variable {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι}

protected theorem TendstoLocallyUniformlyOn.uniformContinuousOn
    (h : TendstoLocallyUniformlyOn F f p s)
    (hc : ∀ᶠ n in p, UniformContinuousOn (F n) s) [Filter.NeBot p] : UniformContinuousOn f s := by
  sorry

protected theorem TendstoUniformly.uniformContinuous (h : TendstoUniformly F f p)
    (hc : ∀ᶠ n in p, UniformContinuous (F n)) [Filter.NeBot p] : UniformContinuous f := by
  sorry

[Weiyi Wang]

Ok this is my first time dealing with uniformality and somehow I got it (the second theorem) while still not fully understand what is happening

import Mathlib
variable {α β ι : Type*} [UniformSpace α] [UniformSpace β]
variable {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι}

theorem TendstoUniformly.uniformContinuous (h : TendstoUniformly F f p)
    (hc : ∀ᶠ n in p, UniformContinuous (F n)) [Filter.NeBot p] : UniformContinuous f := by
  simp_rw [uniformContinuous_iff_eventually] at ⊢ hc
  unfold TendstoUniformly at h
  intro u hu
  simp_rw [Filter.eventually_iff_exists_mem] at ⊢ hc h
  obtain ⟨v, hv, hc⟩ := hc
  obtain ⟨u1, hu1, hu10⟩ := comp_mem_uniformity_sets hu
  obtain ⟨u2, hu2, hsymm, hu21⟩ := comp_symm_of_uniformity hu1
  obtain ⟨v1, hv1, h1⟩ := h u1 hu1
  obtain ⟨v2, hv2, h2⟩ := h u2 hu2
  have hnonempty : (v ∩ v1 ∩ v2).Nonempty := by
    refine Filter.nonempty_of_mem (?_ : v ∩ v1 ∩ v2 ∈ p)
    refine Filter.inter_mem (Filter.inter_mem hv hv1) hv2
  let y := hnonempty.choose
  obtain ⟨a, ha, hc⟩ := hc y (Set.mem_of_subset_of_mem (by grind) hnonempty.choose_spec) u2 hu2
  specialize h1 y (Set.mem_of_subset_of_mem (by grind) hnonempty.choose_spec)
  specialize h2 y (Set.mem_of_subset_of_mem (by grind) hnonempty.choose_spec)
  use a, ha
  intro x hx
  apply Set.mem_of_subset_of_mem hu10
  rw [SetRel.mem_comp]
  use F y x.1, h1 x.1
  apply Set.mem_of_subset_of_mem hu21
  rw [SetRel.mem_comp]
  use F y x.2, (hc x hx)
  apply hsymm
  apply h2

:joy: please golf this

[Aaron Liu]

I have no idea what I'm doing

import Mathlib
variable {α β ι : Type*} [UniformSpace α] [UniformSpace β]
variable {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι}

theorem TendstoUniformly.uniformContinuous (h : TendstoUniformly F f p)
    (hc : ∀ᶠ n in p, UniformContinuous (F n)) [Filter.NeBot p] : UniformContinuous f := by
  rw [tendstoUniformly_iff_tendsto, ← Filter.principal_univ,
    Filter.tendsto_iff_forall_eventually_mem] at h
  simp_rw [Filter.eventually_prod_principal_iff, Set.mem_univ, true_imp_iff] at h
  intro U hU
  obtain ⟨V, hV, hVU⟩ := comp3_mem_uniformity hU
  obtain ⟨k, hkV, hF⟩ := ((h (SetRel.symmetrize V) (symmetrize_mem_uniformity hV)).and hc).exists
  specialize hF hV
  rw [Filter.mem_map] at hF ⊢
  apply Filter.mem_of_superset hF
  intro x hx
  apply hVU
  exact SetRel.prodMk_mem_comp (hkV x.1).1 (SetRel.prodMk_mem_comp hx (hkV x.2).2)

this seems shorter than what you put

[Weiyi Wang]

Thanks! I have cleaned it up and opened PR #32079

[Aaron Liu]

hmmm is this a desirable generalization

import Mathlib
variable {α β ι : Type*} [UniformSpace α] [UniformSpace β]
variable {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι}

theorem TendstoUniformly.uniformContinuous (h : TendstoUniformly F f p)
    (hc : ∃ᶠ n in p, UniformContinuous (F n)) [Filter.NeBot p] : UniformContinuous f := by
  rw [tendstoUniformly_iff_tendsto, ← Filter.principal_univ,
    Filter.tendsto_iff_forall_eventually_mem] at h
  simp_rw [Filter.eventually_prod_principal_iff, Set.mem_univ, true_imp_iff] at h
  intro U hU
  obtain ⟨V, hV, hVU⟩ := comp3_mem_uniformity hU
  obtain ⟨k, hkV, hF⟩ := ((h (SetRel.symmetrize V) (symmetrize_mem_uniformity hV)).and_frequently hc).exists
  specialize hF hV
  rw [Filter.mem_map] at hF ⊢
  apply Filter.mem_of_superset hF
  intro x hx
  apply hVU
  exact SetRel.prodMk_mem_comp (hkV x.1).1 (SetRel.prodMk_mem_comp hx (hkV x.2).2)

feels kind of trivial but

[Weiyi Wang]

Interesting. Does this also work on the existing TendstoUniformly.continuous?

[Aaron Liu]

yes it does

[Aaron Liu]

the proof only needs some continuous function at a specified closeness to the limiting function, it doesn't need every function past a certain point to be continuous

[Weiyi Wang]

Let me update the new code with this since why not. Then I can open another PR to change the existing one (unless I find out there isn't much to fix downstream welp I already hit 3 errors so next PR it is)

[Aaron Liu]

and we can also drop [p.NeBot] since it's implied by hc