OAI/NumberTheory/Ostmann/Characters/CharacterHCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.surviving_anchor_is_reserved line 10
2. theorem OAI.Ostmann.characterRole_word_unique line 34
3. theorem OAI.Ostmann.characterRole_pivot_exists line 46
4. theorem OAI.Ostmann.characterRole_anchor_exists line 60
5. abbrev OAI.Ostmann.CharacterHIndex line 75
6. def OAI.Ostmann.characterHCoordinate line 77
7. theorem OAI.Ostmann.characterHCoordinate_role line 89
8. theorem OAI.Ostmann.characterHCoordinate_origin line 100
9. theorem OAI.Ostmann.characterHCoordinate_injective line 111
10. theorem OAI.Ostmann.characterHCoordinate_surjective line 135
11. def OAI.Ostmann.characterHEquiv line 167
12. theorem OAI.Ostmann.character_H_product line 174

    Source documentation

    Exactly the full words, future pivot groups, and the two fresh anchors occur in H. Inactive copies make no contribution.

    theorem character_H_product {k n : ℕ} (hn : n < k) {M : Type*} [CommMonoid M]
        (w : CharacterRole k → M) :
        (∏ h : CopyScheduleH (characterRole k) n, w (copyScheduleOrigin n h.val)) =
          w (true, none) ^ (2 ^ n) *
            ((∏ j : {j : Fin k // n < j.val}, w (characterPivotAtom j.val)) *
              ∏ b : Bool, w (characterAnchorAtom ⟨n, hn⟩ b)) := by
    …

    Mentions: OAI.Ostmann.CharacterRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.characterRole, OAI.Ostmann.copyScheduleOrigin, OAI.Ostmann.characterPivotAtom, OAI.Ostmann.characterAnchorAtom