FrozenSpectatorDiagram.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

One rational diagram for all bulk replacements of fixed nonbulk data

theorem OAI.Ostmann.buildMovingSlotData_frozen_field_diagram line 10

theorem OAI.Ostmann.moving_field_pair_frozen_diagrams line 35

Source documentation

The same pair of diagrams works simultaneously for every actual bulk tuple with the fixed small leaves and fixed internal samples.

theorem moving_field_pair_frozen_diagrams {σ : Type*} {q : ℕ} [Fact q.Prime]
    (base : σ → ℕ) (n : ℕ) (t : Bool → FrequencyTree ℤ n)
    (small : Bool → TreeLeafTuple (List σ) n) (samples : Bool → MovingSampleSlots σ n)
    (hfreq : ∀ b, movingGiantFrequencyUnits q n (t b))
    (hsmall : ∀ b, ((treeLeafProduct n (movingSlotValues base n (small b)) : ℕ) : ZMod q) ≠ 0)
    (hsamples : ∀ b, ((samples b).values base).UnitsAt q)
    (D A B : Bool → (ZMod q)ˣ) :
    ∃ d : Bool → SpectatorDiagram q n,
      (∀ b, (d b).conjugations = transferConjugations n false) ∧
      ∀ (value : σ → ℕ),
        (∀ b, movingSlotValues value n (small b) = movingSlotValues base n (small b)) →
        (∀ b, (samples b).values value = (samples b).values base) →
…

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

theorem OAI.Ostmann.moving_field_pair_frozen_bulk_slots line 66