OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/RetainedChoice.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryAnalyticCentering.retainedChoice line 27
  2. def OAI.OrdinaryAnalyticCentering.removedChoice line 28
  3. def OAI.OrdinaryAnalyticCentering.retainedSet line 29
  4. def OAI.OrdinaryAnalyticCentering.choiceFiber line 30
  5. def OAI.OrdinaryAnalyticCentering.shiftSet line 32
  6. def OAI.OrdinaryAnalyticCentering.fiberCoeff line 34
  7. def OAI.OrdinaryAnalyticCentering.fiberSum line 35
  8. lemma OAI.OrdinaryAnalyticCentering.choice_primes line 40
  9. lemma OAI.OrdinaryAnalyticCentering.fiber_reconstruct line 44
  10. lemma OAI.OrdinaryAnalyticCentering.fiber_removed_inj line 50
  11. lemma OAI.OrdinaryAnalyticCentering.sum_fiber_eq line 69
  12. lemma OAI.OrdinaryAnalyticCentering.regroup_centered line 89