@[reducible, inline]

noncomputable abbrev GeneralizedBlockConditionalGradient.blockGradient {ι : Type v} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] [∀ (i : ι), CompleteSpace (Ei i)] (f : PiLp 2 Ei → EReal) (i : ι) : ((j : ι) → Ei j) → Ei i

The canonical RGBCG block gradient is the Chapter 11 block partial gradient ∇[i] (fun z ↦ (f z).toReal), evaluated at the PiLp point corresponding to the raw block tuple y. This is the Chapter 13 bridge/view map used when translating the source-facing PiLp problem into the Chapter 11 raw-product owner.

@[simp]

theorem GeneralizedBlockConditionalGradient.blockGradient_apply {ι : Type v} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] [∀ (i : ι), CompleteSpace (Ei i)] (f : PiLp 2 Ei → EReal) (i : ι) (y : (j : ι) → Ei j) : blockGradient f i y = (∇[i] fun (z : PiLp 2 Ei) => (f z).toReal) ((PiLp.continuousLinearEquiv 2 ℝ Ei).symm y)

Evaluating the canonical RGBCG block gradient at (i, y) recovers the corresponding block partial gradient of x ↦ (f x).toReal on PiLp 2 Ei.

@[simp]

theorem GeneralizedBlockConditionalGradient.blockGradient_coord_apply {ι : Type v} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] [∀ (i : ι), CompleteSpace (Ei i)] (f : PiLp 2 Ei → EReal) (i : ι) (x : PiLp 2 Ei) : blockGradient f i ((PiLp.continuousLinearEquiv 2 ℝ Ei) x) = (∇[i] fun (z : PiLp 2 Ei) => (f z).toReal) x

Evaluating the RGBCG bridge map at the raw coordinates of x : PiLp 2 Ei recovers the source-facing block partial gradient at x.

class IsGeneralizedBlockConditionalGradientProblem {ι : Type v} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] [∀ (i : ι), CompleteSpace (Ei i)] (f : PiLp 2 Ei → EReal) (g : (i : ι) → Ei i → EReal) (Li : ι → ↑PosReal) : Prop

Assumption 13.28: clauses (A)-(D) for the randomized generalized block conditional-gradient method are expressed directly on the chapter objects f : X → EReal, the block penalties g_i, the canonical PiLp block gradient ∇[i] (fun z ↦ (f z).toReal). The public owner keeps only the primitive regularity, domain-compatibility, differentiability, and block-Lipschitz clauses on the PiLp model; the canonical optimizer set unconstrained_problem_solutions (composite_model_objective f (PiLp.separableSum g)) and optimal value generalized_conditional_gradient_optimal_value f (PiLp.separableSum g) are derived below rather than stored as wrapper parameters. The one-block update and slice are written in the canonical Chapter 11 textbook form x + 𝒰[i] d.

• block_g_proper (i : ι) : IsProperExtendedRealFunction (g i)
• block_g_closed (i : ι) : LowerSemicontinuous (g i)
• block_g_convex (i : ι) : is_convex_function (g i)
• g_effective_domain_compact (i : ι) : IsCompact (effective_domain (g i))
• f_ne_bot (x : PiLp 2 Ei) : f x ≠ ⊥
• f_convex : is_convex_function f
• g_effective_domain_subset_f_effective_domain : effective_domain (PiLp.separableSum g) ⊆ effective_domain f
• f_effective_domain_open : IsOpen (effective_domain f)
• f_toReal_differentiableOn_effective_domain : DifferentiableOn ℝ (fun (x : PiLp 2 Ei) => (f x).toReal) (effective_domain f)
• block_partial_gradient_lipschitz (i : ι) {x : PiLp 2 Ei} {d : Ei i} (hx : x ∈ effective_domain f) (hxd : x + PiLp.single 2 i d ∈ effective_domain f) : ‖(∇[i] fun (z : PiLp 2 Ei) => (f z).toReal) x - (∇[i] fun (z : PiLp 2 Ei) => (f z).toReal) (x + PiLp.single 2 i d)‖ ≤ ↑(Li i) * ‖d‖

instance instIsProperExtendedRealFunctionSmoothTerm {ι : Type v} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] [∀ (i : ι), CompleteSpace (Ei i)] {f : PiLp 2 Ei → EReal} {g : (i : ι) → Ei i → EReal} {Li : ι → ↑PosReal} (h : IsGeneralizedBlockConditionalGradientProblem f g Li) : IsProperExtendedRealFunction f

A generalized block conditional-gradient problem canonically makes the smooth term f a proper extended-real-valued function.

instance instIsProperExtendedRealFunctionBlockPenalty {ι : Type v} [Fintype ι] {Ei : ι → Type v} [(i : ι) → NormedAddCommGroup (Ei i)] [(i : ι) → InnerProductSpace ℝ (Ei i)] [∀ (i : ι), CompleteSpace (Ei i)] {f : PiLp 2 Ei → EReal} {g : (i : ι) → Ei i → EReal} {Li : ι → ↑PosReal} (h : IsGeneralizedBlockConditionalGradientProblem f g Li) (i : ι) : IsProperExtendedRealFunction (g i)

Each block penalty is proper by the source-facing owner field block_g_proper.