OAI/NumberTheory/DirichletL/Supremum.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.Supremum.continuationMargin line 10
  2. theorem OAI.SevenEighths.Supremum.continuationMargin_pos line 12
  3. theorem OAI.SevenEighths.Supremum.continuationMargin_le_gap line 17
  4. theorem OAI.SevenEighths.Supremum.continuationMargin_le_sigma line 21
  5. theorem OAI.SevenEighths.Supremum.continuation_boundary_gt line 25
  6. theorem OAI.SevenEighths.Supremum.max_signal_exponents line 30
  7. theorem OAI.SevenEighths.Supremum.max_normalized_signal_exponents line 39
  8. theorem OAI.SevenEighths.Supremum.exists_gt_supremum_sub line 45
  9. theorem OAI.SevenEighths.Supremum.uniform_bound_below_supremum_false line 51
  10. theorem OAI.SevenEighths.Supremum.exists_gt_supremum_sub_of_insert line 57
  11. theorem OAI.SevenEighths.Supremum.seven_eighths_of_uniform_margin line 68
  12. theorem OAI.SevenEighths.Supremum.seven_eighths_of_uniform_margin_with_sentinel line 79