OAI/NumberTheory/DirichletL/Moments/ActiveSource.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentActiveSource.activeSource line 13
  2. theorem OAI.SevenEighths.CenteredMomentActiveSource.mem_activeSource line 16
  3. theorem OAI.SevenEighths.CenteredMomentActiveSource.supportedColumns_active line 19
  4. theorem OAI.SevenEighths.CenteredMomentActiveSource.active_sum line 25
  5. theorem OAI.SevenEighths.CenteredMomentActiveSource.sourceGaussEnergy_active line 33
  6. def OAI.SevenEighths.CenteredMomentActiveSource.retainedKernel line 46
  7. theorem OAI.SevenEighths.CenteredMomentActiveSource.secondRetainedEnergy_eq_sum line 50
  8. theorem OAI.SevenEighths.CenteredMomentActiveSource.secondRetainedEnergy_active line 67
  9. theorem OAI.SevenEighths.CenteredMomentActiveSource.commonLabel_witnesses line 82
  10. theorem OAI.SevenEighths.CenteredMomentActiveSource.commonLabel_norm_bounds line 95
  11. theorem OAI.SevenEighths.CenteredMomentActiveSource.residualPool_data line 107
  12. theorem OAI.SevenEighths.CenteredMomentActiveSource.source_energy_active_sectors line 124