BanLat/LLexpr.lean
All source files · Download exact source
SHA-256: 313cc63220e11d1b44a792d1cfa88990a63d90e000b82484bdc80165005d1a4d
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Basic6import Mathlib.Analysis.Convex.Topology7import Mathlib.Analysis.LocallyConvex.Separation8import Mathlib.LinearAlgebra.Finsupp.LinearCombination910/-!11# Formal lattice-linear expressions1213This file defines formal lattice-linear expressions in finitely many variables14and their evaluation in an arbitrary real vector lattice. It also develops a15normal-form API: every expression is converted to a signed difference of finite16suprema of real linear combinations, with evaluation preserved in every vector17lattice.1819The main application is the Yudin theorem: a lattice-linear identity between20formal expressions holds in every vector lattice as soon as it holds on `ℝ`.21-/2223/-- A formal lattice-linear expression in `n` variables, built from the24variables by addition, real scalar multiplication, and the binary lattice25operations `⊔` and `⊓`. -/26inductive LLexpr (n : ℕ) where27 | zero : LLexpr n28 | var : Fin n → LLexpr n29 | add : LLexpr n → LLexpr n → LLexpr n30 | smul : ℝ → LLexpr n → LLexpr n31 | sup : LLexpr n → LLexpr n → LLexpr n32 | inf : LLexpr n → LLexpr n → LLexpr n3334namespace LLexpr3536open scoped BigOperators3738variable {n : ℕ}3940/-- Evaluation of a formal lattice-linear expression at an `n`-tuple of vectors41in a vector lattice. -/42def eval {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]43 [VectorLattice X] (x : Fin n → X) : LLexpr n → X44 | .zero => 045 | .var i => x i46 | .add e₁ e₂ => eval x e₁ + eval x e₂47 | .smul r e => r • eval x e48 | .sup e₁ e₂ => eval x e₁ ⊔ eval x e₂49 | .inf e₁ e₂ => eval x e₁ ⊓ eval x e₂5051/-- Rename the variables of an expression along `f`.5253This is used when two expressions depending on different finite tuples are54viewed as expressions in one concatenated tuple, and when a tuple is compressed55to the distinct elements in its range. -/56def reindexExpr {m n : ℕ} (f : Fin n → Fin m) : LLexpr n → LLexpr m57 | .zero => .zero58 | .var i => .var (f i)59 | .add e₁ e₂ => .add (reindexExpr f e₁) (reindexExpr f e₂)60 | .smul r e => .smul r (reindexExpr f e)61 | .sup e₁ e₂ => .sup (reindexExpr f e₁) (reindexExpr f e₂)62 | .inf e₁ e₂ => .inf (reindexExpr f e₁) (reindexExpr f e₂)6364section Evaluation6566variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]67 [VectorLattice X]6869@[simp] theorem eval_zero (x : Fin n → X) : eval x .zero = 0 := rfl7071@[simp] theorem eval_var (x : Fin n → X) (i : Fin n) : eval x (.var i) = x i :=72 rfl7374@[simp] theorem eval_add (x : Fin n → X) (e₁ e₂ : LLexpr n) :75 eval x (.add e₁ e₂) = eval x e₁ + eval x e₂ := rfl7677@[simp] theorem eval_smul (x : Fin n → X) (r : ℝ) (e : LLexpr n) :78 eval x (.smul r e) = r • eval x e := rfl7980@[simp] theorem eval_sup (x : Fin n → X) (e₁ e₂ : LLexpr n) :81 eval x (.sup e₁ e₂) = eval x e₁ ⊔ eval x e₂ := rfl8283@[simp] theorem eval_inf (x : Fin n → X) (e₁ e₂ : LLexpr n) :84 eval x (.inf e₁ e₂) = eval x e₁ ⊓ eval x e₂ := rfl8586@[simp]87theorem eval_reindexExpr {m n : ℕ} (x : Fin m → X)88 (f : Fin n → Fin m) (e : LLexpr n) :89 eval x (reindexExpr f e) = eval (fun i => x (f i)) e := by90 induction e <;> simp [reindexExpr, *]9192/-- Any finite family factors through an injective finite family listing its range.9394The map `f` records, for each original index, the corresponding index in the95range listing. This is useful when reducing an arbitrary finite tuple to a96tuple of distinct entries. -/97theorem exists_injective_reindex {ι : Type*} {n : ℕ} (a : Fin n → ι) :98 ∃ (m : ℕ) (b : Fin m → ι) (_ : Function.Injective b) (f : Fin n → Fin m),99 ∀ i, b (f i) = a i := by100 classical101 let s : Set ι := Set.range a102 have hs : s.Finite := Set.finite_range a103 letI : Fintype s := hs.fintype104 let e : s ≃ Fin (Fintype.card s) := Fintype.equivFin s105 refine ⟨Fintype.card s, fun j => (e.symm j).1, ?_, fun i => e ⟨a i, ⟨i, rfl⟩⟩, ?_⟩106 · intro i j hij107 exact e.symm.injective (Subtype.ext hij)108 · intro i109 simp110111end Evaluation112113/-! ### Lattice-linear combinations of a tuple -/114115section Combinations116117variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]118 [VectorLattice X]119120/-- The set of lattice-linear combinations of a tuple `x : Fin n → X`, i.e. the121image of `LLexpr n` under evaluation at `x`. -/122def combinations (x : Fin n → X) : Set X :=123 Set.range (eval x)124125end Combinations126127/-! ### Yudin's theorem -/128129/-- A formal lattice-linear expression *vanishes* on a vector lattice `X` if its130evaluation is zero for every substitution by vectors of `X`. -/131def Vanishes (X : Type*) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]132 [VectorLattice X] (e : LLexpr n) : Prop :=133 ∀ x : Fin n → X, eval x e = 0134135private theorem sup'_add_right {ι X : Type*} [AddCommGroup X] [Lattice X]136 [IsOrderedAddMonoid X] (s : Finset ι) (hs : s.Nonempty) (f : ι → X) (a : X) :137 s.sup' hs f + a = s.sup' hs (fun i => f i + a) :=138 map_finset_sup' (OrderIso.addRight a) hs f139140private theorem add_left_sup' {ι X : Type*} [AddCommGroup X] [Lattice X]141 [IsOrderedAddMonoid X] (s : Finset ι) (hs : s.Nonempty) (f : ι → X) (a : X) :142 a + s.sup' hs f = s.sup' hs (fun i => a + f i) :=143 map_finset_sup' (OrderIso.addLeft a) hs f144145/-- Non-negative scalar multiplication as a `SupHom`. This packages146`nonneg_smul_sup` so finite suprema can be mapped through scalar147multiplication by `map_finset_sup'`. -/148private def smulSupHom {X : Type*} [AddCommGroup X] [Lattice X]149 [IsOrderedAddMonoid X] [VectorLattice X] (r : ℝ) (hr : 0 ≤ r) : SupHom X X where150 toFun := fun z => r • z151 map_sup' := fun a b => nonneg_smul_sup a b r hr152153/-- A finite nonempty supremum of real linear combinations in `n` variables.154155A value `A : SupLinearCombination n` stores a finite nonempty set of coefficient156vectors. Evaluating it at `x : Fin n → X` gives the supremum of the corresponding157linear combinations of the entries of `x`. -/158structure SupLinearCombination (n : ℕ) where159 /-- The finite set of coefficient vectors. -/160 coeffs : Finset (Fin n → ℝ)161 /-- Nonemptiness of the coefficient set, avoiding any ambient completeness assumption. -/162 nonempty : coeffs.Nonempty163164namespace SupLinearCombination165166/-- Evaluate a finite supremum of linear combinations at a tuple in a vector lattice. -/167noncomputable def eval {X : Type*} [AddCommGroup X] [Lattice X]168 [IsOrderedAddMonoid X] [VectorLattice X] (A : SupLinearCombination n)169 (x : Fin n → X) : X :=170 A.coeffs.sup' A.nonempty (Fintype.linearCombination ℝ x)171172@[simp] private theorem linearCombination_zero_coeff {X : Type*} [AddCommGroup X]173 [Module ℝ X] (x : Fin n → X) :174 Fintype.linearCombination ℝ x (fun _ : Fin n => 0) = 0 := by175 change Fintype.linearCombination ℝ x (0 : Fin n → ℝ) = 0176 exact map_zero (Fintype.linearCombination ℝ x)177178/-- The supremum consisting of a single linear combination with coefficient vector `a`. -/179noncomputable def singleton (a : Fin n → ℝ) : SupLinearCombination n :=180 { coeffs := {a}181 nonempty := Finset.singleton_nonempty a }182183/-- Evaluating a singleton supremum gives the corresponding linear combination. -/184@[simp] theorem eval_singleton {X : Type*} [AddCommGroup X] [Lattice X]185 [IsOrderedAddMonoid X] [VectorLattice X] (a : Fin n → ℝ) (x : Fin n → X) :186 (singleton a).eval x = Fintype.linearCombination ℝ x a := by187 simp [eval, singleton]188189/-- Add two finite suprema by adding each coefficient vector from the first to190each coefficient vector from the second. -/191noncomputable def add (A B : SupLinearCombination n) : SupLinearCombination n := by192 classical193 exact194 { coeffs := A.coeffs.image₂ (fun a b => a + b) B.coeffs195 nonempty := A.nonempty.image₂ B.nonempty }196197/-- Evaluation turns addition of finite suprema into addition in the vector lattice. -/198@[simp] theorem eval_add {X : Type*} [AddCommGroup X] [Lattice X]199 [IsOrderedAddMonoid X] [VectorLattice X] (A B : SupLinearCombination n)200 (x : Fin n → X) :201 (A.add B).eval x = A.eval x + B.eval x := by202 classical203 unfold eval add204 rw [Finset.sup'_image₂_left]205 simp only [map_add]206 simp_rw [← add_left_sup' B.coeffs B.nonempty (fun b => Fintype.linearCombination ℝ x b)]207 rw [← sup'_add_right A.coeffs A.nonempty (fun a => Fintype.linearCombination ℝ x a)]208209/-- The pointwise supremum of two finite suprema, obtained by taking the union210of their coefficient sets. -/211noncomputable def sup (A B : SupLinearCombination n) : SupLinearCombination n :=212 { coeffs := A.coeffs ∪ B.coeffs213 nonempty := A.nonempty.mono Finset.subset_union_left }214215/-- Evaluation turns `SupLinearCombination.sup` into lattice supremum. -/216@[simp] theorem eval_sup {X : Type*} [AddCommGroup X] [Lattice X]217 [IsOrderedAddMonoid X] [VectorLattice X] (A B : SupLinearCombination n)218 (x : Fin n → X) :219 (A.sup B).eval x = A.eval x ⊔ B.eval x := by220 classical221 unfold eval sup222 rw [Finset.sup'_union]223224/-- Scale every coefficient vector in a finite supremum by the scalar `r`. -/225noncomputable def smul (r : ℝ) (A : SupLinearCombination n) :226 SupLinearCombination n := by227 classical228 exact229 { coeffs := A.coeffs.image fun a => r • a230 nonempty := A.nonempty.image _ }231232/-- For non-negative scalars, evaluation turns coefficient scaling into scalar multiplication. -/233@[simp] theorem eval_smul {X : Type*} [AddCommGroup X] [Lattice X]234 [IsOrderedAddMonoid X] [VectorLattice X] {r : ℝ} (hr : 0 ≤ r)235 (A : SupLinearCombination n) (x : Fin n → X) :236 (A.smul r).eval x = r • A.eval x := by237 classical238 unfold eval smul239 rw [Finset.sup'_image]240 change A.coeffs.sup' A.nonempty (fun a => Fintype.linearCombination ℝ x (r • a)) =241 r • A.coeffs.sup' A.nonempty (fun a => Fintype.linearCombination ℝ x a)242 simp_rw [map_smul]243 exact (map_finset_sup' (smulSupHom r hr) A.nonempty244 (fun a => Fintype.linearCombination ℝ x a)).symm245246private theorem continuousLinearMap_apply_eq_linearCombination (f : StrongDual ℝ (Fin n → ℝ))247 (a : Fin n → ℝ) :248 f a = Fintype.linearCombination ℝ249 (fun i => f (Pi.single i (1 : ℝ) : Fin n → ℝ)) a := by250 classical251 have ha : a = ∑ i, a i • (Pi.single i (1 : ℝ) : Fin n → ℝ) := by252 funext j253 simp [Pi.single_apply, Finset.sum_apply]254 calc255 f a = f (∑ i, a i • (Pi.single i (1 : ℝ) : Fin n → ℝ)) := by rw [← ha]256 _ = ∑ i, f (a i • (Pi.single i (1 : ℝ) : Fin n → ℝ)) := by rw [map_sum]257 _ = ∑ i, a i * f (Pi.single i (1 : ℝ) : Fin n → ℝ) := by simp258 _ = Fintype.linearCombination ℝ259 (fun i => f (Pi.single i (1 : ℝ) : Fin n → ℝ)) a := by260 simp [Fintype.linearCombination_apply, smul_eq_mul]261262/-- A finite-dimensional support-function criterion for membership in the263convex hull of `S`.264265If every real linear functional takes value on `p` no larger than its supremum266over `S`, then `p` belongs to the convex hull of `S`. -/267private theorem mem_convexHull_of_forall_le_sup (p : Fin n → ℝ)268 (S : Finset (Fin n → ℝ)) (hS : S.Nonempty)269 (h : ∀ r : Fin n → ℝ,270 Fintype.linearCombination ℝ r p ≤ S.sup' hS (Fintype.linearCombination ℝ r)) :271 p ∈ convexHull ℝ (S : Set (Fin n → ℝ)) := by272 classical273 by_contra hp274 obtain ⟨f, u, hfp, hsep⟩ := _root_.geometric_hahn_banach_point_closed275 (E := Fin n → ℝ)276 (convex_convexHull ℝ (S : Set (Fin n → ℝ))) (S.finite_toSet.isClosed_convexHull ℝ) hp277 let c : Fin n → ℝ := fun i => f (Pi.single i (1 : ℝ) : Fin n → ℝ)278 let r : Fin n → ℝ := fun i => -c i279 have hf_eval : ∀ a : Fin n → ℝ, f a = Fintype.linearCombination ℝ c a := fun a =>280 continuousLinearMap_apply_eq_linearCombination f a281 have hsup_lt :282 S.sup' hS (Fintype.linearCombination ℝ r) < Fintype.linearCombination ℝ r p := by283 rw [Finset.sup'_lt_iff]284 intro q hq285 have hqconv : q ∈ convexHull ℝ (S : Set (Fin n → ℝ)) :=286 subset_convexHull ℝ (S : Set (Fin n → ℝ)) hq287 have hqsep := hsep q hqconv288 have : -f q < -f p := by289 simpa using neg_lt_neg (hfp.trans hqsep)290 have hq_eval : Fintype.linearCombination ℝ r q = -f q := by291 rw [hf_eval q]292 simp [Fintype.linearCombination_apply, r, c, Finset.sum_neg_distrib, smul_eq_mul]293 have hp_eval : Fintype.linearCombination ℝ r p = -f p := by294 rw [hf_eval p]295 simp [Fintype.linearCombination_apply, r, c, Finset.sum_neg_distrib, smul_eq_mul]296 simpa [hq_eval, hp_eval] using this297 exact (not_lt_of_ge (h r)) hsup_lt298299/-- If the coefficient vector `p` is a convex combination of the coefficient300vectors in `B`, then its linear evaluation is bounded by the supremum `B.eval`.301302This is the vector-lattice step: the scalar convex-combination coefficients are303non-negative, so the pointwise order bound can be summed. -/304private theorem linearCombination_le_eval_of_mem_convexHull {X : Type*} [AddCommGroup X]305 [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (B : SupLinearCombination n)306 {p : Fin n → ℝ} (hp : p ∈ convexHull ℝ (B.coeffs : Set (Fin n → ℝ)))307 (x : Fin n → X) :308 Fintype.linearCombination ℝ x p ≤ B.eval x := by309 classical310 rw [Finset.mem_convexHull'] at hp311 obtain ⟨w, hw_nonneg, hw_sum, hw_eq⟩ := hp312 calc313 Fintype.linearCombination ℝ x p =314 Fintype.linearCombination ℝ x (∑ q ∈ B.coeffs, w q • q) := by315 rw [hw_eq]316 _ = ∑ q ∈ B.coeffs, w q • Fintype.linearCombination ℝ x q := by317 simp318 _ ≤ ∑ q ∈ B.coeffs, w q • B.eval x := by319 refine Finset.sum_le_sum fun q hq => ?_320 exact smul_le_smul_of_nonneg_left321 (Finset.le_sup' (Fintype.linearCombination ℝ x) hq) (hw_nonneg q hq)322 _ = B.eval x := by323 rw [← Finset.sum_smul, hw_sum, one_smul]324325/-- If one finite supremum of linear combinations is pointwise below another on326`ℝ^n`, then the same inequality holds after evaluation in any vector lattice. -/327theorem eval_le_of_forall_real_le {X : Type*} [AddCommGroup X]328 [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (A B : SupLinearCombination n)329 (h : ∀ r : Fin n → ℝ, A.eval r ≤ B.eval r) (x : Fin n → X) :330 A.eval x ≤ B.eval x := by331 classical332 unfold eval333 refine Finset.sup'_le A.nonempty (Fintype.linearCombination ℝ x) fun p hp => ?_334 exact linearCombination_le_eval_of_mem_convexHull B335 (mem_convexHull_of_forall_le_sup p B.coeffs B.nonempty fun r =>336 (Finset.le_sup' (Fintype.linearCombination ℝ r) hp).trans (h r)) x337338/-- If two finite suprema of linear combinations agree pointwise on `ℝ^n`, then339they agree after evaluation in any vector lattice. -/340theorem eval_eq_of_forall_real_eq {X : Type*} [AddCommGroup X]341 [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (A B : SupLinearCombination n)342 (h : ∀ r : Fin n → ℝ, A.eval r = B.eval r) (x : Fin n → X) :343 A.eval x = B.eval x :=344 le_antisymm (eval_le_of_forall_real_le A B (fun r => (h r).le) x)345 (eval_le_of_forall_real_le B A (fun r => (h r).ge) x)346347end SupLinearCombination348349/-- A signed normal form `pos - neg`, where both sides are finite suprema of350linear combinations. -/351structure NormalForm (n : ℕ) where352 /-- The positive finite supremum in the signed representation. -/353 pos : SupLinearCombination n354 /-- The negative finite supremum in the signed representation. -/355 neg : SupLinearCombination n356357namespace NormalForm358359/-- Evaluate a signed normal form at a tuple in a vector lattice. -/360noncomputable def eval {X : Type*} [AddCommGroup X] [Lattice X]361 [IsOrderedAddMonoid X] [VectorLattice X] (N : NormalForm n) (x : Fin n → X) : X :=362 N.pos.eval x - N.neg.eval x363364/-- The zero normal form. -/365noncomputable def zero : NormalForm n :=366 { pos := SupLinearCombination.singleton (fun _ : Fin n => 0)367 neg := SupLinearCombination.singleton (fun _ : Fin n => 0) }368369/-- The normal form for the `i`-th variable. -/370noncomputable def var (i : Fin n) : NormalForm n :=371 { pos := SupLinearCombination.singleton (Pi.single i (1 : ℝ) : Fin n → ℝ)372 neg := SupLinearCombination.singleton (fun _ : Fin n => 0) }373374/-- Add two signed normal forms. -/375noncomputable def add (N M : NormalForm n) : NormalForm n :=376 { pos := N.pos.add M.pos377 neg := N.neg.add M.neg }378379/-- Negate a signed normal form by swapping its positive and negative parts. -/380noncomputable def negate (N : NormalForm n) : NormalForm n :=381 { pos := N.neg382 neg := N.pos }383384/-- Scalar multiplication of signed normal forms. -/385noncomputable def smul (r : ℝ) (N : NormalForm n) : NormalForm n :=386 if 0 ≤ r then387 { pos := N.pos.smul r388 neg := N.neg.smul r }389 else390 { pos := N.neg.smul (-r)391 neg := N.pos.smul (-r) }392393/-- The lattice supremum of two signed normal forms. -/394noncomputable def sup (N M : NormalForm n) : NormalForm n :=395 { pos := (N.pos.add M.neg).sup (M.pos.add N.neg)396 neg := N.neg.add M.neg }397398/-- The lattice infimum of two signed normal forms. -/399noncomputable def inf (N M : NormalForm n) : NormalForm n :=400 negate (sup (negate N) (negate M))401402private theorem sup_sub_identity {X : Type*} [AddCommGroup X] [Lattice X]403 [IsOrderedAddMonoid X] (a b c d : X) :404 ((a + d) ⊔ (b + c)) - (c + d) = (a - c) ⊔ (b - d) := by405 have h : ((a - c) ⊔ (b - d)) + (c + d) = (a + d) ⊔ (b + c) := by406 rw [sup_add]407 congr 1 <;> abel408 rw [← h]409 abel410411/-- Evaluating the zero normal form gives zero. -/412@[simp] theorem eval_zero {X : Type*} [AddCommGroup X] [Lattice X]413 [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) :414 (zero : NormalForm n).eval x = 0 := by415 simp [eval, zero]416417/-- Evaluating a variable normal form gives the corresponding tuple entry. -/418@[simp] theorem eval_var {X : Type*} [AddCommGroup X] [Lattice X]419 [IsOrderedAddMonoid X] [VectorLattice X] (i : Fin n) (x : Fin n → X) :420 (var i).eval x = x i := by421 simp [eval, var]422423/-- Evaluation turns addition of normal forms into addition. -/424@[simp] theorem eval_add {X : Type*} [AddCommGroup X] [Lattice X]425 [IsOrderedAddMonoid X] [VectorLattice X] (N M : NormalForm n) (x : Fin n → X) :426 (add N M).eval x = N.eval x + M.eval x := by427 simp [eval, add]428 abel429430/-- Evaluation turns negation of normal forms into negation. -/431@[simp] theorem eval_negate {X : Type*} [AddCommGroup X] [Lattice X]432 [IsOrderedAddMonoid X] [VectorLattice X] (N : NormalForm n)433 (x : Fin n → X) :434 (negate N).eval x = -N.eval x := by435 simp [eval, negate]436437/-- Evaluation turns scalar multiplication of normal forms into scalar multiplication. -/438@[simp] theorem eval_smul {X : Type*} [AddCommGroup X] [Lattice X]439 [IsOrderedAddMonoid X] [VectorLattice X] (r : ℝ) (N : NormalForm n)440 (x : Fin n → X) :441 (smul r N).eval x = r • N.eval x := by442 by_cases hr : 0 ≤ r443 · simp [smul, hr, eval, smul_sub]444 · have hneg : 0 ≤ -r := by linarith445 simp [smul, hr, hneg, eval, smul_sub]446 abel447448/-- Evaluation turns supremum of normal forms into lattice supremum. -/449@[simp] theorem eval_sup {X : Type*} [AddCommGroup X] [Lattice X]450 [IsOrderedAddMonoid X] [VectorLattice X] (N M : NormalForm n) (x : Fin n → X) :451 (sup N M).eval x = N.eval x ⊔ M.eval x := by452 simp [eval, sup, sup_sub_identity]453454/-- Evaluation turns infimum of normal forms into lattice infimum. -/455@[simp] theorem eval_inf {X : Type*} [AddCommGroup X] [Lattice X]456 [IsOrderedAddMonoid X] [VectorLattice X] (N M : NormalForm n) (x : Fin n → X) :457 (inf N M).eval x = N.eval x ⊓ M.eval x := by458 simp [inf, neg_sup]459460end NormalForm461462/-- Convert an arbitrary lattice-linear expression into a signed supremum of463linear combinations, preserving evaluation in every vector lattice. -/464noncomputable def normalize : LLexpr n → NormalForm n465 | .zero => NormalForm.zero466 | .var i => NormalForm.var i467 | .add e₁ e₂ => NormalForm.add (normalize e₁) (normalize e₂)468 | .smul r e => NormalForm.smul r (normalize e)469 | .sup e₁ e₂ => NormalForm.sup (normalize e₁) (normalize e₂)470 | .inf e₁ e₂ => NormalForm.inf (normalize e₁) (normalize e₂)471472/-- The normal form of an expression has the same evaluation as the expression. -/473@[simp] theorem normalize_eval {X : Type*} [AddCommGroup X] [Lattice X]474 [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) (e : LLexpr n) :475 (normalize e).eval x = eval x e := by476 induction e <;> simp [normalize, *]477478/-- Yudin's theorem: a formal lattice-linear expression that vanishes on `ℝ`479vanishes on every vector lattice. -/480theorem vanishes_of_vanishes_real (e : LLexpr n) (h : Vanishes ℝ e)481 (X : Type*) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]482 [VectorLattice X] : Vanishes X e := by483 intro x484 have hreal : ∀ r : Fin n → ℝ, (normalize e).pos.eval r = (normalize e).neg.eval r := by485 intro r486 have hr := h r487 rw [← normalize_eval r e, NormalForm.eval] at hr488 exact sub_eq_zero.mp hr489 have hx :=490 SupLinearCombination.eval_eq_of_forall_real_eq (normalize e).pos (normalize e).neg hreal x491 rw [← normalize_eval x e, NormalForm.eval, hx, sub_self]492493/-- If the difference of two formal expressions vanishes on the reals, their494evaluations agree in every vector lattice. -/495theorem eval_eq_of_vanishes_real {X : Type*} [AddCommGroup X] [Lattice X]496 [IsOrderedAddMonoid X] [VectorLattice X] (x : Fin n → X) (e₁ e₂ : LLexpr n)497 (h : Vanishes ℝ (add e₁ (smul (-1) e₂))) :498 eval x e₁ = eval x e₂ := by499 have hX : eval x e₁ + (-1 : ℝ) • eval x e₂ = 0 :=500 (vanishes_of_vanishes_real (add e₁ (smul (-1) e₂)) h X) x501 apply sub_eq_zero.mp502 simpa [sub_eq_add_neg] using hX503504end LLexpr505