Documentation

Mathlib.Algebra.BigOperators.Balance

Balancing a function #

This file defines the balancing of a function f, defined as f minus its average.

This is the unique function g such that f a - f b = g a - g b for all a and b, and ∑ a, g a = 0. This is particularly useful in Fourier analysis as f and g then have the same Fourier transform, except in the 0-th frequency where the Fourier transform of g vanishes.

source
def Fintype.balance {ι : Type u_1} {G : Type u_4} [Fintype ι] [AddCommGroup G] [Module ℚ≥0 G] (f : ι → G) :
ι → G

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

Equations
Instances For
    source
    theorem Fintype.balance_apply {ι : Type u_1} {G : Type u_4} [Fintype ι] [AddCommGroup G] [Module ℚ≥0 G] (f : ι → G) (x : ι) :
    balance f x = f x - Finset.univ.expect fun (y : ι) => f y
    source
    @[simp]
    theorem Fintype.balance_zero {ι : Type u_1} {G : Type u_4} [Fintype ι] [AddCommGroup G] [Module ℚ≥0 G] :
    balance 0 = 0
    source
    @[simp]
    theorem Fintype.balance_add {ι : Type u_1} {G : Type u_4} [Fintype ι] [AddCommGroup G] [Module ℚ≥0 G] (f g : ι → G) :
    balance (f + g) = balance f + balance g
    source
    @[simp]
    theorem Fintype.balance_sub {ι : Type u_1} {G : Type u_4} [Fintype ι] [AddCommGroup G] [Module ℚ≥0 G] (f g : ι → G) :
    balance (f - g) = balance f - balance g
    source
    @[simp]
    theorem Fintype.balance_neg {ι : Type u_1} {G : Type u_4} [Fintype ι] [AddCommGroup G] [Module ℚ≥0 G] (f : ι → G) :
    balance (-f) = -balance f
    source
    @[simp]
    theorem Fintype.sum_balance {ι : Type u_1} {G : Type u_4} [Fintype ι] [AddCommGroup G] [Module ℚ≥0 G] (f : ι → G) :
    ∑ x : ι, balance f x = 0
    source
    @[simp]
    theorem Fintype.expect_balance {ι : Type u_1} {G : Type u_4} [Fintype ι] [AddCommGroup G] [Module ℚ≥0 G] (f : ι → G) :
    (Finset.univ.expect fun (x : ι) => balance f x) = 0
    source
    @[simp]
    theorem Fintype.balance_idem {ι : Type u_1} {G : Type u_4} [Fintype ι] [AddCommGroup G] [Module ℚ≥0 G] (f : ι → G) :
    balance (balance f) = balance f
    source
    @[simp]
    theorem Fintype.map_balance {ι : Type u_1} {H : Type u_2} {F : Type u_3} {G : Type u_4} [Fintype ι] [AddCommGroup G] [Module ℚ≥0 G] [AddCommGroup H] [Module ℚ≥0 H] [FunLike F G H] [LinearMapClass F ℚ≥0 G H] (g : F) (f : ι → G) (a : ι) :
    g (balance f a) = balance (⇑g ∘ f) a