OAI/NumberTheory/Ostmann/Characters/QuartetStateBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local estimates on every depth-two tree arising from the cut

  1. theorem OAI.Ostmann.rationalTree_quartet_coefficient_le line 13
  2. theorem OAI.Ostmann.rationalTree_quartet_secondMoment_le line 26
  3. theorem OAI.Ostmann.rationalQuartetState_secondMoment_le line 38