Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(UniformConvergenceTopology): add UniformOnFun.uniformity_eq etc #10784

Closed
wants to merge 7 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib/Topology/UniformSpace/Ascoli.lean
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,7 @@ theorem EquicontinuousOn.comap_uniformOnFun_eq {𝔖 : Set (Set X)} (𝔖_compac
-- `K.restrict ∘ F : ι → (K →ᵤ α)` for `K ∈ 𝔖`.
have H1 : (UniformOnFun.uniformSpace X α 𝔖).comap F =
⨅ (K ∈ 𝔖), (UniformFun.uniformSpace _ _).comap (K.restrict ∘ F) := by
simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformSpace.comap_comap]
simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformSpace.comap_comap]; rfl
-- Now, note that a similar fact is true for the uniform structure on `X → α` induced by
-- the map `(⋃₀ 𝔖).restrict : (X → α) → ((⋃₀ 𝔖) → α)`: it is equal to the one induced by
-- all maps `K.restrict : (X → α) → (K → α)` for `K ∈ 𝔖`, which means that the RHS of our
Expand Down
82 changes: 51 additions & 31 deletions Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
Original file line number Diff line number Diff line change
Expand Up @@ -596,7 +596,8 @@ declared as an instance on `α →ᵤ[𝔖] β`. It is defined as the infimum, f
by `S.restrict`, the map of restriction to `S`, of the uniform structure `𝒰(s, β, uβ)` on
`↥S →ᵤ β`. We will denote it `𝒱(α, β, 𝔖, uβ)`, where `uβ` is the uniform structure on `β`. -/
instance uniformSpace : UniformSpace (α →ᵤ[𝔖] β) :=
⨅ (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap s.restrict 𝒰(s, β, _)
⨅ (s : Set α) (_ : s ∈ 𝔖),
.comap (UniformFun.ofFun ∘ s.restrict ∘ UniformOnFun.toFun 𝔖) 𝒰(s, β, _)

local notation "𝒱(" α ", " β ", " 𝔖 ", " u ")" => @UniformOnFun.uniformSpace α β u 𝔖

Expand Down Expand Up @@ -735,6 +736,47 @@ protected theorem uniformContinuous_restrict (h : s ∈ 𝔖) :

variable {α}

/-- A version of `UniformOnFun.hasBasis_uniformity_of_basis`
with weaker conclusion and weaker assumptions.

We make no assumptions about the set `𝔖`
but conclude only that the uniformity is equal to some indexed infimum. -/
protected theorem uniformity_eq_of_basis {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)}
(h : (𝓤 β).HasBasis p V) :
𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)) := by
simp_rw [iInf_uniformity, uniformity_comap,
(UniformFun.hasBasis_uniformity_of_basis _ _ h).eq_biInf, comap_iInf, comap_principal,
Function.comp_apply, UniformFun.gen, Subtype.forall]
rfl

protected theorem uniformity_eq : 𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V) :=
UniformOnFun.uniformity_eq_of_basis _ _ (𝓤 β).basis_sets

protected theorem gen_mem_uniformity (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) :
UniformOnFun.gen 𝔖 s V ∈ 𝓤 (α →ᵤ[𝔖] β) := by
rw [UniformOnFun.uniformity_eq]
apply_rules [mem_iInf_of_mem, mem_principal_self]

/-- A version of `UniformOnFun.hasBasis_nhds_of_basis`
with weaker conclusion and weaker assumptions.

We make no assumptions about the set `𝔖`
but conclude only that the neighbourhoods filter is equal to some indexed infimum. -/
protected theorem nhds_eq_of_basis {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)}
(h : (𝓤 β).HasBasis p V) (f : α →ᵤ[𝔖] β) :
𝓝 f = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V i} := by
simp_rw [nhds_eq_comap_uniformity, UniformOnFun.uniformity_eq_of_basis _ _ h, comap_iInf,
comap_principal]; rfl

protected theorem nhds_eq (f : α →ᵤ[𝔖] β) :
𝓝 f = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V} :=
UniformOnFun.nhds_eq_of_basis _ _ (𝓤 β).basis_sets f

protected theorem gen_mem_nhds (f : α →ᵤ[𝔖] β) (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) :
{g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V} ∈ 𝓝 f := by
rw [UniformOnFun.nhds_eq]
apply_rules [mem_iInf_of_mem, mem_principal_self]

/-- Let `u₁`, `u₂` be two uniform structures on `γ` and `𝔖₁ 𝔖₂ : Set (Set α)`. If `u₁ ≤ u₂` and
`𝔖₂ ⊆ 𝔖₁` then `𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂)`. -/
protected theorem mono ⦃u₁ u₂ : UniformSpace γ⦄ (hu : u₁ ≤ u₂) ⦃𝔖₁ 𝔖₂ : Set (Set α)⦄
Expand Down Expand Up @@ -828,30 +870,13 @@ Note that one can easily see that assuming `∀ T ∈ 𝔗, ∃ S ∈ 𝔖, f ''
we will get this for free when we prove that `𝒱(α, β, 𝔖, uβ) = 𝒱(α, β, 𝔖', uβ)` where `𝔖'` is the
***noncovering*** bornology generated by `𝔖`. -/
protected theorem precomp_uniformContinuous {𝔗 : Set (Set γ)} {f : γ → α}
(hf : 𝔗 ⊆ image f ⁻¹' 𝔖) :
UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (g ∘ f) := by
-- Since `comap` distributes on `iInf`, it suffices to prove that
-- `⨅ s ∈ 𝔖, comap s.restrict 𝒰(↥s, β, uβ) ≤ ⨅ t ∈ 𝔗, comap (t.restrict ∘ (— ∘ f)) 𝒰(↥t, β, uβ)`.
simp_rw [uniformContinuous_iff, UniformOnFun.uniformSpace, UniformSpace.comap_iInf, ←
UniformSpace.comap_comap]
-- For any `t ∈ 𝔗`, note `s := f '' t ∈ 𝔖`.
-- We will show that `comap s.restrict 𝒰(↥s, β, uβ) ≤ comap (t.restrict ∘ (— ∘ f)) 𝒰(↥t, β, uβ)`.
refine' le_iInf₂ fun t ht => iInf_le_of_le (f '' t) <| iInf_le_of_le (hf ht) _
-- Let `f'` be the map from `t` to `f '' t` induced by `f`.
let f' : t → f '' t := (mapsTo_image f t).restrict f t (f '' t)
-- By definition `t.restrict ∘ (— ∘ f) = (— ∘ f') ∘ (f '' t).restrict`.
have :
(t.restrict ∘ fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (g ∘ f)) =
(fun g : f '' t → β => g ∘ f') ∘ (f '' t).restrict :=
rfl
-- Thus, we have to show `comap (f '' t).restrict 𝒰(↥(f '' t), β, uβ) ≤`
-- `comap (f '' t).restrict (comap (— ∘ f') 𝒰(↥t, β, uβ))`.
rw [this, @UniformSpace.comap_comap (α →ᵤ[𝔖] β) (f '' t →ᵤ β)]
-- But this is exactly monotonicity of `comap` applied to
-- `UniformFun.precomp_continuous`.
refine' UniformSpace.comap_mono _
rw [← uniformContinuous_iff]
exact UniformFun.precomp_uniformContinuous
(hf : MapsTo (f '' ·) 𝔗 𝔖) :
UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (toFun 𝔖 g ∘ f) := by
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I made the proof much shorter. Should I restore some of the comments?

Copy link
Member

@ADedecker ADedecker Apr 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TBH I'm a bit sad to see my proof go, mostly because I like this kind of argument, but I have no objective argument for keeping it (I suggested a slight golf though). As for comments, I'd say you could just add the following at the beginning of the proof, to match more accurately the new version:

  -- This follows from the fact that `(— ∘ f) × (— ∘ f)` maps `gen (f '' t) V` to `gen t V`.

-- This follows from the fact that `(· ∘ f) × (· ∘ f)` maps `gen (f '' t) V` to `gen t V`.
simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf]
refine fun t ht V hV ↦ tendsto_iInf' (f '' t) <| tendsto_iInf' (hf ht) <|
tendsto_iInf' V <| tendsto_iInf' hV ?_
simpa only [tendsto_principal_principal, UniformOnFun.gen] using fun _ ↦ forall_mem_image.1
#align uniform_on_fun.precomp_uniform_continuous UniformOnFun.precomp_uniformContinuous

/-- Turn a bijection `e : γ ≃ α` such that we have both `∀ T ∈ 𝔗, e '' T ∈ 𝔖` and
Expand Down Expand Up @@ -899,12 +924,7 @@ protected theorem uniformContinuous_toFun (h : ⋃₀ 𝔖 = univ) :
of `TendstoUniformlyOn`) for all `S ∈ 𝔖`. -/
protected theorem tendsto_iff_tendstoUniformlyOn {F : ι → α →ᵤ[𝔖] β} {f : α →ᵤ[𝔖] β} :
Tendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (toFun 𝔖 ∘ F) (toFun 𝔖 f) p s := by
rw [UniformOnFun.topologicalSpace_eq, nhds_iInf, tendsto_iInf]
refine' forall_congr' fun s => _
rw [nhds_iInf, tendsto_iInf]
refine' forall_congr' fun hs => _
rw [nhds_induced (T := _), tendsto_comap_iff, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe,
UniformFun.tendsto_iff_tendstoUniformly]
simp only [UniformOnFun.nhds_eq, tendsto_iInf, tendsto_principal]
rfl
#align uniform_on_fun.tendsto_iff_tendsto_uniformly_on UniformOnFun.tendsto_iff_tendstoUniformlyOn

Expand Down