SummableLocallyUniformlyOn_of_locally_bounded

English

If there is a local bound (locally bounded) for f_n on each compact K ⊂ s, then SummableLocallyUniformlyOn f on s.

Русский

Если для каждой локальной ограниченности на каждом компакте K ⊂ s выполнено неравенство, тогда Sum локально однородно на s.

LaTeX

$$$\\text{If } \\exists u:α→ℝ\\,\\text{with } ∑u<∞ \\text{ and } ∀K⊆s, IsCompact K → (∀ x∈K, ‖f_n x‖≤u_n) , \\Rightarrow \\ SummableLocallyUniformlyOn f s$$$

Lean4

theorem SummableLocallyUniformlyOn_of_locally_bounded [TopologicalSpace β] [LocallyCompactSpace β] {f : α → β → F}
    {s : Set β} (hs : IsOpen s) (hu : ∀ K ⊆ s, IsCompact K → ∃ u : α → ℝ, Summable u ∧ ∀ n, ∀ k ∈ K, ‖f n k‖ ≤ u n) :
    SummableLocallyUniformlyOn f s :=
  by
  apply SummableLocallyUniformlyOn.of_locally_bounded_eventually hs
  intro K hK hKc
  obtain ⟨u, hu1, hu2⟩ := hu K hK hKc
  exact ⟨u, hu1, by filter_upwards using hu2⟩

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