OAI/NumberTheory/Ostmann/QuadraticCenter/OuterDivisorDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exponential decay of all nontrivial sampled outer divisors

  1. theorem OAI.Ostmann.outer_divisor_factor_decay line 12
  2. theorem OAI.Ostmann.eventual_outer_divisor_norm_decay line 36