OAI/Algebra/GroupRing/PatternTotalCoding.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TorsionFreeZeroDivisors.PatternTotalCoding.Code line 12
2. def OAI.TorsionFreeZeroDivisors.PatternTotalCoding.coefficient line 15
3. lemma OAI.TorsionFreeZeroDivisors.PatternTotalCoding.card_code_bound line 18
4. def OAI.TorsionFreeZeroDivisors.PatternTotalCoding.encode line 37
5. theorem OAI.TorsionFreeZeroDivisors.PatternTotalCoding.complete line 47

   Source documentation

   Complete simultaneous code equivalence for graph, every marked vertex side, path words, root and the full affine interval geometry. Padding loses no data.

   theorem complete (a : Data D V P (Fin 0) T H) (side : V → Bool)
       (c : ComparisonCoding.Data P E H)
       (a' : Data D' V' P' (Fin 0) T H) (side' : V' → Bool)
       (c' : ComparisonCoding.Data P' E' H)
       (he : encode R K T I H hR hK hI hD hV hP hE a side c=
         encode R K T I H hR hK hI hD' hV' hP' hE' a' side' c') :
       ∃ f : PatternCoding.Isomorphism a a', ∃ g : ComparisonCoding.Isomorphism H c c',
         f.path=g.path ∧ (∀ d,(Fintype.equivFin D' (f.dart d)).val=(Fintype.equivFin D d).val) ∧
         ∀ v,side v=side' (f.vertex v) := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.ComparisonCoding.Data, OAI.TorsionFreeZeroDivisors.PatternTotalCoding.encode, OAI.TorsionFreeZeroDivisors.PatternCoding.Isomorphism, OAI.TorsionFreeZeroDivisors.ComparisonCoding.Isomorphism

6. structure OAI.TorsionFreeZeroDivisors.BoundedPattern.Data line 82

   Source documentation

   The literal finite pattern data. These are only combinatorial encoding bounds; none of the probability or realizability conclusions is a field.

   structure Data (R K T I H : ℕ) where
   …

7. abbrev OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.Seeds line 121
8. abbrev OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.Marks line 122
9. abbrev OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.lengths line 123
10. def OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.graphData line 126
11. def OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.geometryData line 136
12. def OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.encode line 144
13. theorem OAI.TorsionFreeZeroDivisors.PatternFiniteUnion.bound line 157

    Source documentation

    Quotient-free finite union over a possibly large class of finite graphs. Representatives are chosen only for used codes, and encode equality must preserve the literal sample event.

    theorem bound {P : Type*} {C Ω : Type*} [Fintype C]
        (sample : Finset Ω) (hs : sample.Nonempty) (code : P → C) (good : P → Prop)
        (event : P → Ω → Prop) (B : ℝ) (hB : 0≤B)
        (hinv : ∀ p q, code p=code q → ∀ ω,event p ω → event q ω)
        (hp : ∀ p,good p → ((sample.filter (event p)).card:ℝ)/sample.card≤B) :
        ((sample.filter (fun ω => ∃ p,good p ∧ event p ω)).card:ℝ)/sample.card≤
          (Fintype.card C:ℝ)*B := by
    …

14. def OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.event line 192
15. theorem OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.event_of_encode_eq line 198

    Source documentation

    Equal finite codes transport every fixed matching event, including both pinned source sides. The code does not contain any graph labels.

    theorem event_of_encode_eq (hR : 0<R) (hK : 0<K) (hI : 0<I)
        (he : a.encode hR hK hI=b.encode hR hK hI)
        (rep : ℕ) (x : Types.VertexA rep) (y : Types.VertexB rep) (r : ActualPatternEvent.Match rep)
        (hb : b.event rep x y r) : a.event rep x y r := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.VertexB, OAI.TorsionFreeZeroDivisors.ActualPatternEvent.Match

16. abbrev OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.multiplicity line 260
17. abbrev OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.totalLength line 261
18. structure OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.Good line 265

    Source documentation

    The manuscript's deterministic hypotheses for the bounded first moment. Every condition concerns only the unlabeled graph, paths or comparisons.

    structure Good (B Q M J rep : ℕ) : Prop where
    …

19. lemma OAI.TorsionFreeZeroDivisors.BoundedPattern.Data.probability_bound line 286
20. theorem OAI.TorsionFreeZeroDivisors.BoundedPattern.probability_union line 305

    Source documentation

    Uniform first-moment union over every actual-carrier pattern, not over a postulated finite list of realizations.

    theorem probability_union (R K T I H B Q M J rep : ℕ)
        (hR : 0<R) (hK : 0<K) (hI : 0<I) (hM : 0<M)
        (hs : (samples rep).Nonempty) (hready : PatternUniform.Ready B M Q J rep)
        (x : Types.VertexA rep) (y : Types.VertexB rep) :
        (((samples rep).filter (fun r => ∃ a : Data R K T I H,a.Good B Q M J rep ∧ a.event rep x y r)).card:ℝ)/
          (samples rep).card≤
          (PatternTotalCoding.coefficient R K T I:ℝ)*(H+1:ℕ)^(R+3*I)*
            Real.exp (-(L (size rep):ℝ)/(4800*M)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.PatternUniform.Ready, OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.VertexB, OAI.TorsionFreeZeroDivisors.BoundedPattern.Data, OAI.TorsionFreeZeroDivisors.PatternTotalCoding.coefficient

21. lemma OAI.TorsionFreeZeroDivisors.ActualComplexity.leaf_unique line 330
22. lemma OAI.TorsionFreeZeroDivisors.ActualComplexity.step_not_leaf line 340
23. lemma OAI.TorsionFreeZeroDivisors.ActualComplexity.origin_leaf_head line 347
24. lemma OAI.TorsionFreeZeroDivisors.ActualComplexity.target_leaf_last line 364
25. def OAI.TorsionFreeZeroDivisors.ActualComplexity.start line 379
26. def OAI.TorsionFreeZeroDivisors.ActualComplexity.finish line 380
27. def OAI.TorsionFreeZeroDivisors.ActualComplexity.endpoints line 381
28. lemma OAI.TorsionFreeZeroDivisors.ActualComplexity.endpoints_card line 386
29. lemma OAI.TorsionFreeZeroDivisors.ActualComplexity.start_mem line 394
30. lemma OAI.TorsionFreeZeroDivisors.ActualComplexity.finish_mem line 401
31. lemma OAI.TorsionFreeZeroDivisors.ActualComplexity.leaf_bound line 409
32. lemma OAI.TorsionFreeZeroDivisors.ActualComplexity.dart_count line 429
33. lemma OAI.TorsionFreeZeroDivisors.ActualComplexity.marked_vertices_le line 446
34. theorem OAI.TorsionFreeZeroDivisors.ActualComplexity.bounded_suppression line 460

    Source documentation

    Complexity is uniform before choosing any finite actual image. The coarser 2K leaf bound suffices and does not assume any of the image complexity estimates.

    theorem bounded_suppression (B K : ℕ) : ∃ R : ℕ,0<R ∧
        ∀ {V D P : Type} [Fintype V] [Fintype D] [Fintype P]
          (Γ : PortGraph V D) (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),
          let M := endpoints Γ paths hp
    …

    Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.step, OAI.TorsionFreeZeroDivisors.WeightedCycles.weight, OAI.TorsionFreeZeroDivisors.WeightedPortMoore.edgeWeight, OAI.TorsionFreeZeroDivisors.ActualComplexity.endpoints