OAI/NumberTheory/Ostmann/Characters/PivotSquareExpansion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.pivotResidueKey line 12
2. theorem OAI.Ostmann.pivotResidueKey_eq_iff line 15
3. theorem OAI.Ostmann.pivot_square_expansion line 23

   Source documentation

   The original coefficients are grouped inside the square before the coprime residue condition is replaced by integer divisibility.

   theorem pivot_square_expansion {A : Type*} [Fintype A]
       (M : ℕ) [NeZero M] (L : A → ℕ) (v : A → ℤ)
       (hL : ∀ a, (L a).Coprime M) (c : A → ℂ) :
       (∑ u : Fin M, ‖groupedCoefficient (fun a => pivotResidueKey M (L a) (v a)) c u‖ ^ 2) =
         (∑ a, ∑ b, if (M : ℤ) ∣ v a * L b - v b * L a then c a * conj (c b) else 0).re := by
   …

   Mentions: OAI.Ostmann.groupedCoefficient, OAI.Ostmann.pivotResidueKey

4. theorem OAI.Ostmann.pivot_zero_numerator_iff line 39
5. theorem OAI.Ostmann.pivot_diagonal_expansion line 52

   Source documentation

   The zero-numerator part is the exact equal-product/equal-frequency square, including every ordered arrangement carrying that key.

   theorem pivot_diagonal_expansion {A : Type*} [Fintype A]
       (L : A → ℕ) (v : A → ℤ) (c : A → ℂ)
       (hLpos : ∀ a, 0 < L a) (hv : ∀ a, v a ≠ 0)
       (hlarge : ∀ a q, q.Prime → q ∣ L a → (v a).natAbs < q) :
       (∑ a, ∑ b, if v a * L b - v b * L a = 0 then c a * conj (c b) else 0) =
         ∑ a, ∑ b, if (L a, v a) = (L b, v b) then c a * conj (c b) else 0 := by
   …