OAI/NumberTheory/CubicMoment/Estimates/TypeISelectedHeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The Type-I height bounds with a weight selected independently for every level. Constants are chosen before the selector, so subsequent decompositions may use the original joint smooth-weight family.

  1. theorem OAI.CubicFirstMoment.typeI_selected_finite_levels line 15
  2. theorem OAI.CubicFirstMoment.typeI_selected_height_of_published line 69
  3. theorem OAI.CubicFirstMoment.angular_typeI_selected_height_of_published line 118