OAI/Computability/PerfectCompleteness/Foundations/MultiplicationFormInjectiveLemmas.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.MultiplicationFormInjective.multiplicationForm_injective line 24
  2. theorem OAI.PerfectCompleteness.MultiplicationFormInjective.multiplicationForm_eq_iff line 33
  3. theorem OAI.PerfectCompleteness.MultiplicationFormInjective.optionMap_injective line 38
  4. theorem OAI.PerfectCompleteness.MultiplicationFormInjective.definedEqual_map_of_injective line 42
  5. theorem OAI.PerfectCompleteness.MultiplicationFormInjective.definedEqual_map line 49
  6. theorem OAI.PerfectCompleteness.MultiplicationFormInjective.fullCollision_map line 56
  7. theorem OAI.PerfectCompleteness.MultiplicationFormInjective.collision_map line 63
  8. theorem OAI.PerfectCompleteness.MultiplicationFormInjective.fullCollision_probability line 69
  9. theorem OAI.PerfectCompleteness.MultiplicationFormInjective.collision_probability line 80
  10. def OAI.PerfectCompleteness.SingleResponseResampling.originalLaw line 104
  11. def OAI.PerfectCompleteness.SingleResponseResampling.resampledLaw line 108
  12. theorem OAI.PerfectCompleteness.SingleResponseResampling.probability_rectangle line 112
  13. theorem OAI.PerfectCompleteness.SingleResponseResampling.local_square_bound line 125
  14. theorem OAI.PerfectCompleteness.SingleResponseResampling.success_square_le_collision line 135
  15. theorem OAI.PerfectCompleteness.SingleResponseResampling.success_square_le_event line 151
  16. def OAI.PerfectCompleteness.SparseReplacement.row line 181
  17. theorem OAI.PerfectCompleteness.SparseReplacement.row_weight line 188
  18. def OAI.PerfectCompleteness.SparseReplacement.law line 195
  19. def OAI.PerfectCompleteness.SparseReplacement.markedLaw line 200
  20. theorem OAI.PerfectCompleteness.SparseReplacement.markedLaw_marginal line 207
  21. theorem OAI.PerfectCompleteness.SparseReplacement.ratio_reweight_eq line 232
  22. theorem OAI.PerfectCompleteness.SparseReplacement.projectedLaw_eq line 239
  23. theorem OAI.PerfectCompleteness.SparseReplacement.forward_eq line 258
  24. theorem OAI.PerfectCompleteness.SparseReplacement.markedLaw_posterior_weight line 267
  25. theorem OAI.PerfectCompleteness.SparseReplacement.observed_variation line 281
  26. theorem OAI.PerfectCompleteness.SparseReplacement.adaptive_selection line 294
  27. theorem OAI.PerfectCompleteness.SparseReplacement.observed_uniform_variation line 311
  28. theorem OAI.PerfectCompleteness.SparseReplacement.adaptive_uniform_selection line 327
  29. theorem OAI.PerfectCompleteness.MarkedKernelProduct.physical_marked line 353
  30. def OAI.PerfectCompleteness.MarkedKernelProduct.markEquiv line 367
  31. theorem OAI.PerfectCompleteness.MarkedKernelProduct.marked_product line 377
  32. theorem OAI.PerfectCompleteness.MarkedKernelProduct.law_mixture line 394
  33. theorem OAI.PerfectCompleteness.MarkedKernelProduct.mixture_markedLaw line 405
  34. def OAI.PerfectCompleteness.StochasticSingleResponse.hit line 454
  35. def OAI.PerfectCompleteness.StochasticSingleResponse.tableHit line 459
  36. def OAI.PerfectCompleteness.StochasticSingleResponse.tableCollision line 463
  37. theorem OAI.PerfectCompleteness.StochasticSingleResponse.hit_eq_table_mean line 467
  38. theorem OAI.PerfectCompleteness.StochasticSingleResponse.hit_square_le_table_collision line 491
  39. theorem OAI.PerfectCompleteness.StochasticSingleResponse.hit_square_le_of_supported_tables line 504
  40. theorem OAI.PerfectCompleteness.StochasticSingleResponse.hit_square_le_of_admissible line 513
  41. theorem OAI.PerfectCompleteness.StochasticSingleResponse.hit_square_le_of_probability_one line 525
  42. theorem OAI.PerfectCompleteness.StochasticSingleResponse.mean_hit_square_le_table_collision line 545