Interpolation of finitely many binary selector labels

Lax342547.SelectorInterpolation · concepts/Lax342547/SelectorInterpolation.lean · lax-342547

proven

Loading review…

The second assertion of Lemma 5.1: any u distinct selector evaluation vectors are linearly independent when the degree bound is at least u−1.

Concept map

2 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

Show types on hover

1	import Lax342547.MomentSpace
2	import Mathlib.LinearAlgebra.LinearIndependent.Defs
3
4	/-!
5	---
6	title: Interpolation of finitely many binary selector labels
7	type: lemma
8	---
9	The second assertion of Lemma 5.1: any u distinct selector evaluation
10	vectors are linearly independent when the degree bound is at least u−1.
11	-/
12
13	namespace Lax342547.SelectorInterpolation
14
15	open Lax342547.MomentSpace
16
17	def monomial {b : ℕ} (S : Finset (Fin b)) : (Fin b → Binary) → Binary :=
18	fun s => ∏ i ∈ S, s i
19
20	def selectorSpan (b degree : ℕ) : Submodule Binary ((Fin b → Binary) → Binary) :=
21	Submodule.span Binary {f \| ∃ S : Finset (Fin b), S.card ≤ degree ∧ f = monomial S}
22
23	axiom selectorEval_linearIndependent {ι : Type} [Fintype ι] {b degree : ℕ}
24	(s : ι → Fin b → Binary) (hs : Function.Injective s)
25	(hdegree : Fintype.card ι ≤ degree + 1) :
26	LinearIndependent Binary (fun i => selectorEval (degree := degree) (s i))
27
28	end Lax342547.SelectorInterpolation
29