def
finite_sum_objective
{ι : Type w}
[Fintype ι]
{E : Type u}
{α : Type v}
[AddCommMonoid α]
(f : ι → E → α)
:
E → α
Definition 8.16: the incremental projected subgradient problem uses the aggregate objective
obtained by summing the component functions f i.
Instances For
@[simp]
theorem
finite_sum_objective_apply
{ι : Type w}
[Fintype ι]
{E : Type u}
{α : Type v}
[AddCommMonoid α]
(f : ι → E → α)
(x : E)
:
finite_sum_objective f x = ∑ i : ι, f i x
Evaluating the finite-sum objective at x gives the sum of the component values f i x.
theorem
isMinOn_finite_sum_objective_iff
{ι : Type w}
[Fintype ι]
{E : Type u}
{α : Type v}
[AddCommMonoid α]
[Preorder α]
{f : ι → E → α}
{C : Set E}
{x : E}
:
IsMinOn (finite_sum_objective f) C x ↔ IsMinOn (fun (y : E) => ∑ i : ι, f i y) C x
Minimizing the finite-sum objective on C is exactly minimizing the explicit sum
x ↦ ∑ i, f i x on C.