OAI/NumberTheory/Ostmann/Construction/InitialMixedNormalizer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization cost of the two original mixed half-lists

  1. def OAI.Ostmann.initialHalfNormalizer line 10
  2. theorem OAI.Ostmann.initialHalfNormalizer_nonneg line 16
  3. theorem OAI.Ostmann.initialHalfNormalizer_prime_bound line 29
  4. theorem OAI.Ostmann.initialHalfNormalizer_prod line 46
  5. theorem OAI.Ostmann.initial_mixed_normalizer_identity line 54
  6. theorem OAI.Ostmann.initial_mixed_normalizer_bound line 84
  7. theorem OAI.Ostmann.initial_cell_normalizer_budget line 104