Indicator

theorem translate_indicate {α : Type u_2} (β : Type u_3) [DecidableEq α] [Semiring β] [AddCommGroup α] (a : α) (s : Finset α) : translate a (𝟭 s) = 𝟭 (a +ᵥ s)

@[simp]

theorem conjneg_indicate {α : Type u_2} {β : Type u_3} [DecidableEq α] [CommSemiring β] [StarRing β] [AddCommGroup α] (s : Finset α) : conjneg (𝟭 s) = 𝟭 (-s)

theorem expect_indicate {ι : Type u_1} {β : Type u_3} [Fintype ι] [DecidableEq ι] [Semiring β] [Module ℚ≥0 β] (s : Finset ι) : (Finset.univ.expect fun (x : ι) => 𝟭 s x) = (↑(Fintype.card ι))⁻¹ • ↑s.card

Normalised indicator

theorem translate_mu {α : Type u_2} (β : Type u_3) [DecidableEq α] [DivisionSemiring β] [AddCommGroup α] (a : α) (s : Finset α) : translate a (mu s) = mu (a +ᵥ s)

theorem expect_mu {α : Type u_2} (β : Type u_3) [DecidableEq α] [Semifield β] {s : Finset α} [CharZero β] [Fintype α] (hs : s.Nonempty) : (Finset.univ.expect fun (x : α) => mu s x) = (↑(Fintype.card α))⁻¹

@[simp]

theorem conjneg_mu {α : Type u_2} (β : Type u_3) [DecidableEq α] [Semifield β] [StarRing β] [AddCommGroup α] (s : Finset α) : conjneg (mu s) = mu (-s)