OAI/Combinatorics/BalancedRyser/Local/LocalTwoReuseMean.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Local.TwoReuseAssembly.sum_allTokensDistinct_eq line 10
  2. theorem OAI.Balanced.Local.TwoReuseAssembly.injective_conditional_sum_le_of_embedding_sum line 21
  3. theorem OAI.Balanced.Local.TwoReuseAssembly.sum_le_card_mul_of_mean_le line 38
  4. theorem OAI.Balanced.Local.TwoReuseAssembly.injective_conditional_sum_le_of_embedding_mean line 48
  5. def OAI.Balanced.Local.TwoReuseAssembly.InjectiveTwoReuseMeanEstimate line 66
  6. theorem OAI.Balanced.Local.TwoReuseAssembly.pencilTwoReuses_of_alignment_and_injective_mean line 78
  7. theorem OAI.Balanced.Local.TwoReuseAssembly.pencilTwoReuses_of_injective_mean line 88
  8. theorem OAI.Balanced.Local.TwoReuseAssembly.pencilTwoReuses_of_injective line 92