OAI/NumberTheory/Jacobsthal/Paths/FiniteBoxWordMass.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosSubsetWord.descendingWord line 19
  2. theorem OAI.Erdos970.ErdosSubsetWord.mem_descendingWord line 22
  3. theorem OAI.Erdos970.ErdosSubsetWord.descendingWord_nodup line 26
  4. theorem OAI.Erdos970.ErdosSubsetWord.descendingWord_strict line 29
  5. theorem OAI.Erdos970.ErdosSubsetWord.descendingWord_toFinset line 32
  6. theorem OAI.Erdos970.ErdosSubsetWord.descendingWord_length line 35
  7. theorem OAI.Erdos970.ErdosSubsetWord.descendingWord_product line 44
  8. theorem OAI.Erdos970.ErdosSubsetWord.descendingWord_primes line 50
  9. def OAI.Erdos970.ErdosSearchCount.selectedCount line 66
  10. def OAI.Erdos970.ErdosSearchCount.remainderSum line 67
  11. theorem OAI.Erdos970.ErdosSearchCount.valid_half line 70
  12. theorem OAI.Erdos970.ErdosSearchCount.child_gap_third line 73
  13. theorem OAI.Erdos970.ErdosSearchCount.initial_gap_le_search_power line 84
  14. def OAI.Erdos970.ErdosSearchCount.searchFlag line 117
  15. def OAI.Erdos970.ErdosSearchCount.searchCount line 119
  16. theorem OAI.Erdos970.ErdosSearchCount.searchCount_labels line 122
  17. theorem OAI.Erdos970.ErdosSearchCount.searchCount_label_invariant line 128
  18. theorem OAI.Erdos970.ErdosSearchCount.nonsearch_exponent_bound line 133
  19. theorem OAI.Erdos970.ErdosSearchCount.remainderSum_le_length_mul line 162
  20. theorem OAI.Erdos970.ErdosSearchCount.source_remainder_bound line 176
  21. theorem OAI.Erdos970.ErdosSearchCount.nonsearch_budget_le line 201
  22. theorem OAI.Erdos970.ErdosSearchCount.nonsearch_budget_small line 233
  23. theorem OAI.Erdos970.ErdosSearchCount.logarithmic_count_of_power line 237
  24. theorem OAI.Erdos970.ErdosSearchCount.actual_search_count line 249
  25. def OAI.Erdos970.ErdosSearchCount.searchConstant line 267
  26. theorem OAI.Erdos970.ErdosSearchCount.searchConstant_pos line 268
  27. theorem OAI.Erdos970.ErdosSearchCount.actual_search_count_uniform line 270
  28. theorem OAI.Erdos970.ErdosSearchCount.paper_incoming_geometry line 297
  29. theorem OAI.Erdos970.ErdosSearchCount.paper_search_count line 319
  30. theorem OAI.Erdos970.ErdosSearchCount.literal_source_search_count line 336
  31. theorem OAI.Erdos970.ErdosSearchCount.nonsearch_error_littleO line 364
  32. theorem OAI.Erdos970.ErdosSearchCount.selectedCount_eq_sum line 376
  33. def OAI.Erdos970.ErdosSearchCount.searchIndexSet line 382
  34. theorem OAI.Erdos970.ErdosSearchCount.searchCount_ofFn line 386
  35. theorem OAI.Erdos970.ErdosStoppedReferenceUpper.actual_stopped_reference_upper line 406
  36. theorem OAI.Erdos970.ErdosStoppedReferenceUpper.floored_source_stopped_reference_upper line 464
  37. def OAI.Erdos970.ErdosSubsetWord.globalBins line 514
  38. def OAI.Erdos970.ErdosSubsetWord.occupiedSearch line 516
  39. theorem OAI.Erdos970.ErdosSubsetWord.selected_prime_label line 520
  40. theorem OAI.Erdos970.ErdosSubsetWord.global_word_length line 527
  41. theorem OAI.Erdos970.ErdosSubsetWord.word_source_membership line 533
  42. theorem OAI.Erdos970.ErdosSubsetWord.word_search_count line 543
  43. theorem OAI.Erdos970.ErdosSubsetWord.word_search_count_eq_occupied line 565
  44. theorem OAI.Erdos970.ErdosSubsetWord.global_label_mono line 593
  45. theorem OAI.Erdos970.ErdosSubsetWord.word_label_count line 607
  46. theorem OAI.Erdos970.ErdosSubsetWord.word_labels_ordered line 633
  47. theorem OAI.Erdos970.ErdosSubsetWord.selection_label_word_eq line 643
  48. theorem OAI.Erdos970.ErdosSubsetWord.selection_prefix_labels_eq line 656
  49. theorem OAI.Erdos970.NumberTheoryLean.FiniteBoxWordMass.word_injective line 674
  50. def OAI.Erdos970.NumberTheoryLean.FiniteBoxWordMass.wordBox line 682
  51. theorem OAI.Erdos970.NumberTheoryLean.FiniteBoxWordMass.wordBox_mass line 685
  52. theorem OAI.Erdos970.NumberTheoryLean.FiniteBoxWordMass.wordBoxes_disjoint line 697
  53. def OAI.Erdos970.NumberTheoryLean.FiniteBoxWordMass.boxWords line 712
  54. theorem OAI.Erdos970.NumberTheoryLean.FiniteBoxWordMass.total_box_mass_eq line 715