Tropicalization of finitary operations #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
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).
list α are defined as producing a value in
with_top α so proofs about lists do not
directly transfer to minima over multisets or finsets.
Note we cannot use
i ∈ s instead of
i : s here
as it is simply not true on conditionally complete lattices!