OAI/NumberTheory/SiegelZeros/Structure/SumLogPrimeFactors.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.sum_log_primeFactors_le line 17
  2. theorem OAI.SiegelZeros.WeightedTorusJets.sum_log_div_primeFactors_le line 29
  3. theorem OAI.SiegelZeros.WeightedTorusJets.sum_log_div_filter_dvd_le line 36
  4. theorem OAI.SiegelZeros.WeightedTorusJets.sum_log_div_filter_le_cutoff line 47
  5. theorem OAI.SiegelZeros.WeightedTorusJets.prime_mass_partition_le line 56
  6. theorem OAI.SiegelZeros.WeightedTorusJets.good_mass_of_estimates line 92
  7. theorem OAI.SiegelZeros.WeightedTorusJets.good_prime_mass_of_primebias line 108
  8. theorem OAI.SiegelZeros.WeightedTorusJets.source_analytic_lemma line 146
  9. theorem OAI.SiegelZeros.WeightedTorusJets.source_hadamard_logDeriv_identity line 217
  10. theorem OAI.SiegelZeros.WeightedTorusJets.source_logDeriv_upper line 234
  11. theorem OAI.SiegelZeros.WeightedTorusJets.logDeriv_real_of_complex line 253
  12. theorem OAI.SiegelZeros.WeightedTorusJets.source_hadamard_logDeriv_identity_real line 264
  13. theorem OAI.SiegelZeros.WeightedTorusJets.completedL_analyticOrderAt_eq_LFunction line 288
  14. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_analyticOrderAt_eq_LFunction line 316
  15. theorem OAI.SiegelZeros.WeightedTorusJets.exists_radius_LFunction_ne_zero line 323
  16. theorem OAI.SiegelZeros.WeightedTorusJets.exists_radius_LFunction_ne_zero_fixed_modulus line 336
  17. theorem OAI.SiegelZeros.WeightedTorusJets.exists_gap_fixed_modulus line 355
  18. theorem OAI.SiegelZeros.WeightedTorusJets.exists_gap_bounded_moduli line 368
  19. theorem OAI.SiegelZeros.WeightedTorusJets.exists_small_gap_large_modulus line 391
  20. theorem OAI.SiegelZeros.WeightedTorusJets.exists_contrary_sequence line 420