OAI/NumberTheory/Ostmann/Characters/CharacterScheduleRoles.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The finite role set used in the nonquadratic character argument

A positive word, finitely many pivot groups, two fresh anchors at each step, and one filler have independent negative copies. Only the positive word, pivots and anchors participate in the copy schedule.

  1. abbrev OAI.Ostmann.CharacterCell line 15
  2. abbrev OAI.Ostmann.CharacterRole line 16
  3. def OAI.Ostmann.characterPositiveRole line 18
  4. def OAI.Ostmann.characterRole line 24
  5. def OAI.Ostmann.characterCellSize line 27
  6. def OAI.Ostmann.characterSize line 32
  7. def OAI.Ostmann.characterPivotAtom line 35
  8. def OAI.Ostmann.characterAnchorAtom line 38
  9. theorem OAI.Ostmann.characterRole_word line 41
  10. theorem OAI.Ostmann.characterRole_pivot line 42
  11. theorem OAI.Ostmann.characterRole_anchor line 44
  12. theorem OAI.Ostmann.characterSize_word line 47
  13. theorem OAI.Ostmann.characterSize_pivot line 49
  14. theorem OAI.Ostmann.characterSize_anchor line 51
  15. def OAI.Ostmann.characterWordEquiv line 55

    Source documentation

    The actual positive word, including its one top label.

    noncomputable def characterWordEquiv {k : ℕ} (m : ℕ) (r : Fin k → ℕ) (f : ℕ) :
    Fin (m + 1) ≃ {i : Σ v, Fin (characterSize m r f v) // characterRole k i.1 = .word} :=
…

    Mentions: OAI.Ostmann.characterSize, OAI.Ostmann.characterRole

  16. theorem OAI.Ostmann.characterPivotAtom_unique line 74
  17. def OAI.Ostmann.characterPivot line 92

    Source documentation

    Extend the finitely many real pivots by an arbitrary existing word slot. All transfer theorems use only the genuine prefix.

    noncomputable def characterPivot {k : ℕ} (m : ℕ) (r : Fin k → ℕ) (f : ℕ)
    (hr : ∀ j, 0 < r j) (j : ℕ) : Σ v, Fin (characterSize m r f v) :=
…

    Mentions: OAI.Ostmann.characterSize

  18. theorem OAI.Ostmann.characterPivot_role line 97
  19. def OAI.Ostmann.characterAnchor line 102
  20. theorem OAI.Ostmann.characterAnchor_role line 106
  21. theorem OAI.Ostmann.characterAnchor_ne line 109
  22. theorem OAI.Ostmann.characterSchedule_matching line 118

    Source documentation

    Every retained H permutation preserves the original signed character.

    theorem characterSchedule_matching {k : ℕ} (m : ℕ) (r : Fin k → ℕ) (f : ℕ)
    (χ : ∀ p : ℕ, DirichletCharacter ℂ p) (n : ℕ)
    (e : Equiv.Perm (CopyScheduleH
      (fun i : Σ v, Fin (characterSize m r f v) => characterRole k i.1) n))
    (h : CopyScheduleH
      (fun i : Σ v, Fin (characterSize m r f v) => characterRole k i.1) n) :
    signedAtomCharacter (initialWordSize (m + 1) (characterCellSize r f)) χ
        (copyScheduleOrigin n (e h).val) =
      signedAtomCharacter (initialWordSize (m + 1) (characterCellSize r f)) χ
        (copyScheduleOrigin n h.val) :=
…

    Mentions: OAI.Ostmann.CopyScheduleH, OAI.Ostmann.characterSize, OAI.Ostmann.characterRole, OAI.Ostmann.signedAtomCharacter, OAI.Ostmann.initialWordSize, OAI.Ostmann.characterCellSize, OAI.Ostmann.copyScheduleOrigin