OAI/NumberTheory/Ostmann/Arithmetic/BulkSlotFieldBridge.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.treeNaturalLift_iff_indexed line 11
2. theorem OAI.Ostmann.movingSlotValues_indexed line 29
3. def OAI.Ostmann.bulkSlotLeaves line 40
4. theorem OAI.Ostmann.bulkSlotLeaves_naturalLift line 44
5. theorem OAI.Ostmann.moving_field_pair_bulk_slots line 59

   Source documentation

   The same labelled slot map is used in both histories, with precisely the specified permutation. The rational diagrams are chosen before the bulk primes.

   theorem moving_field_pair_bulk_slots {σ : Type*} {q : ℕ} [Fact q.Prime]
       (value : σ → ℕ) (n m : ℕ) (t : Bool → FrequencyTree ℤ n)
       (small : Bool → TreeLeafTuple (List σ) n) (samples : Bool → MovingSampleSlots σ n)
       (hfreq : ∀ side, movingGiantFrequencyUnits q n (t side))
       (hsmall : ∀ side, ((treeLeafProduct n (movingSlotValues value n (small side)) : ℕ) : ZMod q) ≠ 0)
       (hsamples : ∀ side, ((samples side).values value).UnitsAt q)
       (D A B : Bool → (ZMod q)ˣ) :
       ∃ d : Bool → SpectatorDiagram q n,
         (∀ side, (d side).conjugations = transferConjugations n false) ∧
         ∀ (g : ZMod q → ℂ) (slot : TreeLeafIndex n × Fin m → σ)
           (e : Equiv.Perm (TreeLeafIndex n × Fin m)) (z : TreeLeafIndex n × Fin m → (ZMod q)ˣ),
           (∀ j, (value (slot j) : ZMod q) = (z j : ZMod q)) →
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingGiantFrequencyUnits, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.movingSlotValues, OAI.Ostmann.SpectatorDiagram, OAI.Ostmann.transferConjugations, OAI.Ostmann.TreeLeafIndex