Coordinates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

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.

def OAI.MatrixMultiplication.AuxiliarySeparation.finiteCoordinateState line 19
Source documentation
Extend a functional on a finite coordinate set by zero outside that set.
```
def finiteCoordinateState {S : Type*} (H : Finset S)
    (L : (H → ℝ) →ₗ[ℝ] ℝ) (x : S) : ℝ := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.finiteCoordinateState_eq_zero_of_not_mem line 24
theorem OAI.MatrixMultiplication.AuxiliarySeparation.linearCombination_finiteCoordinateState line 37
Source documentation
Evaluating a finitely supported integral vector against the extended state agrees with restricting its coordinates and applying the functional.
```
theorem linearCombination_finiteCoordinateState {S : Type*}
    (H : Finset S) (L : (H → ℝ) →ₗ[ℝ] ℝ) (v : S →₀ ℤ) :
    Finsupp.linearCombination ℤ (finiteCoordinateState H L) v =
      L (fun j : H ↦ (v j : ℝ)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.finiteCoordinateState