OAI/NumberTheory/CubicMoment/Estimates/OverlapScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Elementary powers and logarithmic absorption for model overlap.

  1. lemma OAI.CubicFirstMoment.negative_sixth_square_scale line 11
  2. lemma OAI.CubicFirstMoment.model_overlap_scale line 20
  3. lemma OAI.CubicFirstMoment.norm_le_bilinear_of_square line 32
  4. lemma OAI.CubicFirstMoment.overlap_power_log_saving line 46