-- Mathlib/Combinatorics/Additive/Randomisation.lean
/-- One can randomise by a function of dissociated support. -/
lemma AddDissociated.randomisation (c : AddChar G ℂ → ℝ) (d : AddChar G ℂ → ℂ)
    (hcd : AddDissociated {ψ | d ψ ≠ 0}) : 𝔼 a, ∏ ψ, (c ψ + (d ψ * ψ a).re) = ∏ ψ, c ψ

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
⊢ ∑ j ∈ t.powerset,
      𝔼 i : G, (∏ i_1 ∈ j, d i_1 * i_1 i) * ∏ i_1 ∈ t \ j, (starRingEnd ℂ) (d i_1) * (starRingEnd ℂ) (i_1 i) =
    0

Tactic:
refine sum_eq_zero fun u _ ↦ ?_

Result:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ 𝔼 i : G, (∏ i_1 ∈ u, d i_1 * i_1 i) * ∏ i_1 ∈ t \ u, (starRingEnd ℂ) (d i_1) * (starRingEnd ℂ) (i_1 i) = 0

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ ((∀ a ∈ u, d a ≠ 0) ∧ ∀ a ∈ t \ u, (starRingEnd ℂ) (d a) ≠ 0) → ∑ ψ ∈ u, ψ ≠ ∑ ψ ∈ t \ u, ψ

Tactic:
exact fun h ↦ hcd.ne h.1 (by simpa only [map_ne_zero] using h.2)
  (sdiff_ne_right.2 <| .inl ht).symm

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ 𝔼 i : G, (∏ i_1 ∈ u, d i_1 * i_1 i) * ∏ i_1 ∈ t \ u, (starRingEnd ℂ) (d i_1) * (starRingEnd ℂ) (i_1 i) = 0

Tactic:
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 := ?_

Result:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ)) * 𝔼 a : G, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a = 0

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
h : (∀ a ∈ u, d a ≠ 0) ∧ ∀ a ∈ t \ u, (starRingEnd ℂ) (d a) ≠ 0
⊢ t \ u ∈ {t | ↑t ⊆ {ψ | d ψ ≠ 0}}

Tactic:
simpa only [map_ne_zero] using h.2

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ ↑(𝔼 a : G, ∏ ψ : AddChar G ℂ, (c ψ + (d ψ * ψ a).re)) = ↑(∏ ψ : AddChar G ℂ, c ψ)

Tactic:
push_cast

Result:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i : G, ∏ x : AddChar G ℂ, (↑(c x) + ↑(d x * x i).re) = ∏ i : AddChar G ℂ, ↑(c i)

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
⊢ 𝔼 a : G, ∏ ψ ∈ t, (d ψ * ψ a + (starRingEnd ℂ) (d ψ * ψ a)) / 2 = 0

Tactic:
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, compl_eq_empty_iff,
  false_and, or_false]

Result:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
⊢ ∑ j ∈ t.powerset,
      𝔼 i : G, (∏ i_1 ∈ j, d i_1 * i_1 i) * ∏ i_1 ∈ t \ j, (starRingEnd ℂ) (d i_1) * (starRingEnd ℂ) (i_1 i) =
    0

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ 𝔼 a : G, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ) * (starRingEnd ℂ) (ψ a) =
    ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ)) * 𝔼 a : G, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a

Tactic:
simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
  ← prod_mul_distrib, AddChar.map_neg_eq_conj]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ (𝔼 a : G, ∏ ψ ∈ ∅, (d ψ * ψ a + (starRingEnd ℂ) (d ψ * ψ a)) / 2) * ∏ ψ ∈ ∅ᶜ, ↑(c ψ) = ∏ ψ : AddChar G ℂ, ↑(c ψ)

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i : G, ∏ x : AddChar G ℂ, (↑(c x) + ↑(d x * x i).re) = ∏ i : AddChar G ℂ, ↑(c i)

Tactic:
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

Result:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
⊢ 𝔼 a : G, ∏ ψ ∈ t, (d ψ * ψ a + (starRingEnd ℂ) (d ψ * ψ a)) / 2 = 0

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 a : G, ∏ ψ : AddChar G ℂ, (c ψ + (d ψ * ψ a).re) = ∏ ψ : AddChar G ℂ, c ψ

Tactic:
refine Complex.ofReal_injective ?_

Result:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ ↑(𝔼 a : G, ∏ ψ : AddChar G ℂ, (c ψ + (d ψ * ψ a).re)) = ↑(∏ ψ : AddChar G ℂ, c ψ)

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ)) * 𝔼 a : G, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a = 0

Tactic:
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]

Result:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ ((∀ a ∈ u, d a ≠ 0) ∧ ∀ a ∈ t \ u, (starRingEnd ℂ) (d a) ≠ 0) → ∑ ψ ∈ u, ψ ≠ ∑ ψ ∈ t \ u, ψ

Proof state:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i : G, ∏ x : AddChar G ℂ, (↑(c x) + ↑(d x * x i).re) =
    ∑ t : Finset (AddChar G ℂ), (𝔼 a : G, ∏ ψ ∈ t, (d ψ * ψ a + (starRingEnd ℂ) (d ψ * ψ a)) / 2) * ∏ ψ ∈ tᶜ, ↑(c ψ)

Tactic:
simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
  Complex.re_eq_add_conj]

Result:
no goals