OAI/NumberTheory/CubicMoment/Estimates/FlatTripleGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The largest coordinate of a flat triple gives a genuine transition range. All lower bounds come from the original nonzero box.

  1. lemma OAI.CubicFirstMoment.largeTuple_singleton_product line 17
  2. lemma OAI.CubicFirstMoment.largeTuple_other_le_square line 25
  3. lemma OAI.CubicFirstMoment.largeTuple_product_le_cube line 35
  4. lemma OAI.CubicFirstMoment.eventually_maximum_triple_scale line 44
  5. lemma OAI.CubicFirstMoment.flatTriple_transition_lower line 58
  6. theorem OAI.CubicFirstMoment.eventually_flatTriple_transition_geometry line 73