OAI/NumberTheory/DirichletL/RowCompletion/DensityTransfer.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalRowCompletion.canonicalShortState_from_certificate line 88
  2. theorem OAI.CanonicalRowCompletion.canonicalLog_actual_step line 149
  3. theorem OAI.CanonicalRowCompletion.outsideLogEnergy_finite_rank line 256
  4. def OAI.CanonicalRowCompletion.canonicalDescentPadding line 374
  5. theorem OAI.CanonicalRowCompletion.canonicalDescentPadding_budget line 376
  6. theorem OAI.CanonicalRowCompletion.outsideLogEnergy_state_small_power line 386
  7. theorem OAI.CanonicalRowCompletion.outsideLogEnergy_small_power line 418
  8. theorem OAI.CanonicalRowCompletion.initialCanonicalState line 453
  9. theorem OAI.CanonicalRowCompletion.canonicalInitialThreshold line 501
  10. theorem OAI.SecondPassIntegration.densityChildEnergy_from_canonical_heights line 524
  11. theorem OAI.QuadraticAllOddCRT.quadratic_ray_cross line 567
  12. theorem OAI.QuadraticAllOddCRT.quadraticRayValue_ne_zero_of_odd line 603