OAI/RingTheory/BassTrace/SimplexMeasures.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.Sparse.treeAreaMeasure line 15
  2. lemma OAI.BassTrace.Sparse.treeAreaMeasure_apply line 19
  3. def OAI.BassTrace.Sparse.simplexAreaMeasure line 24
  4. lemma OAI.BassTrace.Sparse.simplexAreaMeasure_apply line 29
  5. lemma OAI.BassTrace.Sparse.simplexArea_union line 34
  6. lemma OAI.BassTrace.Sparse.measure_surgery_gain line 40
  7. lemma OAI.BassTrace.Sparse.simplexArea_surgery_gain line 49
  8. def OAI.BassTrace.Sparse.simplexEmbed line 68
  9. lemma OAI.BassTrace.Sparse.simplexCoordinates_embed line 74
  10. lemma OAI.BassTrace.Sparse.simplexEmbed_support line 86
  11. lemma OAI.BassTrace.Sparse.simplexEmbed_coordinates line 96
  12. lemma OAI.BassTrace.Sparse.simplexEmbed_injective line 111
  13. lemma OAI.BassTrace.Sparse.simplexEmbed_preimage line 115
  14. def OAI.BassTrace.Sparse.originalAreaMeasure line 127
  15. lemma OAI.BassTrace.Sparse.originalAreaMeasure_apply line 132
  16. lemma OAI.BassTrace.Sparse.support_of_mem_sourceInterior line 149
  17. lemma OAI.BassTrace.Sparse.originalArea_eq_measure line 157
  18. def OAI.BassTrace.Sparse.relabelCoefficients line 176
  19. lemma OAI.BassTrace.Sparse.sum_relabelCoefficients line 185
  20. lemma OAI.BassTrace.Sparse.relabelCoefficients_single line 188
  21. def OAI.BassTrace.Sparse.edgeVector line 199
  22. lemma OAI.BassTrace.Sparse.sum_edgeVector line 201
  23. lemma OAI.BassTrace.Sparse.relabel_edgeVector line 204
  24. lemma OAI.BassTrace.Sparse.coefficient_ext_total line 208
  25. lemma OAI.BassTrace.Sparse.treeParam_difference line 219
  26. lemma OAI.BassTrace.Sparse.treeCoordinates_edgeVector line 244
  27. def OAI.BassTrace.Sparse.treeEdgePermutation line 254
  28. lemma OAI.BassTrace.Sparse.mapped_treeEdge_out line 258
  29. lemma OAI.BassTrace.Sparse.exists_treeEdge_signs line 283
  30. def OAI.BassTrace.Sparse.signedEdgeMap line 310
  31. lemma OAI.BassTrace.Sparse.signedEdgeMap_isometry line 316
  32. lemma OAI.BassTrace.Sparse.signedEdgeMap_sum line 327
  33. lemma OAI.BassTrace.Sparse.treeTransition_sub line 342
  34. lemma OAI.BassTrace.Sparse.treeTransition_isometry line 357
  35. lemma OAI.BassTrace.Sparse.treeArea_relabel line 366
  36. def OAI.BassTrace.Sparse.spanningTreeRelabel line 398
  37. lemma OAI.BassTrace.Sparse.simplexArea_relabel line 410