OAI/Algebra/GroupRing/WeightedGirth.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorsionFreeZeroDivisors.WeightedGirth.middle line 13
  2. def OAI.TorsionFreeZeroDivisors.WeightedGirth.bundle line 17
  3. lemma OAI.TorsionFreeZeroDivisors.WeightedGirth.bundle_card line 25
  4. lemma OAI.TorsionFreeZeroDivisors.WeightedGirth.self_mem_bundle line 42
  5. lemma OAI.TorsionFreeZeroDivisors.WeightedGirth.weight_eq_indicator line 45
  6. lemma OAI.TorsionFreeZeroDivisors.WeightedGirth.edges_covered line 50
  7. lemma OAI.TorsionFreeZeroDivisors.WeightedGirth.length_le_three_weight line 87

    Source documentation

    In a genuine subdivision cycle every middle edge supports at most two spokes. Thus girth measured in three-edge subdivisions implies the literal unit macro-edge weighted girth used by the pattern theorem.

    lemma length_le_three_weight {a : V⊕D} (p : Γ.subdivision.Walk a a) (hp : p.IsCycle) :
    (p.length:ℝ)≤3*weight (edgeWeight (fun _ : D => (1:ℝ))) p := by
…
  8. lemma OAI.TorsionFreeZeroDivisors.WeightedGirth.weighted_girth line 104
  9. def OAI.TorsionFreeZeroDivisors.SumGirth.inlWalk line 115
  10. lemma OAI.TorsionFreeZeroDivisors.SumGirth.map_inlWalk line 119
  11. lemma OAI.TorsionFreeZeroDivisors.SumGirth.inlWalk_length line 128
  12. lemma OAI.TorsionFreeZeroDivisors.SumGirth.inlWalk_cycle line 133
  13. lemma OAI.TorsionFreeZeroDivisors.SumGirth.le_egirth line 137
  14. lemma OAI.TorsionFreeZeroDivisors.SumGirth.walk_side line 152
  15. lemma OAI.TorsionFreeZeroDivisors.SumGirth.diameter line 158
  16. def OAI.TorsionFreeZeroDivisors.SumPort.graph line 188
  17. def OAI.TorsionFreeZeroDivisors.SumPort.subdivisionIso line 197
  18. lemma OAI.TorsionFreeZeroDivisors.SumPort.girth line 203
  19. def OAI.TorsionFreeZeroDivisors.SumPort.side line 208
  20. lemma OAI.TorsionFreeZeroDivisors.SumPort.side_edge line 209
  21. def OAI.TorsionFreeZeroDivisors.SumPort.leftV line 212
  22. def OAI.TorsionFreeZeroDivisors.SumPort.rightV line 216
  23. lemma OAI.TorsionFreeZeroDivisors.SumPort.leftV_injective line 220
  24. lemma OAI.TorsionFreeZeroDivisors.SumPort.rightV_injective line 227
  25. def OAI.TorsionFreeZeroDivisors.SumPort.leftD line 237
  26. def OAI.TorsionFreeZeroDivisors.SumPort.rightD line 241
  27. lemma OAI.TorsionFreeZeroDivisors.SumPort.leftD_injective line 245
  28. lemma OAI.TorsionFreeZeroDivisors.SumPort.rightD_injective line 252
  29. lemma OAI.TorsionFreeZeroDivisors.SumPort.root_value line 259
  30. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.VA line 275
  31. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.VB line 276
  32. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.DA line 277
  33. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.DB line 278
  34. def OAI.TorsionFreeZeroDivisors.SampleGraph.A line 279
  35. def OAI.TorsionFreeZeroDivisors.SampleGraph.B line 280
  36. def OAI.TorsionFreeZeroDivisors.SampleGraph.graph line 281
  37. def OAI.TorsionFreeZeroDivisors.SampleGraph.label line 282
  38. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.label_reverse line 283
  39. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.immersed line 287
  40. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.girth line 298
  41. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.weighted_girth line 303
  42. def OAI.TorsionFreeZeroDivisors.SampleGraph.embeddingA line 308
  43. def OAI.TorsionFreeZeroDivisors.SampleGraph.embeddingB line 326
  44. structure OAI.TorsionFreeZeroDivisors.SampleGraph.BoundedSystem line 346