OAI/Combinatorics/KServer/JointExperiment.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

The posterior counting measure is built from labeled hidden positions. Integrating adapted metric tests is exactly conditional expectation, and prefix quota domination is relative to this measure, not an extra premise.

  1. def OAI.KServer.PosteriorCounting.atoms line 20
  2. def OAI.KServer.PosteriorCounting.measure line 22
  3. lemma OAI.KServer.PosteriorCounting.atoms_nonneg line 26
  4. lemma OAI.KServer.PosteriorCounting.atoms_total line 29
  5. lemma OAI.KServer.PosteriorCounting.measure_nonneg line 36
  6. lemma OAI.KServer.PosteriorCounting.measure_adapted line 40
  7. lemma OAI.KServer.PosteriorCounting.measure_total line 44
  8. lemma OAI.KServer.PosteriorCounting.atoms_integral line 50
  9. lemma OAI.KServer.PosteriorCounting.conditional_integral line 57
  10. lemma OAI.KServer.PosteriorCounting.conditional_mean line 71
  11. lemma OAI.KServer.PosteriorCounting.prefix_mass line 79
  12. lemma OAI.KServer.PosteriorCounting.size_prefix_bound line 101
  13. abbrev OAI.KServer.PositiveExperiment.Support line 128
  14. def OAI.KServer.PositiveExperiment.weight line 130
  15. lemma OAI.KServer.PositiveExperiment.weight_pos line 133
  16. lemma OAI.KServer.PositiveExperiment.sum_support line 135
  17. lemma OAI.KServer.PositiveExperiment.weight_sum line 145
  18. lemma OAI.KServer.PositiveExperiment.mass_support line 149
  19. lemma OAI.KServer.PositiveExperiment.numerator_support line 154
  20. lemma OAI.KServer.PositiveExperiment.posterior_support line 160
  21. lemma OAI.KServer.PositiveExperiment.measure_support line 164
  22. instance OAI.KServer.JointExperiment.(instance at line 185) line 185
  23. abbrev OAI.KServer.JointExperiment.Tape line 189
  24. def OAI.KServer.JointExperiment.tapeWeight line 192
  25. lemma OAI.KServer.JointExperiment.tapeWeight_sum line 195
  26. lemma OAI.KServer.JointExperiment.tapeWeight_nonneg line 204
  27. def OAI.KServer.JointExperiment.tapeLaw line 208
  28. abbrev OAI.KServer.JointExperiment.Raw line 211
  29. def OAI.KServer.JointExperiment.rawWeight line 216
  30. abbrev OAI.KServer.JointExperiment.Atom line 217
  31. def OAI.KServer.JointExperiment.weight line 218
  32. lemma OAI.KServer.JointExperiment.raw_nonneg line 220
  33. lemma OAI.KServer.JointExperiment.weight_pos line 222
  34. lemma OAI.KServer.JointExperiment.weight_nonneg line 223
  35. lemma OAI.KServer.JointExperiment.weight_sum line 224
  36. lemma OAI.KServer.JointExperiment.avg_raw line 227
  37. lemma OAI.KServer.JointExperiment.request_pos line 231
  38. lemma OAI.KServer.JointExperiment.tape_pos line 236
  39. def OAI.KServer.JointExperiment.history line 241
  40. lemma OAI.KServer.JointExperiment.history_refines line 243
  41. lemma OAI.KServer.JointExperiment.history_eq line 247
  42. def OAI.KServer.JointExperiment.hidden line 254
  43. def OAI.KServer.JointExperiment.maps line 256
  44. lemma OAI.KServer.JointExperiment.maps_adapted line 260
  45. lemma OAI.KServer.JointExperiment.measure_eq line 272
  46. lemma OAI.KServer.JointExperiment.request_history line 285
  47. lemma OAI.KServer.JointExperiment.hidden_covers line 289
  48. lemma OAI.KServer.JointExperiment.scale_mean line 294
  49. instance OAI.KServer.LevelKeys.alphabetFintype line 319
  50. lemma OAI.KServer.ScheduledEndpoint.masked_value_bound line 338
  51. lemma OAI.KServer.ScheduledEndpoint.actual_bound line 355