OAI/NumberTheory/PrimePackets/RootOverlaps.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.RootBox.overlapBox line 73
  2. lemma OAI.PrimeDegreePackets.RootBox.overlapBox_domain_subset line 78
  3. lemma OAI.PrimeDegreePackets.RootBox.overlapBox_translate_domain_subset line 81
  4. theorem OAI.PrimeDegreePackets.RootBox.mass_translate_on_overlap line 88
  5. theorem OAI.PrimeDegreePackets.RootBox.local_mass_translate_of_endpoints line 127
  6. theorem OAI.PrimeDegreePackets.root_invariant_of_haar_conditionals line 145
  7. theorem OAI.PrimeDegreePackets.full_invariance_of_haar_conditionals line 169
  8. theorem OAI.PrimeDegreePackets.measure_eq_haar_of_haar_conditionals line 180
  9. lemma OAI.PrimeDegreePackets.complex_summable_fintype_prod line 196
  10. lemma OAI.PrimeDegreePackets.complex_tsum_fintype_prod line 206
  11. lemma OAI.PrimeDegreePackets.complex_tsum_multiset_prod line 236
  12. lemma OAI.PrimeDegreePackets.zetaSummand_norm_lt_one line 270
  13. lemma OAI.PrimeDegreePackets.primary_ideal_complex_series line 280
  14. lemma OAI.PrimeDegreePackets.norm_fiber_complex_tsum line 308
  15. lemma OAI.PrimeDegreePackets.primary_ideal_tsum_by_norm line 320
  16. lemma OAI.PrimeDegreePackets.ideal_local_complex_euler line 335
  17. lemma OAI.PrimeDegreePackets.primePower_succ_injective line 348
  18. theorem OAI.PrimeDegreePackets.complex_multiplicative_tsum_ne_zero line 356
  19. lemma OAI.PrimeDegreePackets.dedekindZeta_ne_zero_of_one_lt_re line 390
  20. lemma OAI.PrimeDegreePackets.dedekindZeta_analyticAt_of_one_lt_re line 427
  21. lemma OAI.PrimeDegreePackets.dedekindZeta_logDeriv_analyticAt_of_one_lt_re line 436
  22. def OAI.PrimeDegreePackets.completionExponential line 449
  23. def OAI.PrimeDegreePackets.totallyRealCompletedXi line 453
  24. lemma OAI.PrimeDegreePackets.half_ne_nonpositive_integer line 458
  25. lemma OAI.PrimeDegreePackets.completionExponential_ne_zero line 466
  26. lemma OAI.PrimeDegreePackets.completionExponential_hasDerivAt line 469
  27. lemma OAI.PrimeDegreePackets.completionExponential_logDeriv line 481
  28. lemma OAI.PrimeDegreePackets.gammaHalf_hasDerivAt line 487
  29. lemma OAI.PrimeDegreePackets.gammaHalf_logDeriv line 495
  30. lemma OAI.PrimeDegreePackets.totallyRealCompletedXi_ne_zero line 501
  31. lemma OAI.PrimeDegreePackets.totallyRealCompletedXi_differentiableAt line 514
  32. lemma OAI.PrimeDegreePackets.totallyRealCompletedXi_logDeriv line 521
  33. lemma OAI.PrimeDegreePackets.completionExponential_eq_cpow line 569
  34. lemma OAI.PrimeDegreePackets.totallyRealCompletedXi_eq_GammaReal line 582
  35. lemma OAI.PrimeDegreePackets.totallyRealCompletedXi_analyticAt line 592
  36. lemma OAI.PrimeDegreePackets.dedekindZeta_ofReal line 601
  37. lemma OAI.PrimeDegreePackets.dedekindZeta_logDeriv_re line 606
  38. lemma OAI.PrimeDegreePackets.totallyRealCompletedXi_logDeriv_re line 618