OAI/NumberTheory/Ostmann/Characters/QuartetProductFibers.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Independent product fibers at the bottom quartet level

  1. def OAI.Ostmann.quartetBlockTupleEquiv line 12
  2. theorem OAI.Ostmann.quartetBlockTupleEquiv_succ line 17
  3. def OAI.Ostmann.quartetBlockEquiv line 22
  4. def OAI.Ostmann.quartetProducts line 26
  5. abbrev OAI.Ostmann.QuartetProductFiber line 30
  6. instance OAI.Ostmann.quartetProductFiberFintype line 33
  7. def OAI.Ostmann.quartetProductFiberEquiv line 41

    Source documentation

    Given the bottom quartet products, their interiors are independent uniform fibers; the maps do not depend on any tree parameters.

    def quartetProductFiberEquiv {U : Type*} [CommGroup U] (n : ℕ) (P : TreeLeafIndex n → U) :
    QuartetProductFiber U n P ≃ ((i : TreeLeafIndex n) → TreeLeafFiber U 2 (P i)) where
…

    Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.QuartetProductFiber, OAI.Ostmann.TreeLeafFiber

  8. theorem OAI.Ostmann.quartetProductFiberEquiv_symm line 58
  9. theorem OAI.Ostmann.card_quartetProductFiber line 64
  10. theorem OAI.Ostmann.sum_quartetProductFiber_product line 71
  11. theorem OAI.Ostmann.average_quartetProductFiber_product line 83
  12. theorem OAI.Ostmann.sum_treeLeafTuple_by_quartetProducts line 96