OAI/Algebra/GroupRing/TypedGraphs.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.TypedGraphs.size line 13

   Source documentation

   Admissible sizes are exactly the multiplicities of the empirical table.

   def size (rep : ℕ) : ℕ := 2 * 16513 ^ 2 * rep

2. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.size_tendsto line 15
3. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.eventual_carrier line 21
4. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.eventual_nonempty line 34

   Source documentation

   Both jointly conditioned graph spaces really exist for all sufficiently large admissible sizes; no high-girth existence is a standing assumption.

   theorem eventual_nonempty : ∀ᶠ rep : ℕ in atTop,
       (Matching.conditioned (label := label (@outgoingA rep)) (bar := inverse)
   …

   Mentions: OAI.TorsionFreeZeroDivisors.TypedGraphs.label

5. theorem OAI.TorsionFreeZeroDivisors.TypedGraphs.reduced_circuit_length line 44

   Source documentation

   The simple-graph girth says exactly what is required of the original multigraph's immersed closed paths. Loops and parallel edges were not discarded.

   theorem reduced_circuit_length {V D : Type*} (Γ : PortGraph V D) (L : ℕ)
       (hg : (3 * L : ℕ) ≤ Γ.subdivision.egirth) {v : V}
       (p : Γ.Walk v v) (hp : p.IsReduced) (hne : 0 < p.length) : L ≤ p.length := by
   …

6. abbrev OAI.TorsionFreeZeroDivisors.TypedStage.sideA line 62
7. abbrev OAI.TorsionFreeZeroDivisors.TypedStage.sideB line 75
8. theorem OAI.TorsionFreeZeroDivisors.TypedStage.conditionsA line 88
9. theorem OAI.TorsionFreeZeroDivisors.TypedStage.conditionsB line 115
10. def OAI.TorsionFreeZeroDivisors.StageCost.cost line 148

    Source documentation

    The exact vertex/table/prescription factor, before the retained turn cost.

    def cost (n p r : ℝ) (f i e : ℕ) : ℝ := n^(f+i)*p^i/r^e

11. theorem OAI.TorsionFreeZeroDivisors.StageCost.cost_exp line 150
12. theorem OAI.TorsionFreeZeroDivisors.StageCost.cost_chain_exp line 164
13. theorem OAI.TorsionFreeZeroDivisors.StageCost.uniform_bound line 176

    Source documentation

    Uniform error bound, with a bounded number q of chains and e ≤ k L edges. It keeps the exact exponent f-q, including negative and zero cases.

    theorem uniform_bound (n p r : ℝ) (hn : 0<n) (hp : 0<p) (hp1 : p≤1)
        (hr : 0<r) (hrnp : r≤n*p) (f i e q Q : ℕ) (he : i+q=e) (hq : q≤Q)
        (k L : ℝ) (heL : (e:ℝ)≤k*L) :
        cost n p r f i e ≤ Real.exp
          (((f:ℝ)-q)*Real.log n + (Q:ℝ)*(-Real.log p) + k*L*Real.log (n*p/r)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageCost.cost

14. theorem OAI.TorsionFreeZeroDivisors.StageCost.internal_add_chains line 189
15. def OAI.TorsionFreeZeroDivisors.StageDenominator.carrier line 206
16. def OAI.TorsionFreeZeroDivisors.StageDenominator.denominator line 207
17. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.carrier_eq line 210
18. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.L_ratio line 214
19. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.spent_ratio line 228
20. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.eventually_room line 233
21. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.eventually_pos line 242
22. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.denominator_ratio line 246
23. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.relative_ratio line 256
24. def OAI.TorsionFreeZeroDivisors.StageDenominator.penalty line 267
25. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.penalty_tendsto line 269
26. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.penalty_nonneg line 274
27. def OAI.TorsionFreeZeroDivisors.StageDenominator.error line 280
28. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.error_ratio line 283
29. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.room line 305

    Source documentation

    Each side has the SAME empirical carrier denominator, not the sum of the sizes of the two disjoint graphs. This bound is uniform in every stage.

    theorem room (K rep e : ℕ) (hr : K*L (size rep)+exclusion (size rep) ≤ carrier rep)
        (he : e ≤ K*L (size rep)) :
        denominator K rep+e+4*132^(2*(3*L (size rep))+1) ≤ 4260354*rep := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageDenominator.carrier, OAI.TorsionFreeZeroDivisors.StageDenominator.denominator

30. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.conditionsA line 316
31. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.conditionsB line 324
32. theorem OAI.TorsionFreeZeroDivisors.StageDenominator.joint_cost_bound line 334

    Source documentation

    The edge/table cost is an exponential of f-q log n plus a uniform o(L), for two sides jointly. The signed value f-q is NOT replaced by its positive part.

    theorem joint_cost_bound (A B : Side) (K Q rep : ℕ) (hn : 0<size rep)
        (hr : 0<denominator K rep) (ha : ∀c,0<A.len c) (hb : ∀c,0<B.len c)
        (hQ : Fintype.card A.C+Fintype.card B.C ≤ Q)
        (hE : A.edges+B.edges ≤ K*L (size rep)) :
        A.cost (size rep) (129/16513) (denominator K rep) *
          B.cost (size rep) (129/16513) (denominator K rep) ≤
          Real.exp ((((A.freeMarks+B.freeMarks:ℕ):ℝ)-
            (Fintype.card A.C+Fintype.card B.C:ℕ))*Real.log (size rep)+error K Q rep) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageDenominator.denominator, OAI.TorsionFreeZeroDivisors.StageDenominator.error