OAI/NumberTheory/DirichletL/Moments/DetectorPlainMarkedState.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMarkedState.source_slot_coefficient line 27
  2. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMarkedState.retained_eq_initial_energy line 40
  3. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMarkedState.plain_length_eq line 74
  4. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMarkedState.marked_capacity line 81
  5. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMarkedState.selected_widths line 89
  6. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMarkedState.source_profile_uniform line 95
  7. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMarkedState.source_relative_fixed_gates line 102
  8. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMarkedState.fixed_window_data line 109
  9. theorem OAI.SevenEighths.CenteredMomentDetectorPlainMarkedState.source_batch_marked_initial line 119