OAI/RingTheory/BassTrace/OrbitForms.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.Sparse.FinProbability.push line 13
  2. lemma OAI.BassTrace.Sparse.FinProbability.push_coeff_apply line 22
  3. lemma OAI.BassTrace.Sparse.FinProbability.push_support line 25
  4. lemma OAI.BassTrace.Sparse.FinProbability.push_refl line 28
  5. lemma OAI.BassTrace.Sparse.FinProbability.push_trans line 32
  6. lemma OAI.BassTrace.Sparse.FinProbability.push_symm_push line 37
  7. lemma OAI.BassTrace.Sparse.FinProbability.push_expectation line 42
  8. lemma OAI.BassTrace.Sparse.FinProbability.push_gap line 49
  9. lemma OAI.BassTrace.Sparse.FinProbability.transport_push_le line 53
  10. lemma OAI.BassTrace.Sparse.FinProbability.transport_push line 62
  11. lemma OAI.BassTrace.Sparse.FinProbability.rho_push line 71
  12. lemma OAI.BassTrace.Sparse.smul_probability_coeff line 97
  13. lemma OAI.BassTrace.Sparse.smul_probability_support line 100
  14. lemma OAI.BassTrace.Sparse.smul_probability_rho line 103
  15. def OAI.BassTrace.Sparse.OrbitForms.push line 117
  16. lemma OAI.BassTrace.Sparse.OrbitForms.push_apply line 120
  17. lemma OAI.BassTrace.Sparse.OrbitForms.push_one line 123
  18. lemma OAI.BassTrace.Sparse.OrbitForms.push_mul line 125
  19. lemma OAI.BassTrace.Sparse.OrbitForms.push_inv_push line 129
  20. structure OAI.BassTrace.Sparse.OrbitForms.Data line 132
  21. def OAI.BassTrace.Sparse.OrbitForms.form line 139
  22. lemma OAI.BassTrace.Sparse.OrbitForms.form_apply line 142
  23. lemma OAI.BassTrace.Sparse.OrbitForms.form_translate line 145
  24. lemma OAI.BassTrace.Sparse.OrbitForms.form_ne_zero_support line 150
  25. lemma OAI.BassTrace.Sparse.OrbitForms.finite_form_ne_zero line 160
  26. lemma OAI.BassTrace.Sparse.OrbitForms.finite_relevant line 171
  27. def OAI.BassTrace.Sparse.OrbitForms.relevant line 184
  28. lemma OAI.BassTrace.Sparse.OrbitForms.mem_relevant line 186
  29. lemma OAI.BassTrace.Sparse.OrbitForms.irrelevant_vanish line 189
  30. lemma OAI.BassTrace.Sparse.OrbitForms.relevant_translate line 197
  31. def OAI.BassTrace.Sparse.OrbitForms.relevantEquiv line 207
  32. lemma OAI.BassTrace.Sparse.OrbitForms.relevantEquiv_form line 216
  33. abbrev OAI.BassTrace.Sparse.BallOrbitForms.Index line 234
  34. def OAI.BassTrace.Sparse.BallOrbitForms.data line 236
  35. lemma OAI.BassTrace.Sparse.BallOrbitForms.push_coeff line 246
  36. lemma OAI.BassTrace.Sparse.BallOrbitForms.branch_apply line 251
  37. lemma OAI.BassTrace.Sparse.BallOrbitForms.exists_maximizer line 257
  38. lemma OAI.BassTrace.Sparse.BallOrbitForms.distance_le_iff line 276
  39. lemma OAI.BassTrace.Sparse.BallOrbitForms.distance_ge_iff line 285
  40. lemma OAI.BassTrace.Sparse.BallOrbitForms.distance_eq_iff line 294
  41. def OAI.BassTrace.Sparse.OrbitForms.cuts line 321
  42. lemma OAI.BassTrace.Sparse.OrbitForms.cuts_map line 328
  43. def OAI.BassTrace.Sparse.OrbitForms.Equivariant line 342
  44. lemma OAI.BassTrace.Sparse.OrbitForms.refineFamily_equivariant line 347