OAI/NumberTheory/Ostmann/Arithmetic/MovingFieldGiant.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingFieldGiantAmplitude line 10
2. theorem OAI.Ostmann.MovingGiantTree.exists_field_diagram line 27

   Source documentation

   This is a field identity on all bulk residues, so the later averaging does not require an integer lift satisfying the original division tests.

   theorem MovingGiantTree.exists_field_diagram {q : ℕ} [Fact q.Prime]
       {n C : ℕ} (T : MovingGiantTree n C) (hT : T.UnitsAt q) :
       ∃ (U : (ZMod q)ˣ) (R : RationalTreeData (ZMod q)ˣ n U),
         (C : ZMod q) = U ∧ (T.frequency : ZMod q) = R.frequency ∧
         ∀ (g : ZMod q → ℂ) (D A B : (ZMod q)ˣ)
           (z : TreeLeafTuple (ZMod q)ˣ n) (b : Bool),
           (if b then conj (movingFieldGiantAmplitude g D T A B z)
             else movingFieldGiantAmplitude g D T A B z) =
             rationalTreeAmplitude g D R A B (transferConjugations n b) z := by
   …

   Mentions: OAI.Ostmann.MovingGiantTree, OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingFieldGiantAmplitude, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.transferConjugations