OAI/NumberTheory/Ostmann/Tree/PairedPartitions.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.card_pairedMaps line 13
2. theorem OAI.Ostmann.pairedMaps_correlation_eq line 26
3. theorem OAI.Ostmann.pairedMaps_correlation_sq_le line 44
4. theorem OAI.Ostmann.partitionProduct_cycleMultiply line 65
5. theorem OAI.Ostmann.pairedPartitions_projection line 81

   Source documentation

   Exact counting normalization of the paired-component projection step.

   theorem pairedPartitions_projection {L C G : Type*}
       [Fintype L] [Fintype C] [DecidableEq L] [DecidableEq C]
       [CommGroup G] [Fintype G] [DecidableEq G]
       (component₁ component₂ : L → C)
       (pivot₁ : ∀ c, {i : L // component₁ i = c})
       (pivot₂ : ∀ c, {i : L // component₂ i = c})
       (sign : L → ℤ)
       (hs : ∀ c, ∑ i ∈ Finset.univ.filter (fun i => component₁ i = c), sign i = 0)
       (f g : (L → G) → ℂ) :
       ‖((Fintype.card (L → G) : ℂ) *
           (Fintype.card G ^ (Fintype.card L - Fintype.card C) : ℕ))⁻¹ *
         (∑ x : L → G, ∑ y : L → G,
   …