OAI/NumberTheory/SiegelZeros/Characters/SumCharacterPeriodZero.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.sum_character_period_eq_zero line 19
  2. theorem OAI.SiegelZeros.WeightedTorusJets.norm_sum_character_range_lt line 34
  3. theorem OAI.SiegelZeros.WeightedTorusJets.norm_sum_character_Icc_lt line 51
  4. theorem OAI.SiegelZeros.WeightedTorusJets.isBigO_sum_character_Icc_one line 60
  5. theorem OAI.SiegelZeros.WeightedTorusJets.mellin_partial_sum_neg line 68
  6. theorem OAI.SiegelZeros.WeightedTorusJets.differentiableAt_partial_sum_integral line 85
  7. theorem OAI.SiegelZeros.WeightedTorusJets.LFunction_eq_partial_sum_integral line 121
  8. theorem OAI.SiegelZeros.WeightedTorusJets.LFunction_eq_partial_sum_integral_of_re_pos line 137
  9. theorem OAI.SiegelZeros.WeightedTorusJets.integrableOn_min_mul_rpow line 170
  10. theorem OAI.SiegelZeros.WeightedTorusJets.integral_min_mul_rpow_exact line 182
  11. theorem OAI.SiegelZeros.WeightedTorusJets.integral_min_mul_rpow_le line 227
  12. theorem OAI.SiegelZeros.WeightedTorusJets.norm_sum_character_Icc_le_min line 262
  13. theorem OAI.SiegelZeros.WeightedTorusJets.norm_LFunction_le_rpow_near_one line 274
  14. theorem OAI.SiegelZeros.WeightedTorusJets.LFunction_uniform_closedBall_bound line 300
  15. theorem OAI.SiegelZeros.WeightedTorusJets.one_le_zeta_mul_LFunction line 330
  16. theorem OAI.SiegelZeros.WeightedTorusJets.riemannZeta_re_eq_tsum_rpow line 350
  17. theorem OAI.SiegelZeros.WeightedTorusJets.riemannZeta_re_le_one_add_inv line 361
  18. theorem OAI.SiegelZeros.WeightedTorusJets.one_div_zeta_re_le_LFunction_re line 384
  19. theorem OAI.SiegelZeros.WeightedTorusJets.half_mul_le_LFunction_one_add_re line 392
  20. theorem OAI.SiegelZeros.RealCharacterAnalysis.lFunction_positive_of_one_lt line 429
  21. theorem OAI.SiegelZeros.RealCharacterAnalysis.lFunction_positive_at_one line 438
  22. theorem OAI.SiegelZeros.WeightedTorusJets.real_character_LFunction_eq_real_part line 455
  23. theorem OAI.SiegelZeros.WeightedTorusJets.real_character_LFunction_one_re_pos line 464
  24. theorem OAI.SiegelZeros.WeightedTorusJets.real_character_LFunction_re_zero_iff line 471
  25. theorem OAI.SiegelZeros.WeightedTorusJets.norm_second_deriv_le_of_closedBall line 492
  26. theorem OAI.SiegelZeros.WeightedTorusJets.real_deriv_eq_re_complex_deriv line 510
  27. theorem OAI.SiegelZeros.WeightedTorusJets.differentiable_real_restriction line 515
  28. theorem OAI.SiegelZeros.WeightedTorusJets.differentiable_deriv_real_restriction line 520
  29. theorem OAI.SiegelZeros.WeightedTorusJets.real_second_deriv_eq_re_complex_second_deriv line 525
  30. theorem OAI.SiegelZeros.WeightedTorusJets.abs_real_second_deriv_le_of_closedBall line 532
  31. theorem OAI.SiegelZeros.WeightedTorusJets.siegel_parameter_selection line 550
  32. theorem OAI.SiegelZeros.WeightedTorusJets.value_one_lower_bound_of_real_zero_gap line 613
  33. theorem OAI.SiegelZeros.WeightedTorusJets.siegel_LFunction_one_lower_bound_of_zero_gap line 659
  34. theorem OAI.SiegelZeros.WeightedTorusJets.siegel_LFunction_one_lower_bound line 714