OAI/NumberTheory/DirichletL/RowCompletion/CubicReopening.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalRowCompletion.outside_pool_coprime_excluded line 86
  2. theorem OAI.CanonicalRowCompletion.cubeIdeal_eq_primeProduct_span line 102
  3. theorem OAI.CanonicalRowCompletion.cubeIdeal_primeProduct_norm line 112
  4. theorem OAI.CanonicalRowCompletion.progressingActiveBin_cube_bound line 118
  5. theorem OAI.CanonicalRowCompletion.progressingCanonicalBin_closed_step line 139
  6. def OAI.CanonicalUnitEuler.unitSupplement line 270
  7. lemma OAI.CanonicalUnitEuler.supported_good line 282
  8. lemma OAI.CanonicalUnitEuler.unitSupplement_norm line 288
  9. lemma OAI.CanonicalUnitEuler.norm_eval_residue line 294
  10. lemma OAI.CanonicalUnitEuler.norm_residue_congruent line 306
  11. lemma OAI.CanonicalUnitEuler.supported_span_congruent_mod_thirty_six line 327
  12. theorem OAI.CanonicalUnitEuler.unitSupplement_periodic line 342
  13. lemma OAI.CanonicalUnitEuler.rowTwist_zero_of_common_prime line 354
  14. theorem OAI.CanonicalUnitEuler.rowTwist_unitSupplement line 365
  15. theorem OAI.CanonicalUnitEuler.rowTwist_unitSupplement_base line 391
  16. theorem OAI.CanonicalUnitEuler.unitRowFamily_transport line 399
  17. theorem OAI.CanonicalUnitEuler.unitSupplement_mul_periodic line 407
  18. lemma OAI.CubicEisenstein.kernelBarrier_sublevel_isCompact line 422
  19. def OAI.CubicEisenstein.kernelExhaustionProfile line 442
  20. def OAI.CubicEisenstein.kernelExhaustionCutoff line 445
  21. lemma OAI.CubicEisenstein.kernelExhaustionProfile_smooth line 448
  22. lemma OAI.CubicEisenstein.kernelExhaustionCutoff_smooth line 453
  23. lemma OAI.CubicEisenstein.kernelExhaustionProfile_bounds line 458
  24. lemma OAI.CubicEisenstein.kernelExhaustionProfile_one line 465
  25. lemma OAI.CubicEisenstein.kernelExhaustionProfile_zero line 470
  26. lemma OAI.CubicEisenstein.kernelExhaustionCutoff_hasCompactSupport line 475
  27. lemma OAI.CubicEisenstein.kernelExhaustionCutoff_bounds line 484
  28. lemma OAI.CubicEisenstein.kernelExhaustionCutoff_eventually_one line 488
  29. lemma OAI.CubicEisenstein.kernelExhaustionCutoff_eventually_one_near line 496
  30. lemma OAI.CubicEisenstein.cuspTransition_euler_bounded line 512
  31. lemma OAI.CubicEisenstein.cuspRemainderProfile_contDiffAt line 525
  32. lemma OAI.CubicEisenstein.cuspRemainderProfile_euler line 529
  33. lemma OAI.CubicEisenstein.cuspRemainderProfile_euler_bound line 541
  34. lemma OAI.CubicEisenstein.cuspRemainderProfile_deriv_zero line 560
  35. lemma OAI.CubicEisenstein.rowLogD_hyperbolic_bound line 567
  36. lemma OAI.CubicEisenstein.cuspRemainder_row_scaled_deriv_bound line 580
  37. theorem OAI.CanonicalRowCompletion.progressingCanonicalFamily_closed_step line 610