OAI/Computability/PerfectCompleteness/Decoding/CollisionAveragingLemmas.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.CollisionAveraging.mean_square_le line 19
  2. theorem OAI.PerfectCompleteness.CollisionAveraging.average_square_bound line 24
  3. theorem OAI.PerfectCompleteness.CollisionAveraging.eighth_square_bound line 37
  4. theorem OAI.PerfectCompleteness.CollisionAveraging.average_collision line 49
  5. theorem OAI.PerfectCompleteness.CollisionAveraging.actual_eighth_square_bound line 58
  6. def OAI.PerfectCompleteness.SparseProjection.localDensity line 85
  7. theorem OAI.PerfectCompleteness.SparseProjection.local_mean line 89
  8. theorem OAI.PerfectCompleteness.SparseProjection.local_second_moment line 102
  9. def OAI.PerfectCompleteness.SparseProjection.density line 118
  10. theorem OAI.PerfectCompleteness.SparseProjection.density_mean line 121
  11. theorem OAI.PerfectCompleteness.SparseProjection.density_second_moment line 128
  12. theorem OAI.PerfectCompleteness.SparseProjection.density_second_moment_le line 155
  13. def OAI.PerfectCompleteness.SparseProjection.projectedLaw line 173
  14. theorem OAI.PerfectCompleteness.SparseProjection.projected_weight line 181
  15. theorem OAI.PerfectCompleteness.SparseProjection.observed_variation line 189
  16. def OAI.PerfectCompleteness.ProjectionPosterior.bernoulli line 215
  17. theorem OAI.PerfectCompleteness.ProjectionPosterior.bernoulli_true line 220
  18. def OAI.PerfectCompleteness.ProjectionPosterior.posterior line 227
  19. theorem OAI.PerfectCompleteness.ProjectionPosterior.localDensity_positive line 231
  20. theorem OAI.PerfectCompleteness.ProjectionPosterior.posterior_nonnegative line 237
  21. theorem OAI.PerfectCompleteness.ProjectionPosterior.posterior_le_one line 244
  22. theorem OAI.PerfectCompleteness.ProjectionPosterior.posterior_le line 252
  23. def OAI.PerfectCompleteness.ProjectionPosterior.posteriorMask line 263
  24. def OAI.PerfectCompleteness.ProjectionPosterior.forward line 270
  25. def OAI.PerfectCompleteness.ProjectionPosterior.reverse line 279
  26. theorem OAI.PerfectCompleteness.ProjectionPosterior.forward_reverse_weight line 287
  27. theorem OAI.PerfectCompleteness.ProjectionPosterior.probability_reverse line 309
  28. theorem OAI.PerfectCompleteness.AdaptiveProjection.probability_selected_le line 334
  29. theorem OAI.PerfectCompleteness.AdaptiveProjection.posteriorMask_marginal line 366
  30. theorem OAI.PerfectCompleteness.AdaptiveProjection.adaptive_selection line 384