OAI/Algebra/GroupRing/MultiplicityBound.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TorsionFreeZeroDivisors.MultiplicityBound.closed_weight line 16

   Source documentation

   Every nonempty reduced closed walk pays at least the cycle girth, even when subdivision spokes have zero weight.

   theorem closed_weight (w : Sym2 V → ℝ) (hw : ∀ e, 0 ≤ w e)
       (L : ℝ) (hg : ∀ a (c : G.Walk a a), c.IsCycle → L ≤ weight w c)
       {a : V} (p : G.Walk a a) (hp : p.edges.IsChain (· ≠ ·)) (hne : ¬ p.Nil) :
       L ≤ weight w p := by
   …

2. theorem OAI.TorsionFreeZeroDivisors.MultiplicityBound.visit_bound line 26

   Source documentation

   Vertex visits in any reduced walk are uniformly bounded in terms of expanded length divided by girth. This counts occurrences, not just edges.

   theorem visit_bound [DecidableEq V] (w : Sym2 V → ℝ) (hw : ∀ e, 0 ≤ w e)
       (L : ℝ) (hL : 0 ≤ L)
       (hg : ∀ a (c : G.Walk a a), c.IsCycle → L ≤ weight w c)
       {a b : V} (p : G.Walk a b) (hp : p.edges.IsChain (· ≠ ·)) (x : V) :
       (p.support.count x : ℝ)*L ≤ weight w p + L := by
   …

3. def OAI.TorsionFreeZeroDivisors.PathMultiplicity.pathChain line 94

   Source documentation

   Convert a literal nonempty dart path to the dependent chain encoding.

   def pathChain (x : D) : (xs : List D) → Chain D xs.length
     | [] => x
     | y::ys => (x,pathChain y ys)

4. lemma OAI.TorsionFreeZeroDivisors.PathMultiplicity.pathChain_head line 98
5. lemma OAI.TorsionFreeZeroDivisors.PathMultiplicity.pathChain_word line 101
6. lemma OAI.TorsionFreeZeroDivisors.PathMultiplicity.pathChain_good line 106
7. lemma OAI.TorsionFreeZeroDivisors.PathMultiplicity.draw_count line 115

   Source documentation

   A port appears once per traversal of its undirected edge in the physical subdivision walk, in either direction. Spoke vertices do not add occurrences.

   lemma draw_count {k : ℕ} (p : Chain D k) (hp : Good Γ p) (x : D) :
       (draw Γ p hp).support.count (Sum.inr x) =
         (outWord p).count x + (outWord p).count (Γ.reverse x) := by
   …

8. lemma OAI.TorsionFreeZeroDivisors.PathMultiplicity.pathChain_cost line 141
9. theorem OAI.TorsionFreeZeroDivisors.PathMultiplicity.path_edge_bound line 153

   Source documentation

   The undirected edge count for a literal port path bounds each orientation in particular.

   theorem path_edge_bound (L : ℝ) (hL : 0≤L)
       (hg : ∀ a (c : Γ.subdivision.Walk a a), c.IsCycle →
         L ≤ weight (edgeWeight (fun _ : D => 1)) c)
       (p : List D) (hp : p.IsChain (PortWalk.step Γ.origin Γ.reverse)) (x : D) :
       ((p.count x + p.count (Γ.reverse x):ℕ):ℝ)*L ≤ p.length + L := by
   …

10. lemma OAI.TorsionFreeZeroDivisors.ChainPaths.reverse_mem_word line 182
11. lemma OAI.TorsionFreeZeroDivisors.ChainPaths.undirected_multiplicity_constant line 206
12. theorem OAI.TorsionFreeZeroDivisors.PathMultiplicity.total_edge_bound line 222

    Source documentation

    Summing the literal edge-multiplicity estimate over the given path system.

    theorem total_edge_bound (L : ℝ) (hL : 0≤L)
        (hg : ∀ a (c : Γ.subdivision.Walk a a), c.IsCycle →
          L ≤ weight (edgeWeight (fun _ : D => 1)) c)
        (p : I → List D) (hp : ∀ i, (p i).IsChain (WeightedMoore.PortWalk.step Γ.origin Γ.reverse))
        (x : D) :
        (∑ i, ((p i).count x + (p i).count (Γ.reverse x)):ℕ)*L ≤
          (∑ i, (p i).length : ℕ)+(Fintype.card I:ℝ)*L := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.step

13. lemma OAI.TorsionFreeZeroDivisors.ChainPaths.start_mem_word line 245
14. lemma OAI.TorsionFreeZeroDivisors.ChainPaths.sum_count_eq_length line 250
15. theorem OAI.TorsionFreeZeroDivisors.ChainPaths.total_chain_bound line 260

    Source documentation

    The number of chain traversals is bounded independently of their lengths.

    theorem total_chain_bound {I : Type*} [Fintype I]
        (L : ℝ) (hL : 0≤L)
        (hg : ∀ a (c : Γ.subdivision.Walk a a), c.IsCycle →
          L ≤ weight (edgeWeight (fun _ : D => 1)) c)
        (ds : I → List B)
        (hp : ∀ i, ((ds i).flatMap (word Γ mark h2)).IsChain (PortWalk.step Γ.origin Γ.reverse)) :
        (∑ i, (ds i).length : ℕ)*L ≤ (Fintype.card B:ℝ)*
          ((∑ i, ((ds i).flatMap (word Γ mark h2)).length : ℕ)+(Fintype.card I:ℝ)*L) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainPaths.word

16. theorem OAI.TorsionFreeZeroDivisors.ChainPaths.bounded_chain_traversals line 290

    Source documentation

    A uniform integer bound in terms of the length, path count, and chain count.

    theorem bounded_chain_traversals {I : Type*} [Fintype I]
        (C : ℝ) (hC : 0≤C) (K R : ℕ) (hI : Fintype.card I≤K) (hB : Fintype.card B≤R)
        (L : ℝ) (hL : 0<L)
        (hg : ∀ a (c : Γ.subdivision.Walk a a), c.IsCycle →
          L ≤ weight (edgeWeight (fun _ : D => 1)) c)
        (ds : I → List B)
        (hp : ∀ i, ((ds i).flatMap (word Γ mark h2)).IsChain (PortWalk.step Γ.origin Γ.reverse))
        (hH : (∑ i, ((ds i).flatMap (word Γ mark h2)).length : ℕ) ≤ C*L) :
        ∑ i, (ds i).length ≤ ⌈(R:ℝ)*(C+K)⌉₊ := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainPaths.word

17. structure OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages line 322

    Source documentation

    An incidence remembers its occurrence and which (oriented) half-edge it uses. Passages pair incidences at a vertex; path endpoints are fixed points.

    structure Passages (origin : D → V) (port : O → D) extends Pairing O where
    …

18. abbrev OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.AtVertex line 329
19. def OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.localPairing line 331
20. def OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.multiplicity line 335
21. def OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.maxMultiplicity line 336
22. theorem OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.local_multiplicity line 340
23. theorem OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.local_balance line 352
24. theorem OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.sum_vertex_cards line 372
25. theorem OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.sum_endpoint_cards line 378
26. theorem OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.total_balance line 395

    Source documentation

    Exact incidence balance before any probabilities or asymptotic estimates. It remains valid when a loop contributes two distinct half-edges at a vertex.

    theorem total_balance :
        2 * (∑ v : V, maxMultiplicity (origin := origin) (port := port) v) ≤
    …

    Mentions: OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.maxMultiplicity

27. theorem OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.image_vertex_bound line 406

    Source documentation

    Each edge occurrence has two incidences, and zero or one interval contributes zero or two endpoints.

    theorem image_vertex_bound (H iota : ℕ) (hH : Fintype.card O = 2*H)
        (hiota : Fintype.card P.toPairing.Unmatched = 2*iota) :
        (∑ v : V, maxMultiplicity (origin := origin) (port := port) v) ≤ H+iota := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.maxMultiplicity