OAI/NumberTheory/SiegelZeros/Selection/GreedyPivots.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_floor_square_bound line 17
  2. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_second_sum_bound line 25
  3. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_lower_bound_quarter line 34
  4. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_lower_constant line 43
  5. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_ratio_bound line 57
  6. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_ratio_le_twelfth line 68
  7. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_scale_ge_one line 78
  8. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_dimension_eq_cube line 90
  9. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_scale_cube line 95
  10. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_primary_scale line 103
  11. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_count_threshold line 110
  12. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_primary_scale_ge_N line 114
  13. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_floor_count_eventually line 122
  14. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_coordinates_of_weight line 135
  15. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_weight_of_rectangle line 149
  16. theorem OAI.SiegelZeros.WeightedTorusJets.card_filter_lt_le_mul line 165
  17. theorem OAI.SiegelZeros.WeightedTorusJets.card_sq_le_twice_mul_sum_add line 179
  18. theorem OAI.SiegelZeros.WeightedTorusJets.sum_lower_of_bounded_multiplicity line 216
  19. theorem OAI.SiegelZeros.WeightedTorusJets.coordinate_fiber_card_le line 227
  20. theorem OAI.SiegelZeros.WeightedTorusJets.first_coordinate_sum_lower line 248
  21. theorem OAI.SiegelZeros.WeightedTorusJets.weighted_pivot_bounds line 258
  22. theorem OAI.SiegelZeros.WeightedTorusJets.weighted_pivot_ratio_le_twelfth line 301
  23. def OAI.SiegelZeros.WeightedTorusJets.greedyPivots line 324
  24. theorem OAI.SiegelZeros.WeightedTorusJets.greedyPivots_subset_range line 333
  25. theorem OAI.SiegelZeros.WeightedTorusJets.greedyPivots_linearIndepOn line 345
  26. theorem OAI.SiegelZeros.WeightedTorusJets.span_greedyPivots line 356
  27. theorem OAI.SiegelZeros.WeightedTorusJets.mem_greedyPivots_succ_self line 370
  28. theorem OAI.SiegelZeros.WeightedTorusJets.greedyPivots_mono line 381
  29. theorem OAI.SiegelZeros.WeightedTorusJets.mem_greedyPivots_iff line 390
  30. theorem OAI.SiegelZeros.WeightedTorusJets.card_greedyPivots line 413
  31. theorem OAI.SiegelZeros.WeightedTorusJets.earlier_row_mem_span_greedyPivots line 422
  32. theorem OAI.SiegelZeros.WeightedTorusJets.smaller_weight_row_mem_span_greedyPivots line 427
  33. theorem OAI.SiegelZeros.WeightedTorusJets.card_greedyPivots_of_span_eq_top line 433
  34. theorem OAI.SiegelZeros.WeightedTorusJets.greedyPivots_eq_of_span_eq_top line 438
  35. theorem OAI.SiegelZeros.WeightedTorusJets.exists_weight_sorted_enumeration line 453
  36. def OAI.SiegelZeros.WeightedTorusJets.extendFiniteFamily line 475
  37. theorem OAI.SiegelZeros.WeightedTorusJets.image_extendFiniteFamily_range line 478
  38. theorem OAI.SiegelZeros.WeightedTorusJets.monotone_extendFiniteFamily line 489
  39. theorem OAI.SiegelZeros.WeightedTorusJets.exists_weight_sorted_cutoff_sequence line 500