OAI/Algebra/GroupRing/CoreStripping.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorsionFreeZeroDivisors.CoreStripping.degree line 13
  2. def OAI.TorsionFreeZeroDivisors.CoreStripping.Symmetric line 15
  3. def OAI.TorsionFreeZeroDivisors.CoreStripping.delete line 17
  4. lemma OAI.TorsionFreeZeroDivisors.CoreStripping.delete_subset line 19
  5. lemma OAI.TorsionFreeZeroDivisors.CoreStripping.degree_pos line 22
  6. lemma OAI.TorsionFreeZeroDivisors.CoreStripping.leaf_unique line 25
  7. lemma OAI.TorsionFreeZeroDivisors.CoreStripping.leaf_not_loop line 34
  8. lemma OAI.TorsionFreeZeroDivisors.CoreStripping.delete_symmetric line 39
  9. lemma OAI.TorsionFreeZeroDivisors.CoreStripping.delete_degree_leaf line 50
  10. lemma OAI.TorsionFreeZeroDivisors.CoreStripping.delete_degree_neighbor line 59
  11. lemma OAI.TorsionFreeZeroDivisors.CoreStripping.delete_degree_other line 78
  12. def OAI.TorsionFreeZeroDivisors.CoreStripping.surplus line 94

    Source documentation

    Euler surplus without counting isolated vertices. It equals the sum of branch excesses minus the number of leaves.

    def surplus (n : ℕ) : ℤ := if n=0 then 0 else (n:ℤ)-2
  13. lemma OAI.TorsionFreeZeroDivisors.CoreStripping.surplus_succ line 96
  14. def OAI.TorsionFreeZeroDivisors.CoreStripping.potential line 104
  15. lemma OAI.TorsionFreeZeroDivisors.CoreStripping.delete_potential line 106
  16. theorem OAI.TorsionFreeZeroDivisors.CoreStripping.exists_core line 129

    Source documentation

    Actual repeated leaf deletion. The terminal subgraph has minimum degree two on every surviving dart; Euler surplus can only increase.

    theorem exists_core (S : Finset D) (hs : Symmetric Γ S) :
    ∃ Q : Finset D, Q⊆S ∧ Symmetric Γ Q ∧
      (∀ d∈Q, 2≤degree Γ Q (Γ.origin d)) ∧ potential Γ S≤potential Γ Q := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.CoreStripping.Symmetric, OAI.TorsionFreeZeroDivisors.CoreStripping.degree, OAI.TorsionFreeZeroDivisors.CoreStripping.potential

  17. def OAI.TorsionFreeZeroDivisors.ImageComplexity.restrict line 158

    Source documentation

    The actual symmetric subgraph on a specified set of original darts.

    def restrict (Q : Finset D) (hs : Symmetric Γ Q) : PortGraph V Q where
…
  18. def OAI.TorsionFreeZeroDivisors.ImageComplexity.inclusion line 164
  19. lemma OAI.TorsionFreeZeroDivisors.ImageComplexity.inclusion_injective line 176
  20. lemma OAI.TorsionFreeZeroDivisors.ImageComplexity.restrict_degree line 180
  21. lemma OAI.TorsionFreeZeroDivisors.ImageComplexity.inclusion_weight line 195
  22. lemma OAI.TorsionFreeZeroDivisors.ImageComplexity.fiber_count line 208

    Source documentation

    Vertexwise counting, including loops through their two different darts.

    lemma fiber_count (S : Finset D) (P : V → Prop) [DecidablePred P] :
    ∑ v, (if P v then degree Γ S v else 0) = (S.filter (fun d => P (Γ.origin d))).card := by
…
  23. lemma OAI.TorsionFreeZeroDivisors.ImageComplexity.surplus_excess line 222
  24. lemma OAI.TorsionFreeZeroDivisors.ImageComplexity.surplus_le_branch line 226
  25. lemma OAI.TorsionFreeZeroDivisors.ImageComplexity.excess_le_potential_add_leaves line 231
  26. lemma OAI.TorsionFreeZeroDivisors.ImageComplexity.branch_degrees_bound_excess line 242
  27. theorem OAI.TorsionFreeZeroDivisors.ImageComplexity.bounded_image_branches line 252

    Source documentation

    Bounded branching in the actual image, not in a hypothesized bounded-rank pattern. A bounded number of leaves is the only endpoint correction.

    theorem bounded_image_branches (C : ℝ) (hC : 0 ≤ C) (leaves : ℕ) :
    ∃ R : ℕ, ∀ {V D : Type} [Fintype V] [Fintype D] (Γ : PortGraph V D)
      (L : ℝ) (_ : 0 < L)
      (_ : (Fintype.card D:ℝ) ≤ 2*C*L)
      (_ : ∀ a (c : Γ.subdivision.Walk a a), c.IsCycle →
        L ≤ weight (edgeWeight (fun _ : D => (1:ℝ))) c)
      (_ : (Finset.univ.filter (fun v => degree Γ Finset.univ v=1)).card ≤ leaves),
      (Finset.univ.filter (fun d => 3≤degree Γ Finset.univ (Γ.origin d))).card ≤ R := by
…
  28. def OAI.TorsionFreeZeroDivisors.SystemLeaves.AtMostOneNeighbor line 308

    Source documentation

    The combinatorial leaf condition, stated without assuming local finiteness.

    def AtMostOneNeighbor (x : W) : Prop := ∀ a b, G.Adj x a → G.Adj x b → a=b
  29. lemma OAI.TorsionFreeZeroDivisors.SystemLeaves.leaf_in_reduced_walk line 310
  30. def OAI.TorsionFreeZeroDivisors.SystemLeaves.CyclicallyReduced line 332

    Source documentation

    Including the closing turn, not just linear immersion.

    def CyclicallyReduced {a : W} (p : G.Walk a a) : Prop :=
…
  31. lemma OAI.TorsionFreeZeroDivisors.SystemLeaves.leaf_not_in_cyclic line 335
  32. def OAI.TorsionFreeZeroDivisors.SystemLeaves.degree line 346
  33. lemma OAI.TorsionFreeZeroDivisors.SystemLeaves.leaf_original line 348
  34. lemma OAI.TorsionFreeZeroDivisors.SystemLeaves.actual_image_leaf_endpoints line 364

    Source documentation

    In the actual image of any number of cyclically immersed closed walks and one immersed interval, every leaf is an endpoint of that interval.

    lemma actual_image_leaf_endpoints {J : Type*} (base : J → V)
    (loops : ∀ j, Γ.subdivision.Walk (.inl (base j)) (.inl (base j)))
    (hloops : ∀ j, CyclicallyReduced (loops j)) (hne : ∀ j, ¬(loops j).Nil)
    {a b : V} (p : Γ.subdivision.Walk (.inl a) (.inl b))
    (hp : p.edges.IsChain (· ≠ ·))
    (himage : ∀ d : D, Sum.inl (Γ.origin d)∈p.support ∨
      ∃ j, Sum.inl (Γ.origin d)∈(loops j).support)
    (v : V) (hv : degree Γ v=1) : v=a ∨ v=b := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.SystemLeaves.CyclicallyReduced, OAI.TorsionFreeZeroDivisors.SystemLeaves.degree

  35. lemma OAI.TorsionFreeZeroDivisors.SystemLeaves.actual_image_at_most_two_leaves line 384