OAI/NumberTheory/SiegelZeros/Selection/SelectionBridge.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.W29.rowSpan line 28
  2. def OAI.SiegelZeros.WeightedTorusJets.W29.insertIfIndependent line 31
  3. def OAI.SiegelZeros.WeightedTorusJets.W29.processed line 34
  4. def OAI.SiegelZeros.WeightedTorusJets.W29.retained line 37
  5. lemma OAI.SiegelZeros.WeightedTorusJets.W29.rowSpan_insert line 41
  6. lemma OAI.SiegelZeros.WeightedTorusJets.W29.insertIfIndependent_span line 45
  7. lemma OAI.SiegelZeros.WeightedTorusJets.W29.insertIfIndependent_independent line 56
  8. lemma OAI.SiegelZeros.WeightedTorusJets.W29.insertIfIndependent_subset line 65
  9. lemma OAI.SiegelZeros.WeightedTorusJets.W29.processed_zero line 73
  10. lemma OAI.SiegelZeros.WeightedTorusJets.W29.processed_succ line 76
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W29.retained_subset_processed line 80
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W29.retained_independent line 88
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W29.retained_span line 94
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W29.earlier_row_mem_retained_span line 103
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W29.retained_weight_bound line 111
  16. theorem OAI.SiegelZeros.WeightedTorusJets.W29.cutoff_mem_retained_span line 120
  17. abbrev OAI.SiegelZeros.SiegelZerosAwei.W31.MultiIndex line 134
  18. def OAI.SiegelZeros.SiegelZerosAwei.W31.weight line 136
  19. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.scale_identity line 139
  20. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.rectangle_weight_le line 145
  21. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.short_coordinate_sum_le line 161
  22. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.short_coordinates_le line 174
  23. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.short_sum_le_96 line 183
  24. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.short_sum_le_192 line 192
  25. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.pivot_S2_bound line 202
  26. lemma OAI.SiegelZeros.WeightedTorusJets.W29.subset_insertIfIndependent line 226
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W29.retained_monotone line 234
  28. lemma OAI.SiegelZeros.WeightedTorusJets.W29.not_mem_of_row_not_mem_span line 241
  29. theorem OAI.SiegelZeros.WeightedTorusJets.W29.retained_card_succ line 247
  30. theorem OAI.SiegelZeros.WeightedTorusJets.W29.retained_succ_of_dependent line 259
  31. theorem OAI.SiegelZeros.WeightedTorusJets.W29.retained_succ_of_independent line 266
  32. def OAI.SiegelZeros.WeightedTorusJets.W29.finiteEnumeration line 285
  33. lemma OAI.SiegelZeros.WeightedTorusJets.W29.finiteEnumeration_mem line 288
  34. lemma OAI.SiegelZeros.WeightedTorusJets.W29.finiteEnumeration_complete line 293
  35. theorem OAI.SiegelZeros.WeightedTorusJets.W29.finiteEnumeration_strictMono line 300
  36. theorem OAI.SiegelZeros.WeightedTorusJets.W29.finiteEnumeration_weight_mono line 307
  37. theorem OAI.SiegelZeros.WeightedTorusJets.W29.processed_finiteEnumeration line 315
  38. def OAI.SiegelZeros.WeightedTorusJets.W29.finiteSelection line 326
  39. theorem OAI.SiegelZeros.WeightedTorusJets.W29.finiteSelection_independent line 329
  40. theorem OAI.SiegelZeros.WeightedTorusJets.W29.finiteSelection_span line 333
  41. theorem OAI.SiegelZeros.WeightedTorusJets.W29.finiteSelection_subset line 338
  42. theorem OAI.SiegelZeros.WeightedTorusJets.W29.finiteSelection_span_top line 343
  43. theorem OAI.SiegelZeros.WeightedTorusJets.W29.retained_prefix_subset_earlier line 359
  44. theorem OAI.SiegelZeros.WeightedTorusJets.W29.earlier_row_mem_final_earlier_span line 374
  45. theorem OAI.SiegelZeros.WeightedTorusJets.W29.lower_index_mem_selected_span line 388
  46. structure OAI.SiegelZeros.WeightedTorusJets.W62.Index line 412
  47. def OAI.SiegelZeros.WeightedTorusJets.W62.weight line 416
  48. def OAI.SiegelZeros.WeightedTorusJets.W62.key line 419
  49. theorem OAI.SiegelZeros.WeightedTorusJets.W62.key_injective line 422
  50. instance OAI.SiegelZeros.WeightedTorusJets.W62.(instance at line 440) line 440
  51. theorem OAI.SiegelZeros.WeightedTorusJets.W62.lt_of_weight_lt line 442
  52. theorem OAI.SiegelZeros.WeightedTorusJets.W62.weight_monotone line 446
  53. theorem OAI.SiegelZeros.WeightedTorusJets.W62.coordinate_le_weight line 451
  54. def OAI.SiegelZeros.WeightedTorusJets.W62.cutoff line 464
  55. theorem OAI.SiegelZeros.WeightedTorusJets.W62.mem_cutoff line 468
  56. def OAI.SiegelZeros.WeightedTorusJets.W62.zeroIndex line 482
  57. def OAI.SiegelZeros.WeightedTorusJets.W62.enumeration line 484
  58. theorem OAI.SiegelZeros.WeightedTorusJets.W62.enumeration_weight_le line 487
  59. theorem OAI.SiegelZeros.WeightedTorusJets.W62.enumeration_complete line 491
  60. theorem OAI.SiegelZeros.WeightedTorusJets.W62.enumeration_strictMono line 496
  61. theorem OAI.SiegelZeros.WeightedTorusJets.W62.lower_weight_earlier line 500
  62. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.greedy_ordered_earlier_span line 527
  63. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.greedy_ordered_det_of_spanning line 539
  64. def OAI.SiegelZeros.WeightedTorusJets.W62.selected line 557
  65. theorem OAI.SiegelZeros.WeightedTorusJets.W62.selected_independent line 560
  66. theorem OAI.SiegelZeros.WeightedTorusJets.W62.selected_span line 564
  67. theorem OAI.SiegelZeros.WeightedTorusJets.W62.selected_weight_le line 569
  68. theorem OAI.SiegelZeros.WeightedTorusJets.W62.lower_weight_mem_earlier_span line 573
  69. theorem OAI.SiegelZeros.WeightedTorusJets.W62.selected_card_of_spanning line 585
  70. theorem OAI.SiegelZeros.WeightedTorusJets.W62.selected_det_ne_zero_of_spanning line 592
  71. theorem OAI.SiegelZeros.WeightedTorusJets.W62.real_weight_eq line 601
  72. theorem OAI.SiegelZeros.WeightedTorusJets.W62.coords_injective line 605
  73. def OAI.SiegelZeros.WeightedTorusJets.W62.selectedCoords line 612
  74. theorem OAI.SiegelZeros.WeightedTorusJets.W62.selectedCoords_card line 615
  75. theorem OAI.SiegelZeros.WeightedTorusJets.W62.selectedCoords_real_weight_le line 620
  76. theorem OAI.SiegelZeros.WeightedTorusJets.W62.selectedCoords_short_sum line 627