OAI/NumberTheory/Jacobsthal/Siegel/RealLogDerivConductorCompletedLDivisorTsum.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.real_logDeriv_conductorCompletedL_eq_divisor_tsum line 27
  2. theorem OAI.Erdos970.WeightedTorusJets.abs_reciprocal_sub_re_le_normSq line 62
  3. theorem OAI.Erdos970.WeightedTorusJets.abs_reciprocal_re_le_normSq line 102
  4. theorem OAI.Erdos970.WeightedTorusJets.summable_abs_reciprocal_sub_re line 109
  5. theorem OAI.Erdos970.WeightedTorusJets.summable_abs_reciprocal_re line 121
  6. theorem OAI.Erdos970.WeightedTorusJets.divisorZeroIndex_val_zero line 136
  7. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_divisorIndex_re_mem_Ioo line 145
  8. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_abs_reciprocal_summable line 153
  9. theorem OAI.Erdos970.WeightedTorusJets.exists_divisorZeroIndex_val_eq_of_zero line 166
  10. theorem OAI.Erdos970.WeightedTorusJets.real_zero_le_divisor_reciprocal_tsum line 179
  11. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_zero_sum_absolutely_summable line 212
  12. theorem OAI.Erdos970.WeightedTorusJets.real_logDeriv_conductorCompletedL_eq_divisor_tsum_source line 220
  13. theorem OAI.Erdos970.WeightedTorusJets.real_zero_le_conductorCompletedL_logDeriv line 233
  14. lemma OAI.Erdos970.WeightedTorusJets.analyticAt_Gamma_of_re_pos line 252
  15. theorem OAI.Erdos970.WeightedTorusJets.exists_bound_Gamma_logDeriv_parity line 265
  16. theorem OAI.Erdos970.WeightedTorusJets.character_parity_parameter line 291
  17. theorem OAI.Erdos970.WeightedTorusJets.character_parity_parameter_real line 297
  18. theorem OAI.Erdos970.WeightedTorusJets.character_gamma_argument_mem_Icc line 303
  19. theorem OAI.Erdos970.WeightedTorusJets.logDeriv_GammaR_add line 315
  20. theorem OAI.Erdos970.WeightedTorusJets.gammaFactor_logDeriv_real_parity line 342
  21. theorem OAI.Erdos970.WeightedTorusJets.conductor_gamma_correction_real line 362
  22. theorem OAI.Erdos970.WeightedTorusJets.exists_bound_gammaFactor_logDeriv line 374
  23. theorem OAI.Erdos970.WeightedTorusJets.exists_upper_bound_conductor_gammaFactor_logDeriv line 394
  24. lemma OAI.Erdos970.WeightedTorusJets.riemannZeta₁_ne_zero_of_one_le_re line 420
  25. lemma OAI.Erdos970.WeightedTorusJets.logDeriv_riemannZeta₁ line 429
  26. theorem OAI.Erdos970.WeightedTorusJets.exists_bound_zeta_logDeriv line 438
  27. theorem OAI.Erdos970.WeightedTorusJets.exists_upper_bound_zeta_logDeriv_re line 457
  28. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_logDeriv_decomposition line 475
  29. theorem OAI.Erdos970.WeightedTorusJets.logDeriv_upper_of_completedL_lower line 508