theorem FABL.complexUniformInner_eq_expect.{u_1}
  {Ω : Type u_1} [Fintype Ω]
  (f g : Ω → ℂ) :
  FABL.complexUniformInner f g =
    Finset.univ.expect fun x =>
      (starRingEnd ℂ) (f x) * g x

theorem FABL.complexUniformInner_self_eq_expect_absSq.{u_1}
  {Ω : Type u_1} [Fintype Ω] (f : Ω → ℂ) :
  FABL.complexUniformInner f f =
    Finset.univ.expect fun x =>
      (starRingEnd ℂ) (f x) * f x

theorem FABL.character_eq_zero_or_expect_eq_zero.{u_1}
  {G : Type u_1} [AddCommGroup G]
  [Fintype G]
  (χ : FABL.AbelianCharacter G) :
  χ = 0 ∨
    (Finset.univ.expect fun x => χ x) = 0

theorem FABL.expect_character_eq_ite.{u_1}
  {G : Type u_1} [AddCommGroup G]
  [Fintype G]
  (χ : FABL.AbelianCharacter G) :
  (Finset.univ.expect fun x => χ x) =
    if χ = 0 then 1 else 0

theorem FABL.characters_orthonormal.{u_1}
  {G : Type u_1} [AddCommGroup G]
  [Fintype G]
  (φ χ : FABL.AbelianCharacter G) :
  FABL.complexUniformInner ⇑φ ⇑χ =
    if φ = χ then 1 else 0

theorem FABL.card_abelianCharacter_le.{u_1}
  {G : Type u_1} [AddCommGroup G]
  [Fintype G] :
  Fintype.card (FABL.AbelianCharacter G) ≤
    Fintype.card G

theorem FABL.card_abelianCharacter.{u_1}
  {G : Type u_1} [AddCommGroup G]
  [Fintype G] :
  Fintype.card (FABL.AbelianCharacter G) =
    Fintype.card G

theorem FABL.zmodCharacter_injective (m : ℕ)
  [NeZero m] :
  Function.Injective
    (FABL.zmodCharacter m)

theorem FABL.zmodCharacter_intCast (m : ℕ)
  [NeZero m] (j x : ℤ) :
  (FABL.zmodCharacter m ↑j) ↑x =
    Complex.exp
      (2 * ↑Real.pi * (↑↑j * ↑↑x / ↑↑m) *
        Complex.I)

theorem FABL.zmodProductCharacter_apply_single
  (m n : ℕ) [NeZero m]
  (α : Fin n → ZMod m) (i : Fin n)
  (y : ZMod m) :
  (FABL.zmodProductCharacter m n α)
      (Pi.single i y) =
    (FABL.zmodCharacter m (α i)) y

theorem FABL.zmodProductCharacter_injective
  (m n : ℕ) [NeZero m] :
  Function.Injective
    (FABL.zmodProductCharacter m n)

theorem FABL.zmodProductCharacter_bijective
  (m n : ℕ) [NeZero m] :
  Function.Bijective
    (FABL.zmodProductCharacter m n)

theorem FABL.zmodProductCharacter_add (m n : ℕ)
  [NeZero m] (α β : Fin n → ZMod m) :
  FABL.zmodProductCharacter m n (α + β) =
    FABL.zmodProductCharacter m n α *
      FABL.zmodProductCharacter m n β

theorem FABL.zmodProductCharacter_neg (m n : ℕ)
  [NeZero m] (α : Fin n → ZMod m) :
  FABL.zmodProductCharacter m n (-α) =
    (FABL.zmodProductCharacter m n α)⁻¹

theorem FABL.abelianConvolution_apply.{u_1}
  {G : Type u_1} [AddCommGroup G]
  [Fintype G] (f g : G → ℂ) (x : G) :
  FABL.abelianConvolution f g x =
    Finset.univ.expect fun y =>
      f y * g (x - y)

theorem FABL.abelianConvolution_apply_swap.{u_1}
  {G : Type u_1} [AddCommGroup G]
  [Fintype G] (f g : G → ℂ) (x : G) :
  FABL.abelianConvolution f g x =
    Finset.univ.expect fun y =>
      f (x - y) * g y

theorem FABL.abelianFourierCoeff_convolution.{u_1}
  {G : Type u_1} [AddCommGroup G]
  [Fintype G] (f g : G → ℂ)
  (χ : FABL.AbelianCharacter G) :
  FABL.abelianFourierCoeff
      (FABL.abelianConvolution f g) χ =
    FABL.abelianFourierCoeff f χ *
      FABL.abelianFourierCoeff g χ