theorem recessionCone_sum_epigraph_prod_finite_contra {n m : ℕ} {f f0_plus : Fin m → (Fin n → ℝ) → EReal} {g : (Fin m → Fin n → ℝ) → EReal} (hg : g = fun (x : Fin m → Fin n → ℝ) => ∑ i : Fin m, f i (x i)) (hnotbot : ∀ (i : Fin m) (x : Fin n → ℝ), f i x ≠ ⊥) (_hnotbot0 : ∀ (i : Fin m) (x : Fin n → ℝ), f0_plus i x ≠ ⊥) (_hrec_i : ∀ (i : Fin m), (epigraph Set.univ (f i)).recessionCone = epigraph Set.univ (f0_plus i)) {p : (Fin m → Fin n → ℝ) × ℝ} {i0 : Fin m} {a : Fin m → ℝ} {x0 : Fin n → ℝ} {μ0 t : ℝ} (hgt0 : f i0 (x0 + t • p.1 i0) > ↑(μ0 + t * a i0)) (_hx0 : f i0 x0 ≤ ↑μ0) (ha_sum : ∑ i : Fin m, a i = p.2) {x : Fin m → Fin n → ℝ} {μ : Fin m → ℝ} (hxi0 : x i0 = x0) (hμi0 : μ i0 = μ0) (_hxle : ∀ (i : Fin m), f i (x i) ≤ ↑(μ i)) {ε : Fin m → ℝ} (hslack : ∀ (i : Fin m), i ≠ i0 → ↑(μ i + t * a i - ε i) ≤ f i (x i + t • p.1 i)) (hε : ∑ i ∈ Finset.univ.erase i0, ε i < (f i0 (x0 + t • p.1 i0)).toReal - (μ0 + t * a i0)) (hmem''' : g (x + t • p.1) ≤ ↑(∑ i : Fin m, μ i) + ↑t * ↑p.2) (htopg : ¬∃ (i : Fin m), f i (x i + t • p.1 i) = ⊤) : False

Finite-case contradiction in the non-⊤ branch of recessionCone_sum_epigraph_prod.

theorem sum_lt_sum_of_one_lt {m : ℕ} {a b : Fin m → ℝ} {i0 : Fin m} (hlt : a i0 < b i0) (hEq : ∀ (i : Fin m), i ≠ i0 → a i = b i) : ∑ i : Fin m, a i < ∑ i : Fin m, b i

A strict inequality at one component gives a strict inequality for the total sum.

theorem ereal_sum_lt_sum_of_one_lt {m : ℕ} {β : Fin m → EReal} {b : Fin m → ℝ} {i0 : Fin m} (hbot : ∀ (i : Fin m), β i ≠ ⊥) (htop : ∀ (i : Fin m), β i ≠ ⊤) (hlt : ↑(b i0) < β i0) (hEq : ∀ (i : Fin m), i ≠ i0 → β i = ↑(b i)) : ∑ i : Fin m, β i > ∑ i : Fin m, ↑(b i)

A strict inequality at one component of a finite EReal sum gives a strict inequality for the total sum (when the other components agree with the real bounds).

theorem recessionCone_sum_epigraph_prod_of_components {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {g : (Fin m → Fin n → ℝ) → EReal} (hg : g = fun (x : Fin m → Fin n → ℝ) => ∑ i : Fin m, f i (x i)) (hm : 0 < m) {v : Fin m → Fin n → ℝ} {a : Fin m → ℝ} (hnotbot : ∀ (i : Fin m) (x : Fin n → ℝ), f i x ≠ ⊥) (hrec : ∀ (i : Fin m), (v i, a i) ∈ (epigraph Set.univ (f i)).recessionCone) : (v, ∑ i : Fin m, a i) ∈ {p : (Fin m → Fin n → ℝ) × ℝ | g p.1 ≤ ↑p.2}.recessionCone

Componentwise recession directions give a recession direction for the summed epigraph.

theorem recessionCone_sum_epigraph_prod {n m : ℕ} {f f0_plus : Fin m → (Fin n → ℝ) → EReal} (hnotbot : ∀ (i : Fin m) (x : Fin n → ℝ), f i x ≠ ⊥) (hnotbot0 : ∀ (i : Fin m) (x : Fin n → ℝ), f0_plus i x ≠ ⊥) (hconv_i : ∀ (i : Fin m), Convex ℝ (epigraph Set.univ (f i))) (hrec_i : ∀ (i : Fin m), (epigraph Set.univ (f i)).recessionCone = epigraph Set.univ (f0_plus i)) : have g := fun (x : Fin m → Fin n → ℝ) => ∑ i : Fin m, f i (x i); have g0_plus := fun (x : Fin m → Fin n → ℝ) => ∑ i : Fin m, f0_plus i (x i); {p : (Fin m → Fin n → ℝ) × ℝ | g p.1 ≤ ↑p.2}.recessionCone = {p : (Fin m → Fin n → ℝ) × ℝ | g0_plus p.1 ≤ ↑p.2}

Recession cone of the sum-epigraph on the product space.