OAI/NumberTheory/Ostmann/Characters/CharacterCellIntervals.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The pivot lists, two anchors and filler give the actual character cells

  1. def OAI.Ostmann.characterCellIndex line 10

    Source documentation

    A selected ordered list is used once in each signed copy.

    def characterCellIndex {k : ℕ} (w : Fin k → List ℕ)
    (a : Fin k → Bool → ℕ) (u : List ℕ) :
    (v : CharacterCell k) → Fin (characterCellSize (fun j => (w j).length) u.length v) → ℕ
  | .inl j, i => (w j).get i
  | .inr (.inl (j, b)), _ => a j b
  | .inr (.inr _), i => u.get i

    Mentions: OAI.Ostmann.CharacterCell, OAI.Ostmann.characterCellSize

  2. theorem OAI.Ostmann.characterCellIndex_target line 17
  3. theorem OAI.Ostmann.characterCellIndex_product_bounds line 41
  4. theorem OAI.Ostmann.characterCellIndex_prime_bounds line 55