OAI/NumberTheory/Ostmann/Characters/PivotSquareSplit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.finite_key_square_nonneg line 14

   Source documentation

   A finite family has a nonnegative equal-key square even when its keys range over an infinite type.

   theorem finite_key_square_nonneg {A K : Type*} [Fintype A]
       (key : A → K) (c : A → ℂ) :
       0 ≤ (∑ a, ∑ b, if key a = key b then c a * conj (c b) else 0).re := by
   …

2. def OAI.Ostmann.pivotDiagonal line 23
3. def OAI.Ostmann.pivotOffDiagonal line 27
4. theorem OAI.Ostmann.pivot_square_split line 32
5. theorem OAI.Ostmann.pivotDiagonal_nonneg line 51
6. theorem OAI.Ostmann.pivotOffDiagonal_eq_frequency_sum line 66

   Source documentation

   The off-diagonal is indexed by the genuine signed output frequency, with no extra multiplicity.

   theorem pivotOffDiagonal_eq_frequency_sum {A : Type*} [Fintype A]
       (M B H V : ℕ) (hM : 0 < M) (L : A → ℕ) (v : A → ℤ) (c : A → ℂ)
       (hv : ∀ a, (v a).natAbs ≤ B) (hL : ∀ a, L a ≤ H)
       (hscale : 2 * B * H ≤ V * M) :
       pivotOffDiagonal M L v c = ∑ s ∈ transferFrequencyRange V,
         ∑ a, ∑ b, if s ≠ 0 ∧ v a * L b - v b * L a = s * M
           then c a * conj (c b) else 0 := by
   …

   Mentions: OAI.Ostmann.pivotOffDiagonal, OAI.Ostmann.transferFrequencyRange