OAI/NumberTheory/DirichletL/Detector/HighRowsPrime.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbeEuler.sourceRowTerm line 13
  2. theorem OAI.SevenEighths.ProbeEuler.sourceRowTerm_pos line 20
  3. theorem OAI.SevenEighths.ProbePhysical.bareSourceCoefficient_unit_frequency line 37
  4. theorem OAI.SevenEighths.ProbePhysical.bareSourceCoefficient_row_prime_formula line 48
  5. theorem OAI.SevenEighths.ProbePhysical.bareSourceCoefficient_row_weighted_prime line 70
  6. theorem OAI.SevenEighths.ProbePhysical.bareIdealHighCoefficient_row_at_prime line 96
  7. theorem OAI.SevenEighths.ProbePhysical.bareIdealHighSummand_row_at_prime line 115
  8. theorem OAI.SevenEighths.ProbePhysical.idealRowHighLocalFactor_eq_source line 133