OAI/NumberTheory/DirichletL/Inversion/FirstGlobalCaps.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseFirstGlobalCaps.outerNorms line 20
  2. def OAI.SevenEighths.InverseFirstGlobalCaps.outerGate line 28
  3. def OAI.SevenEighths.InverseFirstGlobalCaps.outerCell line 31
  4. def OAI.SevenEighths.InverseFirstGlobalCaps.parentCell line 34
  5. theorem OAI.SevenEighths.InverseFirstGlobalCaps.mem_parentCell line 39
  6. def OAI.SevenEighths.InverseFirstGlobalCaps.originalNorms line 51
  7. lemma OAI.SevenEighths.InverseFirstGlobalCaps.originalNorms_outer line 57
  8. lemma OAI.SevenEighths.InverseFirstGlobalCaps.originalNorms_frequency line 61
  9. theorem OAI.SevenEighths.InverseFirstGlobalCaps.sourceCell_outer line 64
  10. lemma OAI.SevenEighths.InverseFirstGlobalCaps.outerNorms_ge_one line 79
  11. lemma OAI.SevenEighths.InverseFirstGlobalCaps.source_norms_ge_one line 92
  12. theorem OAI.SevenEighths.InverseFirstGlobalCaps.sourceCell_frequency line 110
  13. lemma OAI.SevenEighths.InverseFirstGlobalCaps.outerGate_dyads line 123
  14. lemma OAI.SevenEighths.InverseFirstGlobalCaps.commonSelector_norm line 132
  15. lemma OAI.SevenEighths.InverseFirstGlobalCaps.live_common_dyads line 139
  16. lemma OAI.SevenEighths.InverseFirstGlobalCaps.sourceIdeal_norm line 150
  17. theorem OAI.SevenEighths.InverseFirstGlobalCaps.parentCell_cube_bounds line 155
  18. def OAI.SevenEighths.InverseFirstGlobalCaps.dyadicExponent line 166
  19. lemma OAI.SevenEighths.InverseFirstGlobalCaps.rpow_dyadicExponent line 168
  20. lemma OAI.SevenEighths.InverseFirstGlobalCaps.dyad_power_bounds line 172
  21. theorem OAI.SevenEighths.InverseFirstGlobalCaps.parentCell_norm_bounds line 181
  22. theorem OAI.SevenEighths.InverseFirstGlobalCaps.parentCell_ideal_bounds line 202
  23. def OAI.SevenEighths.InverseFirstGlobalCaps.jNorm line 220
  24. def OAI.SevenEighths.InverseFirstGlobalCaps.labelParentCell line 224
  25. theorem OAI.SevenEighths.InverseFirstGlobalCaps.labelParentCell_bounds line 230
  26. theorem OAI.SevenEighths.InverseFirstGlobalCaps.raw_column_exponent line 244
  27. theorem OAI.SevenEighths.InverseFirstGlobalCaps.columnScales_exponents line 250
  28. theorem OAI.SevenEighths.InverseFirstGlobalCaps.columnScales_products line 256
  29. theorem OAI.SevenEighths.InverseFirstGlobalCaps.sourceCell_parent line 261
  30. theorem OAI.SevenEighths.InverseFirstGlobalCaps.outerCell_eq_of_first_five line 272
  31. lemma OAI.SevenEighths.InverseFirstGlobalCaps.live_selector_norm_le_one line 279
  32. theorem OAI.SevenEighths.InverseFirstGlobalCaps.sourceCell_actual_ratios line 285