Closed-Subspace Selection With A Frequently Bounded Hilbert Component

This is a closed-subspace selection lemma in a product of normed spaces.

Let $X$ be a real normed space, let $H$ be a complete real Hilbert space, and let $G\subseteq X\times H$ be a closed real submodule. Suppose sequences $x_n\in X$ and $y_n\in H$ satisfy

1. $(x_n,y_n)\in G$ for every $n$;
2. $x_n\to x_0$;
3. for some real $L$, the inequality $\|y_n\|\le L$ holds frequently along $n\to\infty$.

Then there exists $y_0\in H$ such that

The Lean declaration is exists_mem_of_isClosed_of_frequently_norm_le_readable. “Frequently” is the filter-theoretic condition along atTop, not an eventual bound.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy. Shown in its original module context. Proof omitted.

theorem exists_mem_of_isClosed_of_frequently_norm_le
    {G : Submodule ℝ (X × H)} (hG : IsClosed (G : Set (X × H)))
    {x : ℕ → X} {y : ℕ → H} (hxy : ∀ n, (x n, y n) ∈ G)
    {x₀ : X} (hx : Tendsto x atTop (𝓝 x₀)) {L : ℝ} (hL : ∃ᶠ n in atTop, ‖y n‖ ≤ L) :
    ∃ y₀ : H, (x₀, y₀) ∈ G ∧ ‖y₀‖ ≤ L

Module navigation

Module: Energy/Relaxation/LinearPMap.

Next: sequentialRelaxation_ofLinearPMap_le.

Source excerpt, lines 51–55 · Frozen source 408915f.