Theorems · Definition · harmonic analysis

Fintype.balance

{ι : Type u_1} → {G : Type u_4} → [Fintype ι] → [inst : AddCommGroup G] → [Module ℚ≥0 G] → (ι → G) → ι → G

The balancing of a function, namely the function minus its average.

Defined in

Mathlib.Algebra.BigOperators.Balance

Cited by

17 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeAddCommGroupModule