OAI/NumberTheory/CubicMoment/Estimates/SparseStoppingLabels.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual final-bin and two-occupancy index set in the stopping construction has logarithmic size. No complete occupancy vector occurs.

  1. def OAI.CubicFirstMoment.stoppingFactorLimit line 15
  2. def OAI.CubicFirstMoment.stoppingLabelBox line 17
  3. lemma OAI.CubicFirstMoment.stoppingFactorLimit_bound line 22
  4. lemma OAI.CubicFirstMoment.stopping_prime_factor_count line 28
  5. lemma OAI.CubicFirstMoment.stoppingLabelBox_card line 45
  6. lemma OAI.CubicFirstMoment.stoppingLabelBox_card_logarithmic line 55
  7. def OAI.CubicFirstMoment.stoppingRemainingTest line 89

    Source documentation

    The exact remaining-side predicate in the stopping split.

    def stoppingRemainingTest (bin : Eisenstein → ℕ) (j l : ℕ) (e : Eisenstein) : Prop :=
…

    Mentions: OAI.CubicFirstMoment.Eisenstein

  8. lemma OAI.CubicFirstMoment.actual_stopping_label_mem_box line 93
  9. lemma OAI.CubicFirstMoment.stopping_scalar_norm_le_one line 122