OAI/NumberTheory/Jacobsthal/Siegel/SumCharacterPeriodZero.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.sum_character_period_eq_zero line 20
  2. theorem OAI.Erdos970.WeightedTorusJets.norm_sum_character_range_lt line 35
  3. theorem OAI.Erdos970.WeightedTorusJets.norm_sum_character_Icc_lt line 52
  4. theorem OAI.Erdos970.WeightedTorusJets.isBigO_sum_character_Icc_one line 61
  5. theorem OAI.Erdos970.WeightedTorusJets.mellin_partial_sum_neg line 69
  6. theorem OAI.Erdos970.WeightedTorusJets.differentiableAt_partial_sum_integral line 86
  7. theorem OAI.Erdos970.WeightedTorusJets.LFunction_eq_partial_sum_integral line 122
  8. theorem OAI.Erdos970.WeightedTorusJets.LFunction_eq_partial_sum_integral_of_re_pos line 138
  9. theorem OAI.Erdos970.WeightedTorusJets.integrableOn_min_mul_rpow line 171
  10. theorem OAI.Erdos970.WeightedTorusJets.integral_min_mul_rpow_exact line 183
  11. theorem OAI.Erdos970.WeightedTorusJets.integral_min_mul_rpow_le line 228
  12. theorem OAI.Erdos970.WeightedTorusJets.norm_sum_character_Icc_le_min line 263
  13. theorem OAI.Erdos970.WeightedTorusJets.norm_LFunction_le_rpow_near_one line 275
  14. theorem OAI.Erdos970.WeightedTorusJets.LFunction_uniform_closedBall_bound line 301
  15. theorem OAI.Erdos970.WeightedTorusJets.one_le_zeta_mul_LFunction line 331
  16. theorem OAI.Erdos970.WeightedTorusJets.riemannZeta_re_eq_tsum_rpow line 351
  17. theorem OAI.Erdos970.WeightedTorusJets.riemannZeta_re_le_one_add_inv line 362
  18. theorem OAI.Erdos970.WeightedTorusJets.one_div_zeta_re_le_LFunction_re line 385
  19. theorem OAI.Erdos970.WeightedTorusJets.half_mul_le_LFunction_one_add_re line 393
  20. theorem OAI.Erdos970.RealCharacterAnalysis.lFunction_positive_of_one_lt line 430
  21. theorem OAI.Erdos970.RealCharacterAnalysis.lFunction_positive_at_one line 439
  22. theorem OAI.Erdos970.WeightedTorusJets.real_character_LFunction_eq_real_part line 456
  23. theorem OAI.Erdos970.WeightedTorusJets.real_character_LFunction_one_re_pos line 465
  24. theorem OAI.Erdos970.WeightedTorusJets.real_character_LFunction_re_zero_iff line 472
  25. theorem OAI.Erdos970.WeightedTorusJets.norm_second_deriv_le_of_closedBall line 493
  26. theorem OAI.Erdos970.WeightedTorusJets.real_deriv_eq_re_complex_deriv line 511
  27. theorem OAI.Erdos970.WeightedTorusJets.differentiable_real_restriction line 516
  28. theorem OAI.Erdos970.WeightedTorusJets.differentiable_deriv_real_restriction line 521
  29. theorem OAI.Erdos970.WeightedTorusJets.real_second_deriv_eq_re_complex_second_deriv line 526
  30. theorem OAI.Erdos970.WeightedTorusJets.abs_real_second_deriv_le_of_closedBall line 533
  31. theorem OAI.Erdos970.WeightedTorusJets.siegel_parameter_selection line 551
  32. theorem OAI.Erdos970.WeightedTorusJets.value_one_lower_bound_of_real_zero_gap line 614
  33. theorem OAI.Erdos970.WeightedTorusJets.siegel_LFunction_one_lower_bound_of_zero_gap line 660
  34. theorem OAI.Erdos970.WeightedTorusJets.siegel_LFunction_one_lower_bound line 715