mathlib3 documentation

algebra.tropical.big_operators

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 #

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.

theorem list.trop_sum {R : Type u_1} [add_monoid R] (l : list R) :

tropical.trop l.sum = (list.map tropical.trop l).prod

theorem multiset.trop_sum {R : Type u_1} [add_comm_monoid R] (s : multiset R) :

tropical.trop s.sum = (multiset.map tropical.trop s).prod

theorem trop_sum {R : Type u_1} {S : Type u_2} [add_comm_monoid R] (s : finset S) (f : S → R) :

tropical.trop (s.sum (λ (i : S), f i)) = s.prod (λ (i : S), tropical.trop (f i))

theorem list.untrop_prod {R : Type u_1} [add_monoid R] (l : list (tropical R)) :

tropical.untrop l.prod = (list.map tropical.untrop l).sum

theorem multiset.untrop_prod {R : Type u_1} [add_comm_monoid R] (s : multiset (tropical R)) :

tropical.untrop s.prod = (multiset.map tropical.untrop s).sum

theorem untrop_prod {R : Type u_1} {S : Type u_2} [add_comm_monoid R] (s : finset S) (f : S → tropical R) :

tropical.untrop (s.prod (λ (i : S), f i)) = s.sum (λ (i : S), tropical.untrop (f i))

theorem list.trop_minimum {R : Type u_1} [linear_order R] (l : list R) :

tropical.trop l.minimum = (list.map (tropical.trop ∘ coe) l).sum

theorem multiset.trop_inf {R : Type u_1} [linear_order R] [order_top R] (s : multiset R) :

tropical.trop s.inf = (multiset.map tropical.trop s).sum

theorem finset.trop_inf {R : Type u_1} {S : Type u_2} [linear_order R] [order_top R] (s : finset S) (f : S → R) :

tropical.trop (s.inf f) = s.sum (λ (i : S), tropical.trop (f i))

theorem trop_Inf_image {R : Type u_1} {S : Type u_2} [conditionally_complete_linear_order R] (s : finset S) (f : S → with_top R) :

tropical.trop (has_Inf.Inf (f '' ↑s)) = s.sum (λ (i : S), tropical.trop (f i))

theorem trop_infi {R : Type u_1} {S : Type u_2} [conditionally_complete_linear_order R] [fintype S] (f : S → with_top R) :

tropical.trop (⨅ (i : S), f i) = finset.univ.sum (λ (i : S), tropical.trop (f i))

theorem multiset.untrop_sum {R : Type u_1} [linear_order R] [order_top R] (s : multiset (tropical R)) :

tropical.untrop s.sum = (multiset.map tropical.untrop s).inf

theorem finset.untrop_sum' {R : Type u_1} {S : Type u_2} [linear_order R] [order_top R] (s : finset S) (f : S → tropical R) :

tropical.untrop (s.sum (λ (i : S), f i)) = s.inf (tropical.untrop ∘ f)

theorem untrop_sum_eq_Inf_image {R : Type u_1} {S : Type u_2} [conditionally_complete_linear_order R] (s : finset S) (f : S → tropical (with_top R)) :

tropical.untrop (s.sum (λ (i : S), f i)) = has_Inf.Inf (tropical.untrop ∘ f '' ↑s)

theorem untrop_sum {R : Type u_1} {S : Type u_2} [conditionally_complete_linear_order R] [fintype S] (f : S → tropical (with_top R)) :

tropical.untrop (finset.univ.sum (λ (i : S), f i)) = ⨅ (i : S), tropical.untrop (f i)

theorem finset.untrop_sum {R : Type u_1} {S : Type u_2} [conditionally_complete_linear_order R] (s : finset S) (f : S → tropical (with_top R)) :

tropical.untrop (s.sum (λ (i : S), f i)) = ⨅ (i : ↥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!