OAI/NumberTheory/DirichletL/Moments/DetectorPlainMomentParameters.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.delta line 20
  2. def OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.stageError line 21
  3. def OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.kappaPlain line 22
  4. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.fixed_parameters line 24
  5. lemma OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.source_base_gt_one line 39
  6. lemma OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.witness_length_cap line 43
  7. lemma OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.original_width_bounds line 46
  8. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.actual_fiber_lengths line 56
  9. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.batch_fiber_parameters line 67
  10. lemma OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.width_bands line 89
  11. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.marked_state_admission line 102
  12. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.unmarked_state_admission line 122
  13. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.source_label_fixed_allowance line 143
  14. lemma OAI.SevenEighths.CenteredMomentDetectorPlainMomentParameters.final_exponent_budget line 151