Equiv.perm.sum_comp and Finsets

Stream: new members

[Nathan]

How do I get this working?

example (n : ℕ) : ∑ i : Fin n, (n-i.val-1) = (n-1) * n / 2 :=
  let f : ℕ → ℕ := λ x => if x < n then n-1-x else x
  let σ : Equiv.Perm ℕ := ⟨f, f, sorry, sorry⟩
  have swap := Equiv.Perm.sum_comp σ (Fin n) f sorry
  sorry

I get this error
Screenshot 2025-09-29 at 10.29.05 AM.png
I can see that (Fin n) is not a Finset but can I use something like Finset.univ to convert it to a Finset? Or should I avoid Fin completely and just use a Finset instead?

[Robin Arnez]

You might want docs#Finset.range and docs#Finset.sum_range to transfer between the two

[Nathan]

ah, but I want to use i.prop inside the sum (the code i posted is a toy example) so i don't think this will work

[Nathan]

let me post more code...

[Nathan]

idk what code to post actually. but i feel like i might need a Finset of Fin

[Nathan]

that way, hopefully i can use prop inside the sum, and i can also use sum_comp

[Nathan]

how do i construct a Finset?

[Nathan]

someone said

If your subtype is finite, you can prove this and register it as an instance of the typeclass FinType.

[Nathan]

does lean have list comprehension?

[Ruben Van de Velde]

docs#Equiv.Perm.sum_comp

[Nathan]

yeah i need a finset to use that

[Ruben Van de Velde]

As far as I can tell, you should be able to make it work with Finset.range n if you replace i.val by i

[Nathan]

i won't be able to use i.prop in that case

[Ruben Van de Velde]

But you're not using that in your example

[Nathan]

i know, it's a toy example

[Nathan]

This is the real thing

def d (n : ℕ) := n.divisors.sort (· ≤ ·)
def S (n : ℕ) := ∑ i : (Fin ((d n).length-1)), (d n)[i.val] * (d n)[i.val+1]

theorem t1 (n : ℕ) : S n < n^2 :=
  let k := (d n).length - 1
  let f : ℕ → ℕ := λ x => if x < k then k-1-x else x
  let σ : Equiv.Perm ℕ := ⟨f, f, sorry, sorry⟩
  have swap := Equiv.Perm.sum_comp σ (Fin ((d n).length-1)) f sorry
  sorry

[Nathan]

it's not explicitly using i.prop but i think it is implicitly. if you change Fin to range in the definition of S, then you can't index into (d n).

[Nathan]

actually i guess it's more like this

def d (n : ℕ) := n.divisors.sort (· ≤ ·)
def S (n : ℕ) := ∑ i : Fin ((d n).length-1), (d n)[i.val] * (d n)[i.val+1]

theorem t1 (n : ℕ) : S n < n^2 :=
  let k := (d n).length - 1
  let f₁ : ℕ → ℕ := λ x => if x < k then k-1-x else x
  let σ : Equiv.Perm ℕ := ⟨f₁, f₁, sorry, sorry⟩
  let f₂ : (i : Fin k) → ℕ := λ i => (d n)[i.val] * (d n)[i.val+1]
  have swap := Equiv.Perm.sum_comp σ (Fin ((d n).length-1)) f₂ sorry
  sorry

[Aaron Liu]

Nathan said:

How do I get this working?

example (n : ℕ) : ∑ i : Fin n, (n-i.val-1) = (n-1) * n / 2 :=
  let f : ℕ → ℕ := λ x => if x < n then n-1-x else x
  let σ : Equiv.Perm ℕ := ⟨f, f, sorry, sorry⟩
  have swap := Equiv.Perm.sum_comp σ (Fin n) f sorry
  sorry

I get this error
Screenshot 2025-09-29 at 10.29.05 AM.png
I can see that (Fin n) is not a Finset but can I use something like Finset.univ to convert it to a Finset? Or should I avoid Fin completely and just use a Finset instead?

Yeah just put in Finset.univ should work

[Nathan]

I couldn't figure out how to use Finset.univ

[Nathan]

I can take another look at Finset.univ after lunch

[Aaron Liu]

I can show you how once I get home in an hour

[Nathan]

thanks

[Ruben Van de Velde]

I'm not sure how it helps with your goal, but maybe something like

import Mathlib

def d (n : ℕ) := n.divisors.sort (· ≤ ·)
def S (n : ℕ) := ∑ i : Fin ((d n).length-1), (d n)[i.val] * (d n)[i.val+1]

theorem t1 (n : ℕ) : S n < n^2 := by
  let k := (d n).length - 1
  let f₁ : Fin k → Fin k := λ x => -x
  let σ : Equiv.Perm (Fin k) := ⟨f₁, f₁, fun _ => by simp [f₁], fun _ => by simp [f₁]⟩
  let f₂ : (i : Fin k) → ℕ := λ i => (d n)[i.val] * (d n)[i.val+1]
  have swap := Equiv.Perm.sum_comp σ Finset.univ f₂ sorry
  sorry

[Nathan]

i think you're right to change the type of f₁ to Fin k → Fin k

[Nathan]

oh wow Finset.univ goes there?

[Nathan]

wait this seems good. also, what's the behavior of λ x => -x?

[Aaron Liu]

@loogle Equiv, Fintype, Finset.sum

[loogle]

:search: Equiv.sum_comp, Fintype.sum_equiv, and 7 more

[Aaron Liu]

Nathan said:

wait this seems good. also, what's the behavior of λ x => -x?

takes input x and returns its negative (mod n) -x

[Nathan]

oh perfect

[Aaron Liu]

here we go

import Mathlib

def d (n : ℕ) := n.divisors.sort (· ≤ ·)
def S (n : ℕ) := ∑ i : Fin ((d n).length-1), (d n)[i.val] * (d n)[i.val+1]

theorem t1 (n : ℕ) : S n < n^2 :=
  let k := (d n).length - 1
  let σ : Equiv.Perm (Fin k) := Fin.revPerm
  let f₂ (i : Fin k) : ℕ := (d n)[i.val] * (d n)[i.val+1]
  have swap : ∑ i : Fin k, f₂ (σ i) = ∑ i : Fin k, f₂ i := Equiv.sum_comp σ f₂
  sorry

[Aaron Liu]

wait no probably not Fin.revPerm

[Aaron Liu]

like this

import Mathlib

def d (n : ℕ) := n.divisors.sort (· ≤ ·)
def S (n : ℕ) := ∑ i : Fin ((d n).length-1), (d n)[i.val] * (d n)[i.val+1]

theorem t1 (n : ℕ) : S n < n^2 :=
  let k := (d n).length - 1
  let σ : Equiv.Perm (Fin k) := Equiv.neg (Fin k)
  let f₂ (i : Fin k) : ℕ := (d n)[i.val] * (d n)[i.val+1]
  have swap : ∑ i : Fin k, f₂ (σ i) = ∑ i : Fin k, f₂ i := Equiv.sum_comp σ f₂
  sorry

[Nathan]

yeah i just realized it can be done with Equiv.sum_comp which takes fewer inputs

[Nathan]

Nice, thank you so much :pray:

[Nathan]

so clean :ok: