OAI/NumberTheory/Ostmann/Construction/DiagonalTransfer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Grouping the transfer diagonal before expanding the square

  1. def OAI.Ostmann.groupedCoefficient line 11
  2. theorem OAI.Ostmann.diagonal_grouped_identity line 17

    Source documentation

    The key comprises the inherited product and its frequency. Ordered arrangements with that key are summed inside the square.

    theorem diagonal_grouped_identity {A K : Type*} [Fintype A] [Fintype K]
    (key : A → K) (z : A → ℂ) (w : K → ℂ) :
    (∑ a : A, ∑ b : A, if key a = key b then w (key a) * z a * star (z b) else 0) =
      ∑ k : K, w k * groupedCoefficient key z k * star (groupedCoefficient key z k) := by
…

    Mentions: OAI.Ostmann.groupedCoefficient

  3. theorem OAI.Ostmann.diagonal_real_eq_sum_sq line 34
  4. theorem OAI.Ostmann.diagonal_real_nonneg line 42