OAI/RingTheory/BassTrace/TransportMetric.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

The dual transportation metric on finitely supported probability vectors.

  1. structure OAI.BassTrace.Sparse.FinProbability line 11
  2. theorem OAI.BassTrace.Sparse.FinProbability.ext_coeff line 20
  3. def OAI.BassTrace.Sparse.FinProbability.expectation line 26
  4. lemma OAI.BassTrace.Sparse.FinProbability.expectation_const line 29
  5. lemma OAI.BassTrace.Sparse.FinProbability.expectation_add line 35
  6. lemma OAI.BassTrace.Sparse.FinProbability.expectation_sub line 40
  7. lemma OAI.BassTrace.Sparse.FinProbability.expectation_neg line 45
  8. lemma OAI.BassTrace.Sparse.FinProbability.expectation_mono line 50
  9. lemma OAI.BassTrace.Sparse.FinProbability.expectation_nonneg line 55
  10. lemma OAI.BassTrace.Sparse.FinProbability.abs_expectation_le line 60
  11. def OAI.BassTrace.Sparse.FinProbability.gap line 72
  12. lemma OAI.BassTrace.Sparse.FinProbability.gap_const line 75
  13. lemma OAI.BassTrace.Sparse.FinProbability.gap_sub_const line 78
  14. lemma OAI.BassTrace.Sparse.FinProbability.gap_neg line 83
  15. lemma OAI.BassTrace.Sparse.FinProbability.gap_add line 88
  16. lemma OAI.BassTrace.Sparse.FinProbability.gap_telescope line 95
  17. lemma OAI.BassTrace.Sparse.FinProbability.coeff_support_nonempty line 100
  18. lemma OAI.BassTrace.Sparse.FinProbability.gap_bound line 107
  19. def OAI.BassTrace.Sparse.FinProbability.transport line 128
  20. lemma OAI.BassTrace.Sparse.FinProbability.potential_values_nonempty line 131
  21. lemma OAI.BassTrace.Sparse.FinProbability.potential_values_bddAbove line 136
  22. lemma OAI.BassTrace.Sparse.FinProbability.gap_le_transport line 144
  23. lemma OAI.BassTrace.Sparse.FinProbability.abs_gap_le_transport line 148
  24. lemma OAI.BassTrace.Sparse.FinProbability.transport_nonneg line 157
  25. lemma OAI.BassTrace.Sparse.FinProbability.transport_le line 161
  26. lemma OAI.BassTrace.Sparse.FinProbability.transport_self line 167
  27. lemma OAI.BassTrace.Sparse.FinProbability.transport_triangle line 173
  28. lemma OAI.BassTrace.Sparse.FinProbability.transport_comm line 180
  29. lemma OAI.BassTrace.Sparse.FinProbability.expectation_vertex_indicator line 191
  30. lemma OAI.BassTrace.Sparse.FinProbability.coordinate_control line 199
  31. lemma OAI.BassTrace.Sparse.FinProbability.transport_eq_zero_iff line 215
  32. lemma OAI.BassTrace.Sparse.FinProbability.expectation_eq_zero_of_support line 227
  33. lemma OAI.BassTrace.Sparse.FinProbability.exists_support_le_expectation line 235
  34. lemma OAI.BassTrace.Sparse.FinProbability.expectation_distance_support_le line 251
  35. lemma OAI.BassTrace.Sparse.FinProbability.exists_support_pair_dist_le line 265
  36. def OAI.BassTrace.Sparse.FinProbability.rho line 275
  37. lemma OAI.BassTrace.Sparse.FinProbability.rho_nonneg line 278
  38. lemma OAI.BassTrace.Sparse.FinProbability.rho_triangle line 281
  39. lemma OAI.BassTrace.Sparse.FinProbability.rho_comm line 287
  40. lemma OAI.BassTrace.Sparse.FinProbability.sqrt_mul_rho line 290
  41. lemma OAI.BassTrace.Sparse.FinProbability.coordinate_control_rho line 296
  42. lemma OAI.BassTrace.Sparse.FinProbability.support_distance_rho line 302