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 #
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 WithTop α so proofs about lists do not
directly transfer to minima over multisets or finsets.
theorem
List.trop_sum
{R : Type u_1}
[AddMonoid R]
(l : List R)
:
Tropical.trop (List.sum l) = List.prod (List.map Tropical.trop l)
theorem
Multiset.trop_sum
{R : Type u_1}
[AddCommMonoid R]
(s : Multiset R)
:
Tropical.trop (Multiset.sum s) = Multiset.prod (Multiset.map Tropical.trop s)
theorem
trop_sum
{R : Type u_1}
{S : Type u_2}
[AddCommMonoid R]
(s : Finset S)
(f : S → R)
:
Tropical.trop (Finset.sum s fun (i : S) => f i) = Finset.prod s fun (i : S) => Tropical.trop (f i)
theorem
Multiset.untrop_prod
{R : Type u_1}
[AddCommMonoid R]
(s : Multiset (Tropical R))
:
Tropical.untrop (Multiset.prod s) = Multiset.sum (Multiset.map Tropical.untrop s)
theorem
untrop_prod
{R : Type u_1}
{S : Type u_2}
[AddCommMonoid R]
(s : Finset S)
(f : S → Tropical R)
:
Tropical.untrop (Finset.prod s fun (i : S) => f i) = Finset.sum s fun (i : S) => Tropical.untrop (f i)
theorem
List.trop_minimum
{R : Type u_1}
[LinearOrder R]
(l : List R)
:
Tropical.trop (List.minimum l) = List.sum (List.map (Tropical.trop ∘ WithTop.some) l)
theorem
Multiset.trop_inf
{R : Type u_1}
[LinearOrder R]
[OrderTop R]
(s : Multiset R)
:
Tropical.trop (Multiset.inf s) = Multiset.sum (Multiset.map Tropical.trop s)
theorem
Finset.trop_inf
{R : Type u_1}
{S : Type u_2}
[LinearOrder R]
[OrderTop R]
(s : Finset S)
(f : S → R)
:
Tropical.trop (Finset.inf s f) = Finset.sum s fun (i : S) => Tropical.trop (f i)
theorem
trop_sInf_image
{R : Type u_1}
{S : Type u_2}
[ConditionallyCompleteLinearOrder R]
(s : Finset S)
(f : S → WithTop R)
:
Tropical.trop (sInf (f '' ↑s)) = Finset.sum s fun (i : S) => Tropical.trop (f i)
theorem
trop_iInf
{R : Type u_1}
{S : Type u_2}
[ConditionallyCompleteLinearOrder R]
[Fintype S]
(f : S → WithTop R)
:
Tropical.trop (⨅ (i : S), f i) = Finset.sum Finset.univ fun (i : S) => Tropical.trop (f i)
theorem
Multiset.untrop_sum
{R : Type u_1}
[LinearOrder R]
[OrderTop R]
(s : Multiset (Tropical R))
:
Tropical.untrop (Multiset.sum s) = Multiset.inf (Multiset.map Tropical.untrop s)
theorem
Finset.untrop_sum'
{R : Type u_1}
{S : Type u_2}
[LinearOrder R]
[OrderTop R]
(s : Finset S)
(f : S → Tropical R)
:
Tropical.untrop (Finset.sum s fun (i : S) => f i) = Finset.inf s (Tropical.untrop ∘ f)
theorem
untrop_sum_eq_sInf_image
{R : Type u_1}
{S : Type u_2}
[ConditionallyCompleteLinearOrder R]
(s : Finset S)
(f : S → Tropical (WithTop R))
:
Tropical.untrop (Finset.sum s fun (i : S) => f i) = sInf (Tropical.untrop ∘ f '' ↑s)
theorem
untrop_sum
{R : Type u_1}
{S : Type u_2}
[ConditionallyCompleteLinearOrder R]
[Fintype S]
(f : S → Tropical (WithTop R))
:
Tropical.untrop (Finset.sum Finset.univ fun (i : S) => f i) = ⨅ (i : S), Tropical.untrop (f i)
theorem
Finset.untrop_sum
{R : Type u_1}
{S : Type u_2}
[ConditionallyCompleteLinearOrder R]
(s : Finset S)
(f : S → Tropical (WithTop R))
:
Tropical.untrop (Finset.sum s fun (i : S) => f i) = ⨅ (i : { x : S // x ∈ s }), Tropical.untrop (f ↑i)
Note we cannot use i ∈ s instead of i : s here
as it is simply not true on conditionally complete lattices!