OAI/Computability/PerfectCompleteness/Foundations/ManyGoodRowsLemmas.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.ManyGoodRows.RowMap line 31
  2. def OAI.PerfectCompleteness.ManyGoodRows.GoodRow line 34
  3. structure OAI.PerfectCompleteness.ManyGoodRows.Witness line 40
  4. def OAI.PerfectCompleteness.ManyGoodRows.selectWitness line 50
  5. def OAI.PerfectCompleteness.ManyGoodRows.IsGoodPoint line 57
  6. def OAI.PerfectCompleteness.ManyGoodRows.goodMass line 61
  7. def OAI.PerfectCompleteness.ManyGoodRows.adviceMass line 64
  8. theorem OAI.PerfectCompleteness.ManyGoodRows.GoodRow.mono line 69
  9. theorem OAI.PerfectCompleteness.ManyGoodRows.isGoodPoint_of_witness line 78
  10. theorem OAI.PerfectCompleteness.ManyGoodRows.dense_restriction_rowMap line 87
  11. theorem OAI.PerfectCompleteness.ManyGoodRows.goodMass_ge line 101
  12. theorem OAI.PerfectCompleteness.ManyGoodRows.goodMass_le_card_mul_adviceMass line 130
  13. theorem OAI.PerfectCompleteness.ManyGoodRows.adviceMass_ge line 155
  14. theorem OAI.PerfectCompleteness.ManyGoodRows.exists_uniform_parameters line 169
  15. theorem OAI.PerfectCompleteness.FamilyGoodRows.expectation_le_threshold_add_probability line 207
  16. theorem OAI.PerfectCompleteness.FamilyGoodRows.threshold_probability_ge line 223
  17. theorem OAI.PerfectCompleteness.FamilyGoodRows.probability_mul_le_expectation line 230
  18. theorem OAI.PerfectCompleteness.FamilyGoodRows.nonzeroAgreement_le_one line 254
  19. theorem OAI.PerfectCompleteness.FamilyGoodRows.adviceMass_nonneg line 268
  20. theorem OAI.PerfectCompleteness.FamilyGoodRows.mean_adviceMass_ge line 285
  21. abbrev OAI.PerfectCompleteness.ProductEvaluation.F2 line 324
  22. inductive OAI.PerfectCompleteness.ProductEvaluation.Generator line 328
  23. def OAI.PerfectCompleteness.ProductEvaluation.displayedJoint line 332
  24. def OAI.PerfectCompleteness.ProductEvaluation.generatorValue line 336
  25. def OAI.PerfectCompleteness.ProductEvaluation.generator line 340
  26. def OAI.PerfectCompleteness.ProductEvaluation.productSpan line 346
  27. def OAI.PerfectCompleteness.ProductEvaluation.spanGenerator line 351
  28. theorem OAI.PerfectCompleteness.ProductEvaluation.functional_ext line 357
  29. def OAI.PerfectCompleteness.ProductEvaluation.realizingPoint line 378
  30. theorem OAI.PerfectCompleteness.ProductEvaluation.realizingPoint_joint line 383
  31. def OAI.PerfectCompleteness.ProductEvaluation.restoredRows line 387
  32. theorem OAI.PerfectCompleteness.ProductEvaluation.restoredRows_apply line 391
  33. def OAI.PerfectCompleteness.ProductEvaluation.labelExtension line 395
  34. def OAI.PerfectCompleteness.ProductEvaluation.labelFunctional line 399
  35. theorem OAI.PerfectCompleteness.ProductEvaluation.labelFunctional_generators line 403
  36. theorem OAI.PerfectCompleteness.ProductEvaluation.labelFunctional_unique line 409
  37. theorem OAI.PerfectCompleteness.ProductEvaluation.exists_unique_labelFunctional line 418
  38. theorem OAI.PerfectCompleteness.ProductEvaluation.labelFunctional_eq_of_restoredRows_eq line 427
  39. theorem OAI.PerfectCompleteness.ProductEvaluation.labelExtension_restrict line 436
  40. theorem OAI.PerfectCompleteness.ProductEvaluation.exists_labelExtension line 440
  41. theorem OAI.PerfectCompleteness.ProductEvaluation.extension_generators line 446
  42. theorem OAI.PerfectCompleteness.ProductEvaluation.extension_one line 456
  43. theorem OAI.PerfectCompleteness.ProductEvaluation.extension_products line 462
  44. theorem OAI.PerfectCompleteness.ProductEvaluation.extension_productMatrix line 470