OAI/NumberTheory/Ostmann/ZeroDensity/DensityPolynomialBalance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The balanced exponent and logarithms in the polynomial alternative

  1. theorem OAI.Ostmann.density_balance_at_most line 9
  2. theorem OAI.Ostmann.density_target_at_least line 15
  3. theorem OAI.Ostmann.density_polynomial_balanced_powers line 21
  4. theorem OAI.Ostmann.density_balanced_log_cost line 40