TendstoUniformlyOn - supremum norm goes to zero

Stream: new members

[Tainnor]

If my brain isn't completely fried by now, the following should be true:

import Mathlib

open Filter Topology
example {f : ℕ → ℝ → ℝ} (unf : TendstoUniformlyOn f F atTop S) :
    Tendsto (fun k ↦ sSup (norm ∘ (f k - F) '' S)) atTop (𝓝 0) := by
  sorry

But I don't know how to prove it. I suspect it may have something to do with this page, but that's a bit "above my paygrade": https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.html#UniformOnFun.uniformSpace

[Tainnor]

I managed to find a proof, but it seems very pedestrian to me. I feel like there must be a better way, so if somebody finds one, I'll be happy to know. Otherwise, I'll proceed with this proof for the moment. Oh, and happy holidays!

example {f : ℕ → ℝ → ℝ} (unf : TendstoUniformlyOn f F atTop S) :
    Tendsto (fun i ↦ sSup ((norm ∘ (f i - F)) '' S)) atTop (𝓝 0) := by
  by_cases nempty : S = ∅
  . simp [nempty]
  obtain ⟨c, cIn⟩ := Set.nonempty_iff_ne_empty.mpr nempty
  rw [tendstoUniformlyOn_iff_tendsto, tendsto_uniformity_iff_dist_tendsto_zero] at unf
  simp [dist] at unf
  rw [tendsto_prod_iff] at unf
  rw [tendsto_nhds]
  intro s sOpen zIn
  simp
  obtain ⟨r, rpos, ballSub⟩ := Metric.isOpen_iff.mp sOpen 0 zIn
  obtain ⟨ρ, ρpos, ρlt⟩ := exists_between rpos
  let t := Metric.closedBall (0 : ℝ) ρ
  have tSub : t ⊆ s := by
    intro x xIn
    apply (subset_trans _ ballSub) xIn
    simp [t]
    intro y yIn
    simp at yIn ⊢
    linarith
  have tNbhd : t ∈ 𝓝 0 := Metric.closedBall_mem_nhds 0 ρpos
  obtain ⟨U, Uin, V, Vin, h⟩ := unf t tNbhd
  obtain ⟨N, h'⟩ := mem_atTop_sets.mp Uin
  simp at Vin
  use N
  intro n nN
  specialize h' n nN
  suffices mball : sSup ((norm ∘ (f n - F)) '' S) ∈ Metric.ball 0 r by
    exact ballSub mball
  simp
  apply lt_of_le_of_lt _ ρlt
  rw [abs_of_nonneg]; rotate_left
  . apply Real.sSup_nonneg
    intro x xIn
    simp at xIn
    obtain ⟨y, _, yeq⟩ := xIn
    rw [← yeq]
    exact abs_nonneg _
  rw [csSup_le_iff]; rotate_right
  . refine' ⟨‖f n c - F c‖, c, cIn, _⟩
    simp
  intro x xIn; rotate_left
  rw [bddAbove_iff_exists_ge ρ]
  refine' ⟨ρ, le_refl _, _⟩
  intro x xIn
  all_goals
    obtain ⟨y, yIn, yeq⟩ := xIn
    simp at yeq
    have yIn' : y ∈ V := Vin yIn
    specialize h n y h' yIn'
    simp [t] at h
    rwa [← yeq, abs_sub_comm]