OAI/Algebra/GroupRing/ChainUsage.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.ChainUsage.Used line 22
2. lemma OAI.TorsionFreeZeroDivisors.ChainUsage.representative_used line 25
3. lemma OAI.TorsionFreeZeroDivisors.ChainUsage.multiplicity_pos line 37
4. lemma OAI.TorsionFreeZeroDivisors.ChainUsage.traversal_card line 47
5. lemma OAI.TorsionFreeZeroDivisors.ChainUsage.multiplicity_le line 52
6. lemma OAI.TorsionFreeZeroDivisors.ChainUsage.flatMap_length_le line 59
7. lemma OAI.TorsionFreeZeroDivisors.ChainUsage.length_le_total_of_mem line 71
8. lemma OAI.TorsionFreeZeroDivisors.ChainUsage.chain_length_le line 78
9. lemma OAI.TorsionFreeZeroDivisors.ChainUsage.rep_card_le line 85
10. theorem OAI.TorsionFreeZeroDivisors.SourcePattern.marked_bound line 97

    Source documentation

    The uniformly bounded number of marked darts is derived, not required of an original pattern. Extra marks are just the prescribed path endpoints.

    theorem marked_bound (B K : ℕ) : ∃ R : ℕ,0<R ∧
        ∀ {V D P : Type} [Fintype V] [Fintype D] [Fintype P]
          (Γ : PortGraph V D) (M : Finset V) (_hM : M.card≤2*K)
          (paths : P → List D) (_hp : ∀ p,paths p≠[])
          (_ : Fintype.card P≤K) (_ : Function.Surjective Γ.origin)
          (_ : ∀ p,(paths p).IsChain (WeightedMoore.PortWalk.step Γ.origin Γ.reverse))
          (_ : ∀ d,∃ p,d∈paths p ∨ Γ.reverse d∈paths p)
          (L : ℝ) (_ : 0<L) (_ : (∑ p,(paths p).length:ℕ)≤(B:ℝ)*L)
          (_ : ∀ a (c : Γ.subdivision.Walk a a),c.IsCycle →
            L≤WeightedCycles.weight (WeightedPortMoore.edgeWeight (fun _ : D => (1:ℝ))) c),
          Fintype.card {d : D // turn Γ.origin (marks Γ M) (marks_degree_two Γ M) d=d}≤R ∧
            Fintype.card (Mark (marks Γ M))≤R := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.SourcePattern.R, OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.step, OAI.TorsionFreeZeroDivisors.WeightedCycles.weight, OAI.TorsionFreeZeroDivisors.WeightedPortMoore.edgeWeight

11. abbrev OAI.TorsionFreeZeroDivisors.SourcePattern.Seeds line 127
12. def OAI.TorsionFreeZeroDivisors.SourcePattern.R line 130
13. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.R_pos line 131
14. def OAI.TorsionFreeZeroDivisors.SourcePattern.T line 132
15. structure OAI.TorsionFreeZeroDivisors.SourcePattern.Data line 136

    Source documentation

    The actual suppressed form of source paths. No bound on the resulting skeleton, chain lengths, multiplicities or number of traversals is assumed.

    structure Data (B K I rep : ℕ) where
    …

16. abbrev OAI.TorsionFreeZeroDivisors.SourcePattern.Data.mark line 189
17. abbrev OAI.TorsionFreeZeroDivisors.SourcePattern.Data.degree_two line 190
18. abbrev OAI.TorsionFreeZeroDivisors.SourcePattern.Data.words line 191
19. abbrev OAI.TorsionFreeZeroDivisors.SourcePattern.Data.totalLength line 192
20. abbrev OAI.TorsionFreeZeroDivisors.SourcePattern.Data.lengths line 193
21. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.Data.words_nonempty line 196
22. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.Data.lengths_le line 204
23. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.Data.upper_bound line 210
24. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.Data.lower_bound line 213
25. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.Data.covered line 216
26. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.Data.mark_bounds line 225
27. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.Data.total_traversals_le line 232
28. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.Data.traversal_le line 241
29. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.Data.offset_bounds line 245
30. def OAI.TorsionFreeZeroDivisors.SourcePattern.Data.bounded line 264
31. lemma OAI.TorsionFreeZeroDivisors.SourcePattern.Data.bounded_good line 297
32. lemma OAI.TorsionFreeZeroDivisors.BoundedPattern.polynomial_exp_tendsto line 328
33. lemma OAI.TorsionFreeZeroDivisors.BoundedPattern.mem_samples line 353
34. lemma OAI.TorsionFreeZeroDivisors.BoundedPattern.samples_eventually_nonempty line 359
35. theorem OAI.TorsionFreeZeroDivisors.BoundedPattern.eventually_avoids line 371

    Source documentation

    With the bounds fixed beforehand, for every sufficiently large admissible size there is an actual pair of conditioned matchings avoiding every bounded pattern. The roots are universally quantified after the size threshold.

    theorem eventually_avoids (R K T I B Q M J : ℕ)
        (hR : 0<R) (hK : 0<K) (hI : 0<I) (hM : 0<M) :
        ∀ᶠ rep in atTop,∀ (x : Types.VertexA rep) (y : Types.VertexB rep),
          ∃ r∈samples rep,∀ a : Data R K T I (B*L (size rep)),
            a.Good B Q M J rep → ¬a.event rep x y r := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.VertexB, OAI.TorsionFreeZeroDivisors.BoundedPattern.Data