/-
  StarG/Algebra.lean, Lean 4.29 / current Mathlib compatible
-/
import StarG.Basic

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

open Finset BigOperators Matrix

noncomputable section

namespace GroupTensor

variable {G : Type*} [Group G] [Fintype G] [DecidableEq G]
variable {ℓ m p : ℕ}

theorem starG_add_right
    (A : GroupTensor G ℓ m) (B C : GroupTensor G m p) :
    A ⋆ (B + C) = A ⋆ B + A ⋆ C := by
  funext c i j
  simp only [starG, Pi.add_apply, Matrix.add_apply, mul_add, Finset.sum_add_distrib]

theorem starG_add_left
    (A B : GroupTensor G ℓ m) (C : GroupTensor G m p) :
    (A + B) ⋆ C = A ⋆ C + B ⋆ C := by
  funext c i j
  simp only [starG, Pi.add_apply, Matrix.add_apply, add_mul, Finset.sum_add_distrib]

theorem starG_identity_right (A : GroupTensor G ℓ m) :
    A ⋆ (starIdentity : GroupTensor G m m) = A := by
  funext c i j; simp only [starG, starIdentity]
  have h : ∀ k : Fin m,
      ∑ a : G, A a i k * (if a⁻¹ * c = 1 then (1 : Matrix _ _ ℝ) else 0) k j =
      A c i k * (1 : Matrix (Fin m) (Fin m) ℝ) k j := by
    intro k; rw [Fintype.sum_eq_single c]
    · simp [inv_mul_cancel]
    · intro a ha; simp [show a⁻¹ * c ≠ 1 from fun h => ha (by rwa [inv_mul_eq_one] at h)]
  simp_rw [h]; simp [Matrix.one_apply]

theorem starG_identity_left (A : GroupTensor G ℓ m) :
    (starIdentity : GroupTensor G ℓ ℓ) ⋆ A = A := by
  funext c i j; simp only [starG, starIdentity]
  have h : ∀ k : Fin ℓ,
      ∑ a : G, (if a = 1 then (1 : Matrix _ _ ℝ) else 0) i k * A (a⁻¹ * c) k j =
      (1 : Matrix (Fin ℓ) (Fin ℓ) ℝ) i k * A c k j := by
    intro k; rw [Fintype.sum_eq_single (1 : G)]
    · simp
    · intro a ha; simp [ha]
  simp_rw [h]; simp [Matrix.one_apply]

/-! ### Associativity -/

theorem starG_assoc {q : ℕ}
    (A : GroupTensor G ℓ m) (B : GroupTensor G m p) (C : GroupTensor G p q) :
    (A ⋆ B) ⋆ C = A ⋆ (B ⋆ C) := by
  funext c i j; simp only [starG, Finset.sum_mul, Finset.mul_sum, mul_assoc]
  set F : Fin p → G → Fin m → G → ℝ := fun k₂ b k₁ a =>
    A a i k₁ * (B (a⁻¹ * b) k₁ k₂ * (C (b⁻¹ * c) k₂ j)) with hF
  have key : ∀ k₁ a k₂,
      ∑ b : G, F k₂ b k₁ a =
      ∑ a' : G, A a i k₁ * (B a' k₁ k₂ * (C (a'⁻¹ * (a⁻¹ * c)) k₂ j)) := by
    intro k₁ a k₂; simp only [hF]
    let e : G ≃ G := ⟨(a⁻¹ * ·), (a * ·), fun b => by simp, fun b => by simp⟩
    exact Fintype.sum_equiv e _ _ (fun b => by
      show A a i k₁ * (B (a⁻¹ * b) k₁ k₂ * (C (b⁻¹ * c) k₂ j)) =
           A a i k₁ * (B (a⁻¹ * b) k₁ k₂ * (C ((a⁻¹ * b)⁻¹ * (a⁻¹ * c)) k₂ j))
      congr 3; group)
  calc ∑ k₂, ∑ b, ∑ k₁, ∑ a, F k₂ b k₁ a
      = ∑ k₂, ∑ k₁, ∑ b, ∑ a, F k₂ b k₁ a := by
        apply Finset.sum_congr rfl; intro k₂ _; exact Finset.sum_comm
    _ = ∑ k₁, ∑ k₂, ∑ b, ∑ a, F k₂ b k₁ a := Finset.sum_comm
    _ = ∑ k₁, ∑ k₂, ∑ a, ∑ b, F k₂ b k₁ a := by
        apply Finset.sum_congr rfl; intro k₁ _
        apply Finset.sum_congr rfl; intro k₂ _; exact Finset.sum_comm
    _ = ∑ k₁, ∑ a, ∑ k₂, ∑ b, F k₂ b k₁ a := by
        apply Finset.sum_congr rfl; intro k₁ _; exact Finset.sum_comm
    _ = _ := by
        apply Finset.sum_congr rfl; intro k₁ _
        apply Finset.sum_congr rfl; intro a _
        apply Finset.sum_congr rfl; intro k₂ _
        exact key k₁ a k₂

/-! ### Transpose reversal -/

theorem starG_transpose_mul
    (A : GroupTensor G ℓ m) (B : GroupTensor G m p) :
    starTranspose (A ⋆ B) = starTranspose B ⋆ starTranspose A := by
  funext c i j; simp only [starTranspose, starG]
  apply Finset.sum_congr rfl; intro k _
  let e : G ≃ G := ⟨(c * ·), (c⁻¹ * ·), fun a => by simp, fun a => by simp⟩
  exact Fintype.sum_equiv e _ _ (fun a => by
    dsimp [e]
    simp only [_root_.inv_inv, _root_.mul_inv_rev, _root_.inv_mul_cancel_left]
    ring)

/-! ### Frobenius norm -/

def frobNormSq (A : GroupTensor G ℓ m) : ℝ :=
  ∑ g : G, ∑ i : Fin ℓ, ∑ j : Fin m, A g i j ^ 2

theorem frobNormSq_nonneg (A : GroupTensor G ℓ m) : 0 ≤ frobNormSq A :=
  Finset.sum_nonneg fun _ _ => Finset.sum_nonneg fun _ _ =>
    Finset.sum_nonneg fun _ _ => sq_nonneg _

end GroupTensor
end