OAI/NumberTheory/PrimePackets/ZetaDerivatives.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PrimeDegreePackets.residue_upper_reciprocal_of_deriv line 58
  2. theorem OAI.PrimeDegreePackets.uniform_zeta_scale_of_large_discr_deriv line 89
  3. lemma OAI.PrimeDegreePackets.realDedekindZeta_differentiableAt line 182
  4. lemma OAI.PrimeDegreePackets.realDedekindZeta_deriv_nonpos line 189
  5. lemma OAI.PrimeDegreePackets.realDedekindZeta_pos line 197
  6. lemma OAI.PrimeDegreePackets.logRegularizedDedekindZeta_deriv line 201
  7. def OAI.PrimeDegreePackets.archimedeanZetaTerm line 221
  8. lemma OAI.PrimeDegreePackets.complex_digamma_continuousAt_of_re_pos line 224
  9. lemma OAI.PrimeDegreePackets.archimedeanZetaTerm_continuousOn line 240
  10. lemma OAI.PrimeDegreePackets.archimedeanZetaTerm_bounded line 257
  11. theorem OAI.PrimeDegreePackets.logRegularized_deriv_bound_of_zero_sum line 267
  12. theorem OAI.PrimeDegreePackets.haar_barycenter line 339
  13. theorem OAI.PrimeDegreePackets.measure_eq_haar_of_condExpKernel_invariance line 352
  14. lemma OAI.PrimeDegreePackets.mem_thickLattices_iff line 377
  15. lemma OAI.PrimeDegreePackets.exists_mem_thickLattices line 402
  16. lemma OAI.PrimeDegreePackets.exists_mem_countable_thickLattices line 421
  17. def OAI.PrimeDegreePackets.coordinateContractionWeights line 433
  18. lemma OAI.PrimeDegreePackets.coordinateContractionWeights_sum line 436
  19. lemma OAI.PrimeDegreePackets.coordinateContraction_vector line 440
  20. lemma OAI.PrimeDegreePackets.no_coordinate_zero_of_recurrence line 451
  21. theorem OAI.PrimeDegreePackets.ae_no_coordinate_zero line 482