OAI/NumberTheory/DirichletL/Descent/FirstChildWindowsCells.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.InverseMomentFirstChildWindows.SourceIndex line 14
  2. def OAI.SevenEighths.InverseMomentFirstChildWindows.sourceNorms line 16
  3. def OAI.SevenEighths.InverseMomentFirstChildWindows.sourceIndex line 19
  4. def OAI.SevenEighths.InverseMomentFirstChildWindows.sourceKeys line 20
  5. def OAI.SevenEighths.InverseMomentFirstChildWindows.sourceCell line 21
  6. def OAI.SevenEighths.InverseMomentFirstChildWindows.commonKeys line 24
  7. def OAI.SevenEighths.InverseMomentFirstChildWindows.commonSelector line 27
  8. def OAI.SevenEighths.InverseMomentFirstChildWindows.rawScales line 30
  9. lemma OAI.SevenEighths.InverseMomentFirstChildWindows.rawScales_pos line 34
  10. lemma OAI.SevenEighths.InverseMomentFirstChildWindows.sourceNorms_ge_one line 39
  11. lemma OAI.SevenEighths.InverseMomentFirstChildWindows.sourceCell_ratios line 51
  12. theorem OAI.SevenEighths.InverseMomentFirstChildWindows.actual_original_cell_ratios line 61
  13. lemma OAI.SevenEighths.InverseMomentFirstChildWindows.sum_source_cells line 89
  14. lemma OAI.SevenEighths.InverseMomentFirstChildWindows.common_key_of_index line 94
  15. lemma OAI.SevenEighths.InverseMomentFirstChildWindows.sum_common_cells line 100
  16. theorem OAI.SevenEighths.InverseMomentFirstChildWindows.original_signed_partition line 110