Formal lattice-linear expressions

This file defines formal lattice-linear expressions in finitely many variables and their evaluation in an arbitrary real vector lattice. It also develops a normal-form API: every expression is converted to a signed difference of finite suprema of real linear combinations, with evaluation preserved in every vector lattice.

The main application is the Yudin theorem: a lattice-linear identity between formal expressions holds in every vector lattice as soon as it holds on ℝ.

inductive LLexpr (n : ℕ) : Type

A formal lattice-linear expression in n variables, built from the variables by addition, real scalar multiplication, and the binary lattice operations ⊔ and ⊓.

• zero {n : ℕ} : LLexpr n
• var {n : ℕ} : Fin n → LLexpr n
• add {n : ℕ} : LLexpr n → LLexpr n → LLexpr n
• smul {n : ℕ} : ℝ → LLexpr n → LLexpr n
• sup {n : ℕ} : LLexpr n → LLexpr n → LLexpr n
• inf {n : ℕ} : LLexpr n → LLexpr n → LLexpr n

def LLexpr.eval {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) : LLexpr n → X

Evaluation of a formal lattice-linear expression at an n-tuple of vectors in a vector lattice.

Equations

• LLexpr.eval x LLexpr.zero = 0
• LLexpr.eval x (LLexpr.var i) = x i
• LLexpr.eval x (e₁.add e₂) = LLexpr.eval x e₁ + LLexpr.eval x e₂
• LLexpr.eval x (LLexpr.smul r e) = r • LLexpr.eval x e
• LLexpr.eval x (e₁.sup e₂) = LLexpr.eval x e₁ ⊔ LLexpr.eval x e₂
• LLexpr.eval x (e₁.inf e₂) = LLexpr.eval x e₁ ⊓ LLexpr.eval x e₂

def LLexpr.reindexExpr {m n : ℕ} (f : Fin n → Fin m) : LLexpr n → LLexpr m

Rename the variables of an expression along f.

This is used when two expressions depending on different finite tuples are viewed as expressions in one concatenated tuple, and when a tuple is compressed to the distinct elements in its range.

Equations

• LLexpr.reindexExpr f LLexpr.zero = LLexpr.zero
• LLexpr.reindexExpr f (LLexpr.var i) = LLexpr.var (f i)
• LLexpr.reindexExpr f (e₁.add e₂) = (LLexpr.reindexExpr f e₁).add (LLexpr.reindexExpr f e₂)
• LLexpr.reindexExpr f (LLexpr.smul r e) = LLexpr.smul r (LLexpr.reindexExpr f e)
• LLexpr.reindexExpr f (e₁.sup e₂) = (LLexpr.reindexExpr f e₁).sup (LLexpr.reindexExpr f e₂)
• LLexpr.reindexExpr f (e₁.inf e₂) = (LLexpr.reindexExpr f e₁).inf (LLexpr.reindexExpr f e₂)

@[simp]

theorem LLexpr.eval_zero {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) : eval x zero = 0

@[simp]

theorem LLexpr.eval_var {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) (i : Fin n) : eval x (var i) = x i

@[simp]

theorem LLexpr.eval_add {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) (e₁ e₂ : LLexpr n) : eval x (e₁.add e₂) = eval x e₁ + eval x e₂

@[simp]

theorem LLexpr.eval_smul {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) (r : ℝ) (e : LLexpr n) : eval x (smul r e) = r • eval x e

@[simp]

theorem LLexpr.eval_sup {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) (e₁ e₂ : LLexpr n) : eval x (e₁.sup e₂) = eval x e₁ ⊔ eval x e₂

@[simp]

theorem LLexpr.eval_inf {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) (e₁ e₂ : LLexpr n) : eval x (e₁.inf e₂) = eval x e₁ ⊓ eval x e₂

@[simp]

theorem LLexpr.eval_reindexExpr {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {m n : ℕ} (x : Fin m → X) (f : Fin n → Fin m) (e : LLexpr n) : eval x (reindexExpr f e) = eval (fun (i : Fin n) => x (f i)) e

theorem LLexpr.exists_injective_reindex {ι : Type u_2} {n : ℕ} (a : Fin n → ι) : ∃ (m : ℕ) (b : Fin m → ι) (_ : Function.Injective b) (f : Fin n → Fin m), ∀ (i : Fin n), b (f i) = a i

Any finite family factors through an injective finite family listing its range.

The map f records, for each original index, the corresponding index in the range listing. This is useful when reducing an arbitrary finite tuple to a tuple of distinct entries.

Lattice-linear combinations of a tuple

def LLexpr.combinations {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) : Set X

The set of lattice-linear combinations of a tuple x : Fin n → X, i.e. the image of LLexpr n under evaluation at x.

Equations

• LLexpr.combinations x = Set.range (LLexpr.eval x)

Yudin's theorem

def LLexpr.Vanishes {n : ℕ} (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : LLexpr n) : Prop

A formal lattice-linear expression vanishes on a vector lattice X if its evaluation is zero for every substitution by vectors of X.

Equations

• LLexpr.Vanishes X e = ∀ (x : Fin n → X), LLexpr.eval x e = 0

structure LLexpr.SupLinearCombination (n : ℕ) : Type

A finite nonempty supremum of real linear combinations in n variables.

A value A : SupLinearCombination n stores a finite nonempty set of coefficient vectors. Evaluating it at x : Fin n → X gives the supremum of the corresponding linear combinations of the entries of x.

• coeffs : Finset (Fin n → ℝ)

  The finite set of coefficient vectors.

• nonempty : self.coeffs.Nonempty

  Nonemptiness of the coefficient set, avoiding any ambient completeness assumption.

noncomputable def LLexpr.SupLinearCombination.eval {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (A : SupLinearCombination n) (x : Fin n → X) : X

Evaluate a finite supremum of linear combinations at a tuple in a vector lattice.

Equations

• A.eval x = A.coeffs.sup' ⋯ ⇑(Fintype.linearCombination ℝ x)

noncomputable def LLexpr.SupLinearCombination.singleton {n : ℕ} (a : Fin n → ℝ) : SupLinearCombination n

The supremum consisting of a single linear combination with coefficient vector a.

Equations

• LLexpr.SupLinearCombination.singleton a = { coeffs := {a}, nonempty := ⋯ }

@[simp]

theorem LLexpr.SupLinearCombination.eval_singleton {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (a : Fin n → ℝ) (x : Fin n → X) : (singleton a).eval x = (Fintype.linearCombination ℝ x) a

Evaluating a singleton supremum gives the corresponding linear combination.

noncomputable def LLexpr.SupLinearCombination.add {n : ℕ} (A B : SupLinearCombination n) : SupLinearCombination n

Add two finite suprema by adding each coefficient vector from the first to each coefficient vector from the second.

Equations

• A.add B = { coeffs := Finset.image₂ (fun (a b : Fin n → ℝ) => a + b) A.coeffs B.coeffs, nonempty := ⋯ }

@[simp]

theorem LLexpr.SupLinearCombination.eval_add {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (A B : SupLinearCombination n) (x : Fin n → X) : (A.add B).eval x = A.eval x + B.eval x

Evaluation turns addition of finite suprema into addition in the vector lattice.

noncomputable def LLexpr.SupLinearCombination.sup {n : ℕ} (A B : SupLinearCombination n) : SupLinearCombination n

The pointwise supremum of two finite suprema, obtained by taking the union of their coefficient sets.

Equations

• A.sup B = { coeffs := A.coeffs ∪ B.coeffs, nonempty := ⋯ }

@[simp]

theorem LLexpr.SupLinearCombination.eval_sup {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (A B : SupLinearCombination n) (x : Fin n → X) : (A.sup B).eval x = A.eval x ⊔ B.eval x

Evaluation turns SupLinearCombination.sup into lattice supremum.

noncomputable def LLexpr.SupLinearCombination.smul {n : ℕ} (r : ℝ) (A : SupLinearCombination n) : SupLinearCombination n

Scale every coefficient vector in a finite supremum by the scalar r.

Equations

• LLexpr.SupLinearCombination.smul r A = { coeffs := Finset.image (fun (a : Fin n → ℝ) => r • a) A.coeffs, nonempty := ⋯ }

@[simp]

theorem LLexpr.SupLinearCombination.eval_smul {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {r : ℝ} (hr : 0 ≤ r) (A : SupLinearCombination n) (x : Fin n → X) : (smul r A).eval x = r • A.eval x

For non-negative scalars, evaluation turns coefficient scaling into scalar multiplication.

theorem LLexpr.SupLinearCombination.eval_le_of_forall_real_le {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (A B : SupLinearCombination n) (h : ∀ (r : Fin n → ℝ), A.eval r ≤ B.eval r) (x : Fin n → X) : A.eval x ≤ B.eval x

If one finite supremum of linear combinations is pointwise below another on ℝ^n, then the same inequality holds after evaluation in any vector lattice.

theorem LLexpr.SupLinearCombination.eval_eq_of_forall_real_eq {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (A B : SupLinearCombination n) (h : ∀ (r : Fin n → ℝ), A.eval r = B.eval r) (x : Fin n → X) : A.eval x = B.eval x

If two finite suprema of linear combinations agree pointwise on ℝ^n, then they agree after evaluation in any vector lattice.

structure LLexpr.NormalForm (n : ℕ) : Type

A signed normal form pos - neg, where both sides are finite suprema of linear combinations.

• pos : SupLinearCombination n

  The positive finite supremum in the signed representation.

• neg : SupLinearCombination n

  The negative finite supremum in the signed representation.

noncomputable def LLexpr.NormalForm.eval {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (N : NormalForm n) (x : Fin n → X) : X

Evaluate a signed normal form at a tuple in a vector lattice.

Equations

• N.eval x = N.pos.eval x - N.neg.eval x

noncomputable def LLexpr.NormalForm.zero {n : ℕ} : NormalForm n

The zero normal form.

Equations

• LLexpr.NormalForm.zero = { pos := LLexpr.SupLinearCombination.singleton fun (x : Fin n) => 0, neg := LLexpr.SupLinearCombination.singleton fun (x : Fin n) => 0 }

noncomputable def LLexpr.NormalForm.var {n : ℕ} (i : Fin n) : NormalForm n

The normal form for the i-th variable.

Equations

• LLexpr.NormalForm.var i = { pos := LLexpr.SupLinearCombination.singleton (Pi.single i 1), neg := LLexpr.SupLinearCombination.singleton fun (x : Fin n) => 0 }

noncomputable def LLexpr.NormalForm.add {n : ℕ} (N M : NormalForm n) : NormalForm n

Add two signed normal forms.

Equations

• N.add M = { pos := N.pos.add M.pos, neg := N.neg.add M.neg }

noncomputable def LLexpr.NormalForm.negate {n : ℕ} (N : NormalForm n) : NormalForm n

Negate a signed normal form by swapping its positive and negative parts.

Equations

• N.negate = { pos := N.neg, neg := N.pos }

noncomputable def LLexpr.NormalForm.smul {n : ℕ} (r : ℝ) (N : NormalForm n) : NormalForm n

Scalar multiplication of signed normal forms.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LLexpr.NormalForm.sup {n : ℕ} (N M : NormalForm n) : NormalForm n

The lattice supremum of two signed normal forms.

Equations

• N.sup M = { pos := (N.pos.add M.neg).sup (M.pos.add N.neg), neg := N.neg.add M.neg }

noncomputable def LLexpr.NormalForm.inf {n : ℕ} (N M : NormalForm n) : NormalForm n

The lattice infimum of two signed normal forms.

Equations

• N.inf M = (N.negate.sup M.negate).negate

@[simp]

theorem LLexpr.NormalForm.eval_zero {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) : zero.eval x = 0

Evaluating the zero normal form gives zero.

@[simp]

theorem LLexpr.NormalForm.eval_var {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (i : Fin n) (x : Fin n → X) : (var i).eval x = x i

Evaluating a variable normal form gives the corresponding tuple entry.

@[simp]

theorem LLexpr.NormalForm.eval_add {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (N M : NormalForm n) (x : Fin n → X) : (N.add M).eval x = N.eval x + M.eval x

Evaluation turns addition of normal forms into addition.

@[simp]

theorem LLexpr.NormalForm.eval_negate {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (N : NormalForm n) (x : Fin n → X) : N.negate.eval x = -N.eval x

Evaluation turns negation of normal forms into negation.

@[simp]

theorem LLexpr.NormalForm.eval_smul {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (r : ℝ) (N : NormalForm n) (x : Fin n → X) : (smul r N).eval x = r • N.eval x

Evaluation turns scalar multiplication of normal forms into scalar multiplication.

@[simp]

theorem LLexpr.NormalForm.eval_sup {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (N M : NormalForm n) (x : Fin n → X) : (N.sup M).eval x = N.eval x ⊔ M.eval x

Evaluation turns supremum of normal forms into lattice supremum.

@[simp]

theorem LLexpr.NormalForm.eval_inf {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (N M : NormalForm n) (x : Fin n → X) : (N.inf M).eval x = N.eval x ⊓ M.eval x

Evaluation turns infimum of normal forms into lattice infimum.

noncomputable def LLexpr.normalize {n : ℕ} : LLexpr n → NormalForm n

Convert an arbitrary lattice-linear expression into a signed supremum of linear combinations, preserving evaluation in every vector lattice.

Equations

• LLexpr.zero.normalize = LLexpr.NormalForm.zero
• (LLexpr.var i).normalize = LLexpr.NormalForm.var i
• (e₁.add e₂).normalize = e₁.normalize.add e₂.normalize
• (LLexpr.smul r e).normalize = LLexpr.NormalForm.smul r e.normalize
• (e₁.sup e₂).normalize = e₁.normalize.sup e₂.normalize
• (e₁.inf e₂).normalize = e₁.normalize.inf e₂.normalize

@[simp]

theorem LLexpr.normalize_eval {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) (e : LLexpr n) : e.normalize.eval x = eval x e

The normal form of an expression has the same evaluation as the expression.

theorem LLexpr.vanishes_of_vanishes_real {n : ℕ} (e : LLexpr n) (h : Vanishes ℝ e) (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : Vanishes X e

Yudin's theorem: a formal lattice-linear expression that vanishes on ℝ vanishes on every vector lattice.

theorem LLexpr.eval_eq_of_vanishes_real {n : ℕ} {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) (e₁ e₂ : LLexpr n) (h : Vanishes ℝ (e₁.add (smul (-1) e₂))) : eval x e₁ = eval x e₂

If the difference of two formal expressions vanishes on the reals, their evaluations agree in every vector lattice.