OAI/RingTheory/BassTrace/ProbabilityGeometry.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Sparse.FinProbability.expectation_on_finset line 20
  2. lemma OAI.BassTrace.Sparse.FinProbability.total_on_finset line 27
  3. lemma OAI.BassTrace.Sparse.FinProbability.gap_on_finset line 33
  4. def OAI.BassTrace.Sparse.centerBranchValue line 41
  5. def OAI.BassTrace.Sparse.ballBranch line 44
  6. lemma OAI.BassTrace.Sparse.ballBranch_apply line 49
  7. lemma OAI.BassTrace.Sparse.ballBranch_eq_pairing line 57
  8. lemma OAI.BassTrace.Sparse.ballBranch_vanish line 72
  9. theorem OAI.BassTrace.Sparse.exists_ballBranch_maximizer line 82
  10. lemma OAI.BassTrace.Sparse.rho_le_iff_ballBranches line 114
  11. lemma OAI.BassTrace.Sparse.rho_eq_iff_ballBranches line 121
  12. def OAI.BassTrace.Sparse.coefficientSum line 143
  13. lemma OAI.BassTrace.Sparse.coefficientSum_apply line 146
  14. lemma OAI.BassTrace.Sparse.coefficientSum_single line 150
  15. def OAI.BassTrace.Sparse.probabilitySet line 153
  16. lemma OAI.BassTrace.Sparse.convex_probabilitySet line 156
  17. lemma OAI.BassTrace.Sparse.single_mem_probabilitySet line 171
  18. lemma OAI.BassTrace.Sparse.sum_single_of_support_subset line 180
  19. lemma OAI.BassTrace.Sparse.sum_coeff_of_support_subset line 191
  20. lemma OAI.BassTrace.Sparse.convexHull_single_eq_probabilitySet line 196
  21. lemma OAI.BassTrace.Sparse.FinProbability.mem_geometric_simplex line 212
  22. lemma OAI.BassTrace.Sparse.probabilitySet_eq line 219
  23. lemma OAI.BassTrace.Sparse.geometric_simplex_compact line 228
  24. lemma OAI.BassTrace.Sparse.onFinsupp_faces line 239
  25. lemma OAI.BassTrace.Sparse.onFinsupp_space line 243
  26. def OAI.BassTrace.Sparse.FinProbability.rhoMetric line 264
  27. def OAI.BassTrace.Sparse.simplexProbability line 275
  28. lemma OAI.BassTrace.Sparse.simplexProbability_support line 279
  29. lemma OAI.BassTrace.Sparse.potentialVertices_nonempty line 282
  30. lemma OAI.BassTrace.Sparse.rho_eq_vertex_sup line 288
  31. lemma OAI.BassTrace.Sparse.continuous_simplexProbability line 302
  32. lemma OAI.BassTrace.Sparse.isCompact_probability_simplex line 329