theorem
composite_objective_effective_domain_iff_separableSum
{p : ℕ}
{Ei : Fin p → Type u}
{f : ((i : Fin p) → Ei i) → ℝ}
{g : (i : Fin p) → Ei i → EReal}
{z : (i : Fin p) → Ei i}
:
z ∈ effective_domain (composite_model_objective (Function.toEReal f) (separableSum g)) ↔ z ∈ effective_domain (separableSum g)
Helper for Chapter 14 composite-domain API: the effective domain of
f.toEReal + separableSum g is exactly the effective domain of separableSum g.
theorem
composite_objective_ne_bot
{p : ℕ}
{Ei : Fin p → Type u}
[(i : Fin p) → NormedAddCommGroup (Ei i)]
[(i : Fin p) → NormedSpace ℝ (Ei i)]
{f : ((i : Fin p) → Ei i) → ℝ}
{g : (i : Fin p) → Ei i → EReal}
(hmodel : IsAlternatingMinimizationCompositeModel (Function.toEReal f) g)
(z : (i : Fin p) → Ei i)
:
composite_model_objective (Function.toEReal f) (separableSum g) z ≠ ⊥
Helper for Chapter 14 composite-domain API: the composite objective
f.toEReal + separableSum g never takes the value -∞.
theorem
composite_block_mem_effective_domain_of_mem
{p : ℕ}
{Ei : Fin p → Type u}
[(i : Fin p) → NormedAddCommGroup (Ei i)]
[(i : Fin p) → NormedSpace ℝ (Ei i)]
{f : ((i : Fin p) → Ei i) → ℝ}
{g : (i : Fin p) → Ei i → EReal}
(hmodel : IsAlternatingMinimizationCompositeModel (Function.toEReal f) g)
{x : (i : Fin p) → Ei i}
(hx : x ∈ effective_domain (composite_model_objective (Function.toEReal f) (separableSum g)))
(i : Fin p)
:
x i ∈ effective_domain (g i)
Helper for Chapter 14 composite-domain API: finiteness of the composite objective at x
forces each block value g_i(x_i) to be finite.
theorem
composite_update_mem_effective_domain_of_block_mem
{p : ℕ}
{Ei : Fin p → Type u}
[(i : Fin p) → NormedAddCommGroup (Ei i)]
[(i : Fin p) → NormedSpace ℝ (Ei i)]
{f : ((i : Fin p) → Ei i) → ℝ}
{g : (i : Fin p) → Ei i → EReal}
(hmodel : IsAlternatingMinimizationCompositeModel (Function.toEReal f) g)
{x : (i : Fin p) → Ei i}
(i : Fin p)
{yi : Ei i}
(hx : x ∈ effective_domain (composite_model_objective (Function.toEReal f) (separableSum g)))
(hyi : yi ∈ effective_domain (g i))
:
Function.update x i yi ∈ effective_domain (composite_model_objective (Function.toEReal f) (separableSum g))
Helper for Chapter 14 composite-domain API: replacing one block by another point of
effective_domain (g i) preserves membership in the effective domain of
f.toEReal + separableSum g.