OAI/NumberTheory/Ostmann/Tree/PairedRationalReduction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.pairedPartitionCorrelation line 12
2. theorem OAI.Ostmann.card_pairedPartitions line 23

   Source documentation

   The counting denominator is exactly the size of the equal-total sample space.

   theorem card_pairedPartitions {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}) :
       (Finset.univ.filter fun xy : (L → G) × (L → G) =>
         partitionProduct component₁ xy.1 = partitionProduct component₂ xy.2).card =
           Fintype.card (L → G) * Fintype.card G ^ (Fintype.card L - Fintype.card C) :=
   …

   Mentions: OAI.Ostmann.partitionProduct

3. theorem OAI.Ostmann.pairedRationalTree_projection line 34

   Source documentation

   The projection reduction in tree-projection-reduction, for the actual diagram values.

   theorem pairedRationalTree_projection {p : ℕ} [Fact p.Prime]
       (hp : 3 ≤ p) (g : ZMod p → ℂ) (hg : g 0 = 0)
       (henergy : (∑ x : ZMod p, ‖g x‖ ^ 2) ≤ (p : ℝ))
       (n : ℕ) {C : Type*} [Fintype C] [DecidableEq C]
       (component₁ component₂ : TreeLeafIndex (n + 2) → C)
       (pivot₁ : ∀ c, {i : TreeLeafIndex (n + 2) // component₁ i = c})
       (pivot₂ : ∀ c, {i : TreeLeafIndex (n + 2) // component₂ i = c})
       (hc : Fintype.card C ≤ 3 * 2 ^ n)
       (D₁ D₂ : (ZMod p)ˣ) {K₁ K₂ : (ZMod p)ˣ}
       (T₁ : RationalTreeData (ZMod p)ˣ (n + 2) K₁)
       (T₂ : RationalTreeData (ZMod p)ˣ (n + 2) K₂)
       (XL₁ XR₁ XL₂ XR₂ : (ZMod p)ˣ) (c₁ c₂ : TreeLeafTuple Bool (n + 2)) :
   …

   Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple