noncomputable def OrbitBasis.rep (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] (O : MulAction.orbitRel.Quotient G α) : α

Choose a representative element from each orbit class.

theorem OrbitBasis.rep_mem_orbit (G : Type u_1) [Group G] (α : Type u_2) [Fintype α] [DecidableEq α] [MulAction G α] (O : MulAction.orbitRel.Quotient G α) : rep G α O ∈ O.orbit

theorem OrbitBasis.mk_rep (G : Type u_1) [Group G] (α : Type u_2) [Fintype α] [DecidableEq α] [MulAction G α] (O : MulAction.orbitRel.Quotient G α) : Quotient.mk'' (rep G α O) = O

def OrbitBasis.invariantSubspace (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] : Submodule ℝ (α →₀ ℝ)

The G-invariant subspace: vectors in ℝ^α fixed by every group element.

theorem OrbitBasis.invariant_iff_constant_on_orbits {G : Type u_1} [Group G] {α : Type u_2} [Fintype α] [DecidableEq α] [MulAction G α] {v : α →₀ ℝ} : v ∈ invariantSubspace G α ↔ ∀ (a b : α), Quotient.mk'' a = Quotient.mk'' b → v a = v b

A vector is G-invariant iff its coefficients are constant on orbits.

noncomputable def OrbitBasis.orbitSum {G : Type u_1} [Group G] {α : Type u_2} [Fintype α] [MulAction G α] (O : MulAction.orbitRel.Quotient G α) : α →₀ ℝ

The orbit sum: for an orbit O, define v_O = ∑_{a ∈ O} e_a.

theorem OrbitBasis.orbitSum_apply {G : Type u_1} [Group G] {α : Type u_2} [Fintype α] [DecidableEq α] [MulAction G α] (O : MulAction.orbitRel.Quotient G α) (a : α) : (orbitSum O) a = if a ∈ O.orbit then 1 else 0

theorem OrbitBasis.orbitSum_mem_invariantSubspace {G : Type u_1} [Group G] {α : Type u_2} [Fintype α] [DecidableEq α] [MulAction G α] (O : MulAction.orbitRel.Quotient G α) : orbitSum O ∈ invariantSubspace G α

theorem OrbitBasis.quotient_eq_of_mem_orbit {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {a : α} {O : MulAction.orbitRel.Quotient G α} (h : a ∈ O.orbit) : Quotient.mk'' a = O

theorem OrbitBasis.sum_orbit_indicator {G : Type u_1} [Group G] {α : Type u_2} [Fintype α] [MulAction G α] (c : MulAction.orbitRel.Quotient G α → ℝ) (a : α) (O₀ : MulAction.orbitRel.Quotient G α) (ha : a ∈ O₀.orbit) : (∑ O : MulAction.orbitRel.Quotient G α, c O * if a ∈ O.orbit then 1 else 0) = c O₀

Key summation lemma: ∑O c(O) * 1{a ∈ O} = c(⟦a⟧).

theorem OrbitBasis.orbitSum_linearIndependent {G : Type u_1} [Group G] {α : Type u_2} [Fintype α] [DecidableEq α] [MulAction G α] : LinearIndependent ℝ fun (O : MulAction.orbitRel.Quotient G α) => ⟨orbitSum O, ⋯⟩

The orbit sums are linearly independent in the invariant subspace.

theorem OrbitBasis.orbitSum_span {G : Type u_1} [Group G] {α : Type u_2} [Fintype α] [DecidableEq α] [MulAction G α] : ⊤ ≤ Submodule.span ℝ (Set.range fun (O : MulAction.orbitRel.Quotient G α) => ⟨orbitSum O, ⋯⟩)

The orbit sums span the invariant subspace.

noncomputable def OrbitBasis.orbitSumBasis {G : Type u_1} [Group G] {α : Type u_2} [Fintype α] [DecidableEq α] [MulAction G α] : Module.Basis (MulAction.orbitRel.Quotient G α) ℝ ↥(invariantSubspace G α)

Lemma 5.7. The orbit sums form a basis for the G-invariant subspace of ℝ^α. For each orbit O of G acting on α, define v_O = ∑_{a ∈ O} e_a. Then {v_O : O an orbit} is a basis for (ℝ^α)^G. (Lemma 5.7, Stanley's Algebraic Combinatorics)