OAI/NumberTheory/DirichletL/CubicSieve/CutoffOrders.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.exists_polynomial_cutoff_order line 78
  2. theorem OAI.SecondPassArithmetic.canonicalFirstTail_reopening_order line 96
  3. theorem OAI.SecondPassArithmetic.reopening_terminal_order line 118
  4. theorem OAI.CanonicalUnitEuler.sixth_roots_reduce_injective line 139
  5. lemma OAI.CanonicalUnitEuler.unit_pow_six line 160
  6. theorem OAI.CanonicalUnitEuler.actualSextic_unit_euler line 165
  7. lemma OAI.CubicEisenstein.kernel_mass_le_weighted_mass_add_core line 196
  8. lemma OAI.CubicEisenstein.kernel_compact_coercivity_extend line 222
  9. lemma OAI.CubicEisenstein.kernel_barrier_coercivity_of_ground_state line 235
  10. theorem OAI.CubicEisenstein.ground_state_test_fderiv line 257
  11. theorem OAI.CubicEisenstein.ground_state_fderiv_inequality line 283
  12. def OAI.CubicEisenstein.kernelGroundStateTest line 297
  13. theorem OAI.CubicEisenstein.kernelGroundStateTest_apply line 310
  14. theorem OAI.CubicEisenstein.kernelGroundStateTest_tsupport line 315
  15. def OAI.CubicEisenstein.kernelTruncatedWeight line 325
  16. theorem OAI.CubicEisenstein.kernelTruncatedWeight_apply line 335
  17. theorem OAI.CubicEisenstein.kernelRealLift_contDiffAt line 340
  18. theorem OAI.CubicEisenstein.kernelEuclideanProjection_continuousAt line 347
  19. theorem OAI.CubicEisenstein.kernelTruncatedWeight_field_eq line 352
  20. theorem OAI.CubicEisenstein.kernelTruncatedPotential_memLp line 365
  21. theorem OAI.CubicEisenstein.ground_state_ofReal_fderiv line 380
  22. theorem OAI.CubicEisenstein.ground_state_self_product line 387
  23. theorem OAI.CubicEisenstein.kernelEnergyDensity_euclidean line 392
  24. theorem OAI.CubicEisenstein.kernelGroundState_pair_le_at line 402
  25. theorem OAI.CubicEisenstein.kernelGroundState_pair_le line 438
  26. theorem OAI.CubicEisenstein.kernel_ground_state_inequality line 460
  27. theorem OAI.CubicEisenstein.kernel_actual_barrier_ground_state line 517
  28. theorem OAI.CubicEisenstein.kernel_global_exterior_coercivity line 526
  29. theorem OAI.SecondPassArithmetic.lowerCubeBin_mass_product line 537
  30. theorem OAI.SecondPassArithmetic.canonicalBudget_sqrt_product line 548
  31. theorem OAI.SecondPassArithmetic.canonicalPairBudget_normalized line 562