OAI/NumberTheory/DirichletL/LogarithmicControl.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.LogarithmicControl.differentiableOn_of_exp_eq line 18
  2. theorem OAI.SevenEighths.LogarithmicControl.exists_holomorphic_log line 37
  3. theorem OAI.SevenEighths.LogarithmicControl.exists_holomorphic_log_normalized line 52
  4. theorem OAI.SevenEighths.LogarithmicControl.log_eqOn_of_eq_center line 66
  5. theorem OAI.SevenEighths.LogarithmicControl.borel_caratheodory_closedBall line 87
  6. theorem OAI.SevenEighths.LogarithmicControl.three_circles line 109
  7. theorem OAI.SevenEighths.LogarithmicControl.three_circles_power_bound line 162
  8. def OAI.SevenEighths.LogarithmicControl.uniformTheta line 208
  9. theorem OAI.SevenEighths.LogarithmicControl.uniformTheta_mem line 210
  10. theorem OAI.SevenEighths.LogarithmicControl.three_circles_exponent_uniform line 221
  11. theorem OAI.SevenEighths.LogarithmicControl.exp_sublinear_le line 263
  12. def OAI.SevenEighths.LogarithmicControl.outerConstant line 294
  13. theorem OAI.SevenEighths.LogarithmicControl.outerConstant_ge_one line 296
  14. theorem OAI.SevenEighths.LogarithmicControl.outer_log_bound line 302
  15. theorem OAI.SevenEighths.LogarithmicControl.inner_log_bound line 330
  16. theorem OAI.SevenEighths.LogarithmicControl.logarithm_derivative_bound line 351
  17. theorem OAI.SevenEighths.LogarithmicControl.zero_free_disk_logarithm line 375
  18. theorem OAI.SevenEighths.LogarithmicControl.logarithmic_derivative_eq line 405
  19. theorem OAI.SevenEighths.LogarithmicControl.logarithmic_control line 419
  20. theorem OAI.SevenEighths.LogarithmicControl.conductor_height_scale_ge_exp line 467
  21. theorem OAI.SevenEighths.LogarithmicControl.absorb_polynomial_constant line 473
  22. theorem OAI.SevenEighths.LogarithmicControl.disk_re_gt line 498
  23. theorem OAI.SevenEighths.LogarithmicControl.same_height_mem_disk line 510
  24. theorem OAI.SevenEighths.LogarithmicControl.principal_regularizer_norm_le_one line 520
  25. theorem OAI.SevenEighths.LogarithmicControl.principal_reciprocal_transfer line 530