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.
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
- Fintype.balance f = f - Function.const ι (Finset.univ.expect fun (y : ι) => f y)
Instances For
theorem
Fintype.balance_apply
{ι : Type u_1}
{G : Type u_4}
[Fintype ι]
[AddCommGroup G]
[Module ℚ≥0 G]
(f : ι → G)
(x : ι)
:
Fintype.balance f x = f x - Finset.univ.expect fun (y : ι) => f y
@[simp]
theorem
Fintype.balance_zero
{ι : Type u_1}
{G : Type u_4}
[Fintype ι]
[AddCommGroup G]
[Module ℚ≥0 G]
:
Fintype.balance 0 = 0
@[simp]
theorem
Fintype.balance_add
{ι : Type u_1}
{G : Type u_4}
[Fintype ι]
[AddCommGroup G]
[Module ℚ≥0 G]
(f g : ι → G)
:
Fintype.balance (f + g) = Fintype.balance f + Fintype.balance g
@[simp]
theorem
Fintype.balance_sub
{ι : Type u_1}
{G : Type u_4}
[Fintype ι]
[AddCommGroup G]
[Module ℚ≥0 G]
(f g : ι → G)
:
Fintype.balance (f - g) = Fintype.balance f - Fintype.balance g
@[simp]
theorem
Fintype.balance_neg
{ι : Type u_1}
{G : Type u_4}
[Fintype ι]
[AddCommGroup G]
[Module ℚ≥0 G]
(f : ι → G)
:
@[simp]
theorem
Fintype.sum_balance
{ι : Type u_1}
{G : Type u_4}
[Fintype ι]
[AddCommGroup G]
[Module ℚ≥0 G]
(f : ι → G)
:
∑ x : ι, Fintype.balance f x = 0
@[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 : ι) => Fintype.balance f x) = 0
@[simp]
theorem
Fintype.balance_idem
{ι : Type u_1}
{G : Type u_4}
[Fintype ι]
[AddCommGroup G]
[Module ℚ≥0 G]
(f : ι → G)
:
@[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 (Fintype.balance f a) = Fintype.balance (⇑g ∘ f) a