OAI/NumberTheory/DirichletL/PrimeRows/DiskControl.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.ProbeHighRowFamily.poleRemoved_eq_regularizedL line 13
  2. lemma OAI.SevenEighths.ProbeHighRowFamily.regular_eq_of_mask line 20
  3. lemma OAI.SevenEighths.ProbeHighRowFamily.regular_eq_detector line 33
  4. lemma OAI.SevenEighths.ProbeHighRowFamily.regular_nonzero_of_detector line 39
  5. lemma OAI.SevenEighths.ProbeHighRowFamily.reciprocal_norm_le_regular_inverse_on_positive line 50
  6. theorem OAI.SevenEighths.ProbeHighRowFamily.original_regular_disk_control line 78
  7. theorem OAI.SevenEighths.ProbeHighRowFamily.buffered_regular_control line 139
  8. theorem OAI.SevenEighths.ProbeHighRowFamily.buffered_rectangle_reciprocal_bound line 157