OAI/NumberTheory/SiegelZeros/Characters/RealLogDerivConductorCompletedLDivisorTsum.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.real_logDeriv_conductorCompletedL_eq_divisor_tsum line 26
  2. theorem OAI.SiegelZeros.WeightedTorusJets.abs_reciprocal_sub_re_le_normSq line 59
  3. theorem OAI.SiegelZeros.WeightedTorusJets.abs_reciprocal_re_le_normSq line 99
  4. theorem OAI.SiegelZeros.WeightedTorusJets.summable_abs_reciprocal_sub_re line 106
  5. theorem OAI.SiegelZeros.WeightedTorusJets.summable_abs_reciprocal_re line 118
  6. theorem OAI.SiegelZeros.WeightedTorusJets.divisorZeroIndex_val_zero line 131
  7. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_divisorIndex_re_mem_Ioo line 140
  8. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_abs_reciprocal_summable line 148
  9. theorem OAI.SiegelZeros.WeightedTorusJets.exists_divisorZeroIndex_val_eq_of_zero line 161
  10. theorem OAI.SiegelZeros.WeightedTorusJets.real_zero_le_divisor_reciprocal_tsum line 174
  11. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_zero_sum_absolutely_summable line 206
  12. theorem OAI.SiegelZeros.WeightedTorusJets.real_logDeriv_conductorCompletedL_eq_divisor_tsum_source line 214
  13. theorem OAI.SiegelZeros.WeightedTorusJets.real_zero_le_conductorCompletedL_logDeriv line 227
  14. lemma OAI.SiegelZeros.WeightedTorusJets.analyticAt_Gamma_of_re_pos line 243
  15. theorem OAI.SiegelZeros.WeightedTorusJets.exists_bound_Gamma_logDeriv_parity line 256
  16. theorem OAI.SiegelZeros.WeightedTorusJets.character_parity_parameter line 279
  17. theorem OAI.SiegelZeros.WeightedTorusJets.character_parity_parameter_real line 285
  18. theorem OAI.SiegelZeros.WeightedTorusJets.character_gamma_argument_mem_Icc line 291
  19. theorem OAI.SiegelZeros.WeightedTorusJets.logDeriv_GammaR_add line 301
  20. theorem OAI.SiegelZeros.WeightedTorusJets.gammaFactor_logDeriv_real_parity line 328
  21. theorem OAI.SiegelZeros.WeightedTorusJets.conductor_gamma_correction_real line 348
  22. theorem OAI.SiegelZeros.WeightedTorusJets.exists_bound_gammaFactor_logDeriv line 360
  23. theorem OAI.SiegelZeros.WeightedTorusJets.exists_upper_bound_conductor_gammaFactor_logDeriv line 380
  24. lemma OAI.SiegelZeros.WeightedTorusJets.riemannZeta₁_ne_zero_of_one_le_re line 400
  25. lemma OAI.SiegelZeros.WeightedTorusJets.logDeriv_riemannZeta₁ line 409
  26. theorem OAI.SiegelZeros.WeightedTorusJets.exists_bound_zeta_logDeriv line 418
  27. theorem OAI.SiegelZeros.WeightedTorusJets.exists_upper_bound_zeta_logDeriv_re line 437
  28. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_logDeriv_decomposition line 452
  29. theorem OAI.SiegelZeros.WeightedTorusJets.logDeriv_upper_of_completedL_lower line 485