OAI/NumberTheory/CubicMoment/Estimates/OuterCostMonotone.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniformize the three primal powers without attaching an epsilon loss to the zero-frequency A term.

  1. lemma OAI.CubicFirstMoment.outer_cost_mono line 10
  2. lemma OAI.CubicFirstMoment.quotient_scale_bound line 30