Finset of subtype

Stream: new members

[Patrick Stevens]

I am proving, in effect, that the mean of a bounded finset is less than or equal to its bound. (I'm doing this in a form that has cleared the denominators, because ultimately I want this lemma for finset nat.) The proof of mean_le_biggest_aux is fine - to get the induction to go through, I needed the elements to know individually that they were bounded, so I proved it for finset {x : A // f x <= m }. But now I can't work out how to convert a pair (s : finset A, proof that every x in s is bounded by m) into a finset {x : A // f x <= m}. I've noted the existence of subtype.coind, which lets me construct a finset {x : A // a ∈ s -> f a <= m}, and in about ten lines I can probably squeeze this into the thing I need, but this seems torturous. Is there a better way?

import data.subtype
import tactic

open_locale big_operators

lemma mean_le_biggest_aux {A B : Type*} [decidable_eq A] [ordered_semiring B]
  (f : A → B) {m : B} : ∀ (s : finset { x : A // f x ≤ m }), ∑ i in s, f i ≤ m * (s.card) :=
begin
  intros s,
  apply finset.induction_on s,
  {simp,},
  { intros a s a_not_in ind,
    rw [finset.card_insert_of_not_mem a_not_in, finset.sum_insert a_not_in],
    calc f a + (∑ i in s, f i)
        = (∑ i in s, f i) + f a : add_comm _ _
    ... ≤ (∑ i in s, f i) + m : add_le_add_left a.property _
    ... ≤ (m * ↑(s.card)) + m : add_le_add_right ind m
    ... = (m * ↑(s.card)) + (m * 1) : by simp only [mul_one m]
    ... = m * (↑(s.card) + 1) : (mul_add m ↑(finset.card s) 1).symm, },
end

/--
"The mean of a bounded list is less than or equal to the bound".
-/
lemma mean_le_biggest {A B : Type*} [decidable_eq A] [ordered_semiring B]
  (f : A → B) {m : B} (s : finset A) (bound : ∀ x ∈ s, f x ≤ m) : ∑ i in s, f i ≤ m * (s.card) :=
begin
  --let u := finset.image (@subtype.coind A A id (λ a, a ∈ s → f a ≤ m) bound) s,
  sorry
end

[Bhavik Mehta]

Take a look at finset.attach, I think

[Reid Barton]

Obvious statements like this should not require induction. Take a look at sum_le_sum and sum_const.

[Reid Barton]

If you have to resort to induction to prove a statement like this, it means there is a gap in the library.

[Bhavik Mehta]

If I change the statement a little, I can manage it:

lemma mean_le_biggest {A B : Type*} [decidable_eq A] [ordered_semiring B]
  (f : A → B) {m : B} (s : finset A) (bound : ∀ x ∈ s, f x ≤ m) : ∑ i in s, f i ≤ s.card * m :=
begin
  rw [← add_monoid.smul_eq_mul, ← finset.sum_const],
  apply finset.sum_le_sum bound,
end

[Bhavik Mehta]

There's a bunch of useful stuff in algebra.big_operators, just in case you're not aware

[Patrick Stevens]

I'm aware of the existence of big_operators, but there's a lot of stuff there and I still don't have a good story for discovering things in it

[Patrick Stevens]

In this instance I'm not sure I would have thought of going via sum_le_sum for a long time - I wrote a maths proof before starting and it went "easy induction", not "every element of [max, max,…] is bigger than [a1, a2,…]; now take sums"

[Jalex Stark]

weird, the latter is definitely the easier math proof

[Jalex Stark]

I think big_operators is not such a scary file, it may save you time in the long run to read all the theorem statements once

[Jalex Stark]

I guess you can get just the theorem statements from the docs page

i don't understand the docs linkifier yet

[Jalex Stark]

does src#algebra.big_operators work? no, I guess we either need a better linkifier or better documentation for it (this is brand new obviously it's not supposed to be optimized yet)

[Bhavik Mehta]

Jalex Stark said:

I think big_operators is not such a scary file, it may save you time in the long run to read all the theorem statements once

Yeah this was my strategy

[Bhavik Mehta]

src#finset.sum_le_sum

[Bryan Gin-ge Chen]

Jalex Stark said:

does src#algebra.big_operators work? no, I guess we either need a better linkifier or better documentation for it (this is brand new obviously it's not supposed to be optimized yet)

The linkifier relies on mathlib_docs/find which currently only contains redirects for actual declaration names, not mathlib module names.

[Bryan Gin-ge Chen]

I think algebra.big_operators could use some more extensive module docs and a linting run, if you feel like contributing while going over it.

[Bhavik Mehta]

By the way I figured out how to do it without having to change your statement, in case that's useful:

lemma mean_le_biggest {A B : Type*} [decidable_eq A] [ordered_semiring B]
  (f : A → B) {m : B} (s : finset A) (bound : ∀ x ∈ s, f x ≤ m) : ∑ i in s, f i ≤ m * s.card :=
begin
  rw [← add_monoid.smul_eq_mul', ← finset.sum_const],
  apply finset.sum_le_sum bound,
end

[Patrick Stevens]

Thanks - I was happy rewriting commutativity at the call site