summable_of_locally_summable_norm

English

If a family of ContinuousMaps {F_i} is locally summable in the sense that for every compact K the restrictions have summable norms, then the whole family is summable.

Русский

Если семейство отображений {F_i} локально суммируемо по нормам ограниченных ограничений, то вся сумма по i сходится.

LaTeX

$$Summable F given Summable norms of restrictions on compacts$$

Lean4

theorem summable_of_locally_summable_norm {ι : Type*} {F : ι → C(X, E)}
    (hF : ∀ K : Compacts X, Summable fun i => ‖(F i).restrict K‖) : Summable F := by
  classical
  refine (ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => ?_
  lift K to Compacts X using hK
  have A : ∀ s : Finset ι, restrict K (∑ i ∈ s, F i) = ∑ i ∈ s, restrict K (F i) :=
    by
    intro s
    ext1 x
    simp [-SetLike.coe_sort_coe]
  simpa only [HasSum, A] using (hF K).of_norm

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