theorem exists_shadowLimit_of_fejerMonotone {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {C : Set H} (hC_nonempty : C.Nonempty) (hC_closed : IsClosed C) (hC_convex : Convex ℝ C) (xₙ : ℕ → H) (hxₙ : FejerMonotone C xₙ) : ∃ z ∈ C, Filter.Tendsto (fun (n : ℕ) => P[C, ⋯] (xₙ n)) Filter.atTop (nhds z)

Proposition 5.7 (1): if C is a nonempty closed convex subset of a real Hilbert space and xₙ is Fejer monotone with respect to C, then the projection shadow n ↦ P (xₙ n) converges strongly to some z ∈ C, where P := projectionPoint C (isChebyshev_of_nonempty_isClosed_convex hC_nonempty hC_closed hC_convex).

theorem exists_sqNorm_limits_of_fejerMonotone {H : Type u} [NormedAddCommGroup H] {C : Set H} (xₙ : ℕ → H) (hxₙ : FejerMonotone C xₙ) {z x : H} (hz : z ∈ C) (hx : x ∈ C) : ∃ (a : ℝ) (b : ℝ), Filter.Tendsto (fun (n : ℕ) => ‖xₙ n - z‖ ^ 2) Filter.atTop (nhds a) ∧ Filter.Tendsto (fun (n : ℕ) => ‖xₙ n - x‖ ^ 2) Filter.atTop (nhds b)

Proposition 5.7 (2): for a Fejér-monotone sequence and any two points z, x ∈ C, the squared-distance sequences from xₙ to z and to x admit real limits. This is the source-facing two-point packaging of the canonical one-point owner theorem FejerMonotone.dist_tendsto.

theorem sqNorm_limit_add_sqNorm_le_limit_of_shadowLimit {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {C : Set H} (hC_nonempty : C.Nonempty) (hC_closed : IsClosed C) (hC_convex : Convex ℝ C) (xₙ : ℕ → H) {z : H} (hz : Filter.Tendsto (fun (n : ℕ) => P[C, ⋯] (xₙ n)) Filter.atTop (nhds z)) {x : H} (hx : x ∈ C) {a b : ℝ} (ha : Filter.Tendsto (fun (n : ℕ) => ‖xₙ n - z‖ ^ 2) Filter.atTop (nhds a)) (hb : Filter.Tendsto (fun (n : ℕ) => ‖xₙ n - x‖ ^ 2) Filter.atTop (nhds b)) : a + ‖x - z‖ ^ 2 ≤ b

Proposition 5.7 (3): if the shadow sequence converges strongly to z and a, b are the limits of the squared-distance sequences from xₙ to z and to x ∈ C, then a + ‖x - z‖ ^ 2 ≤ b.