Mean / Average of a Sequence

Stream: new members

[Colin Jones ⚛️]

Do we have something in Mathlib like this?

import Mathlib

open BigOperators Nat Real Finset Fin

noncomputable def mean (n : ℕ) (f : ℕ → ℂ) : ℂ :=
  ∑ i in range n, f i / n

[Colin Jones ⚛️]

It takes complex numbers because that's most general type that I could put in

[Kevin Buzzard]

I think you could have put in some more general object :-) Probably some general vector space over the rationals, for example? Are you sure you want to divide all the individual terms by n instead of doing the entire sum first and then dividing by n at the end?

[Riccardo Brasca]

Maybe it is a crazy way of viewing it, but it is the integral wrt to the finite probability measure.

[Colin Jones ⚛️]

Thanks @Riccardo Brasca. Do you know where in Mathlib it is?

[Colin Jones ⚛️]

@Kevin, It can definitely be more generalized, but that's the limit of my ability for now

[Riccardo Brasca]

I really don't know that part of the library, and I am not sure it's a good idea. What is your goal?

[Colin Jones ⚛️]

That's okay. I need a mean function to prove some stuff about linear regression.

[Riccardo Brasca]

You can have a look here https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/MeanInequalities.html