OAI/NumberTheory/Ostmann/Characters/CycleAction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal multiplication on cycle leaves

An integer sign on each leaf specifies multiplication by z or its inverse. A block whose signs sum to zero has its product preserved by this action. Thus a balanced cycle preserves both component totals and quartet totals.

  1. def OAI.Ostmann.cycleMultiply line 19
  2. def OAI.Ostmann.leafCycleAction line 22
  3. theorem OAI.Ostmann.cycleMultiply_product line 35
  4. theorem OAI.Ostmann.cycleMultiply_preserves_product line 45
  5. def OAI.Ostmann.cycleAverage line 50
  6. theorem OAI.Ostmann.cycleAverage_energy_le line 54
  7. theorem OAI.Ostmann.cycleAverage_block_correlation line 61

    Source documentation

    Tests depending only on balanced block products are unchanged by projection.

    theorem cycleAverage_block_correlation {I J G : Type*} [CommGroup G]
    [Fintype G] [Fintype I] [DecidableEq I]
    (blocks : J → Finset I) (sign : I → ℤ)
    (hs : ∀ j, ∑ i ∈ blocks j, sign i = 0)
    (f : (I → G) → ℂ) (h : (J → G) → ℂ) :
    (∑ m : I → G, cycleAverage sign f m * conj (h (fun j => ∏ i ∈ blocks j, m i))) =
      ∑ m : I → G, f m * conj (h (fun j => ∏ i ∈ blocks j, m i)) := by
…

    Mentions: OAI.Ostmann.cycleAverage