OAI/NumberTheory/Jacobsthal/Paths/FullWordHighAlignment.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.SubsetTagFailureMass.badSelections line 19
  2. def OAI.Erdos970.NumberTheoryLean.SubsetTagFailureMass.badMass line 26
  3. theorem OAI.Erdos970.NumberTheoryLean.SubsetTagFailureMass.bad_mass_le_alignment line 30
  4. theorem OAI.Erdos970.NumberTheoryLean.SubsetTagFailureMass.bad_mass_le_wrong line 42
  5. def OAI.Erdos970.NumberTheoryLean.HardTagBoxMass.hardBadSelections line 75
  6. def OAI.Erdos970.NumberTheoryLean.HardTagBoxMass.hardBadMass line 82
  7. theorem OAI.Erdos970.NumberTheoryLean.HardTagBoxMass.hardBad_subset_bad line 86
  8. theorem OAI.Erdos970.NumberTheoryLean.HardTagBoxMass.hardBadMass_le_badMass line 101
  9. theorem OAI.Erdos970.NumberTheoryLean.SafeAnchorSearchCount.safe_anchor_search_count line 118
  10. theorem OAI.Erdos970.NumberTheoryLean.HardTagWordFamily.finite_union_mass_le line 153
  11. def OAI.Erdos970.NumberTheoryLean.HardTagWordFamily.hardBadWords line 165
  12. theorem OAI.Erdos970.NumberTheoryLean.HardTagWordFamily.hardBadWords_mass line 169
  13. def OAI.Erdos970.NumberTheoryLean.HardTagWordFamily.hardWordFamily line 186
  14. theorem OAI.Erdos970.NumberTheoryLean.HardTagWordFamily.hardWordFamily_mass_le line 191
  15. theorem OAI.Erdos970.NumberTheoryLean.SafeBoxTagRate.safe_box_tag_rate line 216
  16. def OAI.Erdos970.NumberTheoryLean.RegularBadTagWords.badWordTest line 280
  17. def OAI.Erdos970.NumberTheoryLean.RegularBadTagWords.regularBadWords line 288
  18. theorem OAI.Erdos970.NumberTheoryLean.RegularBadTagWords.regularBadWords_subset line 293
  19. theorem OAI.Erdos970.NumberTheoryLean.RegularBadTagWords.regularBadWords_mass_le line 313
  20. theorem OAI.Erdos970.NumberTheoryLean.GlobalSafeTagCapture.finite_candidate_sum line 332
  21. theorem OAI.Erdos970.NumberTheoryLean.GlobalSafeTagCapture.global_bad_tag_mass_small line 344
  22. theorem OAI.Erdos970.NumberTheoryLean.PaperSafeTagCapture.paper_safe_hard_tag_capture line 396
  23. theorem OAI.Erdos970.NumberTheoryLean.PaperSafeWordCapture.paper_safe_hard_word_capture line 448
  24. theorem OAI.Erdos970.NumberTheoryLean.PaperRegularTagCapture.paper_regular_bad_tag_mass line 480
  25. theorem OAI.Erdos970.NumberTheoryLean.FullWordHighAlignment.parent_prime_factors line 520
  26. theorem OAI.Erdos970.NumberTheoryLean.FullWordHighAlignment.full_word_high_alignment line 532
  27. theorem OAI.Erdos970.NumberTheoryLean.FullWordHighAlignment.full_word_high_alignment_fixed_cutoff line 558