OAI/Probability/SwitchChain/PairEqualityBudget.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.PairEquality.assignmentNormalizedEquiv line 17
  2. theorem OAI.Problem315.PairEquality.assignmentVector_eq_raw line 22
  3. theorem OAI.Problem315.PairEquality.restriction_projection_energy_eq_raw line 50
  4. theorem OAI.Problem315.PairEquality.assignment_projection_budget line 66
  5. theorem OAI.Problem315.PairEquality.assignmentRestriction_projection_eq_zero_of_inactive line 91
  6. theorem OAI.Problem315.PairEquality.sum_array_subtype line 101
  7. theorem OAI.Problem315.PairEquality.sum_array_eq_subtype line 111
  8. theorem OAI.Problem315.PairEquality.assignment_projection_sum_eq_singletons line 132
  9. theorem OAI.Problem315.PairEquality.sum_assignmentRestriction_norm_sq line 150
  10. theorem OAI.Problem315.PairEquality.sum_assignmentRestriction_family_norm_sq line 162
  11. theorem OAI.Problem315.PairEquality.sum_norm_sq_le_of_assignment_restriction_budget line 172
  12. def OAI.Problem315.PairEquality.orderedGain line 185
  13. theorem OAI.Problem315.PairEquality.orderedGain_of_distinct line 189
  14. theorem OAI.Problem315.PairEquality.assignment_orderedGain_norm_sq line 195
  15. theorem OAI.Problem315.PairEquality.sum_array_subtype_le line 215
  16. theorem OAI.Problem315.PairEquality.assignment_ordered_projection_budget line 231
  17. theorem OAI.Problem315.PairEquality.ordered_projection_budget line 252