OAI/Combinatorics/SharpRamsey/Learning/PreparedPointProposals.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpLogRamsey.PreparedRow.total_cutoff_intersection line 18
  2. def OAI.SharpLogRamsey.PreparedRow.ambientCounts line 40
  3. def OAI.SharpLogRamsey.PreparedRow.coordinateSupport line 43
  4. def OAI.SharpLogRamsey.PreparedRow.ambientRate line 45
  5. lemma OAI.SharpLogRamsey.PreparedRow.ambientCounts_restrict line 49
  6. lemma OAI.SharpLogRamsey.PreparedRow.restrict_ambientCounts line 58
  7. theorem OAI.SharpLogRamsey.PreparedRow.ambientCounts_hasLaw line 63
  8. lemma OAI.SharpLogRamsey.PreparedRow.sum_ambientCounts line 105
  9. lemma OAI.SharpLogRamsey.PreparedRow.ambient_rate_uniform line 114
  10. theorem OAI.SharpLogRamsey.PreparedRow.ambient_proposal_success line 128