monotone decreasing ```ℕ → ℕ```

Stream: new members

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Kenny Lau]

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

[Damiano Testa]

(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]

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]

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

[Damiano Testa]

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]

then generalize the lemma and remove rev_at

[Damiano Testa]

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]

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

[Kenny Lau]

also generalize the domain and codomain

[Damiano Testa]

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]

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

[Kenny Lau]

yeah now you can prove it

[Kenny Lau]

you don't need decidable for mon

[Kenny Lau]

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

[Damiano Testa]

Kenny Lau said:

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

What does this mean?

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Damiano Testa]

ok, i knew one curly bracket, but not two

[Damiano Testa]

i see, thanks!

[Johan Commelin]

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

[Johan Commelin]

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]

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]

make hs explicit

[Kenny Lau]

and also mf

[Kenny Lau]

and also use more newlines

[Kenny Lau]

wow we can copy codes now?

[Kenny Lau]

also indentation is 2 spaces not 1

[Kenny Lau]

also \{{x not \{{ x

[Damiano Testa]

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

[Kenny Lau]

also hs.image f

[Damiano Testa]

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

[Kenny Lau]

by exact can go

[Damiano Testa]

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

[Kenny Lau]

what does the goal say?

[Damiano Testa]

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)

[Damiano Testa]

good, thanks!

[Damiano Testa]

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]

we should really have finset.forall_mem_image

[Kenny Lau]

like list.forall_mem_map iirc