OAI/Combinatorics/SharpRamsey/Validation/ProducedExclusion.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpLogRamsey.Validation.produced_exclusion line 13
  2. theorem OAI.SharpLogRamsey.PublicTables.failure_exp line 40
  3. theorem OAI.SharpLogRamsey.Incidence.low_incidence_half_target_mass line 62
  4. theorem OAI.SharpLogRamsey.Validation.projective_low_card line 145
  5. theorem OAI.SharpLogRamsey.Validation.projective_cap_mean line 165
  6. theorem OAI.SharpLogRamsey.Validation.projective_ideal_acceptance line 176
  7. def OAI.SharpLogRamsey.PublicTables.rowAt line 207
  8. def OAI.SharpLogRamsey.PublicTables.firstIndex line 211
  9. theorem OAI.SharpLogRamsey.PublicTables.reconstruct_first line 216
  10. theorem OAI.SharpLogRamsey.PublicTables.first_valid line 231
  11. theorem OAI.SharpLogRamsey.PublicTables.index_valid line 242
  12. def OAI.SharpLogRamsey.Validation.GoodCap line 257
  13. lemma OAI.SharpLogRamsey.Validation.cap_capture line 263
  14. theorem OAI.SharpLogRamsey.Validation.decoded_cap line 277
  15. lemma OAI.SharpLogRamsey.Validation.uniform_sum_mono line 287
  16. theorem OAI.SharpLogRamsey.Validation.original_exclusion line 305
  17. theorem OAI.SharpLogRamsey.Validation.projective_public_validation line 331
  18. theorem OAI.SharpLogRamsey.Validation.ready_exclusion line 370
  19. lemma OAI.SharpLogRamsey.PublicTables.integral_weighted_sum line 413
  20. lemma OAI.SharpLogRamsey.Validation.kernel_uniform line 439
  21. def OAI.SharpLogRamsey.Validation.missFraction line 442
  22. lemma OAI.SharpLogRamsey.Validation.missFraction_eq line 446
  23. lemma OAI.SharpLogRamsey.Validation.incidence_kernel_sum line 459
  24. theorem OAI.SharpLogRamsey.Validation.ready_fraction line 470
  25. theorem OAI.SharpLogRamsey.Validation.independent_loss line 518