OAI/Computability/PerfectCompleteness/Sampling/CommonProductVariationLemmas.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.CommonProductVariation.product_totalVariation line 19
  2. theorem OAI.PerfectCompleteness.CommonProductVariation.observed_product_le line 29
  3. theorem OAI.PerfectCompleteness.CommonProductVariation.observed_product_le_of_bound line 36
  4. theorem OAI.PerfectCompleteness.ConditionalVariation.sigma_totalVariation line 57
  5. theorem OAI.PerfectCompleteness.ConditionalVariation.observed_sigma_le line 71
  6. theorem OAI.PerfectCompleteness.ConditionalVariation.observed_sigma_le_of_bound line 80
  7. theorem OAI.PerfectCompleteness.ConditionalVariation.observed_sigma_le_const line 88
  8. abbrev OAI.PerfectCompleteness.DummyElimination.Slice.Lifted line 113
  9. abbrev OAI.PerfectCompleteness.DummyElimination.Slice.ProjectedMatrices line 114
  10. abbrev OAI.PerfectCompleteness.DummyElimination.Slice.HomogeneousMaps line 115
  11. def OAI.PerfectCompleteness.DummyElimination.Slice.chosenLift line 117
  12. def OAI.PerfectCompleteness.DummyElimination.Slice.liftedEquivProduct line 122
  13. theorem OAI.PerfectCompleteness.DummyElimination.Slice.liftedEquivProduct_fst line 143
  14. theorem OAI.PerfectCompleteness.DummyElimination.Slice.expect_projected line 146