OAI/NumberTheory/Jacobsthal/Siegel/GreedyPivots.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.pivot_floor_square_bound line 19
  2. theorem OAI.Erdos970.WeightedTorusJets.pivot_second_sum_bound line 27
  3. theorem OAI.Erdos970.WeightedTorusJets.pivot_lower_bound_quarter line 36
  4. theorem OAI.Erdos970.WeightedTorusJets.pivot_lower_constant line 45
  5. theorem OAI.Erdos970.WeightedTorusJets.pivot_ratio_bound line 59
  6. theorem OAI.Erdos970.WeightedTorusJets.pivot_ratio_le_twelfth line 70
  7. theorem OAI.Erdos970.WeightedTorusJets.pivot_scale_ge_one line 80
  8. theorem OAI.Erdos970.WeightedTorusJets.pivot_dimension_eq_cube line 92
  9. theorem OAI.Erdos970.WeightedTorusJets.pivot_scale_cube line 97
  10. theorem OAI.Erdos970.WeightedTorusJets.pivot_primary_scale line 105
  11. theorem OAI.Erdos970.WeightedTorusJets.pivot_count_threshold line 112
  12. theorem OAI.Erdos970.WeightedTorusJets.pivot_primary_scale_ge_N line 116
  13. theorem OAI.Erdos970.WeightedTorusJets.pivot_floor_count_eventually line 124
  14. theorem OAI.Erdos970.WeightedTorusJets.pivot_coordinates_of_weight line 137
  15. theorem OAI.Erdos970.WeightedTorusJets.pivot_weight_of_rectangle line 151
  16. theorem OAI.Erdos970.WeightedTorusJets.card_filter_lt_le_mul line 167
  17. theorem OAI.Erdos970.WeightedTorusJets.card_sq_le_twice_mul_sum_add line 181
  18. theorem OAI.Erdos970.WeightedTorusJets.sum_lower_of_bounded_multiplicity line 218
  19. theorem OAI.Erdos970.WeightedTorusJets.coordinate_fiber_card_le line 229
  20. theorem OAI.Erdos970.WeightedTorusJets.first_coordinate_sum_lower line 250
  21. theorem OAI.Erdos970.WeightedTorusJets.weighted_pivot_bounds line 260
  22. theorem OAI.Erdos970.WeightedTorusJets.weighted_pivot_ratio_le_twelfth line 303
  23. def OAI.Erdos970.WeightedTorusJets.greedyPivots line 326
  24. theorem OAI.Erdos970.WeightedTorusJets.greedyPivots_subset_range line 335
  25. theorem OAI.Erdos970.WeightedTorusJets.greedyPivots_linearIndepOn line 347
  26. theorem OAI.Erdos970.WeightedTorusJets.span_greedyPivots line 358
  27. theorem OAI.Erdos970.WeightedTorusJets.mem_greedyPivots_succ_self line 372
  28. theorem OAI.Erdos970.WeightedTorusJets.greedyPivots_mono line 383
  29. theorem OAI.Erdos970.WeightedTorusJets.mem_greedyPivots_iff line 392
  30. theorem OAI.Erdos970.WeightedTorusJets.card_greedyPivots line 415
  31. theorem OAI.Erdos970.WeightedTorusJets.earlier_row_mem_span_greedyPivots line 424
  32. theorem OAI.Erdos970.WeightedTorusJets.smaller_weight_row_mem_span_greedyPivots line 429
  33. theorem OAI.Erdos970.WeightedTorusJets.card_greedyPivots_of_span_eq_top line 435
  34. theorem OAI.Erdos970.WeightedTorusJets.greedyPivots_eq_of_span_eq_top line 440
  35. theorem OAI.Erdos970.WeightedTorusJets.exists_weight_sorted_enumeration line 455
  36. def OAI.Erdos970.WeightedTorusJets.extendFiniteFamily line 477
  37. theorem OAI.Erdos970.WeightedTorusJets.image_extendFiniteFamily_range line 480
  38. theorem OAI.Erdos970.WeightedTorusJets.monotone_extendFiniteFamily line 491
  39. theorem OAI.Erdos970.WeightedTorusJets.exists_weight_sorted_cutoff_sequence line 502