[Merged by Bors] - feat(topology): basis for 𝓤 C(α, β) and convergence of a series of f : C(α, β)

[hrmacbeth]

• add filter.has_basis.compact_convergence_uniformity;
• add a few facts about compacts X;
• add summable_of_locally_summable_norm.

---

[Ruben-VandeVelde]

Some nits

[ocfnash]

I think the results here skip over a few intermediate results that it would be nice to have. In particular the specialisations to compact domain and to a codomain that is a metric space do not have to happen together. An immediate benefit is that decoupling these should allow us to carry out the equivalent work for the space of bounded continuous functions (either as part of this work, or later).

I spent a bit of time this morning seeing how far I could get but I ran out of time. The below shows the sort of thing I have in mind:

import topology.metric_space.basic
import topology.uniform_space.compact_convergence

noncomputable theory
open_locale uniformity ennreal nnreal
open filter set

namespace continuous_map

variables {α β : Type*} [topological_space α]

/-- When the domain is compact, there is a special basis for the filter of entourages. -/
lemma qux [compact_space α] [uniform_space β] :
  has_basis (𝓤 C(α, β)) (λ V : set (β × β), V ∈ 𝓤 β)
            (λ V, { fg : C(α, β) × C(α, β) | ∀ x, (fg.1 x, fg.2 x) ∈ V }) :=
begin
  apply has_basis_compact_convergence_uniformity.to_has_basis,
  { exact λ p hp, ⟨p.2, hp.2, λ fg hfg x hx, hfg x⟩, },
  { exact λ V hV, ⟨⟨univ, V⟩, ⟨compact_univ, hV⟩, λ fg hfg x, hfg x (mem_univ x)⟩, },
end

section emetric_space

variables [emetric_space β]

/-- When the uniform structure arises from an `emetric_space`, there is another special basis. -/
lemma foo :
  has_basis (𝓤 C(α, β)) (λ p : set α × ℝ≥0∞, is_compact p.1 ∧ 0 < p.2)
            (λ p, { fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, edist (fg.1 x) (fg.2 x) < p.2 }) :=
begin
  apply has_basis_compact_convergence_uniformity.to_has_basis,
  { rintros ⟨K, V⟩ ⟨hK, hV⟩,
    obtain ⟨ε, hε₀, hε₁⟩ := mem_uniformity_edist.mp hV,
    exact ⟨⟨K, ε⟩, ⟨hK, hε₀⟩, λ fg hfg x hx, hε₁ (hfg x hx)⟩, },
  { rintros ⟨K, ε⟩ ⟨hK, hε₀⟩,
    exact ⟨⟨K, {p : β × β | edist p.1 p.2 < ε }⟩, ⟨hK, edist_mem_uniformity hε₀⟩, λ fg hfg, hfg⟩, },
end

/-- When the domain is compact and the uniform structure arises from an `emetric_space`, there is
a very special basis. -/
lemma bar [compact_space α] :
  has_basis (𝓤 C(α, β)) (λ ε : ℝ≥0, 0 < ε)
            (λ ε, { fg : C(α, β) × C(α, β) | ∀ x, edist (fg.1 x) (fg.2 x) < ε }) :=
begin
  -- TODO Use `qux` to simplify this proof.
  apply foo.to_has_basis,
  { rintros ⟨K, ε⟩ ⟨hK, hε₀⟩,
    by_cases hε₁ : ε = ∞,
    { subst hε₁,
      exact ⟨1, zero_lt_one, λ fg hfg x hx, (hfg x).trans ennreal.one_lt_top⟩, },
    lift ε to ℝ≥0 using hε₁,
    exact ⟨ε, ennreal.coe_pos.mp hε₀, λ fg hfg x hx, hfg x⟩, },
  { intros ε hε₀,
    exact ⟨⟨univ, ε⟩, ⟨compact_univ, ennreal.coe_pos.mpr hε₀⟩, λ fg hfg x, hfg x (mem_univ x)⟩, },
end

protected def emetric_space : emetric_space C(α, β) :=
{ edist := λ f g, ⨆ x, edist (f x) (g x),
  eq_of_edist_eq_zero := sorry,
  edist_self := sorry,
  edist_comm := sorry,
  edist_triangle := λ f g h, by sorry, }

end emetric_space

section metric_space

variables [metric_space β]

/-- When the domain is compact and the uniform structure arises from a `metric_space`, there is
a very, very special basis! -/
lemma baz [compact_space α] :
  has_basis (𝓤 C(α, β)) (λ ε : ℝ, 0 < ε)
            (λ ε, { fg : C(α, β) × C(α, β) | ∀ x, dist (fg.1 x) (fg.2 x) < ε }) :=
begin
  refine bar.to_has_basis _ _,
  { exact λ ε hε₀, ⟨ε, hε₀, by simp⟩, },
  { intros ε hε₀,
    refine ⟨ε.to_nnreal, real.to_nnreal_pos.mpr hε₀, λ fg hfg x, _⟩,
    rw ← real.to_nnreal_lt_to_nnreal_iff hε₀,
    simpa only [edist_lt_coe, nndist_dist] using hfg x, },
end

instance [compact_space α] : metric_space C(α, β) :=
{ to_uniform_space := continuous_map.compact_convergence_uniform_space,
  uniformity_dist  :=
  begin
    rw baz.eq_binfi,
    { -- Slightly fiddly but should be easy.
      sorry, },
    { apply_instance, },
  end,
  .. @emetric_space.to_metric_space _ continuous_map.emetric_space sorry, }

end metric_space

end continuous_map

[urkud]

The uniformity fix went to #11665. @hrmacbeth , could you please update the description? Otherwise LGTM but I wrote large part of the current diff.

[ocfnash]

Thank you both!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests