theorem
IsBlockProximalGradientProblem.randomized_block_proximal_gradient_iterate_mem_effective_domain
{ι : Type u}
[Fintype ι]
{Ei : ι → Type v}
[(i : ι) → NormedAddCommGroup (Ei i)]
[(i : ι) → InnerProductSpace ℝ (Ei i)]
[∀ (i : ι), ProperSpace (Ei i)]
{Li : ι → ↑PosReal}
{f : ((i : ι) → Ei i) → EReal}
{g : (i : ι) → Ei i → EReal}
{block_gradient : (i : ι) → ((j : ι) → Ei j) → Ei i}
{XStar : Set ((i : ι) → Ei i)}
{FOpt : ℝ}
(hproblem : IsBlockProximalGradientProblem f g block_gradient XStar FOpt Li)
(x0 : ↑(effective_domain (separableSum g)))
(sampled_block : ℕ → ι)
(k : ℕ)
:
randomized_block_proximal_gradient_method hproblem (↑(hproblem.interior_effective_domain_point x0)) sampled_block k ∈ effective_domain (separableSum g)
Every realized RBPG iterate remains in the effective domain of the block-separable regularizer, provided the initial point does.
theorem
RandomizedBlockProximalGradientAssumptions.randomized_block_proximal_gradient_sufficient_decrease
{ι : Type u}
[Fintype ι]
{Ei : ι → Type v}
[(i : ι) → NormedAddCommGroup (Ei i)]
[(i : ι) → InnerProductSpace ℝ (Ei i)]
[∀ (i : ι), ProperSpace (Ei i)]
{Li : ι → ↑PosReal}
{f : ((i : ι) → Ei i) → EReal}
{g : (i : ι) → Ei i → EReal}
{block_gradient : (i : ι) → ((j : ι) → Ei j) → Ei i}
{XStar : Set ((i : ι) → Ei i)}
{FOpt : ℝ}
(hproblem : RandomizedBlockProximalGradientAssumptions f g block_gradient XStar FOpt Li)
(x0 : ↑(effective_domain (separableSum g)))
(sampled_block : ℕ → ι)
(k : ℕ)
:
composite_model_objective f (separableSum g)
(randomized_block_proximal_gradient_method ⋯ (↑(⋯.interior_effective_domain_point x0)) sampled_block k) - composite_model_objective f (separableSum g)
(randomized_block_proximal_gradient_method ⋯ (↑(⋯.interior_effective_domain_point x0)) sampled_block (k + 1)) ≥ ↑(1 / (2 * ↑(Li (sampled_block k))) * ‖⋯.gradient_mapping (Li (sampled_block k)) (sampled_block k)
(randomized_block_proximal_gradient_method ⋯ (↑(⋯.interior_effective_domain_point x0)) sampled_block k)‖ ^ 2)
Theorem 11.13: along any realized RBPG sample path, each step decreases the composite
objective by at least (1 / (2 L_{i_k})) ‖G^{i_k}_{L_{i_k}}(x^k)‖^2.