OAI/Combinatorics/SharpRamsey/Learning/PreparedProposals.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SharpLogRamsey.PublicTables.Law line 10
  2. def OAI.SharpLogRamsey.PublicTables.Table line 17
  3. instance OAI.SharpLogRamsey.PublicTables.instFintypeTable line 21
  4. def OAI.SharpLogRamsey.PublicTables.tableWeight line 28
  5. def OAI.SharpLogRamsey.PublicTables.first line 32
  6. def OAI.SharpLogRamsey.PublicTables.outcome line 36
  7. def OAI.SharpLogRamsey.PublicTables.integral line 40
  8. def OAI.SharpLogRamsey.PublicTables.accepted line 43
  9. def OAI.SharpLogRamsey.PublicTables.acceptProb line 46
  10. theorem OAI.SharpLogRamsey.PublicTables.tableWeight_nonneg line 49
  11. theorem OAI.SharpLogRamsey.PublicTables.tableWeight_total line 55
  12. theorem OAI.SharpLogRamsey.PublicTables.acceptProb_nonneg line 66
  13. theorem OAI.SharpLogRamsey.PublicTables.acceptProb_le_one line 72
  14. theorem OAI.SharpLogRamsey.PublicTables.rejectProb line 79
  15. theorem OAI.SharpLogRamsey.PublicTables.integral_succ line 87
  16. theorem OAI.SharpLogRamsey.PublicTables.integral_formula line 118
  17. theorem OAI.SharpLogRamsey.PublicTables.geometric_normalization line 134
  18. theorem OAI.SharpLogRamsey.PublicTables.first_accepted_law line 142
  19. theorem OAI.SharpLogRamsey.PublicTables.produced_domination line 149
  20. theorem OAI.SharpLogRamsey.PublicTables.production_probability line 162
  21. def OAI.SharpLogRamsey.PublicTables.Law.fromMeasure line 175
  22. lemma OAI.SharpLogRamsey.PublicTables.acceptProb_fromMeasure line 183
  23. def OAI.SharpLogRamsey.FiniteSchedules.clip line 201
  24. def OAI.SharpLogRamsey.FiniteSchedules.total line 204
  25. lemma OAI.SharpLogRamsey.FiniteSchedules.coordinate_le_total line 206
  26. lemma OAI.SharpLogRamsey.FiniteSchedules.clip_eq_iff line 209
  27. lemma OAI.SharpLogRamsey.FiniteSchedules.clip_preimage line 225
  28. lemma OAI.SharpLogRamsey.FiniteSchedules.clip_total_iff line 231
  29. lemma OAI.SharpLogRamsey.FiniteSchedules.acceptance_preimage line 245
  30. def OAI.SharpLogRamsey.PoissonLikelihood.law line 267
  31. instance OAI.SharpLogRamsey.PoissonLikelihood.probability line 270
  32. theorem OAI.SharpLogRamsey.PoissonLikelihood.singleton_formula line 274
  33. theorem OAI.SharpLogRamsey.PoissonLikelihood.singleton_ratio line 282
  34. def OAI.SharpLogRamsey.PoissonLikelihood.uniformRate line 291
  35. lemma OAI.SharpLogRamsey.PoissonLikelihood.sum_uniformRate line 294
  36. theorem OAI.SharpLogRamsey.PoissonLikelihood.uniform_singleton_ratio line 302
  37. def OAI.SharpLogRamsey.PreparedProposals.accepts line 329
  38. def OAI.SharpLogRamsey.PreparedProposals.proposal line 333
  39. lemma OAI.SharpLogRamsey.PreparedProposals.proposal_mass line 337
  40. theorem OAI.SharpLogRamsey.PreparedProposals.atom_domination line 343
  41. lemma OAI.SharpLogRamsey.PreparedProposals.accepts_probability line 354
  42. theorem OAI.SharpLogRamsey.PreparedProposals.proposal_success line 362
  43. lemma OAI.SharpLogRamsey.PreparedProposals.hidden_support_ae line 378
  44. lemma OAI.SharpLogRamsey.PreparedProposals.true_success_probability line 393