English
The topology of a NormedSpace 𝕜 E is generated by the single seminorm normSeminorm 𝕜 E.
Русский
Топология нормированного пространства 𝕜 E задаётся одной семинормой normSeminorm 𝕜 E.
LaTeX
$$$norm_withSeminorms\\ (𝕜,E): WithSeminorms\\ (\\lambda _ : Fin 1 => normSeminorm 𝕜 E)$$$
Lean4
/-- Let `E` and `F` be two topological vector spaces over a `NontriviallyNormedField`, and assume
that the topology of `F` is generated by some family of seminorms `q`. For a family `f` of linear
maps from `E` to `F`, the following are equivalent:
* `f` is equicontinuous at `0`.
* `f` is equicontinuous.
* `f` is uniformly equicontinuous.
* For each `q i`, the family of seminorms `k ↦ (q i) ∘ (f k)` is bounded by some continuous
seminorm `p` on `E`.
* For each `q i`, the seminorm `⊔ k, (q i) ∘ (f k)` is well-defined and continuous.
In particular, if you can determine all continuous seminorms on `E`, that gives you a complete
characterization of equicontinuity for linear maps from `E` to `F`. For example `E` and `F` are
both normed spaces, you get `NormedSpace.equicontinuous_TFAE`. -/
protected theorem _root_.WithSeminorms.equicontinuous_TFAE {κ : Type*} {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E]
[IsUniformAddGroup E] [u : UniformSpace F] [hu : IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E]
(f : κ → E →ₛₗ[σ₁₂] F) :
TFAE
[EquicontinuousAt ((↑) ∘ f) 0, Equicontinuous ((↑) ∘ f), UniformEquicontinuous ((↑) ∘ f),
∀ i, ∃ p : Seminorm 𝕜 E, Continuous p ∧ ∀ k, (q i).comp (f k) ≤ p,
∀ i, BddAbove (range fun k ↦ (q i).comp (f k)) ∧ Continuous (⨆ k, (q i).comp (f k))] :=
by
-- We start by reducing to the case where the target is a seminormed space
rw [q.withSeminorms_iff_uniformSpace_eq_iInf.mp hq, uniformEquicontinuous_iInf_rng, equicontinuous_iInf_rng,
equicontinuousAt_iInf_rng]
refine forall_tfae [_, _, _, _, _] fun i ↦ ?_
let _ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
clear u hu hq
simp only [List.map]
tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f
tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous
tfae_have 2 → 1 := fun H ↦ H 0
tfae_have 3 → 5
| H =>
by
have : ∀ᶠ x in 𝓝 0, ∀ k, q i (f k x) ≤ 1 :=
by
filter_upwards [Metric.equicontinuousAt_iff_right.mp (H.equicontinuous 0) 1 one_pos] with x hx k
simpa using (hx k).le
have bdd : BddAbove (range fun k ↦ (q i).comp (f k)) :=
Seminorm.bddAbove_of_absorbent (absorbent_nhds_zero this) (fun x hx ↦ ⟨1, forall_mem_range.mpr hx⟩)
rw [← Seminorm.coe_iSup_eq bdd]
refine ⟨bdd, Seminorm.continuous' (r := 1) ?_⟩
filter_upwards [this] with x hx
simpa only [closedBall_iSup bdd _ one_pos, mem_iInter, mem_closedBall_zero] using hx
tfae_have 5 → 4 := fun H ↦ ⟨⨆ k, (q i).comp (f k), Seminorm.coe_iSup_eq H.1 ▸ H.2, le_ciSup H.1⟩
tfae_have 4 → 1 -- This would work over any `NormedField`
| ⟨p, hp, hfp⟩ =>
Metric.equicontinuousAt_of_continuity_modulus p (map_zero p ▸ hp.tendsto 0) _ <|
Eventually.of_forall fun x k ↦ by simpa using hfp k x
tfae_finish