equicontinuous_TFAE — Mathlib

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

Похожие утверждения