proving lemmas about infi

Stream: new members

[Yakov Pechersky]

What's the proper way to induct on a fintype? I'm trying to prove a lemma like the following:

import algebra.tropical.basic
import data.real.basic

variables {R S α : Type*}

open_locale big_operators
open tropical

lemma trop_infi [fintype S] (f : S → with_top ℝ) :
  trop (⨅ (i : S), f i) = ∑ (i : S), trop (f i) := sorry

[Eric Rodriguez]

docs#fintype.trunc_rec_empty_option?

[Yakov Pechersky]

That's close, but I am not sure how to deconstruct or generalize S here to employ that or docs#fintype.induction_empty_option.

[Eric Wieser]

Why don't you write that in terms of a finset instead?

[Yakov Pechersky]

infi is only defined as over an indexed type.

[Yakov Pechersky]

or do you mean a doubly-coerced finset?

[Eric Wieser]

Oh nevermind, that's inf not prod. But you might still have an easier time with something like:

lemma trop_infi {s : finset α} (f : α → with_top ℝ) :
  trop (Sup (f '' s)) = ∑ i in s, trop (f i) :=
begin
  obtain rfl | h := s.eq_empty_or_nonempty,
  { simp, sorry },
  rw ←finset.sup'_eq_cSup_image _ h,
  sorry
end

[Eric Wieser]

Oh, I mean Inf not Sup

[Eric Wieser]

But anyway, prove the version about finset.inf' first

[Kevin Buzzard]

A mathematician wouldn't induct on a fintype, they'd induct on the size of a fintype (because mathematicians only know about induction on nat). Why not prove "for all n, fintype.card X = n -> (what you want)"

[Kevin Buzzard]

Alternatively prove it for fin n and then prove it moves along bijections

[Eric Wieser]

@[simp] lemma trop_inf [linear_order α] (a b : α) : trop (a ⊓ b) = trop a + trop b := rfl

lemma trop_finset_inf {s : finset α} (f : α → with_top ℝ) :
  trop (s.inf f) = ∑ i in s, trop (f i) :=
begin
  induction s using finset.cons_induction with a s ha ih,
  simp,
  simp [ih],
end

lemma trop_Inf_image {s : finset α} (f : α → with_top ℝ) :
  trop (Inf (f '' s)) = ∑ i in s, trop (f i) :=
begin
  obtain rfl | h := s.eq_empty_or_nonempty,
  { simp, },
  rw [←finset.inf'_eq_cInf_image _ h, finset.inf'_eq_inf, trop_finset_inf],
end

lemma trop_infi [fintype S] (f : S → with_top ℝ) :
  trop (⨅ (i : S), f i) = ∑ (i : S), trop (f i) :=
by rw [infi, ←set.image_univ, ←finset.coe_univ, trop_Inf_image]

[Reid Barton]

Kevin Buzzard said:

A mathematician wouldn't induct on a fintype

Fixed

[Reid Barton]

It would be nice to have some general notion of what it means for a fintype/finset operation to be an n-ary version of a binary operation with unit, and what it means for a function to carry one such operation to another, because the structure of arguments like these are all the same.

[Yakov Pechersky]

It also has to be a commutative operation. Wouldn't the notion be foldr for lists, and then fold and mapped fold for multisets and finsets? One issue we have is that not all multiset fold specializations exist in list (compare multiset.inf vs list.minimum). Also, finset big ops have an additional implied map/image step, compared to multisets. So the general notion could be some sort of metaprogram, that taking a proof of the "correct binary behavior", generates the associated list, multiset, finset, and fintype lemmas.

[Eric Wieser]

Associative, commutative, and with-identity operation; we'd need to unify monoid, add_monoid, and semilattice_inf_bot I think (or translate in a meta-program)

[Johan Commelin]

Can't the is_commutative class be used for that generalisation?

[Eric Wieser]

The generalization I'm referring to would be followed by generalizing monoid_hom A B to something like monoid_hom A B (⊓) (+) or monoid_hom A B (⊓) ⊥ (+) 0