theorem ERealFunction.isMinimizingSequence_of_tendsto_of_mem_argmin_real {f : ℝ → ↑(Set.Ioi ⊥)} (hf : f ∈ Γ₀(ℝ)) {xₙ : ℕ → ℝ} (hxdom : ∀ (n : ℕ), xₙ n ∈ effectiveDomain f) {x : ℝ} (hxmin : x ∈ Argmin (Function.asEReal f)) (hstrong : Filter.Tendsto xₙ Filter.atTop (nhds x)) : IsMinimizingSequence (Function.asEReal f) xₙ

Remark 11.22 (1): clause (i), real case. For a function in Γ₀(ℝ), any sequence in the effective domain that converges strongly to a global minimizer is a minimizing sequence.

theorem ERealFunction.isMinimizingSequence_of_tendsto_of_mem_argmin_of_mem_interior_effectiveDomain {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {f : H → ↑(Set.Ioi ⊥)} (hf : f ∈ Γ₀(H)) {xₙ : ℕ → H} (hxdom : ∀ (n : ℕ), xₙ n ∈ effectiveDomain f) {x : H} (hxmin : x ∈ Argmin (Function.asEReal f)) (hstrong : Filter.Tendsto xₙ Filter.atTop (nhds x)) (hxint : x ∈ interior (effectiveDomain f)) : IsMinimizingSequence (Function.asEReal f) xₙ

Remark 11.22 (2): clause (i), interior-domain case. For a function in Γ₀(H), any sequence in the effective domain that converges strongly to a global minimizer lying in the interior of the effective domain is a minimizing sequence.

theorem ERealFunction.exists_strongly_convergent_to_mem_argmin_not_isMinimizingSequence : ∃ (f : ℝ × ℝ → ↑(Set.Ioi ⊥)) (xₙ : ℕ → ℝ × ℝ) (x : ℝ × ℝ), f ∈ Γ₀(ℝ × ℝ) ∧ (∀ (n : ℕ), xₙ n ∈ effectiveDomain f) ∧ Filter.Tendsto xₙ Filter.atTop (nhds x) ∧ x ∈ Argmin (Function.asEReal f) ∧ ¬IsMinimizingSequence (Function.asEReal f) xₙ

Remark 11.22 (3): clause (ii). Strong convergence to a global minimizer does not force a minimizing sequence in general; there is already a finite-dimensional counterexample.

theorem ERealFunction.orthonormal_weakly_convergent_to_interior_mem_argmin_not_isMinimizingSequence {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {xₙ : ℕ → H} (hxₙ : Orthonormal ℝ xₙ) : Filter.Tendsto (fun (n : ℕ) => (toWeakSpace ℝ H) (xₙ n)) Filter.atTop (nhds ((toWeakSpace ℝ H) 0)) ∧ 0 ∈ interior (dom fun (y : H) => ↑‖y‖) ∧ (0 ∈ Argmin fun (y : H) => ↑‖y‖) ∧ ¬IsMinimizingSequence (fun (y : H) => ↑‖y‖) xₙ

Remark 11.22 (4): clause (iii). Any orthonormal sequence in a real Hilbert space converges weakly to the interior minimizer 0 of the norm function, but it is not a minimizing sequence for x ↦ ‖x‖.

theorem ERealFunction.exists_orthonormal_weakly_convergent_to_interior_mem_argmin_not_isMinimizingSequence {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (h_infinite : ¬FiniteDimensional ℝ H) : ∃ (xₙ : ℕ → H), Orthonormal ℝ xₙ ∧ Filter.Tendsto (fun (n : ℕ) => (toWeakSpace ℝ H) (xₙ n)) Filter.atTop (nhds ((toWeakSpace ℝ H) 0)) ∧ 0 ∈ interior (dom fun (y : H) => ↑‖y‖) ∧ (0 ∈ Argmin fun (y : H) => ↑‖y‖) ∧ ¬IsMinimizingSequence (fun (y : H) => ↑‖y‖) xₙ

Companion bridge for Remark 11.22 (4): in an infinite-dimensional real Hilbert space, the preceding orthonormal-sequence statement yields an explicit weakly convergent non-minimizing counterexample for the norm objective.