OAI/Computability/PerfectCompleteness/Repetition/CleanCountingLemmas.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.CleanCounting.expectation_event_factor line 18
  2. def OAI.PerfectCompleteness.CleanCounting.cleanCount line 34
  3. theorem OAI.PerfectCompleteness.CleanCounting.power_cleanCount line 38
  4. theorem OAI.PerfectCompleteness.CleanCounting.cleanCount_moment line 44
  5. theorem OAI.PerfectCompleteness.CleanCounting.cleanCount_moment_le line 60
  6. theorem OAI.PerfectCompleteness.CleanCounting.kernel_clean_probability line 84
  7. theorem OAI.PerfectCompleteness.CleanCounting.kernel_cleanCount_moment line 98
  8. theorem OAI.PerfectCompleteness.MixedSupport.localKey_unused line 124
  9. theorem OAI.PerfectCompleteness.MixedSupport.localReduction_unused line 135
  10. abbrev OAI.PerfectCompleteness.CleanKeyErasure.Retained line 154
  11. def OAI.PerfectCompleteness.CleanKeyErasure.retain line 157
  12. theorem OAI.PerfectCompleteness.CleanKeyErasure.retain_update_of_not_kept line 160
  13. theorem OAI.PerfectCompleteness.CleanKeyErasure.section_unused_of_retained line 169
  14. theorem OAI.PerfectCompleteness.CleanKeyErasure.section_unused_of_factor line 178
  15. theorem OAI.PerfectCompleteness.CleanKeyErasure.keyFields_dropped_of_retained line 184
  16. theorem OAI.PerfectCompleteness.CleanKeyErasure.reduction_dropped_of_retained line 191
  17. theorem OAI.PerfectCompleteness.CleanKeyErasure.section_unused_of_factoring line 203
  18. theorem OAI.PerfectCompleteness.CleanKeyErasure.keyFields_dropped_of_factoring line 208
  19. theorem OAI.PerfectCompleteness.CleanKeyErasure.reduction_dropped_of_factoring line 213
  20. theorem OAI.PerfectCompleteness.CleanKeyErasure.retainedKeys_only_kept line 224
  21. theorem OAI.PerfectCompleteness.CleanKeyErasure.not_mem_retainedKeys_of_not_kept line 236
  22. theorem OAI.PerfectCompleteness.CleanKeyErasure.keyFields_const line 244
  23. theorem OAI.PerfectCompleteness.CleanKeyErasure.retainedKeys_const line 249
  24. abbrev OAI.PerfectCompleteness.CleanKeyFactorization.retainedSlots line 270
  25. def OAI.PerfectCompleteness.CleanKeyFactorization.fill line 273
  26. theorem OAI.PerfectCompleteness.CleanKeyFactorization.retain_fill line 278
  27. theorem OAI.PerfectCompleteness.CleanKeyFactorization.retain_surjective line 284
  28. theorem OAI.PerfectCompleteness.CleanKeyFactorization.retain_update line 288
  29. theorem OAI.PerfectCompleteness.CleanKeyFactorization.sectionFunction_factor line 294
  30. theorem OAI.PerfectCompleteness.CleanKeyFactorization.keyFields_kept line 303
  31. theorem OAI.PerfectCompleteness.CleanKeyFactorization.reduction_kept line 313
  32. def OAI.PerfectCompleteness.CleanKeyFactorization.embeddedFields line 325
  33. def OAI.PerfectCompleteness.CleanKeyFactorization.embeddedReduction line 329
  34. theorem OAI.PerfectCompleteness.CleanKeyFactorization.keyFields_factor line 333
  35. theorem OAI.PerfectCompleteness.CleanKeyFactorization.reduction_factor line 343
  36. theorem OAI.PerfectCompleteness.CleanKeyFactorization.embeddedReduction_constant line 354
  37. def OAI.PerfectCompleteness.CleanKeyFactorization.retainedMetadata line 366
  38. def OAI.PerfectCompleteness.CleanKeyFactorization.retainedKey line 371
  39. theorem OAI.PerfectCompleteness.CleanKeyFactorization.retainedKeys_factor line 377
  40. theorem OAI.PerfectCompleteness.CleanKeyFactorization.partition_factor line 383
  41. theorem OAI.PerfectCompleteness.CleanKeyFactorization.key_factor line 392
  42. theorem OAI.PerfectCompleteness.CleanKeyFactorization.retainedKey_nonempty line 398
  43. def OAI.PerfectCompleteness.CleanKeyFactorization.retainedQueryKey line 404
  44. theorem OAI.PerfectCompleteness.CleanKeyFactorization.queryKey_factor line 409
  45. theorem OAI.PerfectCompleteness.CleanKeyFactorization.label_factor line 416
  46. def OAI.PerfectCompleteness.CleanKeyFactorization.retainedResponse line 424
  47. theorem OAI.PerfectCompleteness.CleanKeyFactorization.response_factor line 430