Linear functionals on β → ℝ for a finite index type β

• functional_eq_sum — φ v = ∑ b, φ (e_b) * v b;
• coeff_nonneg — if φ is bounded below on the nonnegative orthant, its coefficients φ (e_b) are nonnegative.

Both are used in Dual/Cover.lean, where they turn the separating functional given by the Hahn–Banach theorem into a vector κ ≥ 0 with φ v = ∑_S κ_S v_S.

theorem AaronsonAmbainis.Dual.eq_sum_single {β : Type u_1} [Fintype β] [DecidableEq β] (v : β → ℝ) : v = ∑ b : β, v b • Pi.single b 1

Every vector is the sum of its coordinates times the unit vectors.

theorem AaronsonAmbainis.Dual.functional_eq_sum {β : Type u_1} [Fintype β] [DecidableEq β] (φ : (β → ℝ) →L[ℝ] ℝ) (v : β → ℝ) : φ v = ∑ b : β, φ (Pi.single b 1) * v b

theorem AaronsonAmbainis.Dual.coeff_nonneg {β : Type u_1} [DecidableEq β] (φ : (β → ℝ) →L[ℝ] ℝ) (r : ℝ) (h : ∀ (v : β → ℝ), (∀ (b : β), 0 ≤ v b) → r < φ v) (b : β) : 0 ≤ φ (Pi.single b 1)