OAI/NumberTheory/Jacobsthal/Siegel/WeightedJetIndices.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.weightedJetIndices line 21
  2. theorem OAI.Erdos970.WeightedTorusJets.mem_weightedJetIndices_iff line 25
  3. theorem OAI.Erdos970.WeightedTorusJets.extendFiniteFamily_injOn_range line 46
  4. def OAI.Erdos970.WeightedTorusJets.finiteGreedyPivots line 56
  5. theorem OAI.Erdos970.WeightedTorusJets.finiteGreedyPivots_spec line 63
  6. theorem OAI.Erdos970.WeightedTorusJets.finiteGreedyPivots_weighted_bounds line 107
  7. theorem OAI.Erdos970.WeightedTorusJets.row_space_finrank line 126
  8. theorem OAI.Erdos970.WeightedTorusJets.finiteGreedyPivots_sum line 130
  9. theorem OAI.Erdos970.WeightedTorusJets.sum_embedding_eq_sum_of_range line 143
  10. theorem OAI.Erdos970.WeightedTorusJets.weightedJetIndices_real_weight line 160
  11. theorem OAI.Erdos970.WeightedTorusJets.mem_weightedJetIndices_of_rectangle line 170
  12. theorem OAI.Erdos970.WeightedTorusJets.span_cutoff_eq_top_of_rectangle line 181
  13. theorem OAI.Erdos970.WeightedTorusJets.rectangle_span_yields_sorted_greedy_pivots line 199
  14. theorem OAI.Erdos970.WeightedTorusJets.det_ne_zero_of_linearIndepOn_rows line 234
  15. theorem OAI.Erdos970.WeightedTorusJets.span_rows_eq_top_of_detects line 245
  16. theorem OAI.Erdos970.WeightedTorusJets.detects_of_field_embedding line 259
  17. theorem OAI.Erdos970.WeightedTorusJets.finite_weighted_greedy_package line 276
  18. theorem OAI.Erdos970.WeightedTorusJets.rectangle_greedy_selection_package line 361
  19. theorem OAI.Erdos970.WeightedTorusJets.greedyPivots_filter_lt line 416
  20. theorem OAI.Erdos970.WeightedTorusJets.span_greedyPivots_eq_span_earlier_rows line 427
  21. theorem OAI.Erdos970.WeightedTorusJets.smaller_weight_mem_span_earlier_retained_rows line 453
  22. theorem OAI.Erdos970.WeightedTorusJets.jet_weight_ball_span_eq_top line 466