MovingFieldDiagram.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed diagrams for the separated modular spectator factors

theorem OAI.Ostmann.buildMovingSlotData_field_diagram line 13

Source documentation

The diagram is chosen from the small slots and frequencies before any bulk values or giant residues are supplied.

theorem buildMovingSlotData_field_diagram {σ : Type*} {q : ℕ} [Fact q.Prime]
    (value : σ → ℕ) (n : ℕ) (t : FrequencyTree ℤ n)
    (small : TreeLeafTuple (List σ) n) (samples : MovingSampleSlots σ n)
    (hfreq : movingGiantFrequencyUnits q n t)
    (hsmall : ((treeLeafProduct n (movingSlotValues value n small) : ℕ) : ZMod q) ≠ 0)
    (hsamples : (samples.values value).UnitsAt q) :
    ∃ (U : (ZMod q)ˣ) (R : RationalTreeData (ZMod q)ˣ n U),
      ∀ (g : ZMod q → ℂ) (D A B : (ZMod q)ˣ)
        (bulk : TreeLeafTuple (List σ) n) (z : TreeLeafTuple (ZMod q)ˣ n),
        TreeNaturalLift n (movingSlotValues value n bulk) z →
        movingModularSpectator value q g D (buildMovingSlotData n t small bulk samples) A B =
          rationalTreeAmplitude g D R A B (transferConjugations n false) z := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingGiantFrequencyUnits, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.movingSlotValues, OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeNaturalLift, OAI.Ostmann.movingModularSpectator, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.transferConjugations

theorem OAI.Ostmann.moving_field_pair_diagrams line 33