OAI/NumberTheory/Ostmann/Characters/QuartetOuterAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Averaging the projected bound over all bottom-quartet products

  1. theorem OAI.Ostmann.card_treeLeafTuple_quartet line 12
  2. theorem OAI.Ostmann.mean_treeLeafTuple_by_quartetProducts line 23
  3. theorem OAI.Ostmann.projectedTree_mean_le line 39