Zulip Chat Archive

Stream: new members

Topic: monotone decreasing ```ℕ → ℕ```


view this post on Zulip Damiano Testa (Sep 09 2020 at 08:25):

Dear All,

I want to prove the lemma below, stating essentially which is an easy consequence of the fact that the map rev_at is monotone decreasing. If I formulated it correctly, it says the following. Given a finite subset s of , the "reflected" set, formed of the elements (max s) - e as e ∈ s, has as maximum the "reflection" of the minimum (max s) - (min s).

I found monotone, but I think that it is only non-decreasing. Note that, due to how subtraction works, every natural number above max s squashes to 0: this is not a problem, since I never evaluate at those naturals.

Thanks!

import tactic

open finset

def rev_at (N : ) :    := λ i :  , (N-i)

lemma min_max {s : finset } {hs : s.nonempty} : max' (image (rev_at (max' s hs)) s) (by exact nonempty.image hs (rev_at (max' s hs))) = rev_at (max' s hs) (min' s hs) :=
begin
  sorry,
end

view this post on Zulip Kenny Lau (Sep 09 2020 at 08:29):

I think there's a simpler way to state that a map is monotone decreasing

view this post on Zulip Damiano Testa (Sep 09 2020 at 08:30):

I'd be happy to know how to do it! I tried looking for it, but could not find it...

view this post on Zulip Kenny Lau (Sep 09 2020 at 08:30):

x <= y -> f y <= f x?

view this post on Zulip Damiano Testa (Sep 09 2020 at 08:30):

(I found a lot of lemmas with maxs, mins, sups,... for monotone non-decreasing maps, but I could not find monotone non-increasing lemmas

view this post on Zulip Damiano Testa (Sep 09 2020 at 08:31):

Kenny Lau said:

x <= y -> f y <= f x?

The map rev_at satisfies this condition. Is there then a lemma saying what I want?

view this post on Zulip Kenny Lau (Sep 09 2020 at 08:32):

I'm just objecting your statement that min_max is the right way to say that a map is monotone decreasing

view this post on Zulip Damiano Testa (Sep 09 2020 at 08:33):

Kenny Lau said:

I'm just objecting your statement that min_max is the right way to say that a map is monotone decreasing

Ah, I see! I had meant that my lemma is an immediate consequence of the fact that rev_at is monotone non-increasing! Sorry! I will correct it.

view this post on Zulip Kenny Lau (Sep 09 2020 at 08:33):

then generalize the lemma and remove rev_at

view this post on Zulip Damiano Testa (Sep 09 2020 at 08:35):

Ok, how do I introduce the hypothesis that a map N->N is monotone non-increasing? The lemma that I stated already exists for monotone non-increasing maps and I would like to use something that is already available, if possible

view this post on Zulip Kenny Lau (Sep 09 2020 at 08:36):

just say that x <= y -> f y <= f x

view this post on Zulip Kenny Lau (Sep 09 2020 at 08:36):

also generalize the domain and codomain

view this post on Zulip Damiano Testa (Sep 09 2020 at 08:48):

Is this what you had in mind? The lemma that I want follows easily from the statement below.

import tactic

open finset

def mon {α β : Type} [decidable_linear_order α] [decidable_linear_order β] (f : α  β) :=  (x y : α), x  y  f y  f x

lemma min_max {α β : Type} [decidable_linear_order α] [decidable_linear_order β] {s : finset α} {hs : s.nonempty} {f : α  β} {mf : mon f} : max' (image f s) (by exact nonempty.image hs f) = f (min' s hs) :=
begin
  sorry,
end

view this post on Zulip Damiano Testa (Sep 09 2020 at 08:49):

But I still cannot find this last statement in mathlib...

view this post on Zulip Kenny Lau (Sep 09 2020 at 08:57):

yeah now you can prove it

view this post on Zulip Kenny Lau (Sep 09 2020 at 08:57):

you don't need decidable for mon

view this post on Zulip Kenny Lau (Sep 09 2020 at 08:57):

also make it \{{x y : \a\}}

view this post on Zulip Damiano Testa (Sep 09 2020 at 08:58):

Kenny Lau said:

also make it \{{x y : \a\}}

What does this mean?

view this post on Zulip Johan Commelin (Sep 09 2020 at 08:59):

It's something in between {x y} and (x y)

view this post on Zulip Johan Commelin (Sep 09 2020 at 09:00):

The thing is... if you use (x y), then you have to write them down all the time, when you use your lemma

view this post on Zulip Johan Commelin (Sep 09 2020 at 09:01):

With {x y} and {{x y}} you tell Lean that you want it to figure them out itself.

view this post on Zulip Johan Commelin (Sep 09 2020 at 09:01):

But the difference between the two is how greedy Lean is when trying to do this.

view this post on Zulip Damiano Testa (Sep 09 2020 at 09:01):

ok, i knew one curly bracket, but not two

view this post on Zulip Damiano Testa (Sep 09 2020 at 09:01):

i see, thanks!

view this post on Zulip Johan Commelin (Sep 09 2020 at 09:01):

With {x y} it will try to figure out x and y as soon as possible.

view this post on Zulip Johan Commelin (Sep 09 2020 at 09:02):

But with {{x y}} it will leave them as part of the expression, until you start filling in arguments that come after them.

view this post on Zulip Damiano Testa (Sep 09 2020 at 09:02):

so, I should try to prove this lemma, then?

def mon {α β : Type*} [linear_order α] [linear_order β] (f : α  β) :=  x y : α⦄, x  y  f y  f x

lemma min_max_mon {α β : Type*} [decidable_linear_order α] [decidable_linear_order β]
  {s : finset α} (hs : s.nonempty) {f : α  β} (mf : mon f) :
  max' (image f s) (by exact nonempty.image hs f) = f (min' s hs) :=
begin
  sorry,
end

view this post on Zulip Kenny Lau (Sep 09 2020 at 09:03):

make hs explicit

view this post on Zulip Kenny Lau (Sep 09 2020 at 09:03):

and also mf

view this post on Zulip Kenny Lau (Sep 09 2020 at 09:04):

and also use more newlines

view this post on Zulip Kenny Lau (Sep 09 2020 at 09:05):

wow we can copy codes now?

view this post on Zulip Kenny Lau (Sep 09 2020 at 09:05):

also indentation is 2 spaces not 1

view this post on Zulip Kenny Lau (Sep 09 2020 at 09:05):

also \{{x not \{{ x

view this post on Zulip Damiano Testa (Sep 09 2020 at 09:05):

(I have been updating the code above, so your statements do not seem to make sense!)

view this post on Zulip Kenny Lau (Sep 09 2020 at 09:07):

also hs.image f

view this post on Zulip Damiano Testa (Sep 09 2020 at 09:09):

I cannot believe how many issues there were with my coding grammar...

view this post on Zulip Kenny Lau (Sep 09 2020 at 09:10):

by exact can go

view this post on Zulip Damiano Testa (Sep 09 2020 at 09:10):

One question: using {α β : Type*} can the universes of α and β be different?
A: Yes.

view this post on Zulip Kenny Lau (Sep 09 2020 at 09:11):

what does the goal say?

view this post on Zulip Damiano Testa (Sep 09 2020 at 09:11):

1 goal
α: Type u_1
β: Type u_2
_inst_1: decidable_linear_order α
_inst_2: decidable_linear_order β
s: finset α
hs: s.nonempty
f: α  β
mf: mon f
 (image f s).max' _ = f (s.min' hs)

view this post on Zulip Damiano Testa (Sep 09 2020 at 09:12):

good, thanks!

view this post on Zulip Damiano Testa (Sep 09 2020 at 12:31):

In case anyone is keeping track, below is a solution to my question!
Thanks for @Kenny Lau and @Johan Commelin for helping me!

import tactic

open finset

def mon {α β : Type*} [linear_order α] [linear_order β] (f : α  β) :=  x y : α⦄, x  y  f y  f x

lemma min_max_mon {α β : Type*} [decidable_linear_order α] [decidable_linear_order β]
  {s : finset α} (hs : s.nonempty) {f : α  β} (mf : mon f) :
  max' (image f s) (hs.image f) = f (min' s hs) :=
begin
  apply le_antisymm,
    { refine (image f s).max'_le (nonempty.image hs f) (f (min' s hs)) _,
      intros x hx,
      rw mem_image at hx,
      rcases hx with  b , bs , rfl,
      apply mf,
      apply min'_le,
      assumption, },
    { apply le_max',
      refine mem_image_of_mem f _,
      exact min'_mem s hs, },
end

def rev_at (N : ) :    := λ i :  , (N-i)

lemma min_max {s : finset } {hs : s.nonempty} : max' (image (rev_at (max' s hs)) s) (by exact nonempty.image hs (rev_at (max' s hs))) = rev_at (max' s hs) (min' s hs) :=
begin
  refine min_max_mon hs _,
  intros x y hxy,
  unfold rev_at,
  omega,
end

view this post on Zulip Kenny Lau (Sep 09 2020 at 12:39):

we should really have finset.forall_mem_image

view this post on Zulip Kenny Lau (Sep 09 2020 at 12:39):

like list.forall_mem_map iirc


Last updated: May 08 2021 at 09:11 UTC