OAI/NumberTheory/Ostmann/Tree/UntouchedQuartetBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Conditional second moment of an untouched actual quartet

  1. theorem OAI.Ostmann.sum_samePairMajorant_eq line 14
  2. theorem OAI.Ostmann.rationalQuartet_fiber_secondMoment_le line 26
  3. theorem OAI.Ostmann.untouchedQuartetMajorant_mean_le line 53