Theorems · Theorem · combinatorics

AddDissociated.randomisation

∀ {G : Type u_1} [inst : Fintype G] [inst_1 : AddCommGroup G] (c : AddChar G ℂ → ℝ) (d : AddChar G ℂ → ℂ),
  AddDissociated {ψ | d ψ ≠ 0} → (Finset.univ.expect fun a => ∏ ψ, (c ψ + (d ψ * ψ a).re)) = ∏ ψ, c ψ

One can randomise by a function of dissociated support.

Defined in

Mathlib.Combinatorics.Additive.Randomisation

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeAddCommGroup