OAI/NumberTheory/DirichletL/Inversion/SecondSourceBlocks.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.InverseSecondSourceBlocks.BlockIndex line 15
  2. def OAI.SevenEighths.InverseSecondSourceBlocks.outerNorms line 17
  3. theorem OAI.SevenEighths.InverseSecondSourceBlocks.outerNorms_eq_actual line 21
  4. theorem OAI.SevenEighths.InverseSecondSourceBlocks.outerNorms_ge_one line 30
  5. theorem OAI.SevenEighths.InverseSecondSourceBlocks.frequency_ne_zero_of_gate line 41
  6. theorem OAI.SevenEighths.InverseSecondSourceBlocks.retained_frequency_ne_zero line 45
  7. def OAI.SevenEighths.InverseSecondSourceBlocks.dyadIndex line 53
  8. def OAI.SevenEighths.InverseSecondSourceBlocks.dyadScale line 54
  9. theorem OAI.SevenEighths.InverseSecondSourceBlocks.dyadScale_pos line 56
  10. theorem OAI.SevenEighths.InverseSecondSourceBlocks.dyadIndex_bounds line 58
  11. def OAI.SevenEighths.InverseSecondSourceBlocks.index line 72
  12. def OAI.SevenEighths.InverseSecondSourceBlocks.keys line 75
  13. def OAI.SevenEighths.InverseSecondSourceBlocks.cell line 78
  14. theorem OAI.SevenEighths.InverseSecondSourceBlocks.mem_cell line 82
  15. theorem OAI.SevenEighths.InverseSecondSourceBlocks.cell_subset line 87
  16. theorem OAI.SevenEighths.InverseSecondSourceBlocks.cell_inherits line 91
  17. theorem OAI.SevenEighths.InverseSecondSourceBlocks.cell_conditions line 95
  18. theorem OAI.SevenEighths.InverseSecondSourceBlocks.mem_keys_iff line 100
  19. theorem OAI.SevenEighths.InverseSecondSourceBlocks.cells_disjoint line 111
  20. theorem OAI.SevenEighths.InverseSecondSourceBlocks.cell_ratios line 118
  21. theorem OAI.SevenEighths.InverseSecondSourceBlocks.sum_cells line 131
  22. def OAI.SevenEighths.InverseSecondSourceBlocks.scales line 136
  23. theorem OAI.SevenEighths.InverseSecondSourceBlocks.actual_cell_ratios line 138
  24. theorem OAI.SevenEighths.InverseSecondSourceBlocks.physical_source_partition line 150
  25. def OAI.SevenEighths.InverseSecondSourceBlocks.capBox line 174
  26. theorem OAI.SevenEighths.InverseSecondSourceBlocks.keys_subset_capBox line 178
  27. theorem OAI.SevenEighths.InverseSecondSourceBlocks.keys_card_le_product line 193
  28. def OAI.SevenEighths.InverseSecondSourceBlocks.capConstant line 201
  29. theorem OAI.SevenEighths.InverseSecondSourceBlocks.capConstant_nonneg line 203
  30. theorem OAI.SevenEighths.InverseSecondSourceBlocks.cap_bin_bound line 208
  31. theorem OAI.SevenEighths.InverseSecondSourceBlocks.keys_card_polynomial line 225
  32. theorem OAI.SevenEighths.InverseSecondSourceBlocks.keys_empty line 244
  33. theorem OAI.SevenEighths.InverseSecondSourceBlocks.cell_empty line 248
  34. theorem OAI.SevenEighths.InverseSecondSourceBlocks.cell_empty_of_not_mem line 252
  35. theorem OAI.SevenEighths.InverseSecondSourceBlocks.retained_cell_ratios line 257
  36. theorem OAI.SevenEighths.InverseSecondSourceBlocks.retained_keys_card_polynomial line 272