noncomputable def relaxedProjectionFamily {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {I : Type v} (C : I → Set H) (hC_closed : ∀ (j : I), IsClosed (C j)) (hC_convex : ∀ (j : I), Convex ℝ (C j)) (hC_inter_nonempty : (⋂ (j : I), C j).Nonempty) (β : I → ℝ) : I → H → H

The relaxed projector family Tᵢ = (1 - βᵢ) Id + βᵢ P_{Cᵢ} attached to a family of nonempty closed convex sets with nonempty common intersection.

@[simp]

theorem relaxedProjectionFamily_apply {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {I : Type v} (C : I → Set H) (hC_closed : ∀ (j : I), IsClosed (C j)) (hC_convex : ∀ (j : I), Convex ℝ (C j)) (hC_inter_nonempty : (⋂ (j : I), C j).Nonempty) (β : I → ℝ) (j : I) (x : H) : relaxedProjectionFamily C hC_closed hC_convex hC_inter_nonempty β j x = (1 - β j) • x + β j • P[C j, ⋯] x

Evaluating the relaxed projector family gives the textbook formula Tᵢ x = (1 - βᵢ) x + βᵢ P_{Cᵢ} x.

@[reducible, inline]

noncomputable abbrev stringBlockCompositionOperator {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {I : Type v} {p : ℕ+} (m : Fin ↑p → ℕ+) (i : (k : Fin ↑p) → Fin ↑(m k) → I) (C : I → Set H) (hC_closed : ∀ (j : I), IsClosed (C j)) (hC_convex : ∀ (j : I), Convex ℝ (C j)) (hC_inter_nonempty : (⋂ (j : I), C j).Nonempty) (β : I → ℝ) (k : Fin ↑p) : H → H

The k-th ordered block composition of the relaxed projector family.

@[simp]

theorem stringBlockCompositionOperator_eq_finiteComposition {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {I : Type v} {p : ℕ+} (m : Fin ↑p → ℕ+) (i : (k : Fin ↑p) → Fin ↑(m k) → I) (C : I → Set H) (hC_closed : ∀ (j : I), IsClosed (C j)) (hC_convex : ∀ (j : I), Convex ℝ (C j)) (hC_inter_nonempty : (⋂ (j : I), C j).Nonempty) (β : I → ℝ) (k : Fin ↑p) : stringBlockCompositionOperator m i C hC_closed hC_convex hC_inter_nonempty β k = finiteComposition fun (l : Fin ↑(m k)) => relaxedProjectionFamily C hC_closed hC_convex hC_inter_nonempty β (i k l)

The k-th string block operator is the ordered composition of the relaxed projectors indexed by that block.

@[reducible, inline]

noncomputable abbrev stringAveragedRelaxedProjectionOperator {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {I : Type v} {p : ℕ+} (ω : Fin ↑p → ℝ) (m : Fin ↑p → ℕ+) (i : (k : Fin ↑p) → Fin ↑(m k) → I) (C : I → Set H) (hC_closed : ∀ (j : I), IsClosed (C j)) (hC_convex : ∀ (j : I), Convex ℝ (C j)) (hC_inter_nonempty : (⋂ (j : I), C j).Nonempty) (β : I → ℝ) : H → H

The string-averaged relaxed projection operator given by the weighted average of the ordered block compositions of the relaxed projectors.

@[simp]

theorem stringAveragedRelaxedProjectionOperator_apply {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {I : Type v} {p : ℕ+} (ω : Fin ↑p → ℝ) (m : Fin ↑p → ℕ+) (i : (k : Fin ↑p) → Fin ↑(m k) → I) (C : I → Set H) (hC_closed : ∀ (j : I), IsClosed (C j)) (hC_convex : ∀ (j : I), Convex ℝ (C j)) (hC_inter_nonempty : (⋂ (j : I), C j).Nonempty) (β : I → ℝ) (x : H) : stringAveragedRelaxedProjectionOperator ω m i C hC_closed hC_convex hC_inter_nonempty β x = ∑ k : Fin ↑p, ω k • stringBlockCompositionOperator m i C hC_closed hC_convex hC_inter_nonempty β k x

Evaluating the string-averaged relaxed projection operator gives the weighted sum of the block compositions of the relaxed projector family.

noncomputable def stringAveragedRelaxedProjectionOrbit {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {I : Type v} {p : ℕ+} (ω : Fin ↑p → ℝ) (m : Fin ↑p → ℕ+) (i : (k : Fin ↑p) → Fin ↑(m k) → I) (C : I → Set H) (hC_closed : ∀ (j : I), IsClosed (C j)) (hC_convex : ∀ (j : I), Convex ℝ (C j)) (hC_inter_nonempty : (⋂ (j : I), C j).Nonempty) (β : I → ℝ) (x₀ : H) : ℕ → H

The orbit generated by iterating the string-averaged relaxed projection operator from x₀.

theorem stringAveragedRelaxedProjectionOrbit_succ {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {I : Type v} {p : ℕ+} (ω : Fin ↑p → ℝ) (m : Fin ↑p → ℕ+) (i : (k : Fin ↑p) → Fin ↑(m k) → I) (C : I → Set H) (hC_closed : ∀ (j : I), IsClosed (C j)) (hC_convex : ∀ (j : I), Convex ℝ (C j)) (hC_inter_nonempty : (⋂ (j : I), C j).Nonempty) (β : I → ℝ) (x₀ : H) (n : ℕ) : stringAveragedRelaxedProjectionOrbit ω m i C hC_closed hC_convex hC_inter_nonempty β x₀ (n + 1) = stringAveragedRelaxedProjectionOperator ω m i C hC_closed hC_convex hC_inter_nonempty β (stringAveragedRelaxedProjectionOrbit ω m i C hC_closed hC_convex hC_inter_nonempty β x₀ n)

The string-averaged relaxed projection orbit satisfies the recursion xₙ₊₁ = S xₙ, where S is the associated string-averaged relaxed projection operator.

theorem exists_tendsto_weakly_to_point_in_iInter_of_stringAveragedRelaxedProjectionOrbit {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {I : Type v} {p : ℕ+} (m : Fin ↑p → ℕ+) (i : (k : Fin ↑p) → Fin ↑(m k) → I) (C : I → Set H) (hC_closed : ∀ (j : I), IsClosed (C j)) (hC_convex : ∀ (j : I), Convex ℝ (C j)) (hC_inter_nonempty : (⋂ (j : I), C j).Nonempty) (β : I → ℝ) (hβ : ∀ (j : I), β j ∈ Set.Ioo 0 2) (ω : Fin ↑p → ℝ) (hω : ∀ (k : Fin ↑p), ω k ∈ Set.Ioc 0 1) (hω_sum : ∑ k : Fin ↑p, ω k = 1) (hcover : Function.Surjective fun (q : (k : Fin ↑p) × Fin ↑(m k)) => i q.fst q.snd) (x₀ : H) : ∃ z ∈ ⋂ (j : I), C j, Filter.Tendsto (fun (n : ℕ) => (toWeakSpace ℝ H) (stringAveragedRelaxedProjectionOrbit ω m i C hC_closed hC_convex hC_inter_nonempty β x₀ n)) Filter.atTop (nhds ((toWeakSpace ℝ H) z))

Example 5.21: for a finite family of closed convex sets with nonempty intersection, the orbit generated by weighted string averages of the relaxed projectors Tᵢ = (1 - βᵢ) Id + βᵢ P_{Cᵢ} converges weakly to a point of the common intersection.