OAI/Combinatorics/SharpRamsey/Validation/ValidationTools.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.FiniteSamplingBounds.rowWeight line 14
  2. def OAI.SharpLogRamsey.FiniteSamplingBounds.hitCount line 15
  3. lemma OAI.SharpLogRamsey.FiniteSamplingBounds.rowWeight_nonneg line 18
  4. lemma OAI.SharpLogRamsey.FiniteSamplingBounds.rowWeight_total line 21
  5. lemma OAI.SharpLogRamsey.FiniteSamplingBounds.rowMoment line 27
  6. def OAI.SharpLogRamsey.FiniteSamplingBounds.rowLower line 44
  7. lemma OAI.SharpLogRamsey.FiniteSamplingBounds.rowLower_moment line 47
  8. theorem OAI.SharpLogRamsey.FiniteSamplingBounds.rowLower_exp line 62
  9. theorem OAI.SharpLogRamsey.FiniteSamplingBounds.rowLower_highRank line 89
  10. def OAI.SharpLogRamsey.Validation.uniformMass line 110
  11. lemma OAI.SharpLogRamsey.Validation.uniform_nonneg line 113
  12. lemma OAI.SharpLogRamsey.Validation.uniform_total line 117
  13. lemma OAI.SharpLogRamsey.Validation.uniform_sum line 122
  14. lemma OAI.SharpLogRamsey.Validation.coordinate_mean line 126
  15. lemma OAI.SharpLogRamsey.Validation.hitCount_real line 142
  16. lemma OAI.SharpLogRamsey.Validation.hitCount_mean line 146
  17. def OAI.SharpLogRamsey.Validation.pass line 158
  18. def OAI.SharpLogRamsey.Validation.cap line 161
  19. theorem OAI.SharpLogRamsey.Validation.pointwise_exclusion line 166
  20. theorem OAI.SharpLogRamsey.Validation.pointwise_pass line 190
  21. def OAI.SharpLogRamsey.Validation.prob line 230
  22. lemma OAI.SharpLogRamsey.Validation.prob_nonneg line 233
  23. lemma OAI.SharpLogRamsey.Validation.prob_le_one line 239
  24. lemma OAI.SharpLogRamsey.Validation.cardinal_mean line 247
  25. lemma OAI.SharpLogRamsey.Validation.markov line 257
  26. theorem OAI.SharpLogRamsey.Validation.cap_mean_le line 270
  27. theorem OAI.SharpLogRamsey.Validation.loss_mean_le line 297
  28. theorem OAI.SharpLogRamsey.Validation.acceptance_mass line 326
  29. def OAI.SharpLogRamsey.Validation.rowLaw line 368
  30. def OAI.SharpLogRamsey.Validation.allIn line 373
  31. theorem OAI.SharpLogRamsey.Validation.contained_row_scaling line 377
  32. def OAI.SharpLogRamsey.Validation.implementAccept line 400
  33. theorem OAI.SharpLogRamsey.Validation.accepted_scaling line 403
  34. theorem OAI.SharpLogRamsey.Validation.proposal_acceptance line 420
  35. theorem OAI.SharpLogRamsey.Validation.public_iid_domination line 427