feat(algebra/tropical/big_operators): sum, prod, Inf (#10544)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

src/algebra/tropical/big_operators.lean

@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2021 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import algebra.tropical.lattice
+import algebra.big_operators.basic
+import data.list.min_max
+
+/-!
+
+# Tropicalization of finitary operations
+
+This file provides the "big-op" or notation-based finitary operations on tropicalized types.
+This allows easy conversion between sums to Infs and prods to sums. Results here are important
+for expressing that evaluation of tropical polynomials are the minimum over a finite piecewise
+collection of linear functions.
+
+## Main declarations
+
+* `untrop_sum`
+
+## Implementation notes
+
+No concrete (semi)ring is used here, only ones with inferrable order/lattice structure, to support
+real, rat, ereal, and others (erat is not yet defined).
+
+Minima over `list α` are defined as producing a value in `with_top α` so proofs about lists do not
+directly transfer to minima over multisets or finsets.
+
+-/
+
+
+open_locale big_operators
+
+variables {R S : Type*}
+
+open tropical finset
+
+lemma list.trop_sum [add_monoid R] (l : list R) : trop l.sum = list.prod (l.map trop) :=
+begin
+  induction l with hd tl IH,
+  { simp },
+  { simp [←IH] }
+end
+
+lemma multiset.trop_sum [add_comm_monoid R] (s : multiset R) :
+  trop s.sum = multiset.prod (s.map trop) :=
+quotient.induction_on s (by simpa using list.trop_sum)
+
+lemma trop_sum [add_comm_monoid R] (s : finset S) (f : S → R) :
+  trop (∑ i in s, f i) = ∏ i in s, trop (f i) :=
+begin
+  cases s,
+  convert multiset.trop_sum _,
+  simp
+end
+
+lemma list.untrop_prod [add_monoid R] (l : list (tropical R)) :
+  untrop l.prod = list.sum (l.map untrop) :=
+begin
+  induction l with hd tl IH,
+  { simp },
+  { simp [←IH] }
+end
+
+lemma multiset.untrop_prod [add_comm_monoid R] (s : multiset (tropical R)) :
+  untrop s.prod = multiset.sum (s.map untrop) :=
+quotient.induction_on s (by simpa using list.untrop_prod)
+
+lemma untrop_prod [add_comm_monoid R] (s : finset S) (f : S → tropical R) :
+  untrop (∏ i in s, f i) = ∑ i in s, untrop (f i) :=
+begin
+  cases s,
+  convert multiset.untrop_prod _,
+  simp
+end
+
+lemma list.trop_minimum [linear_order R] (l : list R) :
+  trop l.minimum = list.sum (l.map (trop ∘ coe)) :=
+begin
+  induction l with hd tl IH,
+  { simp },
+  { simp [list.minimum_cons, ←IH] }
+end
+
+lemma multiset.trop_inf [linear_order R] [order_top R] (s : multiset R) :
+  trop s.inf = multiset.sum (s.map trop) :=
+begin
+  induction s using multiset.induction with s x IH,
+  { simp },
+  { simp [←IH] }
+end
+
+lemma finset.trop_inf [linear_order R] [order_top R] (s : finset S) (f : S → R) :
+  trop (s.inf f) = ∑ i in s, trop (f i) :=
+begin
+  cases s,
+  convert multiset.trop_inf _,
+  simp
+end
+
+lemma trop_Inf_image [conditionally_complete_linear_order R] (s : finset S)
+  (f : S → with_top R) : trop (Inf (f '' s)) = ∑ i in s, trop (f i) :=
+begin
+  rcases s.eq_empty_or_nonempty with rfl|h,
+  { simp only [set.image_empty, coe_empty, sum_empty, with_top.cInf_empty, trop_top] },
+  rw [←inf'_eq_cInf_image _ h, inf'_eq_inf],
+  convert s.trop_inf f,
+  refine lattice.ext _,
+  intros,
+  exact iff.rfl
+end
+
+lemma trop_infi [conditionally_complete_linear_order R] [fintype S] (f : S → with_top R) :
+  trop (⨅ (i : S), f i) = ∑ (i : S), trop (f i) :=
+by rw [infi, ←set.image_univ, ←coe_univ, trop_Inf_image]
+
+lemma multiset.untrop_sum [linear_order R] [order_top R] (s : multiset (tropical R)) :
+  untrop s.sum = multiset.inf (s.map untrop) :=
+begin
+  induction s using multiset.induction with s x IH,
+  { simp },
+  { simpa [←IH] }
+end
+
+lemma finset.untrop_sum' [linear_order R] [order_top R] (s : finset S)
+  (f : S → tropical R) : untrop (∑ i in s, f i) = s.inf (untrop ∘ f) :=
+begin
+  cases s,
+  convert multiset.untrop_sum _,
+  simpa
+end
+
+lemma untrop_sum_eq_Inf_image [conditionally_complete_linear_order R] (s : finset S)
+  (f : S → tropical (with_top R)) :
+  untrop (∑ i in s, f i) = Inf (untrop ∘ f '' s) :=
+begin
+  rcases s.eq_empty_or_nonempty with rfl|h,
+  { simp only [set.image_empty, coe_empty, sum_empty, with_top.cInf_empty, untrop_zero] },
+  rw [←inf'_eq_cInf_image _ h, inf'_eq_inf],
+  convert s.untrop_sum' f,
+  refine lattice.ext _,
+  intros,
+  exact iff.rfl
+end
+
+lemma untrop_sum [conditionally_complete_linear_order R] [fintype S]
+  (f : S → tropical (with_top R)) :
+  untrop (∑ i : S, f i) = ⨅ i : S, untrop (f i) :=
+by rw [infi, ←set.image_univ, ←coe_univ, untrop_sum_eq_Inf_image]
+
+/-- Note we cannot use `i ∈ s` instead of `i : s` here
+as it is simply not true on conditionally complete lattices! -/
+lemma finset.untrop_sum [conditionally_complete_linear_order R] (s : finset S)
+  (f : S → tropical (with_top R)) : untrop (∑ i in s, f i) = ⨅ i : s, untrop (f i) :=
+by simpa [←untrop_sum] using sum_attach.symm

src/algebra/tropical/lattice.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2021 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import algebra.tropical.basic
+import order.conditionally_complete_lattice
+
+/-!
+
+# Order on tropical algebraic structure
+
+This file defines the orders induced on tropical algebraic structures by the underlying type.
+
+## Main declarations
+
+* `conditionally_complete_lattice (tropical R)`
+* `conditionally_complete_linear_order (tropical R)`
+
+## Implementation notes
+
+The order induced is the definitionally equal underlying order, which makes the proofs and
+constructions quicker to implement.
+
+-/
+
+variables {R S : Type*}
+
+open tropical
+
+instance [has_sup R] : has_sup (tropical R) :=
+{ sup := λ x y, trop (untrop x ⊔ untrop y) }
+
+instance [has_inf R] : has_inf (tropical R) :=
+{ inf := λ x y, trop (untrop x ⊓ untrop y) }
+
+instance [semilattice_inf R] : semilattice_inf (tropical R) :=
+{ le_inf := λ _ _ _, le_inf,
+  inf_le_left := λ _ _, inf_le_left,
+  inf_le_right := λ _ _, inf_le_right,
+  ..tropical.has_inf,
+  ..tropical.partial_order }
+
+instance [semilattice_sup R] : semilattice_sup (tropical R) :=
+{ sup_le := λ _ _ _, sup_le,
+  le_sup_left := λ _ _, le_sup_left,
+  le_sup_right := λ _ _, le_sup_right,
+  ..tropical.has_sup,
+  ..tropical.partial_order }
+
+instance [lattice R] : lattice (tropical R) :=
+{ ..tropical.semilattice_inf, ..tropical.semilattice_sup }
+
+instance [has_Sup R] : has_Sup (tropical R) :=
+{ Sup := λ s, trop (Sup (untrop '' s)) }
+
+instance [has_Inf R] : has_Inf (tropical R) :=
+{ Inf := λ s, trop (Inf (untrop '' s)) }
+
+instance [conditionally_complete_lattice R] : conditionally_complete_lattice (tropical R) :=
+{ le_cSup := λ s x hs hx, le_cSup
+    (untrop_monotone.map_bdd_above hs)
+    (set.mem_image_of_mem untrop hx),
+  cSup_le := λ s x hs hx, cSup_le
+    (hs.image untrop)
+    (untrop_monotone.mem_upper_bounds_image hx),
+  le_cInf := λ s x hs hx, le_cInf
+    (hs.image untrop)
+    (untrop_monotone.mem_lower_bounds_image hx),
+  cInf_le := λ s x hs hx, cInf_le
+    (untrop_monotone.map_bdd_below hs)
+    (set.mem_image_of_mem untrop hx),
+  ..tropical.has_Sup,
+  ..tropical.has_Inf,
+  ..tropical.lattice }
+
+instance [conditionally_complete_linear_order R] :
+  conditionally_complete_linear_order (tropical R) :=
+{ ..tropical.conditionally_complete_lattice,
+  ..tropical.linear_order }