OAI/Dynamics/StandardMap/Coupling/FiniteProductVariance.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicCoding.expectation_centered_sum_square line 12
  2. lemma OAI.HyperbolicCoding.finiteExpectation_exists_le line 34
  3. lemma OAI.HyperbolicCoding.probability_weight_le_one line 44
  4. lemma OAI.HyperbolicCoding.categorical_variance line 49
  5. lemma OAI.HyperbolicCoding.categorical_mean_zero line 62
  6. def OAI.HyperbolicCoding.assignedMass line 78
  7. def OAI.HyperbolicCoding.fractionalMass line 80
  8. def OAI.HyperbolicCoding.assignmentError line 82
  9. lemma OAI.HyperbolicCoding.expected_row_error_square line 86
  10. lemma OAI.HyperbolicCoding.expected_assignment_error_square line 98
  11. lemma OAI.HyperbolicCoding.expected_assignment_cost line 130
  12. theorem OAI.HyperbolicCoding.exists_deterministic_assignment line 142
  13. def OAI.HyperbolicCoding.MatrixCoupling.conditionalAssignment line 165
  14. lemma OAI.HyperbolicCoding.MatrixCoupling.conditionalAssignment_nonneg line 170
  15. lemma OAI.HyperbolicCoding.MatrixCoupling.conditionalAssignment_sum line 179
  16. lemma OAI.HyperbolicCoding.MatrixCoupling.mul_conditionalAssignment line 187
  17. lemma OAI.HyperbolicCoding.MatrixCoupling.fractionalMass_conditionalAssignment line 197
  18. theorem OAI.HyperbolicCoding.MatrixCoupling.exists_rounded_decoder line 201
  19. lemma OAI.HyperbolicCoding.assignedMass_nonneg line 222
  20. lemma OAI.HyperbolicCoding.assignedMass_sum line 225
  21. def OAI.HyperbolicCoding.MatrixCoupling.assignment line 234
  22. lemma OAI.HyperbolicCoding.MatrixCoupling.assignment_cost line 242
  23. theorem OAI.HyperbolicCoding.MatrixCoupling.repair_assignment line 251
  24. theorem OAI.HyperbolicCoding.MatrixCoupling.exists_decodable_coupling line 298