FiniteFunctionAverage.lean

1 import PaperXI.TranslationAverage
2 
3 /-! Orthogonal averaging for the actual finite-sum Hermitian pairing on functions. -/
4 set_option autoImplicit false
5 noncomputable section
6 open scoped BigOperators
7 namespace PaperXI.FiniteFunctionAverage
8 open TranslationAverage
9 variable {G X : Type*} [Group G] [Fintype G] [Fintype X]
10 
11 theorem pairing_average_left (ρ : Representation ℂ G (X → ℂ)) (f h : X → ℂ) :
12     pairing (FiniteAverage.average ρ f) h =
13       (Fintype.card G : ℂ)⁻¹ * ∑ g : G, pairing (ρ g f) h := by
14   simp only [pairing, FiniteAverage.average_apply, Pi.smul_apply, Finset.sum_apply,
15     smul_eq_mul, star_mul, star_inv₀, star_natCast, star_sum,
16     Finset.mul_sum, Finset.sum_mul]
17   rw [Finset.sum_comm]
18   apply Finset.sum_congr rfl
19   intro g hg
20   apply Finset.sum_congr rfl
21   intro u hu
22   ring
23 
24 theorem pairing_average_right (ρ : Representation ℂ G (X → ℂ)) (f h : X → ℂ) :
25     pairing f (FiniteAverage.average ρ h) =
26       (Fintype.card G : ℂ)⁻¹ * ∑ g : G, pairing f (ρ g h) := by
27   simp only [pairing, FiniteAverage.average_apply, Pi.smul_apply, Finset.sum_apply,
28     smul_eq_mul, Finset.mul_sum]
29   rw [Finset.sum_comm]
30   apply Finset.sum_congr rfl
31   intro g hg
32   apply Finset.sum_congr rfl
33   intro u hu
34   ring
35 
36 theorem self_adjoint (ρ : Representation ℂ G (X → ℂ))
37     (hunitary : ∀ g f h, pairing (ρ g f) (ρ g h) = pairing f h) (f h : X → ℂ) :
38     pairing (FiniteAverage.average ρ f) h = pairing f (FiniteAverage.average ρ h) := by
39   have hmove (g : G) : pairing (ρ g f) h = pairing f (ρ g⁻¹ h) := by
40     simpa only [ρ.self_inv_apply] using hunitary g f (ρ g⁻¹ h)
41   rw [pairing_average_left, pairing_average_right]
42   congr 1
43   simp_rw [hmove]
44   exact Function.Bijective.sum_comp (Equiv.inv G).bijective (fun g => pairing f (ρ g h))
45 
46 theorem residual_orthogonal (ρ : Representation ℂ G (X → ℂ))
47     (hunitary : ∀ g f h, pairing (ρ g f) (ρ g h) = pairing f h)
48     (f : X → ℂ) {h : X → ℂ} (hh : h ∈ ρ.invariants) :
49     pairing (f - FiniteAverage.average ρ f) h = 0 := by
50   have hsub (a b c : X → ℂ) : pairing (a-b) c = pairing a c - pairing b c := by
51     simp [pairing, star_sub, sub_mul, Finset.sum_sub_distrib]
52   rw [hsub, self_adjoint ρ hunitary, FiniteAverage.fixes ρ hh, sub_self]
53 
54 end PaperXI.FiniteFunctionAverage

Back to source controls