Extending a finite coordinate functional

A linear functional on a finite coordinate set determines a state on the whole index type by evaluating coordinate indicators. Its value on any finitely supported integral vector depends only on those finite coordinates.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finiteCoordinateState {S : Type u_1} (H : Finset S) (L : (↥H → ℝ) →ₗ[ℝ] ℝ) (x : S) : ℝ

Extend a functional on a finite coordinate set by zero outside that set.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finiteCoordinateState H L x = L fun (j : ↥H) => if ↑j = x then 1 else 0

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finiteCoordinateState_eq_zero_of_not_mem {S : Type u_1} (H : Finset S) (L : (↥H → ℝ) →ₗ[ℝ] ℝ) {x : S} (hx : x ∉ H) : finiteCoordinateState H L x = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.linearCombination_finiteCoordinateState {S : Type u_1} (H : Finset S) (L : (↥H → ℝ) →ₗ[ℝ] ℝ) (v : S →₀ ℤ) : (Finsupp.linearCombination ℤ (finiteCoordinateState H L)) v = L fun (j : ↥H) => ↑(v ↑j)

Evaluating a finitely supported integral vector against the extended state agrees with restricting its coordinates and applying the functional.