English
Let G be a group, c and d be functions from AddChar(G,ℂ) to ℝ and ℂ respectively, and suppose {ψ | d ψ ≠ 0} is AddDissociated. Then the expectation over a uniform random a ∈ G of the product ∏ψ (c ψ + Re(d ψ ψ(a))) equals ∏ψ c ψ.
Русский
Пусть G — группа, c и d функции в AddChar(G,ℂ) в ℝ и ℂ. Пусть множество {ψ | d ψ ≠ 0} является AddDissociated. Тогда математическое ожидание по случайному a ∈ G от произведения ∏ψ (c ψ + Re(d ψ ψ(a))) равно произведению ∏ψ c ψ.
LaTeX
$$$\mathbb{E}_a \prod_{\psi} \bigl(c(\psi) + \operatorname{Re}(d(\psi) \psi(a))\bigr) = \prod_{\psi} c(\psi)$$$
Lean4
/-- One can randomise by a function of dissociated support. -/
theorem randomisation (c : AddChar G ℂ → ℝ) (d : AddChar G ℂ → ℂ) (hcd : AddDissociated {ψ | d ψ ≠ 0}) :
𝔼 a, ∏ ψ, (c ψ + (d ψ * ψ a).re) = ∏ ψ, c ψ :=
by
refine Complex.ofReal_injective ?_
push_cast
calc
_ = ∑ t, (𝔼 a, ∏ ψ ∈ t, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ tᶜ, (c ψ : ℂ) := by
simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm, Complex.re_eq_add_conj]
_ = (𝔼 a, ∏ ψ ∈ ∅, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ ∅ᶜ, (c ψ : ℂ) :=
(Fintype.sum_eq_single ∅ fun t ht ↦ mul_eq_zero_of_left ?_ _)
_ = ∏ ψ, (c ψ : ℂ) := by simp
simp only [map_mul, prod_div_distrib, prod_add, prod_const, ← expect_div, expect_sum_comm, div_eq_zero_iff,
pow_eq_zero_iff', OfNat.ofNat_ne_zero, ne_eq, card_eq_zero, false_and, or_false]
refine sum_eq_zero fun u _ ↦ ?_
calc
𝔼 a, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, conj (d ψ) * conj (ψ a) =
((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, conj (d ψ)) * 𝔼 a, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a :=
by
simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm, ← prod_mul_distrib,
AddChar.map_neg_eq_conj]
_ = 0 := ?_
rw [mul_eq_zero, AddChar.expect_eq_zero_iff_ne_zero, sub_ne_zero, or_iff_not_imp_left, ← Ne, mul_ne_zero_iff,
prod_ne_zero_iff, prod_ne_zero_iff]
exact fun h ↦ hcd.ne h.1 (by simpa only [map_ne_zero] using h.2) (sdiff_ne_right.2 <| .inl ht).symm
