OAI/NumberTheory/SiegelZeros/Selection/WeightedJetIndices.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.weightedJetIndices line 19
  2. theorem OAI.SiegelZeros.WeightedTorusJets.mem_weightedJetIndices_iff line 23
  3. theorem OAI.SiegelZeros.WeightedTorusJets.extendFiniteFamily_injOn_range line 44
  4. def OAI.SiegelZeros.WeightedTorusJets.finiteGreedyPivots line 54
  5. theorem OAI.SiegelZeros.WeightedTorusJets.finiteGreedyPivots_spec line 61
  6. theorem OAI.SiegelZeros.WeightedTorusJets.finiteGreedyPivots_weighted_bounds line 105
  7. theorem OAI.SiegelZeros.WeightedTorusJets.row_space_finrank line 124
  8. theorem OAI.SiegelZeros.WeightedTorusJets.finiteGreedyPivots_sum line 128
  9. theorem OAI.SiegelZeros.WeightedTorusJets.sum_embedding_eq_sum_of_range line 141
  10. theorem OAI.SiegelZeros.WeightedTorusJets.weightedJetIndices_real_weight line 158
  11. theorem OAI.SiegelZeros.WeightedTorusJets.mem_weightedJetIndices_of_rectangle line 168
  12. theorem OAI.SiegelZeros.WeightedTorusJets.span_cutoff_eq_top_of_rectangle line 179
  13. theorem OAI.SiegelZeros.WeightedTorusJets.rectangle_span_yields_sorted_greedy_pivots line 197
  14. theorem OAI.SiegelZeros.WeightedTorusJets.det_ne_zero_of_linearIndepOn_rows line 232
  15. theorem OAI.SiegelZeros.WeightedTorusJets.span_rows_eq_top_of_detects line 243
  16. theorem OAI.SiegelZeros.WeightedTorusJets.detects_of_field_embedding line 257
  17. theorem OAI.SiegelZeros.WeightedTorusJets.finite_weighted_greedy_package line 274
  18. theorem OAI.SiegelZeros.WeightedTorusJets.rectangle_greedy_selection_package line 359
  19. theorem OAI.SiegelZeros.WeightedTorusJets.greedyPivots_filter_lt line 414
  20. theorem OAI.SiegelZeros.WeightedTorusJets.span_greedyPivots_eq_span_earlier_rows line 425
  21. theorem OAI.SiegelZeros.WeightedTorusJets.smaller_weight_mem_span_earlier_retained_rows line 451
  22. theorem OAI.SiegelZeros.WeightedTorusJets.jet_weight_ball_span_eq_top line 464