simple lemma on sums with equal terms

Stream: Is there code for X?

[Bernardo Anibal Subercaseaux Roa]

I wrote the following embarrassing code:

lemma constant_sum (f: V → ℚ) (v : V) (eq_h : ∀ u v : V, f u = f v): ∑ w : V, (f w) = Fintype.card V * (f v) := by
    have E : ∃ c : ℚ, ∀ u : V, f u = c := by
      use f v; intro u; apply eq_h
    have ⟨c, hc⟩ := E
    simp_all only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]

since I wasn't being able to get Finset.sum_const to directly work when having the equality of the sum terms as a hypothesis. Is there a better way to do this? I tried looking for a more general version of sum_const but failed

[Yaël Dillies]

You can use docs#Finset.sum_eq_card_nsmul

[Bernardo Anibal Subercaseaux Roa]

that sounded promising but I couldn't figure out how to do it; concretely, I have

 have eq_h : ∀ u v : V, μ_v G u = μ_v G v := by
    exact fun u v ↦ vt_avg_dist_from_vertex_eq G hconn h u v

  have p : ∑ v : V, μ_v G v = Fintype.card V * μ_v G u := by
     apply constant_sum (λ x : V => μ_v G x) u eq_h

and I'm trying to replace the application of constant_sum (defined in the OP) by a call to docs#Finset.sum_eq_card_nsmul, but couldn't figure out how to do it

[Bernardo Anibal Subercaseaux Roa]

The simplest code I've gotten is:

let c := μ_v G u
have eq_c : ∀ v : V, μ_v G v = c := by
    exact λ v => eq_h v u
have p' : ∑ v : V, μ_v G v = Fintype.card V * c := by
    simp_all only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]

which is basically inlining the constant_sum above, but I'm curious to see a better way using Finset.sum_eq_card_nsmul

[Yaël Dillies]

Had you provided a #mwe, I would have given you working code

[Yaël Dillies]

Here's an attempted reconstruction of your file:

import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Algebra.Ring.Rat
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Nat.Cast.Basic

variable {V : Type*} [Fintype V]

lemma constant_sum (f : V → ℚ) (v : V) (eq_h : ∀ u v : V, f u = f v) :
    ∑ w, f w = Fintype.card V * f v := by
  rw [← nsmul_eq_mul]; exact Finset.sum_eq_card_nsmul fun _ _ ↦ eq_h _ _

[Yan Yablonovskiy]

Bernardo Anibal Subercaseaux Roa said:

The simplest code I've gotten is:

let c := μ_v G u
have eq_c : ∀ v : V, μ_v G v = c := by
    exact λ v => eq_h v u
have p' : ∑ v : V, μ_v G v = Fintype.card V * c := by
    simp_all only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]

which is basically inlining the constant_sum above, but I'm curious to see a better way using Finset.sum_eq_card_nsmul

A small note but typically using λ is discouraged and 'fun' is (almost?) always used, so doing that would help readability a bit for posts.

As well as => vs ↦

[Eric Wieser]

Here's a shorter proof:

import Mathlib

lemma constant_sum {V} [Fintype V] (f: V → ℚ) (v : V) (eq_h : ∀ u v : V, f u = f v) :
    ∑ w : V, f w = Fintype.card V * f v := by
  simp [← eq_h v]

[Bernardo Anibal Subercaseaux Roa]

thanks everyone! (and sorry for the delay about the MWE)

[Bernardo Anibal Subercaseaux Roa]

Maybe one meta-question: Eric's proof seems to be as short as one can get, but it might be less "readable" insofar the other ones explictly mention Finset.sum_eq_card_nsmulor Finset.sum_const, which reveal what's happening. Are there any community standards or thoughts about this? My feeling is like in pen-and-paper math one optimizes more for comprehensibility that for length, but here a reader could just step in observing the goal changing and still get what's happening, just with perhaps more effort than if the code itself reveals everything

[Ruben Van de Velde]

Note that Eric said "shorter", not "better" :)

[Ruben Van de Velde]

Now, that proof says "replace all f x by f v, and simplify what's left", which succeeds at explicitly mentioning the crucial part in the argument (the constantness)