English
Equicontinuity_TFAE provides several equivalent characterizations of an equicontinuous family of continuous linear maps; broadly, equicontinuity at zero, equicontinuity, uniform equicontinuity, and uniform norm bounds are equivalent.
Русский
TFAE эквивалентно описание равномерной эквиконтинуальности семей непрерывных линейных отображений: равномерная эквиконтинуальность у начала, эквиконтинуальность, равномерная эквicontинуальность и т. д.
LaTeX
$$$$\\text{EquicontinuousAt}((f_i))0 \;\Longleftrightarrow\; \\text{Equicontinuous}((f_i)) \;\Longleftrightarrow\; \\text{UniformEquicontinuous}((f_i)) \;\Longleftrightarrow\; \\exists C>0, \\forall i, \\|f_i\\| \\le C.$$$$
Lean4
/-- Equivalent characterizations for equicontinuity of a family of continuous linear maps
between normed spaces. See also `WithSeminorms.equicontinuous_TFAE` for similar characterizations
between spaces satisfying `WithSeminorms`. -/
protected theorem equicontinuous_TFAE :
List.TFAE
[EquicontinuousAt ((↑) ∘ f) 0, Equicontinuous ((↑) ∘ f), UniformEquicontinuous ((↑) ∘ f),
∃ C, ∀ i x, ‖f i x‖ ≤ C * ‖x‖, ∃ C ≥ 0, ∀ i x, ‖f i x‖ ≤ C * ‖x‖, ∃ C, ∀ i, ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ i, ‖f i‖ ≤ C,
BddAbove (Set.range (‖f ·‖)), (⨆ i, (‖f i‖₊ : ENNReal)) < ⊤] :=
by
-- `1 ↔ 2 ↔ 3` follows from `uniformEquicontinuous_of_equicontinuousAt_zero`
tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f
tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous
tfae_have 2 → 1 := fun H ↦
H
0
-- `4 ↔ 5 ↔ 6 ↔ 7 ↔ 8 ↔ 9` is morally trivial, we just have to use a lot of rewriting
-- and `congr` lemmas
tfae_have 4 ↔ 5 := by
rw [exists_ge_and_iff_exists]
exact fun C₁ C₂ hC ↦ forall₂_imp fun i x ↦ le_trans' <| by gcongr
tfae_have 5 ↔ 7 := by
refine exists_congr (fun C ↦ and_congr_right fun hC ↦ forall_congr' fun i ↦ ?_)
rw [ContinuousLinearMap.opNorm_le_iff hC]
tfae_have 7 ↔ 8 := by simp_rw [bddAbove_iff_exists_ge (0 : ℝ), Set.forall_mem_range]
tfae_have 6 ↔ 8 := by simp_rw [bddAbove_def, Set.forall_mem_range]
tfae_have 8 ↔ 9 := by
rw [ENNReal.iSup_coe_lt_top, ← NNReal.bddAbove_coe, ← Set.range_comp]
rfl
-- `3 ↔ 4` is the interesting part of the result. It is essentially a combination of
-- `WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm` which turns
-- equicontinuity into existence of some continuous seminorm and
-- `Seminorm.bound_of_continuous_normedSpace` which characterize such seminorms.
tfae_have 3 ↔ 4 :=
by
refine ((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans ?_
rw [forall_const]
constructor
· intro ⟨p, hp, hpf⟩
rcases p.bound_of_continuous_normedSpace hp with ⟨C, -, hC⟩
exact ⟨C, fun i x ↦ (hpf i x).trans (hC x)⟩
· intro ⟨C, hC⟩
refine
⟨C.toNNReal • normSeminorm 𝕜 E, ((norm_withSeminorms 𝕜 E).continuous_seminorm 0).const_smul C.toNNReal,
fun i x ↦ ?_⟩
exact (hC i x).trans (mul_le_mul_of_nonneg_right (C.le_coe_toNNReal) (norm_nonneg x))
tfae_finish
