OAI/NumberTheory/DirichletL/PrimeRows/DetectorZeros.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbeHighRowFamily.detectorEntire line 12
  2. lemma OAI.SevenEighths.ProbeHighRowFamily.detectorEntire_eq_nonprincipal line 15
  3. lemma OAI.SevenEighths.ProbeHighRowFamily.detectorEntire_entire line 20
  4. lemma OAI.SevenEighths.ProbeHighRowFamily.detectorEntire_zero_iff line 28
  5. lemma OAI.SevenEighths.ProbeHighRowFamily.detectorEntire_ne_zero_of_one_lt_re line 41
  6. def OAI.SevenEighths.ProbeHighRowFamily.detectorZeros line 46
  7. lemma OAI.SevenEighths.ProbeHighRowFamily.detectorZeros_finite line 49
  8. def OAI.SevenEighths.ProbeHighRowFamily.detectorZeroFinset line 64
  9. lemma OAI.SevenEighths.ProbeHighRowFamily.mem_detectorZeroFinset line 66
  10. def OAI.SevenEighths.ProbeHighRowFamily.detectorFamilyZeros line 74
  11. lemma OAI.SevenEighths.ProbeHighRowFamily.mem_detectorFamilyZeros line 77
  12. def OAI.SevenEighths.ProbeHighRowFamily.detectorRealParts line 82
  13. lemma OAI.SevenEighths.ProbeHighRowFamily.detectorRealParts_nonempty line 85
  14. def OAI.SevenEighths.ProbeHighRowFamily.detectorMaximum line 88
  15. lemma OAI.SevenEighths.ProbeHighRowFamily.detectorMaximum_mem line 91
  16. lemma OAI.SevenEighths.ProbeHighRowFamily.detectorMaximum_bounds line 94
  17. lemma OAI.SevenEighths.ProbeHighRowFamily.detector_zero_re_le_maximum line 105
  18. lemma OAI.SevenEighths.ProbeHighRowFamily.detectorMaximum_attained line 115
  19. lemma OAI.SevenEighths.ProbeHighRowFamily.detectorMaximum_mono line 126
  20. lemma OAI.SevenEighths.ProbeHighRowFamily.detector_nonzero_above_maximum line 134
  21. lemma OAI.SevenEighths.ProbeHighRowFamily.detector_reciprocal_differentiableAt line 141