class is_generated_by_randomized_generalized_block_conditional_gradient_method {Ξ : Type w} {ι : Type v} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] (g : (i : ι) → Ei i → EReal) (block_gradient : (i : ι) → ((j : ι) → Ei j) → Ei i) (x : ℕ → Ξ → PiLp 2 Ei) (sampled_block : ℕ → Ξ → ι) (point : (k : ℕ) → (ω : Ξ) → Ei (sampled_block k ω)) (t : ℕ → ↑(Set.Icc 0 1)) : Prop

Source-faithful generated-sequence owner for Theorem 13.29: along each sample path the iterates satisfy the RGBCG trajectory clauses, and the realized sampled-block minimizer is chosen by a deterministic block rule depending only on the current iterate and sampled block. This keeps the textbook “generated by the RGBCG method” condition on the theorem surface without exposing the point-rule premise as a separate theorem hypothesis.

• trajectory (ω : Ξ) : is_randomized_generalized_block_conditional_gradient_trajectory g block_gradient (fun (n : ℕ) => x n ω) (fun (n : ℕ) => sampled_block n ω) (fun (n : ℕ) => point n ω) t

  Every sample path is a realized RGBCG trajectory.

• point_rule : ∃ (pointRule : (i : ι) → PiLp 2 Ei → Ei i), ∀ (n : ℕ) (ω : Ξ), point n ω = pointRule (sampled_block n ω) (x n ω)

  The sampled-block minimizer is selected by a deterministic point rule.