KMSKernelOrbitsFourier.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Basis-invariant matrix functions have constant actual Fourier coefficients on kernel fibers. This uses ambient automorphism transitivity proved from the first isomorphism theorem, followed by the exact change-of-basis identity for the normalized trace-character transform.

theorem OAI.MaxCutGames.Inverse.KMSKernelOrbitsFourier.coefficient_eq_of_ker_eq line 28
Source documentation
Actual coefficients depend on the kernel, not on the chosen embedding of the quotient into the basis-index space. No coefficient-invariance premise is assumed beyond the original function's basis invariance.
```
theorem coefficient_eq_of_ker_eq (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) (S T : F →ₗ[F2] E) (hker : S.ker = T.ker) :
    linearCoeff f S = linearCoeff f T := by
…
```