FiniteAverage.lean

1 import Mathlib.RepresentationTheory.Invariants
2 import Mathlib.Analysis.InnerProductSpace.Basic
3 
4 /-! Literal finite group averages and their invariant and orthogonal projection properties. -/
5 set_option autoImplicit false
6 noncomputable section
7 open scoped BigOperators
8 namespace PaperXI.FiniteAverage
9 variable {G V : Type*} [Group G] [Fintype G] [AddCommGroup V] [Module ℂ V]
10 
11 def average (ρ : Representation ℂ G V) : V →ₗ[ℂ] V :=
12   (Fintype.card G : ℂ)⁻¹ • ∑ g : G, ρ g
13 
14 @[simp] theorem average_apply (ρ : Representation ℂ G V) (v : V) :
15     average ρ v = (Fintype.card G : ℂ)⁻¹ • ∑ g : G, ρ g v := by
16   simp [average, LinearMap.sum_apply]
17 
18 theorem card_ne_zero : (Fintype.card G : ℂ) ≠ 0 := by
19   exact_mod_cast Fintype.card_ne_zero
20 
21 theorem invariant (ρ : Representation ℂ G V) (v : V) :
22     average ρ v ∈ ρ.invariants := by
23   intro g
24   simp only [average_apply, map_smul, map_sum, ← Module.End.mul_apply, ← map_mul]
25   rw [Function.Bijective.sum_comp (Group.mulLeft_bijective g) (fun h => ρ h v)]
26 
27 theorem fixes (ρ : Representation ℂ G V) {v : V} (hv : v ∈ ρ.invariants) :
28     average ρ v = v := by
29   rw [average_apply]
30   have hf (g : G) : ρ g v = v := hv g
31   simp only [hf, Finset.sum_const, Finset.card_univ]
32   rw [← Nat.cast_smul_eq_nsmul ℂ, smul_smul, inv_mul_cancel₀ (card_ne_zero (G := G)), one_smul]
33 
34 theorem idempotent (ρ : Representation ℂ G V) :
35     (average ρ).comp (average ρ) = average ρ := by
36   ext v
37   exact fixes ρ (invariant ρ v)
38 
39 theorem range_eq (ρ : Representation ℂ G V) :
40     LinearMap.range (average ρ) = ρ.invariants := by
41   ext v
42   constructor
43   · rintro ⟨w, rfl⟩
44     exact invariant ρ w
45   · intro hv
46     exact ⟨v, fixes ρ hv⟩
47 
48 section Inner
49 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
50 
51 theorem self_adjoint (ρ : Representation ℂ G E)
52     (hunitary : ∀ g x y, inner ℂ (ρ g x) (ρ g y) = inner ℂ x y) (x y : E) :
53     inner ℂ (average ρ x) y = inner ℂ x (average ρ y) := by
54   have hmove (g : G) : inner ℂ (ρ g x) y = inner ℂ x (ρ g⁻¹ y) := by
55     simpa only [ρ.self_inv_apply] using hunitary g x (ρ g⁻¹ y)
56   simp only [average_apply, inner_smul_left, inner_smul_right, sum_inner, inner_sum]
57   simp only [map_inv₀, map_natCast]
58   congr 1
59   simp_rw [hmove]
60   exact Function.Bijective.sum_comp (Equiv.inv G).bijective (fun g => inner ℂ x (ρ g y))
61 
62 theorem residual_orthogonal (ρ : Representation ℂ G E)
63     (hunitary : ∀ g x y, inner ℂ (ρ g x) (ρ g y) = inner ℂ x y)
64     (x : E) {y : E} (hy : y ∈ ρ.invariants) :
65     inner ℂ (x - average ρ x) y = 0 := by
66   rw [inner_sub_left, self_adjoint ρ hunitary, fixes ρ hy, sub_self]
67 
68 end Inner
69 end PaperXI.FiniteAverage

Back to source controls