## Stream: new members

### Topic: monotone decreasing ℕ → ℕ

#### 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


#### Kenny Lau (Sep 09 2020 at 08:29):

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

#### 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...

#### Kenny Lau (Sep 09 2020 at 08:30):

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

#### 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

#### 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?

#### 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

#### 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.

#### Kenny Lau (Sep 09 2020 at 08:33):

then generalize the lemma and remove rev_at

#### 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

#### Kenny Lau (Sep 09 2020 at 08:36):

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

#### Kenny Lau (Sep 09 2020 at 08:36):

also generalize the domain and codomain

#### 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


#### Damiano Testa (Sep 09 2020 at 08:49):

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

#### Kenny Lau (Sep 09 2020 at 08:57):

yeah now you can prove it

#### Kenny Lau (Sep 09 2020 at 08:57):

you don't need decidable for mon

#### Kenny Lau (Sep 09 2020 at 08:57):

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

#### Damiano Testa (Sep 09 2020 at 08:58):

Kenny Lau said:

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

What does this mean?

#### Johan Commelin (Sep 09 2020 at 08:59):

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

#### 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

#### 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.

#### Johan Commelin (Sep 09 2020 at 09:01):

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

#### Damiano Testa (Sep 09 2020 at 09:01):

ok, i knew one curly bracket, but not two

i see, thanks!

#### Johan Commelin (Sep 09 2020 at 09:01):

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

#### 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.

#### 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


#### Kenny Lau (Sep 09 2020 at 09:03):

make hs explicit

#### Kenny Lau (Sep 09 2020 at 09:03):

and also mf

#### Kenny Lau (Sep 09 2020 at 09:04):

and also use more newlines

#### Kenny Lau (Sep 09 2020 at 09:05):

wow we can copy codes now?

#### Kenny Lau (Sep 09 2020 at 09:05):

also indentation is 2 spaces not 1

#### Kenny Lau (Sep 09 2020 at 09:05):

also \{{x not \{{ x

#### Damiano Testa (Sep 09 2020 at 09:05):

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

#### Kenny Lau (Sep 09 2020 at 09:07):

also hs.image f

#### Damiano Testa (Sep 09 2020 at 09:09):

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

#### Kenny Lau (Sep 09 2020 at 09:10):

by exact can go

#### Damiano Testa (Sep 09 2020 at 09:10):

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

#### Kenny Lau (Sep 09 2020 at 09:11):

what does the goal say?

#### 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)


good, thanks!

#### 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


#### Kenny Lau (Sep 09 2020 at 12:39):

we should really have finset.forall_mem_image

#### Kenny Lau (Sep 09 2020 at 12:39):

like list.forall_mem_map iirc

Last updated: May 08 2021 at 09:11 UTC