OAI/NumberTheory/Ostmann/Tree/CycleLocalMajorantsCoefficients.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.FiniteField.mellin_const_value line 12
  2. theorem OAI.Ostmann.Tree.CycleQuartet.kind_fiber_bound line 26
  3. def OAI.Ostmann.Tree.CycleQuartet.localMajorant line 52
  4. theorem OAI.Ostmann.Tree.CycleQuartet.localMajorant_selected line 58
  5. theorem OAI.Ostmann.Tree.CycleQuartet.localMajorant_unselected line 64
  6. theorem OAI.Ostmann.Tree.CycleQuartet.localMajorant_nonneg line 70
  7. theorem OAI.Ostmann.Tree.CycleQuartet.localMajorant_mean_small line 79
  8. theorem OAI.Ostmann.Tree.CycleQuartet.localMajorant_mean_total line 87
  9. theorem OAI.Ostmann.Tree.CycleQuartet.localAct_fiber_bound line 97
  10. def OAI.Ostmann.Tree.CycleQuartet.fiberValues line 120
  11. theorem OAI.Ostmann.Tree.CycleQuartet.actionCoefficient_fiber_bound line 124