Evaluating Permutations

Stream: new members

[Callum Cassidy-Nolan]

Hi there, I'm working on the formalization of image.png

I'm running into a little bit of trouble with the permutation sigma,

test.lean

open_locale big_operators

theorem r_eq
    (n : ℕ)
    (x y : ℕ → ℝ)
    (σ : equiv.perm (finset.Ioo 1 n))
    (h : ∀ i : ℕ, i ∈ finset.Ioc 1 n → x i < x (i + 1))
    (h : ∀ i : ℕ, i ∈ finset.Ioc 1 n → y i < y (i + 1)) :
    ∑ i in finset.Ioo 1 n, x (n + 1 - i)  * y i ≤ ∑ i in finset.Ioo 1 n, x (σ i) * y i ∧
    ∑ i in finset.Ioo 1 n, x (σ i) * y i ≤ ∑ i in finset.Ioo 1 n, x i * y i := sorry

causing :

type mismatch at application
  ⇑σ i
term
  i
has type
  ℕ
but is expected to have type
  ↥(finset.Ioo 1 n)
Additional information:
/home/ccn/lean/olympiad-formalization/src/int_alg/section_18_2.lean:36:30: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    ⇑σ ?m_1
  has type
    ↥(finset.Ioo 1 n)
  but is expected to have type
    ℕ

What would be the simplest way to get the coercions to work without making the statement too ugly?

[Kevin Buzzard]

Can you post a mwe? you can sum over the fintype rather than using in

[Callum Cassidy-Nolan]

Your correct - using a sum over i : finset.Ioo 1 n makes it so that all the evaluations work out

[Callum Cassidy-Nolan]

What's the difference between using in and : ?

[Yaël Dillies]

Why are you talking permutations on a subtype? You should rather be taking (σ : equiv.perm ℕ) (hσ : σ.support ⊆ finset.Ioo 1 n)

[Yaël Dillies]

(annoyingly, docs#equiv.perm.support currently only works over fintypes...)

[Reid Barton]

I think x y : fin n → ℝ would be a better start. There should be a nicer way to state that x and y are increasing, for example ∀ i j, i < j -> x i < x j or using some mathlib increasing definition.

[Reid Barton]

It looks like all your os and cs in Ixx are backwards--but better to avoid these intervals in the first place

[Reid Barton]

(For this theorem statement, I mean.)

[Eric Wieser]

docs#strict_mono, as strict_mono x would work. for indicating that the sequence is increasing

[Eric Wieser]

Note we already have file#algebra/order/rearrangement

[Eric Wieser]

Which isn't to say that this is a bad learning exercise; heck, there's even a "solution" to compare against!

[Yaël Dillies]

Oh of course, I didn't recognize the rearrangement inequality :face_palm:

[Yaël Dillies]

Note that I cooked up docs#monovary for the occasion. AFAIK our statement of the rearrangement inequality is absolutely nonstandard.